MAYBE
The TRS could not be proven terminating. The proof attempt took 2739 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 (2ms), DependencyGraph (3ms), PolynomialLinearRange4iUR (213ms), DependencyGraph (3ms), PolynomialLinearRange8NegiUR (2057ms), DependencyGraph (2ms), ReductionPairSAT (170ms), DependencyGraph (3ms), SizeChangePrinciple (20ms)].
The following open problems remain:
Open Dependency Pair Problem 2
Dependency Pairs
| length#(cons(N, L)) | → | U11#(tt, activate(L)) | | U12#(tt, L) | → | length#(activate(L)) |
| U11#(tt, L) | → | U12#(tt, activate(L)) |
Rewrite Rules
| zeros | → | cons(0, n__zeros) | | U11(tt, L) | → | U12(tt, activate(L)) |
| U12(tt, L) | → | s(length(activate(L))) | | length(nil) | → | 0 |
| length(cons(N, L)) | → | U11(tt, activate(L)) | | zeros | → | n__zeros |
| activate(n__zeros) | → | zeros | | activate(X) | → | X |
Original Signature
Termination of terms over the following signature is verified: activate, 0, s, tt, zeros, length, U11, U12, n__zeros, nil, cons
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| activate#(n__zeros) | → | zeros# | | U12#(tt, L) | → | activate#(L) |
| length#(cons(N, L)) | → | U11#(tt, activate(L)) | | U12#(tt, L) | → | length#(activate(L)) |
| U11#(tt, L) | → | activate#(L) | | U11#(tt, L) | → | U12#(tt, activate(L)) |
| length#(cons(N, L)) | → | activate#(L) |
Rewrite Rules
| zeros | → | cons(0, n__zeros) | | U11(tt, L) | → | U12(tt, activate(L)) |
| U12(tt, L) | → | s(length(activate(L))) | | length(nil) | → | 0 |
| length(cons(N, L)) | → | U11(tt, activate(L)) | | zeros | → | n__zeros |
| activate(n__zeros) | → | zeros | | activate(X) | → | X |
Original Signature
Termination of terms over the following signature is verified: activate, 0, s, zeros, tt, length, U11, U12, n__zeros, cons, nil
Strategy
The following SCCs where found
| length#(cons(N, L)) → U11#(tt, activate(L)) | U12#(tt, L) → length#(activate(L)) |
| U11#(tt, L) → U12#(tt, activate(L)) |