YES
The TRS could be proven terminating. The proof took 772 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (28ms).
| – Problem 2 was processed with processor PolynomialLinearRange4iUR (280ms).
| | – Problem 3 was processed with processor PolynomialLinearRange4iUR (152ms).
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| a#(a(x, y), z) | → | a#(y, z) | | a#(lambda(x), y) | → | lambda#(a(x, a(y, t))) |
| a#(lambda(x), y) | → | lambda#(a(x, 1)) | | a#(a(x, y), z) | → | a#(x, a(y, z)) |
| a#(lambda(x), y) | → | a#(y, t) | | a#(lambda(x), y) | → | a#(x, 1) |
| a#(lambda(x), y) | → | a#(x, a(y, t)) |
Rewrite Rules
| a(lambda(x), y) | → | lambda(a(x, 1)) | | a(lambda(x), y) | → | lambda(a(x, a(y, t))) |
| a(a(x, y), z) | → | a(x, a(y, z)) | | lambda(x) | → | x |
| a(x, y) | → | x | | a(x, y) | → | y |
Original Signature
Termination of terms over the following signature is verified: lambda, 1, t, a
Strategy
The following SCCs where found
| a#(a(x, y), z) → a#(y, z) | a#(a(x, y), z) → a#(x, a(y, z)) |
| a#(lambda(x), y) → a#(y, t) | a#(lambda(x), y) → a#(x, 1) |
| a#(lambda(x), y) → a#(x, a(y, t)) |
Problem 2: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| a#(a(x, y), z) | → | a#(y, z) | | a#(a(x, y), z) | → | a#(x, a(y, z)) |
| a#(lambda(x), y) | → | a#(y, t) | | a#(lambda(x), y) | → | a#(x, 1) |
| a#(lambda(x), y) | → | a#(x, a(y, t)) |
Rewrite Rules
| a(lambda(x), y) | → | lambda(a(x, 1)) | | a(lambda(x), y) | → | lambda(a(x, a(y, t))) |
| a(a(x, y), z) | → | a(x, a(y, z)) | | lambda(x) | → | x |
| a(x, y) | → | x | | a(x, y) | → | y |
Original Signature
Termination of terms over the following signature is verified: lambda, 1, t, a
Strategy
Polynomial Interpretation
- 1: 0
- a(x,y): y + x
- a#(x,y): 2y + 2x
- lambda(x): x + 1
- t: 0
Improved Usable rules
| a(lambda(x), y) | → | lambda(a(x, 1)) | | a(x, y) | → | y |
| lambda(x) | → | x | | a(lambda(x), y) | → | lambda(a(x, a(y, t))) |
| a(x, y) | → | x | | a(a(x, y), z) | → | a(x, a(y, z)) |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| a#(lambda(x), y) | → | a#(y, t) | | a#(lambda(x), y) | → | a#(x, 1) |
| a#(lambda(x), y) | → | a#(x, a(y, t)) |
Problem 3: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| a#(a(x, y), z) | → | a#(y, z) | | a#(a(x, y), z) | → | a#(x, a(y, z)) |
Rewrite Rules
| a(lambda(x), y) | → | lambda(a(x, 1)) | | a(lambda(x), y) | → | lambda(a(x, a(y, t))) |
| a(a(x, y), z) | → | a(x, a(y, z)) | | lambda(x) | → | x |
| a(x, y) | → | x | | a(x, y) | → | y |
Original Signature
Termination of terms over the following signature is verified: lambda, 1, t, a
Strategy
Polynomial Interpretation
- 1: 0
- a(x,y): 2y + 2x + 1
- a#(x,y): 2x
- lambda(x): 1
- t: 0
Improved Usable rules
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| a#(a(x, y), z) | → | a#(y, z) | | a#(a(x, y), z) | → | a#(x, a(y, z)) |