MAYBE
The TRS could not be proven terminating. The proof attempt took 37924 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (0ms).
| – Problem 2 was processed with processor PolynomialLinearRange4iUR (0ms).
| | – Problem 3 remains open; application of the following processors failed [DependencyGraph (8ms), PolynomialLinearRange4iUR (2682ms), DependencyGraph (6ms), PolynomialLinearRange8NegiUR (timeout), DependencyGraph (6ms), ReductionPairSAT (1150ms), DependencyGraph (46ms), SizeChangePrinciple (1990ms)].
The following open problems remain:
Open Dependency Pair Problem 3
Dependency Pairs
| incr#(cons(X, Y)) | → | activate#(X) | | adx#(cons(X, Y)) | → | incr#(cons(activate(X), n__adx(activate(Y)))) |
| activate#(n__adx(X)) | → | adx#(X) | | activate#(n__incr(X)) | → | incr#(X) |
| incr#(cons(X, Y)) | → | activate#(Y) |
Rewrite Rules
| nats | → | adx(zeros) | | zeros | → | cons(n__0, n__zeros) |
| incr(cons(X, Y)) | → | cons(n__s(activate(X)), n__incr(activate(Y))) | | adx(cons(X, Y)) | → | incr(cons(activate(X), n__adx(activate(Y)))) |
| hd(cons(X, Y)) | → | activate(X) | | tl(cons(X, Y)) | → | activate(Y) |
| 0 | → | n__0 | | zeros | → | n__zeros |
| s(X) | → | n__s(X) | | incr(X) | → | n__incr(X) |
| adx(X) | → | n__adx(X) | | activate(n__0) | → | 0 |
| activate(n__zeros) | → | zeros | | activate(n__s(X)) | → | s(X) |
| activate(n__incr(X)) | → | incr(X) | | activate(n__adx(X)) | → | adx(X) |
| activate(X) | → | X |
Original Signature
Termination of terms over the following signature is verified: n__incr, tl, hd, n__adx, activate, n__s, nats, 0, n__0, s, zeros, adx, incr, n__zeros, cons
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| incr#(cons(X, Y)) | → | activate#(X) | | adx#(cons(X, Y)) | → | incr#(cons(activate(X), n__adx(activate(Y)))) |
| activate#(n__zeros) | → | zeros# | | nats# | → | zeros# |
| tl#(cons(X, Y)) | → | activate#(Y) | | hd#(cons(X, Y)) | → | activate#(X) |
| activate#(n__incr(X)) | → | incr#(X) | | nats# | → | adx#(zeros) |
| activate#(n__s(X)) | → | s#(X) | | adx#(cons(X, Y)) | → | activate#(Y) |
| activate#(n__adx(X)) | → | adx#(X) | | adx#(cons(X, Y)) | → | activate#(X) |
| activate#(n__0) | → | 0# | | incr#(cons(X, Y)) | → | activate#(Y) |
Rewrite Rules
| nats | → | adx(zeros) | | zeros | → | cons(n__0, n__zeros) |
| incr(cons(X, Y)) | → | cons(n__s(activate(X)), n__incr(activate(Y))) | | adx(cons(X, Y)) | → | incr(cons(activate(X), n__adx(activate(Y)))) |
| hd(cons(X, Y)) | → | activate(X) | | tl(cons(X, Y)) | → | activate(Y) |
| 0 | → | n__0 | | zeros | → | n__zeros |
| s(X) | → | n__s(X) | | incr(X) | → | n__incr(X) |
| adx(X) | → | n__adx(X) | | activate(n__0) | → | 0 |
| activate(n__zeros) | → | zeros | | activate(n__s(X)) | → | s(X) |
| activate(n__incr(X)) | → | incr(X) | | activate(n__adx(X)) | → | adx(X) |
| activate(X) | → | X |
Original Signature
Termination of terms over the following signature is verified: n__incr, tl, hd, n__adx, activate, n__s, nats, 0, n__0, s, zeros, adx, incr, n__zeros, cons
Strategy
The following SCCs where found
| incr#(cons(X, Y)) → activate#(X) | adx#(cons(X, Y)) → incr#(cons(activate(X), n__adx(activate(Y)))) |
| adx#(cons(X, Y)) → activate#(Y) | activate#(n__adx(X)) → adx#(X) |
| adx#(cons(X, Y)) → activate#(X) | activate#(n__incr(X)) → incr#(X) |
| incr#(cons(X, Y)) → activate#(Y) |
Problem 2: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| incr#(cons(X, Y)) | → | activate#(X) | | adx#(cons(X, Y)) | → | incr#(cons(activate(X), n__adx(activate(Y)))) |
| adx#(cons(X, Y)) | → | activate#(Y) | | activate#(n__adx(X)) | → | adx#(X) |
| adx#(cons(X, Y)) | → | activate#(X) | | activate#(n__incr(X)) | → | incr#(X) |
| incr#(cons(X, Y)) | → | activate#(Y) |
Rewrite Rules
| nats | → | adx(zeros) | | zeros | → | cons(n__0, n__zeros) |
| incr(cons(X, Y)) | → | cons(n__s(activate(X)), n__incr(activate(Y))) | | adx(cons(X, Y)) | → | incr(cons(activate(X), n__adx(activate(Y)))) |
| hd(cons(X, Y)) | → | activate(X) | | tl(cons(X, Y)) | → | activate(Y) |
| 0 | → | n__0 | | zeros | → | n__zeros |
| s(X) | → | n__s(X) | | incr(X) | → | n__incr(X) |
| adx(X) | → | n__adx(X) | | activate(n__0) | → | 0 |
| activate(n__zeros) | → | zeros | | activate(n__s(X)) | → | s(X) |
| activate(n__incr(X)) | → | incr(X) | | activate(n__adx(X)) | → | adx(X) |
| activate(X) | → | X |
Original Signature
Termination of terms over the following signature is verified: n__incr, tl, hd, n__adx, activate, n__s, nats, 0, n__0, s, zeros, adx, incr, n__zeros, cons
Strategy
Polynomial Interpretation
- 0: 0
- activate(x): x
- activate#(x): 2x
- adx(x): x + 1
- adx#(x): 2x + 2
- cons(x,y): y + 2x
- hd(x): 0
- incr(x): x
- incr#(x): 2x
- n__0: 0
- n__adx(x): x + 1
- n__incr(x): x
- n__s(x): 0
- n__zeros: 0
- nats: 0
- s(x): 0
- tl(x): 0
- zeros: 0
Improved Usable rules
| activate(n__zeros) | → | zeros | | zeros | → | cons(n__0, n__zeros) |
| activate(n__s(X)) | → | s(X) | | activate(n__0) | → | 0 |
| zeros | → | n__zeros | | 0 | → | n__0 |
| s(X) | → | n__s(X) | | activate(X) | → | X |
| adx(cons(X, Y)) | → | incr(cons(activate(X), n__adx(activate(Y)))) | | incr(X) | → | n__incr(X) |
| activate(n__incr(X)) | → | incr(X) | | activate(n__adx(X)) | → | adx(X) |
| incr(cons(X, Y)) | → | cons(n__s(activate(X)), n__incr(activate(Y))) | | adx(X) | → | n__adx(X) |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| adx#(cons(X, Y)) | → | activate#(Y) | | adx#(cons(X, Y)) | → | activate#(X) |