YES
The TRS could be proven terminating. The proof took 387 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (8ms).
| – Problem 2 was processed with processor SubtermCriterion (1ms).
| – Problem 3 was processed with processor PolynomialLinearRange4iUR (229ms).
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| concat#(cons(U, V), Y) | → | concat#(V, Y) | | lessleaves#(cons(U, V), cons(W, Z)) | → | lessleaves#(concat(U, V), concat(W, Z)) |
| lessleaves#(cons(U, V), cons(W, Z)) | → | concat#(U, V) | | lessleaves#(cons(U, V), cons(W, Z)) | → | concat#(W, Z) |
Rewrite Rules
| concat(leaf, Y) | → | Y | | concat(cons(U, V), Y) | → | cons(U, concat(V, Y)) |
| lessleaves(X, leaf) | → | false | | lessleaves(leaf, cons(W, Z)) | → | true |
| lessleaves(cons(U, V), cons(W, Z)) | → | lessleaves(concat(U, V), concat(W, Z)) |
Original Signature
Termination of terms over the following signature is verified: false, true, leaf, lessleaves, concat, cons
Strategy
The following SCCs where found
| concat#(cons(U, V), Y) → concat#(V, Y) |
| lessleaves#(cons(U, V), cons(W, Z)) → lessleaves#(concat(U, V), concat(W, Z)) |
Problem 2: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| concat#(cons(U, V), Y) | → | concat#(V, Y) |
Rewrite Rules
| concat(leaf, Y) | → | Y | | concat(cons(U, V), Y) | → | cons(U, concat(V, Y)) |
| lessleaves(X, leaf) | → | false | | lessleaves(leaf, cons(W, Z)) | → | true |
| lessleaves(cons(U, V), cons(W, Z)) | → | lessleaves(concat(U, V), concat(W, Z)) |
Original Signature
Termination of terms over the following signature is verified: false, true, leaf, lessleaves, concat, cons
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| concat#(cons(U, V), Y) | → | concat#(V, Y) |
Problem 3: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| lessleaves#(cons(U, V), cons(W, Z)) | → | lessleaves#(concat(U, V), concat(W, Z)) |
Rewrite Rules
| concat(leaf, Y) | → | Y | | concat(cons(U, V), Y) | → | cons(U, concat(V, Y)) |
| lessleaves(X, leaf) | → | false | | lessleaves(leaf, cons(W, Z)) | → | true |
| lessleaves(cons(U, V), cons(W, Z)) | → | lessleaves(concat(U, V), concat(W, Z)) |
Original Signature
Termination of terms over the following signature is verified: false, true, leaf, lessleaves, concat, cons
Strategy
Polynomial Interpretation
- concat(x,y): y + x
- cons(x,y): y + x + 1
- false: 0
- leaf: 0
- lessleaves(x,y): 0
- lessleaves#(x,y): 2y + 1
- true: 0
Improved Usable rules
| concat(cons(U, V), Y) | → | cons(U, concat(V, Y)) | | concat(leaf, Y) | → | Y |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| lessleaves#(cons(U, V), cons(W, Z)) | → | lessleaves#(concat(U, V), concat(W, Z)) |