YES
The TRS could be proven terminating. The proof took 2950 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (189ms).
| – Problem 2 was processed with processor SubtermCriterion (3ms).
| – Problem 3 was processed with processor PolynomialLinearRange4iUR (1690ms).
| | – Problem 4 was processed with processor PolynomialLinearRange4iUR (938ms).
| | | – Problem 5 was processed with processor PolynomialLinearRange4iUR (81ms).
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| eq#(apply(t, s), apply(t', s')) | → | and#(eq(t, t'), eq(s, s')) | | eq#(lambda(x, t), lambda(x', t')) | → | eq#(t, t') |
| ren#(x, y, apply(t, s)) | → | ren#(x, y, t) | | ren#(var(l), var(k), var(l')) | → | eq#(l, l') |
| eq#(cons(t, l), cons(t', l')) | → | eq#(l, l') | | ren#(x, y, lambda(z, t)) | → | ren#(z, var(cons(x, cons(y, cons(lambda(z, t), nil)))), t) |
| eq#(apply(t, s), apply(t', s')) | → | eq#(t, t') | | ren#(var(l), var(k), var(l')) | → | if#(eq(l, l'), var(k), var(l')) |
| eq#(apply(t, s), apply(t', s')) | → | eq#(s, s') | | eq#(cons(t, l), cons(t', l')) | → | eq#(t, t') |
| eq#(lambda(x, t), lambda(x', t')) | → | eq#(x, x') | | eq#(lambda(x, t), lambda(x', t')) | → | and#(eq(x, x'), eq(t, t')) |
| ren#(x, y, lambda(z, t)) | → | ren#(x, y, ren(z, var(cons(x, cons(y, cons(lambda(z, t), nil)))), t)) | | eq#(cons(t, l), cons(t', l')) | → | and#(eq(t, t'), eq(l, l')) |
| ren#(x, y, apply(t, s)) | → | ren#(x, y, s) | | eq#(var(l), var(l')) | → | eq#(l, l') |
Rewrite Rules
| and(true, y) | → | y | | and(false, y) | → | false |
| eq(nil, nil) | → | true | | eq(cons(t, l), nil) | → | false |
| eq(nil, cons(t, l)) | → | false | | eq(cons(t, l), cons(t', l')) | → | and(eq(t, t'), eq(l, l')) |
| eq(var(l), var(l')) | → | eq(l, l') | | eq(var(l), apply(t, s)) | → | false |
| eq(var(l), lambda(x, t)) | → | false | | eq(apply(t, s), var(l)) | → | false |
| eq(apply(t, s), apply(t', s')) | → | and(eq(t, t'), eq(s, s')) | | eq(apply(t, s), lambda(x, t)) | → | false |
| eq(lambda(x, t), var(l)) | → | false | | eq(lambda(x, t), apply(t, s)) | → | false |
| eq(lambda(x, t), lambda(x', t')) | → | and(eq(x, x'), eq(t, t')) | | if(true, var(k), var(l')) | → | var(k) |
| if(false, var(k), var(l')) | → | var(l') | | ren(var(l), var(k), var(l')) | → | if(eq(l, l'), var(k), var(l')) |
| ren(x, y, apply(t, s)) | → | apply(ren(x, y, t), ren(x, y, s)) | | ren(x, y, lambda(z, t)) | → | lambda(var(cons(x, cons(y, cons(lambda(z, t), nil)))), ren(x, y, ren(z, var(cons(x, cons(y, cons(lambda(z, t), nil)))), t))) |
Original Signature
Termination of terms over the following signature is verified: apply, lambda, var, if, true, false, ren, and, eq, nil, cons
Strategy
The following SCCs where found
| eq#(cons(t, l), cons(t', l')) → eq#(t, t') | eq#(lambda(x, t), lambda(x', t')) → eq#(t, t') |
| eq#(lambda(x, t), lambda(x', t')) → eq#(x, x') | eq#(cons(t, l), cons(t', l')) → eq#(l, l') |
| eq#(apply(t, s), apply(t', s')) → eq#(t, t') | eq#(var(l), var(l')) → eq#(l, l') |
| eq#(apply(t, s), apply(t', s')) → eq#(s, s') |
| ren#(x, y, apply(t, s)) → ren#(x, y, t) | ren#(x, y, lambda(z, t)) → ren#(x, y, ren(z, var(cons(x, cons(y, cons(lambda(z, t), nil)))), t)) |
| ren#(x, y, lambda(z, t)) → ren#(z, var(cons(x, cons(y, cons(lambda(z, t), nil)))), t) | ren#(x, y, apply(t, s)) → ren#(x, y, s) |
Problem 2: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| eq#(cons(t, l), cons(t', l')) | → | eq#(t, t') | | eq#(lambda(x, t), lambda(x', t')) | → | eq#(t, t') |
| eq#(lambda(x, t), lambda(x', t')) | → | eq#(x, x') | | eq#(cons(t, l), cons(t', l')) | → | eq#(l, l') |
| eq#(apply(t, s), apply(t', s')) | → | eq#(t, t') | | eq#(var(l), var(l')) | → | eq#(l, l') |
| eq#(apply(t, s), apply(t', s')) | → | eq#(s, s') |
Rewrite Rules
| and(true, y) | → | y | | and(false, y) | → | false |
| eq(nil, nil) | → | true | | eq(cons(t, l), nil) | → | false |
| eq(nil, cons(t, l)) | → | false | | eq(cons(t, l), cons(t', l')) | → | and(eq(t, t'), eq(l, l')) |
| eq(var(l), var(l')) | → | eq(l, l') | | eq(var(l), apply(t, s)) | → | false |
| eq(var(l), lambda(x, t)) | → | false | | eq(apply(t, s), var(l)) | → | false |
| eq(apply(t, s), apply(t', s')) | → | and(eq(t, t'), eq(s, s')) | | eq(apply(t, s), lambda(x, t)) | → | false |
| eq(lambda(x, t), var(l)) | → | false | | eq(lambda(x, t), apply(t, s)) | → | false |
| eq(lambda(x, t), lambda(x', t')) | → | and(eq(x, x'), eq(t, t')) | | if(true, var(k), var(l')) | → | var(k) |
| if(false, var(k), var(l')) | → | var(l') | | ren(var(l), var(k), var(l')) | → | if(eq(l, l'), var(k), var(l')) |
| ren(x, y, apply(t, s)) | → | apply(ren(x, y, t), ren(x, y, s)) | | ren(x, y, lambda(z, t)) | → | lambda(var(cons(x, cons(y, cons(lambda(z, t), nil)))), ren(x, y, ren(z, var(cons(x, cons(y, cons(lambda(z, t), nil)))), t))) |
Original Signature
Termination of terms over the following signature is verified: apply, lambda, var, if, true, false, ren, and, eq, nil, cons
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| eq#(lambda(x, t), lambda(x', t')) | → | eq#(t, t') | | eq#(cons(t, l), cons(t', l')) | → | eq#(t, t') |
| eq#(lambda(x, t), lambda(x', t')) | → | eq#(x, x') | | eq#(cons(t, l), cons(t', l')) | → | eq#(l, l') |
| eq#(apply(t, s), apply(t', s')) | → | eq#(t, t') | | eq#(var(l), var(l')) | → | eq#(l, l') |
| eq#(apply(t, s), apply(t', s')) | → | eq#(s, s') |
Problem 3: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| ren#(x, y, apply(t, s)) | → | ren#(x, y, t) | | ren#(x, y, lambda(z, t)) | → | ren#(x, y, ren(z, var(cons(x, cons(y, cons(lambda(z, t), nil)))), t)) |
| ren#(x, y, lambda(z, t)) | → | ren#(z, var(cons(x, cons(y, cons(lambda(z, t), nil)))), t) | | ren#(x, y, apply(t, s)) | → | ren#(x, y, s) |
Rewrite Rules
| and(true, y) | → | y | | and(false, y) | → | false |
| eq(nil, nil) | → | true | | eq(cons(t, l), nil) | → | false |
| eq(nil, cons(t, l)) | → | false | | eq(cons(t, l), cons(t', l')) | → | and(eq(t, t'), eq(l, l')) |
| eq(var(l), var(l')) | → | eq(l, l') | | eq(var(l), apply(t, s)) | → | false |
| eq(var(l), lambda(x, t)) | → | false | | eq(apply(t, s), var(l)) | → | false |
| eq(apply(t, s), apply(t', s')) | → | and(eq(t, t'), eq(s, s')) | | eq(apply(t, s), lambda(x, t)) | → | false |
| eq(lambda(x, t), var(l)) | → | false | | eq(lambda(x, t), apply(t, s)) | → | false |
| eq(lambda(x, t), lambda(x', t')) | → | and(eq(x, x'), eq(t, t')) | | if(true, var(k), var(l')) | → | var(k) |
| if(false, var(k), var(l')) | → | var(l') | | ren(var(l), var(k), var(l')) | → | if(eq(l, l'), var(k), var(l')) |
| ren(x, y, apply(t, s)) | → | apply(ren(x, y, t), ren(x, y, s)) | | ren(x, y, lambda(z, t)) | → | lambda(var(cons(x, cons(y, cons(lambda(z, t), nil)))), ren(x, y, ren(z, var(cons(x, cons(y, cons(lambda(z, t), nil)))), t))) |
Original Signature
Termination of terms over the following signature is verified: apply, lambda, var, if, true, false, ren, and, eq, nil, cons
Strategy
Polynomial Interpretation
- and(x,y): 0
- apply(x,y): y + x + 2
- cons(x,y): 0
- eq(x,y): 0
- false: 0
- if(x,y,z): 0
- lambda(x,y): y + x
- nil: 2
- ren(x,y,z): z
- ren#(x,y,z): z + y
- true: 1
- var(x): 0
Improved Usable rules
| ren(var(l), var(k), var(l')) | → | if(eq(l, l'), var(k), var(l')) | | if(true, var(k), var(l')) | → | var(k) |
| ren(x, y, lambda(z, t)) | → | lambda(var(cons(x, cons(y, cons(lambda(z, t), nil)))), ren(x, y, ren(z, var(cons(x, cons(y, cons(lambda(z, t), nil)))), t))) | | if(false, var(k), var(l')) | → | var(l') |
| ren(x, y, apply(t, s)) | → | apply(ren(x, y, t), ren(x, y, s)) |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| ren#(x, y, apply(t, s)) | → | ren#(x, y, t) | | ren#(x, y, apply(t, s)) | → | ren#(x, y, s) |
Problem 4: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| ren#(x, y, lambda(z, t)) | → | ren#(x, y, ren(z, var(cons(x, cons(y, cons(lambda(z, t), nil)))), t)) | | ren#(x, y, lambda(z, t)) | → | ren#(z, var(cons(x, cons(y, cons(lambda(z, t), nil)))), t) |
Rewrite Rules
| and(true, y) | → | y | | and(false, y) | → | false |
| eq(nil, nil) | → | true | | eq(cons(t, l), nil) | → | false |
| eq(nil, cons(t, l)) | → | false | | eq(cons(t, l), cons(t', l')) | → | and(eq(t, t'), eq(l, l')) |
| eq(var(l), var(l')) | → | eq(l, l') | | eq(var(l), apply(t, s)) | → | false |
| eq(var(l), lambda(x, t)) | → | false | | eq(apply(t, s), var(l)) | → | false |
| eq(apply(t, s), apply(t', s')) | → | and(eq(t, t'), eq(s, s')) | | eq(apply(t, s), lambda(x, t)) | → | false |
| eq(lambda(x, t), var(l)) | → | false | | eq(lambda(x, t), apply(t, s)) | → | false |
| eq(lambda(x, t), lambda(x', t')) | → | and(eq(x, x'), eq(t, t')) | | if(true, var(k), var(l')) | → | var(k) |
| if(false, var(k), var(l')) | → | var(l') | | ren(var(l), var(k), var(l')) | → | if(eq(l, l'), var(k), var(l')) |
| ren(x, y, apply(t, s)) | → | apply(ren(x, y, t), ren(x, y, s)) | | ren(x, y, lambda(z, t)) | → | lambda(var(cons(x, cons(y, cons(lambda(z, t), nil)))), ren(x, y, ren(z, var(cons(x, cons(y, cons(lambda(z, t), nil)))), t))) |
Original Signature
Termination of terms over the following signature is verified: lambda, apply, if, var, ren, false, true, cons, nil, eq, and
Strategy
Polynomial Interpretation
- and(x,y): 2y
- apply(x,y): 2y + 2
- cons(x,y): 2x
- eq(x,y): 0
- false: 0
- if(x,y,z): x + 1
- lambda(x,y): y + 1
- nil: 0
- ren(x,y,z): z
- ren#(x,y,z): 2z + 2y
- true: 0
- var(x): 1
Improved Usable rules
| ren(var(l), var(k), var(l')) | → | if(eq(l, l'), var(k), var(l')) | | if(true, var(k), var(l')) | → | var(k) |
| eq(nil, nil) | → | true | | eq(lambda(x, t), apply(t, s)) | → | false |
| eq(cons(t, l), cons(t', l')) | → | and(eq(t, t'), eq(l, l')) | | ren(x, y, lambda(z, t)) | → | lambda(var(cons(x, cons(y, cons(lambda(z, t), nil)))), ren(x, y, ren(z, var(cons(x, cons(y, cons(lambda(z, t), nil)))), t))) |
| eq(var(l), lambda(x, t)) | → | false | | ren(x, y, apply(t, s)) | → | apply(ren(x, y, t), ren(x, y, s)) |
| if(false, var(k), var(l')) | → | var(l') | | and(true, y) | → | y |
| eq(apply(t, s), var(l)) | → | false | | and(false, y) | → | false |
| eq(lambda(x, t), lambda(x', t')) | → | and(eq(x, x'), eq(t, t')) | | eq(lambda(x, t), var(l)) | → | false |
| eq(nil, cons(t, l)) | → | false | | eq(apply(t, s), apply(t', s')) | → | and(eq(t, t'), eq(s, s')) |
| eq(apply(t, s), lambda(x, t)) | → | false | | eq(var(l), var(l')) | → | eq(l, l') |
| eq(cons(t, l), nil) | → | false | | eq(var(l), apply(t, s)) | → | false |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| ren#(x, y, lambda(z, t)) | → | ren#(x, y, ren(z, var(cons(x, cons(y, cons(lambda(z, t), nil)))), t)) |
Problem 5: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| ren#(x, y, lambda(z, t)) | → | ren#(z, var(cons(x, cons(y, cons(lambda(z, t), nil)))), t) |
Rewrite Rules
| and(true, y) | → | y | | and(false, y) | → | false |
| eq(nil, nil) | → | true | | eq(cons(t, l), nil) | → | false |
| eq(nil, cons(t, l)) | → | false | | eq(cons(t, l), cons(t', l')) | → | and(eq(t, t'), eq(l, l')) |
| eq(var(l), var(l')) | → | eq(l, l') | | eq(var(l), apply(t, s)) | → | false |
| eq(var(l), lambda(x, t)) | → | false | | eq(apply(t, s), var(l)) | → | false |
| eq(apply(t, s), apply(t', s')) | → | and(eq(t, t'), eq(s, s')) | | eq(apply(t, s), lambda(x, t)) | → | false |
| eq(lambda(x, t), var(l)) | → | false | | eq(lambda(x, t), apply(t, s)) | → | false |
| eq(lambda(x, t), lambda(x', t')) | → | and(eq(x, x'), eq(t, t')) | | if(true, var(k), var(l')) | → | var(k) |
| if(false, var(k), var(l')) | → | var(l') | | ren(var(l), var(k), var(l')) | → | if(eq(l, l'), var(k), var(l')) |
| ren(x, y, apply(t, s)) | → | apply(ren(x, y, t), ren(x, y, s)) | | ren(x, y, lambda(z, t)) | → | lambda(var(cons(x, cons(y, cons(lambda(z, t), nil)))), ren(x, y, ren(z, var(cons(x, cons(y, cons(lambda(z, t), nil)))), t))) |
Original Signature
Termination of terms over the following signature is verified: apply, lambda, var, if, true, false, ren, and, eq, nil, cons
Strategy
Polynomial Interpretation
- and(x,y): 0
- apply(x,y): 0
- cons(x,y): 1
- eq(x,y): 0
- false: 0
- if(x,y,z): 0
- lambda(x,y): y + 2
- nil: 3
- ren(x,y,z): 0
- ren#(x,y,z): z + 1
- true: 0
- var(x): 0
There are no usable rules
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| ren#(x, y, lambda(z, t)) | → | ren#(z, var(cons(x, cons(y, cons(lambda(z, t), nil)))), t) |