MAYBE
The TRS could not be proven terminating. The proof attempt took 396 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (0ms).
| – Problem 2 was processed with processor SubtermCriterion (0ms).
| – Problem 3 remains open; application of the following processors failed [SubtermCriterion (0ms), DependencyGraph (1ms), PolynomialLinearRange4iUR (97ms), DependencyGraph (1ms), PolynomialLinearRange8NegiUR (104ms), DependencyGraph (2ms), ReductionPairSAT (36ms), DependencyGraph (1ms), SizeChangePrinciple (4ms)].
The following open problems remain:
Open Dependency Pair Problem 3
Dependency Pairs
| diff#(X, Y) | → | diff#(p(X), Y) |
Rewrite Rules
| p(0) | → | 0 | | p(s(X)) | → | X |
| leq(0, Y) | → | true | | leq(s(X), 0) | → | false |
| leq(s(X), s(Y)) | → | leq(X, Y) | | if(true, X, Y) | → | activate(X) |
| if(false, X, Y) | → | activate(Y) | | diff(X, Y) | → | if(leq(X, Y), n__0, n__s(diff(p(X), Y))) |
| 0 | → | n__0 | | s(X) | → | n__s(X) |
| activate(n__0) | → | 0 | | activate(n__s(X)) | → | s(X) |
| activate(X) | → | X |
Original Signature
Termination of terms over the following signature is verified: n__s, activate, n__0, 0, s, diff, if, leq, p, false, true
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| leq#(s(X), s(Y)) | → | leq#(X, Y) | | if#(true, X, Y) | → | activate#(X) |
| if#(false, X, Y) | → | activate#(Y) | | activate#(n__0) | → | 0# |
| diff#(X, Y) | → | diff#(p(X), Y) | | diff#(X, Y) | → | if#(leq(X, Y), n__0, n__s(diff(p(X), Y))) |
| p#(0) | → | 0# | | diff#(X, Y) | → | p#(X) |
| diff#(X, Y) | → | leq#(X, Y) | | activate#(n__s(X)) | → | s#(X) |
Rewrite Rules
| p(0) | → | 0 | | p(s(X)) | → | X |
| leq(0, Y) | → | true | | leq(s(X), 0) | → | false |
| leq(s(X), s(Y)) | → | leq(X, Y) | | if(true, X, Y) | → | activate(X) |
| if(false, X, Y) | → | activate(Y) | | diff(X, Y) | → | if(leq(X, Y), n__0, n__s(diff(p(X), Y))) |
| 0 | → | n__0 | | s(X) | → | n__s(X) |
| activate(n__0) | → | 0 | | activate(n__s(X)) | → | s(X) |
| activate(X) | → | X |
Original Signature
Termination of terms over the following signature is verified: activate, n__s, 0, n__0, s, diff, leq, if, p, true, false
Strategy
The following SCCs where found
| leq#(s(X), s(Y)) → leq#(X, Y) |
| diff#(X, Y) → diff#(p(X), Y) |
Problem 2: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| leq#(s(X), s(Y)) | → | leq#(X, Y) |
Rewrite Rules
| p(0) | → | 0 | | p(s(X)) | → | X |
| leq(0, Y) | → | true | | leq(s(X), 0) | → | false |
| leq(s(X), s(Y)) | → | leq(X, Y) | | if(true, X, Y) | → | activate(X) |
| if(false, X, Y) | → | activate(Y) | | diff(X, Y) | → | if(leq(X, Y), n__0, n__s(diff(p(X), Y))) |
| 0 | → | n__0 | | s(X) | → | n__s(X) |
| activate(n__0) | → | 0 | | activate(n__s(X)) | → | s(X) |
| activate(X) | → | X |
Original Signature
Termination of terms over the following signature is verified: activate, n__s, 0, n__0, s, diff, leq, if, p, true, false
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| leq#(s(X), s(Y)) | → | leq#(X, Y) |