YES
The TRS could be proven terminating. The proof took 1638 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (42ms).
| – Problem 2 was processed with processor SubtermCriterion (3ms).
| – Problem 3 was processed with processor SubtermCriterion (11ms).
| – Problem 4 was processed with processor PolynomialLinearRange4iUR (226ms).
| | – Problem 6 was processed with processor PolynomialOrderingProcessor (880ms).
| | | – Problem 7 was processed with processor DependencyGraph (0ms).
| – Problem 5 was processed with processor SubtermCriterion (0ms).
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| if_times#(false, s(x), y) | → | plus#(y, times(x, y)) | | if_times#(true, s(x), y) | → | plus#(times(half(s(x)), y), times(half(s(x)), y)) |
| plus#(s(x), y) | → | plus#(x, y) | | even#(s(s(x))) | → | even#(x) |
| times#(s(x), y) | → | even#(s(x)) | | half#(s(s(x))) | → | half#(x) |
| times#(s(x), y) | → | if_times#(even(s(x)), s(x), y) | | if_times#(false, s(x), y) | → | times#(x, y) |
| if_times#(true, s(x), y) | → | times#(half(s(x)), y) | | if_times#(true, s(x), y) | → | half#(s(x)) |
Rewrite Rules
| even(0) | → | true | | even(s(0)) | → | false |
| even(s(s(x))) | → | even(x) | | half(0) | → | 0 |
| half(s(s(x))) | → | s(half(x)) | | plus(0, y) | → | y |
| plus(s(x), y) | → | s(plus(x, y)) | | times(0, y) | → | 0 |
| times(s(x), y) | → | if_times(even(s(x)), s(x), y) | | if_times(true, s(x), y) | → | plus(times(half(s(x)), y), times(half(s(x)), y)) |
| if_times(false, s(x), y) | → | plus(y, times(x, y)) |
Original Signature
Termination of terms over the following signature is verified: plus, 0, s, times, true, false, half, even, if_times
Strategy
The following SCCs where found
| times#(s(x), y) → if_times#(even(s(x)), s(x), y) | if_times#(false, s(x), y) → times#(x, y) |
| if_times#(true, s(x), y) → times#(half(s(x)), y) |
| plus#(s(x), y) → plus#(x, y) |
| even#(s(s(x))) → even#(x) |
| half#(s(s(x))) → half#(x) |
Problem 2: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| even#(s(s(x))) | → | even#(x) |
Rewrite Rules
| even(0) | → | true | | even(s(0)) | → | false |
| even(s(s(x))) | → | even(x) | | half(0) | → | 0 |
| half(s(s(x))) | → | s(half(x)) | | plus(0, y) | → | y |
| plus(s(x), y) | → | s(plus(x, y)) | | times(0, y) | → | 0 |
| times(s(x), y) | → | if_times(even(s(x)), s(x), y) | | if_times(true, s(x), y) | → | plus(times(half(s(x)), y), times(half(s(x)), y)) |
| if_times(false, s(x), y) | → | plus(y, times(x, y)) |
Original Signature
Termination of terms over the following signature is verified: plus, 0, s, times, true, false, half, even, if_times
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| even#(s(s(x))) | → | even#(x) |
Problem 3: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| plus#(s(x), y) | → | plus#(x, y) |
Rewrite Rules
| even(0) | → | true | | even(s(0)) | → | false |
| even(s(s(x))) | → | even(x) | | half(0) | → | 0 |
| half(s(s(x))) | → | s(half(x)) | | plus(0, y) | → | y |
| plus(s(x), y) | → | s(plus(x, y)) | | times(0, y) | → | 0 |
| times(s(x), y) | → | if_times(even(s(x)), s(x), y) | | if_times(true, s(x), y) | → | plus(times(half(s(x)), y), times(half(s(x)), y)) |
| if_times(false, s(x), y) | → | plus(y, times(x, y)) |
Original Signature
Termination of terms over the following signature is verified: plus, 0, s, times, true, false, half, even, if_times
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| plus#(s(x), y) | → | plus#(x, y) |
Problem 4: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| times#(s(x), y) | → | if_times#(even(s(x)), s(x), y) | | if_times#(false, s(x), y) | → | times#(x, y) |
| if_times#(true, s(x), y) | → | times#(half(s(x)), y) |
Rewrite Rules
| even(0) | → | true | | even(s(0)) | → | false |
| even(s(s(x))) | → | even(x) | | half(0) | → | 0 |
| half(s(s(x))) | → | s(half(x)) | | plus(0, y) | → | y |
| plus(s(x), y) | → | s(plus(x, y)) | | times(0, y) | → | 0 |
| times(s(x), y) | → | if_times(even(s(x)), s(x), y) | | if_times(true, s(x), y) | → | plus(times(half(s(x)), y), times(half(s(x)), y)) |
| if_times(false, s(x), y) | → | plus(y, times(x, y)) |
Original Signature
Termination of terms over the following signature is verified: plus, 0, s, times, true, false, half, even, if_times
Strategy
Polynomial Interpretation
- 0: 1
- even(x): x + 1
- false: 0
- half(x): x
- if_times(x,y,z): 0
- if_times#(x,y,z): 2y
- plus(x,y): 0
- s(x): x + 1
- times(x,y): 0
- times#(x,y): 2x
- true: 0
Improved Usable rules
| 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:
| if_times#(false, s(x), y) | → | times#(x, y) |
Problem 6: PolynomialOrderingProcessor
Dependency Pair Problem
Dependency Pairs
| times#(s(x), y) | → | if_times#(even(s(x)), s(x), y) | | if_times#(true, s(x), y) | → | times#(half(s(x)), y) |
Rewrite Rules
| even(0) | → | true | | even(s(0)) | → | false |
| even(s(s(x))) | → | even(x) | | half(0) | → | 0 |
| half(s(s(x))) | → | s(half(x)) | | plus(0, y) | → | y |
| plus(s(x), y) | → | s(plus(x, y)) | | times(0, y) | → | 0 |
| times(s(x), y) | → | if_times(even(s(x)), s(x), y) | | if_times(true, s(x), y) | → | plus(times(half(s(x)), y), times(half(s(x)), y)) |
| if_times(false, s(x), y) | → | plus(y, times(x, y)) |
Original Signature
Termination of terms over the following signature is verified: plus, 0, s, times, half, false, true, even, if_times
Strategy
Polynomial Interpretation
- 0: -1
- even(x): -1
- false: -1
- half(x): x - 2
- if_times(x,y,z): -2
- if_times#(x,y,z): z + y - 2
- plus(x,y): -2
- s(x): x + 2
- times(x,y): -2
- times#(x,y): y + x - 1
- true: 2
Improved Usable rules
| 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:
| times#(s(x), y) | → | if_times#(even(s(x)), s(x), y) |
Problem 7: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| if_times#(true, s(x), y) | → | times#(half(s(x)), y) |
Rewrite Rules
| even(0) | → | true | | even(s(0)) | → | false |
| even(s(s(x))) | → | even(x) | | half(0) | → | 0 |
| half(s(s(x))) | → | s(half(x)) | | plus(0, y) | → | y |
| plus(s(x), y) | → | s(plus(x, y)) | | times(0, y) | → | 0 |
| times(s(x), y) | → | if_times(even(s(x)), s(x), y) | | if_times(true, s(x), y) | → | plus(times(half(s(x)), y), times(half(s(x)), y)) |
| if_times(false, s(x), y) | → | plus(y, times(x, y)) |
Original Signature
Termination of terms over the following signature is verified: plus, 0, s, times, true, false, half, even, if_times
Strategy
There are no SCCs!
Problem 5: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| half#(s(s(x))) | → | half#(x) |
Rewrite Rules
| even(0) | → | true | | even(s(0)) | → | false |
| even(s(s(x))) | → | even(x) | | half(0) | → | 0 |
| half(s(s(x))) | → | s(half(x)) | | plus(0, y) | → | y |
| plus(s(x), y) | → | s(plus(x, y)) | | times(0, y) | → | 0 |
| times(s(x), y) | → | if_times(even(s(x)), s(x), y) | | if_times(true, s(x), y) | → | plus(times(half(s(x)), y), times(half(s(x)), y)) |
| if_times(false, s(x), y) | → | plus(y, times(x, y)) |
Original Signature
Termination of terms over the following signature is verified: plus, 0, s, times, true, false, half, even, if_times
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| half#(s(s(x))) | → | half#(x) |