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