YES
The TRS could be proven terminating. The proof took 1733 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (82ms).
| – Problem 2 was processed with processor PolynomialLinearRange4iUR (752ms).
| | – Problem 3 was processed with processor PolynomialLinearRange4iUR (445ms).
| | | – Problem 4 was processed with processor PolynomialLinearRange4iUR (248ms).
| | | | – Problem 5 was processed with processor PolynomialLinearRange4iUR (102ms).
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| app#(reverse, l) | → | app#(app(reverse2, l), nil) | | init# | → | app#(compose, tl) |
| app#(app(reverse2, app(app(cons, x), xs)), l) | → | app#(reverse2, xs) | | init# | → | app#(compose, reverse) |
| app#(app(reverse2, app(app(cons, x), xs)), l) | → | app#(cons, x) | | last# | → | app#(app(compose, hd), reverse) |
| init# | → | app#(app(compose, tl), reverse) | | app#(app(app(compose, f), g), x) | → | app#(f, x) |
| last# | → | app#(compose, hd) | | init# | → | app#(app(compose, reverse), app(app(compose, tl), reverse)) |
| app#(reverse, l) | → | app#(reverse2, l) | | app#(app(reverse2, app(app(cons, x), xs)), l) | → | app#(app(cons, x), l) |
| app#(app(app(compose, f), g), x) | → | app#(g, app(f, x)) | | app#(app(reverse2, app(app(cons, x), xs)), l) | → | app#(app(reverse2, xs), app(app(cons, x), l)) |
Rewrite Rules
| app(app(app(compose, f), g), x) | → | app(g, app(f, x)) | | app(reverse, l) | → | app(app(reverse2, l), nil) |
| app(app(reverse2, nil), l) | → | l | | app(app(reverse2, app(app(cons, x), xs)), l) | → | app(app(reverse2, xs), app(app(cons, x), l)) |
| app(hd, app(app(cons, x), xs)) | → | x | | app(tl, app(app(cons, x), xs)) | → | xs |
| last | → | app(app(compose, hd), reverse) | | init | → | app(app(compose, reverse), app(app(compose, tl), reverse)) |
Original Signature
Termination of terms over the following signature is verified: app, reverse, tl, last, compose, init, hd, reverse2, nil, cons
Strategy
The following SCCs where found
| app#(app(reverse2, app(app(cons, x), xs)), l) → app#(app(cons, x), l) | app#(reverse, l) → app#(app(reverse2, l), nil) |
| app#(app(app(compose, f), g), x) → app#(g, app(f, x)) | app#(app(reverse2, app(app(cons, x), xs)), l) → app#(app(reverse2, xs), app(app(cons, x), l)) |
| app#(app(app(compose, f), g), x) → app#(f, x) |
Problem 2: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| app#(app(reverse2, app(app(cons, x), xs)), l) | → | app#(app(cons, x), l) | | app#(reverse, l) | → | app#(app(reverse2, l), nil) |
| app#(app(app(compose, f), g), x) | → | app#(g, app(f, x)) | | app#(app(reverse2, app(app(cons, x), xs)), l) | → | app#(app(reverse2, xs), app(app(cons, x), l)) |
| app#(app(app(compose, f), g), x) | → | app#(f, x) |
Rewrite Rules
| app(app(app(compose, f), g), x) | → | app(g, app(f, x)) | | app(reverse, l) | → | app(app(reverse2, l), nil) |
| app(app(reverse2, nil), l) | → | l | | app(app(reverse2, app(app(cons, x), xs)), l) | → | app(app(reverse2, xs), app(app(cons, x), l)) |
| app(hd, app(app(cons, x), xs)) | → | x | | app(tl, app(app(cons, x), xs)) | → | xs |
| last | → | app(app(compose, hd), reverse) | | init | → | app(app(compose, reverse), app(app(compose, tl), reverse)) |
Original Signature
Termination of terms over the following signature is verified: app, reverse, tl, last, compose, init, hd, reverse2, nil, cons
Strategy
Polynomial Interpretation
- app(x,y): y + x
- app#(x,y): y + x
- compose: 1
- cons: 0
- hd: 0
- init: 0
- last: 0
- nil: 0
- reverse: 0
- reverse2: 0
- tl: 0
Improved Usable rules
| app(app(reverse2, nil), l) | → | l | | app(hd, app(app(cons, x), xs)) | → | x |
| app(app(app(compose, f), g), x) | → | app(g, app(f, x)) | | app(app(reverse2, app(app(cons, x), xs)), l) | → | app(app(reverse2, xs), app(app(cons, x), l)) |
| app(tl, app(app(cons, x), xs)) | → | xs | | app(reverse, l) | → | app(app(reverse2, l), nil) |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| app#(app(app(compose, f), g), x) | → | app#(g, app(f, x)) | | app#(app(app(compose, f), g), x) | → | app#(f, x) |
Problem 3: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| app#(app(reverse2, app(app(cons, x), xs)), l) | → | app#(app(cons, x), l) | | app#(reverse, l) | → | app#(app(reverse2, l), nil) |
| app#(app(reverse2, app(app(cons, x), xs)), l) | → | app#(app(reverse2, xs), app(app(cons, x), l)) |
Rewrite Rules
| app(app(app(compose, f), g), x) | → | app(g, app(f, x)) | | app(reverse, l) | → | app(app(reverse2, l), nil) |
| app(app(reverse2, nil), l) | → | l | | app(app(reverse2, app(app(cons, x), xs)), l) | → | app(app(reverse2, xs), app(app(cons, x), l)) |
| app(hd, app(app(cons, x), xs)) | → | x | | app(tl, app(app(cons, x), xs)) | → | xs |
| last | → | app(app(compose, hd), reverse) | | init | → | app(app(compose, reverse), app(app(compose, tl), reverse)) |
Original Signature
Termination of terms over the following signature is verified: app, reverse, tl, last, init, compose, hd, reverse2, cons, nil
Strategy
Polynomial Interpretation
- app(x,y): y + x
- app#(x,y): y + x
- compose: 0
- cons: 2
- hd: 0
- init: 0
- last: 0
- nil: 0
- reverse: 1
- reverse2: 0
- tl: 0
Improved Usable rules
| app(app(reverse2, nil), l) | → | l | | app(hd, app(app(cons, x), xs)) | → | x |
| app(app(app(compose, f), g), x) | → | app(g, app(f, x)) | | app(app(reverse2, app(app(cons, x), xs)), l) | → | app(app(reverse2, xs), app(app(cons, x), l)) |
| app(tl, app(app(cons, x), xs)) | → | xs | | app(reverse, l) | → | app(app(reverse2, l), nil) |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| app#(reverse, l) | → | app#(app(reverse2, l), nil) |
Problem 4: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| app#(app(reverse2, app(app(cons, x), xs)), l) | → | app#(app(cons, x), l) | | app#(app(reverse2, app(app(cons, x), xs)), l) | → | app#(app(reverse2, xs), app(app(cons, x), l)) |
Rewrite Rules
| app(app(app(compose, f), g), x) | → | app(g, app(f, x)) | | app(reverse, l) | → | app(app(reverse2, l), nil) |
| app(app(reverse2, nil), l) | → | l | | app(app(reverse2, app(app(cons, x), xs)), l) | → | app(app(reverse2, xs), app(app(cons, x), l)) |
| app(hd, app(app(cons, x), xs)) | → | x | | app(tl, app(app(cons, x), xs)) | → | xs |
| last | → | app(app(compose, hd), reverse) | | init | → | app(app(compose, reverse), app(app(compose, tl), reverse)) |
Original Signature
Termination of terms over the following signature is verified: app, reverse, tl, last, compose, init, hd, reverse2, nil, cons
Strategy
Polynomial Interpretation
- app(x,y): y + x
- app#(x,y): x
- compose: 0
- cons: 2
- hd: 0
- init: 0
- last: 0
- nil: 0
- reverse: 0
- reverse2: 0
- tl: 0
Improved Usable rules
| app(app(reverse2, nil), l) | → | l | | app(hd, app(app(cons, x), xs)) | → | x |
| app(app(app(compose, f), g), x) | → | app(g, app(f, x)) | | app(app(reverse2, app(app(cons, x), xs)), l) | → | app(app(reverse2, xs), app(app(cons, x), l)) |
| app(tl, app(app(cons, x), xs)) | → | xs | | app(reverse, l) | → | app(app(reverse2, l), nil) |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| app#(app(reverse2, app(app(cons, x), xs)), l) | → | app#(app(reverse2, xs), app(app(cons, x), l)) |
Problem 5: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| app#(app(reverse2, app(app(cons, x), xs)), l) | → | app#(app(cons, x), l) |
Rewrite Rules
| app(app(app(compose, f), g), x) | → | app(g, app(f, x)) | | app(reverse, l) | → | app(app(reverse2, l), nil) |
| app(app(reverse2, nil), l) | → | l | | app(app(reverse2, app(app(cons, x), xs)), l) | → | app(app(reverse2, xs), app(app(cons, x), l)) |
| app(hd, app(app(cons, x), xs)) | → | x | | app(tl, app(app(cons, x), xs)) | → | xs |
| last | → | app(app(compose, hd), reverse) | | init | → | app(app(compose, reverse), app(app(compose, tl), reverse)) |
Original Signature
Termination of terms over the following signature is verified: app, reverse, tl, last, init, compose, hd, reverse2, cons, nil
Strategy
Polynomial Interpretation
- app(x,y): y + x
- app#(x,y): y + 2x
- compose: 2
- cons: 0
- hd: 0
- init: 0
- last: 0
- nil: 0
- reverse: 1
- reverse2: 1
- tl: 0
Improved Usable rules
| app(app(reverse2, nil), l) | → | l | | app(hd, app(app(cons, x), xs)) | → | x |
| app(app(app(compose, f), g), x) | → | app(g, app(f, x)) | | app(app(reverse2, app(app(cons, x), xs)), l) | → | app(app(reverse2, xs), app(app(cons, x), l)) |
| app(tl, app(app(cons, x), xs)) | → | xs | | app(reverse, l) | → | app(app(reverse2, l), nil) |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| app#(app(reverse2, app(app(cons, x), xs)), l) | → | app#(app(cons, x), l) |