YES
The TRS could be proven terminating. The proof took 1150 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (82ms).
| – Problem 2 was processed with processor SubtermCriterion (1ms).
| – Problem 3 was processed with processor SubtermCriterion (20ms).
| – Problem 4 was processed with processor PolynomialLinearRange4iUR (285ms).
| | – Problem 7 was processed with processor PolynomialOrderingProcessor (272ms).
| – Problem 5 was processed with processor SubtermCriterion (0ms).
| – Problem 6 was processed with processor SubtermCriterion (0ms).
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| odd#(s(s(x))) | → | odd#(x) | | *#(x, s(y)) | → | *#(x, y) |
| f#(x, s(y), z) | → | *#(x, x) | | f#(x, s(y), z) | → | f#(x, y, *(x, z)) |
| f#(x, s(y), z) | → | *#(x, z) | | half#(s(s(x))) | → | half#(x) |
| pow#(x, y) | → | f#(x, y, s(0)) | | f#(x, s(y), z) | → | if#(odd(s(y)), f(x, y, *(x, z)), f(*(x, x), half(s(y)), z)) |
| f#(x, s(y), z) | → | half#(s(y)) | | f#(x, s(y), z) | → | odd#(s(y)) |
| -#(s(x), s(y)) | → | -#(x, y) | | f#(x, s(y), z) | → | f#(*(x, x), half(s(y)), z) |
Rewrite Rules
| -(x, 0) | → | x | | -(s(x), s(y)) | → | -(x, y) |
| *(x, 0) | → | 0 | | *(x, s(y)) | → | +(*(x, y), x) |
| if(true, x, y) | → | x | | if(false, x, y) | → | y |
| odd(0) | → | false | | odd(s(0)) | → | true |
| odd(s(s(x))) | → | odd(x) | | half(0) | → | 0 |
| half(s(0)) | → | 0 | | half(s(s(x))) | → | s(half(x)) |
| if(true, x, y) | → | true | | if(false, x, y) | → | false |
| pow(x, y) | → | f(x, y, s(0)) | | f(x, 0, z) | → | z |
| f(x, s(y), z) | → | if(odd(s(y)), f(x, y, *(x, z)), f(*(x, x), half(s(y)), z)) |
Original Signature
Termination of terms over the following signature is verified: f, 0, pow, s, if, *, +, true, false, half, odd, -
Strategy
The following SCCs where found
| half#(s(s(x))) → half#(x) |
| f#(x, s(y), z) → f#(x, y, *(x, z)) | f#(x, s(y), z) → f#(*(x, x), half(s(y)), z) |
| -#(s(x), s(y)) → -#(x, y) |
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) |
| *(x, 0) | → | 0 | | *(x, s(y)) | → | +(*(x, y), x) |
| if(true, x, y) | → | x | | if(false, x, y) | → | y |
| odd(0) | → | false | | odd(s(0)) | → | true |
| odd(s(s(x))) | → | odd(x) | | half(0) | → | 0 |
| half(s(0)) | → | 0 | | half(s(s(x))) | → | s(half(x)) |
| if(true, x, y) | → | true | | if(false, x, y) | → | false |
| pow(x, y) | → | f(x, y, s(0)) | | f(x, 0, z) | → | z |
| f(x, s(y), z) | → | if(odd(s(y)), f(x, y, *(x, z)), f(*(x, x), half(s(y)), z)) |
Original Signature
Termination of terms over the following signature is verified: f, 0, pow, s, if, *, +, true, false, half, odd, -
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
Rewrite Rules
| -(x, 0) | → | x | | -(s(x), s(y)) | → | -(x, y) |
| *(x, 0) | → | 0 | | *(x, s(y)) | → | +(*(x, y), x) |
| if(true, x, y) | → | x | | if(false, x, y) | → | y |
| odd(0) | → | false | | odd(s(0)) | → | true |
| odd(s(s(x))) | → | odd(x) | | half(0) | → | 0 |
| half(s(0)) | → | 0 | | half(s(s(x))) | → | s(half(x)) |
| if(true, x, y) | → | true | | if(false, x, y) | → | false |
| pow(x, y) | → | f(x, y, s(0)) | | f(x, 0, z) | → | z |
| f(x, s(y), z) | → | if(odd(s(y)), f(x, y, *(x, z)), f(*(x, x), half(s(y)), z)) |
Original Signature
Termination of terms over the following signature is verified: f, 0, pow, s, if, *, +, true, false, half, odd, -
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
Problem 4: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| f#(x, s(y), z) | → | f#(x, y, *(x, z)) | | f#(x, s(y), z) | → | f#(*(x, x), half(s(y)), z) |
Rewrite Rules
| -(x, 0) | → | x | | -(s(x), s(y)) | → | -(x, y) |
| *(x, 0) | → | 0 | | *(x, s(y)) | → | +(*(x, y), x) |
| if(true, x, y) | → | x | | if(false, x, y) | → | y |
| odd(0) | → | false | | odd(s(0)) | → | true |
| odd(s(s(x))) | → | odd(x) | | half(0) | → | 0 |
| half(s(0)) | → | 0 | | half(s(s(x))) | → | s(half(x)) |
| if(true, x, y) | → | true | | if(false, x, y) | → | false |
| pow(x, y) | → | f(x, y, s(0)) | | f(x, 0, z) | → | z |
| f(x, s(y), z) | → | if(odd(s(y)), f(x, y, *(x, z)), f(*(x, x), half(s(y)), z)) |
Original Signature
Termination of terms over the following signature is verified: f, 0, pow, s, if, *, +, true, false, half, odd, -
Strategy
Polynomial Interpretation
- *(x,y): x
- +(x,y): 0
- -(x,y): 0
- 0: 1
- f(x,y,z): 0
- f#(x,y,z): y
- false: 0
- half(x): x
- if(x,y,z): 0
- odd(x): 0
- pow(x,y): 0
- s(x): 2x + 1
- true: 0
Improved Usable rules
| half(s(0)) | → | 0 | | half(0) | → | 0 |
| half(s(s(x))) | → | s(half(x)) |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| f#(x, s(y), z) | → | f#(x, y, *(x, z)) |
Problem 7: PolynomialOrderingProcessor
Dependency Pair Problem
Dependency Pairs
| f#(x, s(y), z) | → | f#(*(x, x), half(s(y)), z) |
Rewrite Rules
| -(x, 0) | → | x | | -(s(x), s(y)) | → | -(x, y) |
| *(x, 0) | → | 0 | | *(x, s(y)) | → | +(*(x, y), x) |
| if(true, x, y) | → | x | | if(false, x, y) | → | y |
| odd(0) | → | false | | odd(s(0)) | → | true |
| odd(s(s(x))) | → | odd(x) | | half(0) | → | 0 |
| half(s(0)) | → | 0 | | half(s(s(x))) | → | s(half(x)) |
| if(true, x, y) | → | true | | if(false, x, y) | → | false |
| pow(x, y) | → | f(x, y, s(0)) | | f(x, 0, z) | → | z |
| f(x, s(y), z) | → | if(odd(s(y)), f(x, y, *(x, z)), f(*(x, x), half(s(y)), z)) |
Original Signature
Termination of terms over the following signature is verified: f, pow, 0, s, if, *, half, false, true, +, odd, -
Strategy
Polynomial Interpretation
- *(x,y): 1
- +(x,y): 2x - 1
- -(x,y): -2
- 0: 0
- f(x,y,z): -2
- f#(x,y,z): z + y + x - 1
- false: -2
- half(x): x - 2
- if(x,y,z): -2
- odd(x): -2
- pow(x,y): -2
- s(x): x + 2
- true: -2
Improved Usable rules
| *(x, s(y)) | → | +(*(x, y), x) | | half(s(0)) | → | 0 |
| *(x, 0) | → | 0 | | half(0) | → | 0 |
| half(s(s(x))) | → | s(half(x)) |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| f#(x, s(y), z) | → | f#(*(x, x), half(s(y)), z) |
Problem 5: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| half#(s(s(x))) | → | half#(x) |
Rewrite Rules
| -(x, 0) | → | x | | -(s(x), s(y)) | → | -(x, y) |
| *(x, 0) | → | 0 | | *(x, s(y)) | → | +(*(x, y), x) |
| if(true, x, y) | → | x | | if(false, x, y) | → | y |
| odd(0) | → | false | | odd(s(0)) | → | true |
| odd(s(s(x))) | → | odd(x) | | half(0) | → | 0 |
| half(s(0)) | → | 0 | | half(s(s(x))) | → | s(half(x)) |
| if(true, x, y) | → | true | | if(false, x, y) | → | false |
| pow(x, y) | → | f(x, y, s(0)) | | f(x, 0, z) | → | z |
| f(x, s(y), z) | → | if(odd(s(y)), f(x, y, *(x, z)), f(*(x, x), half(s(y)), z)) |
Original Signature
Termination of terms over the following signature is verified: f, 0, pow, s, if, *, +, true, false, half, odd, -
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| half#(s(s(x))) | → | half#(x) |
Problem 6: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
Rewrite Rules
| -(x, 0) | → | x | | -(s(x), s(y)) | → | -(x, y) |
| *(x, 0) | → | 0 | | *(x, s(y)) | → | +(*(x, y), x) |
| if(true, x, y) | → | x | | if(false, x, y) | → | y |
| odd(0) | → | false | | odd(s(0)) | → | true |
| odd(s(s(x))) | → | odd(x) | | half(0) | → | 0 |
| half(s(0)) | → | 0 | | half(s(s(x))) | → | s(half(x)) |
| if(true, x, y) | → | true | | if(false, x, y) | → | false |
| pow(x, y) | → | f(x, y, s(0)) | | f(x, 0, z) | → | z |
| f(x, s(y), z) | → | if(odd(s(y)), f(x, y, *(x, z)), f(*(x, x), half(s(y)), z)) |
Original Signature
Termination of terms over the following signature is verified: f, 0, pow, s, if, *, +, true, false, half, odd, -
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed: