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