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