TIMEOUT
The TRS could not be proven terminating. The proof attempt took 60040 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (103ms).
| – Problem 2 was processed with processor BackwardInstantiation (6ms).
| | – Problem 6 remains open; application of the following processors failed [ForwardInstantiation (3ms), Propagation (3ms), ForwardNarrowing (1ms), BackwardInstantiation (2ms), ForwardInstantiation (3ms), Propagation (2ms)].
| – Problem 3 was processed with processor SubtermCriterion (1ms).
| – Problem 4 was processed with processor SubtermCriterion (1ms).
| – Problem 5 was processed with processor SubtermCriterion (0ms).
The following open problems remain:
Open Dependency Pair Problem 2
Dependency Pairs
| if#(even, x, y, z, u) | → | timesIter#(half(x), y, half(z)) | | if#(even, x, y, z, u) | → | timesIter#(half(x), y, half(s(z))) |
| timesIter#(x, y, z) | → | if#(check(x), x, y, z, plus(z, y)) | | if#(odd, x, y, z, u) | → | timesIter#(p(x), y, u) |
Rewrite Rules
| check(0) | → | zero | | check(s(0)) | → | odd |
| check(s(s(0))) | → | even | | check(s(s(s(x)))) | → | check(s(x)) |
| half(0) | → | 0 | | half(s(0)) | → | 0 |
| half(s(s(x))) | → | s(half(x)) | | plus(0, y) | → | y |
| plus(s(x), y) | → | s(plus(x, y)) | | times(x, y) | → | timesIter(x, y, 0) |
| timesIter(x, y, z) | → | if(check(x), x, y, z, plus(z, y)) | | p(s(x)) | → | x |
| p(0) | → | 0 | | if(zero, x, y, z, u) | → | z |
| if(odd, x, y, z, u) | → | timesIter(p(x), y, u) | | if(even, x, y, z, u) | → | plus(timesIter(half(x), y, half(z)), timesIter(half(x), y, half(s(z)))) |
Original Signature
Termination of terms over the following signature is verified: plus, timesIter, 0, s, check, times, if, p, half, even, odd, zero
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| if#(even, x, y, z, u) | → | plus#(timesIter(half(x), y, half(z)), timesIter(half(x), y, half(s(z)))) | | if#(even, x, y, z, u) | → | half#(z) |
| half#(s(s(x))) | → | half#(x) | | if#(even, x, y, z, u) | → | half#(x) |
| if#(odd, x, y, z, u) | → | timesIter#(p(x), y, u) | | if#(odd, x, y, z, u) | → | p#(x) |
| check#(s(s(s(x)))) | → | check#(s(x)) | | times#(x, y) | → | timesIter#(x, y, 0) |
| if#(even, x, y, z, u) | → | timesIter#(half(x), y, half(z)) | | timesIter#(x, y, z) | → | check#(x) |
| if#(even, x, y, z, u) | → | half#(s(z)) | | plus#(s(x), y) | → | plus#(x, y) |
| timesIter#(x, y, z) | → | plus#(z, y) | | timesIter#(x, y, z) | → | if#(check(x), x, y, z, plus(z, y)) |
| if#(even, x, y, z, u) | → | timesIter#(half(x), y, half(s(z))) |
Rewrite Rules
| check(0) | → | zero | | check(s(0)) | → | odd |
| check(s(s(0))) | → | even | | check(s(s(s(x)))) | → | check(s(x)) |
| half(0) | → | 0 | | half(s(0)) | → | 0 |
| half(s(s(x))) | → | s(half(x)) | | plus(0, y) | → | y |
| plus(s(x), y) | → | s(plus(x, y)) | | times(x, y) | → | timesIter(x, y, 0) |
| timesIter(x, y, z) | → | if(check(x), x, y, z, plus(z, y)) | | p(s(x)) | → | x |
| p(0) | → | 0 | | if(zero, x, y, z, u) | → | z |
| if(odd, x, y, z, u) | → | timesIter(p(x), y, u) | | if(even, x, y, z, u) | → | plus(timesIter(half(x), y, half(z)), timesIter(half(x), y, half(s(z)))) |
Original Signature
Termination of terms over the following signature is verified: plus, timesIter, 0, check, s, times, if, p, half, even, zero, odd
Strategy
The following SCCs where found
| plus#(s(x), y) → plus#(x, y) |
| half#(s(s(x))) → half#(x) |
| check#(s(s(s(x)))) → check#(s(x)) |
| if#(even, x, y, z, u) → timesIter#(half(x), y, half(z)) | timesIter#(x, y, z) → if#(check(x), x, y, z, plus(z, y)) |
| if#(even, x, y, z, u) → timesIter#(half(x), y, half(s(z))) | if#(odd, x, y, z, u) → timesIter#(p(x), y, u) |
Problem 2: BackwardInstantiation
Dependency Pair Problem
Dependency Pairs
| if#(even, x, y, z, u) | → | timesIter#(half(x), y, half(z)) | | timesIter#(x, y, z) | → | if#(check(x), x, y, z, plus(z, y)) |
| if#(even, x, y, z, u) | → | timesIter#(half(x), y, half(s(z))) | | if#(odd, x, y, z, u) | → | timesIter#(p(x), y, u) |
Rewrite Rules
| check(0) | → | zero | | check(s(0)) | → | odd |
| check(s(s(0))) | → | even | | check(s(s(s(x)))) | → | check(s(x)) |
| half(0) | → | 0 | | half(s(0)) | → | 0 |
| half(s(s(x))) | → | s(half(x)) | | plus(0, y) | → | y |
| plus(s(x), y) | → | s(plus(x, y)) | | times(x, y) | → | timesIter(x, y, 0) |
| timesIter(x, y, z) | → | if(check(x), x, y, z, plus(z, y)) | | p(s(x)) | → | x |
| p(0) | → | 0 | | if(zero, x, y, z, u) | → | z |
| if(odd, x, y, z, u) | → | timesIter(p(x), y, u) | | if(even, x, y, z, u) | → | plus(timesIter(half(x), y, half(z)), timesIter(half(x), y, half(s(z)))) |
Original Signature
Termination of terms over the following signature is verified: plus, timesIter, 0, check, s, times, if, p, half, even, zero, odd
Strategy
Instantiation
For all potential predecessors l → r of the rule timesIter
#(
x,
y,
z) → if
#(check(
x),
x,
y,
z, plus(
z,
y)) on dependency pair chains it holds that:
- timesIter#(x, y, z) matches r,
- all variables of timesIter#(x, y, z) are embedded in constructor contexts, i.e., each subterm of timesIter#(x, y, z), containing a variable is rooted by a constructor symbol.
Thus, timesIter
#(
x,
y,
z) → if
#(check(
x),
x,
y,
z, plus(
z,
y)) is replaced by instances determined through the above matching. These instances are:
| timesIter#(half(_x), _y, half(_z)) → if#(check(half(_x)), half(_x), _y, half(_z), plus(half(_z), _y)) | timesIter#(p(_x), _y, _u) → if#(check(p(_x)), p(_x), _y, _u, plus(_u, _y)) |
| timesIter#(half(_x), _y, half(s(_z))) → if#(check(half(_x)), half(_x), _y, half(s(_z)), plus(half(s(_z)), _y)) |
Problem 3: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| check#(s(s(s(x)))) | → | check#(s(x)) |
Rewrite Rules
| check(0) | → | zero | | check(s(0)) | → | odd |
| check(s(s(0))) | → | even | | check(s(s(s(x)))) | → | check(s(x)) |
| half(0) | → | 0 | | half(s(0)) | → | 0 |
| half(s(s(x))) | → | s(half(x)) | | plus(0, y) | → | y |
| plus(s(x), y) | → | s(plus(x, y)) | | times(x, y) | → | timesIter(x, y, 0) |
| timesIter(x, y, z) | → | if(check(x), x, y, z, plus(z, y)) | | p(s(x)) | → | x |
| p(0) | → | 0 | | if(zero, x, y, z, u) | → | z |
| if(odd, x, y, z, u) | → | timesIter(p(x), y, u) | | if(even, x, y, z, u) | → | plus(timesIter(half(x), y, half(z)), timesIter(half(x), y, half(s(z)))) |
Original Signature
Termination of terms over the following signature is verified: plus, timesIter, 0, check, s, times, if, p, half, even, zero, odd
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| check#(s(s(s(x)))) | → | check#(s(x)) |
Problem 4: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| half#(s(s(x))) | → | half#(x) |
Rewrite Rules
| check(0) | → | zero | | check(s(0)) | → | odd |
| check(s(s(0))) | → | even | | check(s(s(s(x)))) | → | check(s(x)) |
| half(0) | → | 0 | | half(s(0)) | → | 0 |
| half(s(s(x))) | → | s(half(x)) | | plus(0, y) | → | y |
| plus(s(x), y) | → | s(plus(x, y)) | | times(x, y) | → | timesIter(x, y, 0) |
| timesIter(x, y, z) | → | if(check(x), x, y, z, plus(z, y)) | | p(s(x)) | → | x |
| p(0) | → | 0 | | if(zero, x, y, z, u) | → | z |
| if(odd, x, y, z, u) | → | timesIter(p(x), y, u) | | if(even, x, y, z, u) | → | plus(timesIter(half(x), y, half(z)), timesIter(half(x), y, half(s(z)))) |
Original Signature
Termination of terms over the following signature is verified: plus, timesIter, 0, check, s, times, if, p, half, even, zero, odd
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| half#(s(s(x))) | → | half#(x) |
Problem 5: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| plus#(s(x), y) | → | plus#(x, y) |
Rewrite Rules
| check(0) | → | zero | | check(s(0)) | → | odd |
| check(s(s(0))) | → | even | | check(s(s(s(x)))) | → | check(s(x)) |
| half(0) | → | 0 | | half(s(0)) | → | 0 |
| half(s(s(x))) | → | s(half(x)) | | plus(0, y) | → | y |
| plus(s(x), y) | → | s(plus(x, y)) | | times(x, y) | → | timesIter(x, y, 0) |
| timesIter(x, y, z) | → | if(check(x), x, y, z, plus(z, y)) | | p(s(x)) | → | x |
| p(0) | → | 0 | | if(zero, x, y, z, u) | → | z |
| if(odd, x, y, z, u) | → | timesIter(p(x), y, u) | | if(even, x, y, z, u) | → | plus(timesIter(half(x), y, half(z)), timesIter(half(x), y, half(s(z)))) |
Original Signature
Termination of terms over the following signature is verified: plus, timesIter, 0, check, s, times, if, p, half, even, zero, odd
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| plus#(s(x), y) | → | plus#(x, y) |