MAYBE
The TRS could not be proven terminating. The proof attempt took 2555 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (0ms).
| – Problem 2 remains open; application of the following processors failed [SubtermCriterion (1ms), DependencyGraph (4ms), PolynomialLinearRange4iUR (354ms), DependencyGraph (1ms), PolynomialLinearRange8NegiUR (1476ms), DependencyGraph (1ms), ReductionPairSAT (188ms), DependencyGraph (3ms), SizeChangePrinciple (209ms)].
The following open problems remain:
Open Dependency Pair Problem 2
Dependency Pairs
| length1#(X) | → | length#(activate(X)) | | length#(n__cons(X, Y)) | → | length1#(activate(Y)) |
Rewrite Rules
| from(X) | → | cons(X, n__from(s(X))) | | length(n__nil) | → | 0 |
| length(n__cons(X, Y)) | → | s(length1(activate(Y))) | | length1(X) | → | length(activate(X)) |
| from(X) | → | n__from(X) | | nil | → | n__nil |
| cons(X1, X2) | → | n__cons(X1, X2) | | activate(n__from(X)) | → | from(X) |
| activate(n__nil) | → | nil | | activate(n__cons(X1, X2)) | → | cons(X1, X2) |
| activate(X) | → | X |
Original Signature
Termination of terms over the following signature is verified: activate, n__cons, 0, n__from, s, length, length1, n__nil, from, nil, cons
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| activate#(n__nil) | → | nil# | | from#(X) | → | cons#(X, n__from(s(X))) |
| length#(n__cons(X, Y)) | → | length1#(activate(Y)) | | length1#(X) | → | length#(activate(X)) |
| activate#(n__from(X)) | → | from#(X) | | length#(n__cons(X, Y)) | → | activate#(Y) |
| length1#(X) | → | activate#(X) | | activate#(n__cons(X1, X2)) | → | cons#(X1, X2) |
Rewrite Rules
| from(X) | → | cons(X, n__from(s(X))) | | length(n__nil) | → | 0 |
| length(n__cons(X, Y)) | → | s(length1(activate(Y))) | | length1(X) | → | length(activate(X)) |
| from(X) | → | n__from(X) | | nil | → | n__nil |
| cons(X1, X2) | → | n__cons(X1, X2) | | activate(n__from(X)) | → | from(X) |
| activate(n__nil) | → | nil | | activate(n__cons(X1, X2)) | → | cons(X1, X2) |
| activate(X) | → | X |
Original Signature
Termination of terms over the following signature is verified: activate, n__cons, 0, s, n__from, length, from, n__nil, length1, cons, nil
Strategy
The following SCCs where found
| length#(n__cons(X, Y)) → length1#(activate(Y)) | length1#(X) → length#(activate(X)) |