YES
The TRS could be proven terminating. The proof took 342 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (88ms).
| – Problem 2 was processed with processor SubtermCriterion (1ms).
| – Problem 3 was processed with processor SubtermCriterion (0ms).
| | – Problem 5 was processed with processor PolynomialLinearRange4iUR (159ms).
| – Problem 4 was processed with processor SubtermCriterion (6ms).
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| f#(s(x), s(y), z, u) | → | f#(s(x), -(y, x), z, u) | | f#(s(x), 0, z, u) | → | -#(z, s(x)) |
| f#(s(x), s(y), z, u) | → | if#(<=(x, y), f(s(x), -(y, x), z, u), f(x, u, z, u)) | | f#(s(x), s(y), z, u) | → | <=#(x, y) |
| f#(s(x), s(y), z, u) | → | f#(x, u, z, u) | | perfectp#(s(x)) | → | f#(x, s(0), s(x), s(x)) |
| f#(s(x), 0, z, u) | → | f#(x, u, -(z, s(x)), u) | | <=#(s(x), s(y)) | → | <=#(x, y) |
| f#(s(x), s(y), z, u) | → | -#(y, x) | | -#(s(x), s(y)) | → | -#(x, y) |
Rewrite Rules
| -(x, 0) | → | x | | -(s(x), s(y)) | → | -(x, y) |
| <=(0, y) | → | true | | <=(s(x), 0) | → | false |
| <=(s(x), s(y)) | → | <=(x, y) | | if(true, x, y) | → | x |
| if(false, x, y) | → | y | | perfectp(0) | → | false |
| perfectp(s(x)) | → | f(x, s(0), s(x), s(x)) | | f(0, y, 0, u) | → | true |
| f(0, y, s(z), u) | → | false | | f(s(x), 0, z, u) | → | f(x, u, -(z, s(x)), u) |
| f(s(x), s(y), z, u) | → | if(<=(x, y), f(s(x), -(y, x), z, u), f(x, u, z, u)) |
Original Signature
Termination of terms over the following signature is verified: f, 0, s, <=, if, perfectp, true, false, -
Strategy
The following SCCs where found
| <=#(s(x), s(y)) → <=#(x, y) |
| -#(s(x), s(y)) → -#(x, y) |
| f#(s(x), s(y), z, u) → f#(s(x), -(y, x), z, u) | f#(s(x), s(y), z, u) → f#(x, u, z, u) |
| f#(s(x), 0, z, u) → f#(x, u, -(z, s(x)), u) |
Problem 2: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| -#(s(x), s(y)) | → | -#(x, y) |
Rewrite Rules
| -(x, 0) | → | x | | -(s(x), s(y)) | → | -(x, y) |
| <=(0, y) | → | true | | <=(s(x), 0) | → | false |
| <=(s(x), s(y)) | → | <=(x, y) | | if(true, x, y) | → | x |
| if(false, x, y) | → | y | | perfectp(0) | → | false |
| perfectp(s(x)) | → | f(x, s(0), s(x), s(x)) | | f(0, y, 0, u) | → | true |
| f(0, y, s(z), u) | → | false | | f(s(x), 0, z, u) | → | f(x, u, -(z, s(x)), u) |
| f(s(x), s(y), z, u) | → | if(<=(x, y), f(s(x), -(y, x), z, u), f(x, u, z, u)) |
Original Signature
Termination of terms over the following signature is verified: f, 0, s, <=, if, perfectp, true, false, -
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| -#(s(x), s(y)) | → | -#(x, y) |
Problem 3: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| f#(s(x), s(y), z, u) | → | f#(s(x), -(y, x), z, u) | | f#(s(x), s(y), z, u) | → | f#(x, u, z, u) |
| f#(s(x), 0, z, u) | → | f#(x, u, -(z, s(x)), u) |
Rewrite Rules
| -(x, 0) | → | x | | -(s(x), s(y)) | → | -(x, y) |
| <=(0, y) | → | true | | <=(s(x), 0) | → | false |
| <=(s(x), s(y)) | → | <=(x, y) | | if(true, x, y) | → | x |
| if(false, x, y) | → | y | | perfectp(0) | → | false |
| perfectp(s(x)) | → | f(x, s(0), s(x), s(x)) | | f(0, y, 0, u) | → | true |
| f(0, y, s(z), u) | → | false | | f(s(x), 0, z, u) | → | f(x, u, -(z, s(x)), u) |
| f(s(x), s(y), z, u) | → | if(<=(x, y), f(s(x), -(y, x), z, u), f(x, u, z, u)) |
Original Signature
Termination of terms over the following signature is verified: f, 0, s, <=, if, perfectp, true, false, -
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| f#(s(x), s(y), z, u) | → | f#(x, u, z, u) | | f#(s(x), 0, z, u) | → | f#(x, u, -(z, s(x)), u) |
Problem 5: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| f#(s(x), s(y), z, u) | → | f#(s(x), -(y, x), z, u) |
Rewrite Rules
| -(x, 0) | → | x | | -(s(x), s(y)) | → | -(x, y) |
| <=(0, y) | → | true | | <=(s(x), 0) | → | false |
| <=(s(x), s(y)) | → | <=(x, y) | | if(true, x, y) | → | x |
| if(false, x, y) | → | y | | perfectp(0) | → | false |
| perfectp(s(x)) | → | f(x, s(0), s(x), s(x)) | | f(0, y, 0, u) | → | true |
| f(0, y, s(z), u) | → | false | | f(s(x), 0, z, u) | → | f(x, u, -(z, s(x)), u) |
| f(s(x), s(y), z, u) | → | if(<=(x, y), f(s(x), -(y, x), z, u), f(x, u, z, u)) |
Original Signature
Termination of terms over the following signature is verified: f, 0, s, if, <=, perfectp, false, true, -
Strategy
Polynomial Interpretation
- -(x,y): x
- 0: 3
- <=(x,y): 0
- f(x1,x2,x3,x4): 0
- f#(x1,x2,x3,x4): x3 + x2
- false: 0
- if(x,y,z): 0
- perfectp(x): 0
- s(x): x + 1
- true: 0
Improved Usable rules
| -(s(x), s(y)) | → | -(x, y) | | -(x, 0) | → | x |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| f#(s(x), s(y), z, u) | → | f#(s(x), -(y, x), z, u) |
Problem 4: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| <=#(s(x), s(y)) | → | <=#(x, y) |
Rewrite Rules
| -(x, 0) | → | x | | -(s(x), s(y)) | → | -(x, y) |
| <=(0, y) | → | true | | <=(s(x), 0) | → | false |
| <=(s(x), s(y)) | → | <=(x, y) | | if(true, x, y) | → | x |
| if(false, x, y) | → | y | | perfectp(0) | → | false |
| perfectp(s(x)) | → | f(x, s(0), s(x), s(x)) | | f(0, y, 0, u) | → | true |
| f(0, y, s(z), u) | → | false | | f(s(x), 0, z, u) | → | f(x, u, -(z, s(x)), u) |
| f(s(x), s(y), z, u) | → | if(<=(x, y), f(s(x), -(y, x), z, u), f(x, u, z, u)) |
Original Signature
Termination of terms over the following signature is verified: f, 0, s, <=, if, perfectp, true, false, -
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| <=#(s(x), s(y)) | → | <=#(x, y) |