MAYBE
The TRS could not be proven terminating. The proof attempt took 1041 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 (170ms), DependencyGraph (2ms), PolynomialLinearRange8NegiUR (426ms), DependencyGraph (4ms), ReductionPairSAT (166ms), DependencyGraph (2ms), SizeChangePrinciple (17ms)].
| – Problem 3 was processed with processor SubtermCriterion (0ms).
The following open problems remain:
Open Dependency Pair Problem 2
Dependency Pairs
| if#(true, x, c) | → | help#(x, s(c)) | | help#(x, c) | → | if#(lt(c, x), x, c) |
Rewrite Rules
| lt(0, s(x)) | → | true | | lt(x, 0) | → | false |
| lt(s(x), s(y)) | → | lt(x, y) | | fac(x) | → | help(x, 0) |
| help(x, c) | → | if(lt(c, x), x, c) | | if(true, x, c) | → | times(s(c), help(x, s(c))) |
| if(false, x, c) | → | s(0) |
Original Signature
Termination of terms over the following signature is verified: help, 0, s, times, if, fac, false, true, lt
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| if#(true, x, c) | → | help#(x, s(c)) | | lt#(s(x), s(y)) | → | lt#(x, y) |
| help#(x, c) | → | lt#(c, x) | | fac#(x) | → | help#(x, 0) |
| help#(x, c) | → | if#(lt(c, x), x, c) |
Rewrite Rules
| lt(0, s(x)) | → | true | | lt(x, 0) | → | false |
| lt(s(x), s(y)) | → | lt(x, y) | | fac(x) | → | help(x, 0) |
| help(x, c) | → | if(lt(c, x), x, c) | | if(true, x, c) | → | times(s(c), help(x, s(c))) |
| if(false, x, c) | → | s(0) |
Original Signature
Termination of terms over the following signature is verified: help, 0, s, times, if, fac, true, false, lt
Strategy
The following SCCs where found
| if#(true, x, c) → help#(x, s(c)) | help#(x, c) → if#(lt(c, x), x, c) |
| lt#(s(x), s(y)) → lt#(x, y) |
Problem 3: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| lt#(s(x), s(y)) | → | lt#(x, y) |
Rewrite Rules
| lt(0, s(x)) | → | true | | lt(x, 0) | → | false |
| lt(s(x), s(y)) | → | lt(x, y) | | fac(x) | → | help(x, 0) |
| help(x, c) | → | if(lt(c, x), x, c) | | if(true, x, c) | → | times(s(c), help(x, s(c))) |
| if(false, x, c) | → | s(0) |
Original Signature
Termination of terms over the following signature is verified: help, 0, s, times, if, fac, true, false, lt
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| lt#(s(x), s(y)) | → | lt#(x, y) |