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 (55ms).
| – Problem 2 was processed with processor SubtermCriterion (2ms).
| – Problem 3 was processed with processor SubtermCriterion (0ms).
| – Problem 4 was processed with processor SubtermCriterion (1ms).
| – Problem 5 was processed with processor BackwardInstantiation (2ms).
| | – Problem 6 was processed with processor BackwardInstantiation (2ms).
| | | – Problem 7 was processed with processor Propagation (4ms).
| | | | – Problem 8 remains open; application of the following processors failed [ForwardNarrowing (0ms), BackwardInstantiation (0ms), ForwardInstantiation (0ms), Propagation (0ms)].
The following open problems remain:
Open Dependency Pair Problem 5
Dependency Pairs
| logIter#(x, y) | → | if#(le(s(0), x), le(s(s(0)), x), half(x), inc(y)) | | if#(true, true, x, y) | → | logIter#(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(s(x)) | → | s(inc(x)) | | inc(0) | → | s(0) |
| logarithm(x) | → | logIter(x, 0) | | logIter(x, y) | → | if(le(s(0), x), le(s(s(0)), x), half(x), inc(y)) |
| if(false, b, x, y) | → | logZeroError | | if(true, false, x, s(y)) | → | y |
| if(true, true, x, y) | → | logIter(x, y) | | f | → | g |
| f | → | h |
Original Signature
Termination of terms over the following signature is verified: f, g, half, true, logZeroError, h, logIter, 0, s, le, inc, logarithm, if, false
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| logarithm#(x) | → | logIter#(x, 0) | | le#(s(x), s(y)) | → | le#(x, y) |
| logIter#(x, y) | → | le#(s(0), x) | | logIter#(x, y) | → | half#(x) |
| logIter#(x, y) | → | inc#(y) | | half#(s(s(x))) | → | half#(x) |
| logIter#(x, y) | → | if#(le(s(0), x), le(s(s(0)), x), half(x), inc(y)) | | if#(true, true, x, y) | → | logIter#(x, y) |
| logIter#(x, y) | → | le#(s(s(0)), x) | | inc#(s(x)) | → | inc#(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(s(x)) | → | s(inc(x)) | | inc(0) | → | s(0) |
| logarithm(x) | → | logIter(x, 0) | | logIter(x, y) | → | if(le(s(0), x), le(s(s(0)), x), half(x), inc(y)) |
| if(false, b, x, y) | → | logZeroError | | if(true, false, x, s(y)) | → | y |
| if(true, true, x, y) | → | logIter(x, y) | | f | → | g |
| f | → | h |
Original Signature
Termination of terms over the following signature is verified: f, g, half, true, logZeroError, h, logIter, 0, s, le, inc, logarithm, if, false
Strategy
The following SCCs where found
| le#(s(x), s(y)) → le#(x, y) |
| if#(true, true, x, y) → logIter#(x, y) | logIter#(x, y) → if#(le(s(0), x), le(s(s(0)), x), half(x), inc(y)) |
| half#(s(s(x))) → half#(x) |
Problem 2: 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(s(x)) | → | s(inc(x)) | | inc(0) | → | s(0) |
| logarithm(x) | → | logIter(x, 0) | | logIter(x, y) | → | if(le(s(0), x), le(s(s(0)), x), half(x), inc(y)) |
| if(false, b, x, y) | → | logZeroError | | if(true, false, x, s(y)) | → | y |
| if(true, true, x, y) | → | logIter(x, y) | | f | → | g |
| f | → | h |
Original Signature
Termination of terms over the following signature is verified: f, g, half, true, logZeroError, h, logIter, 0, s, le, inc, logarithm, if, false
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| half#(s(s(x))) | → | half#(x) |
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(s(x)) | → | s(inc(x)) | | inc(0) | → | s(0) |
| logarithm(x) | → | logIter(x, 0) | | logIter(x, y) | → | if(le(s(0), x), le(s(s(0)), x), half(x), inc(y)) |
| if(false, b, x, y) | → | logZeroError | | if(true, false, x, s(y)) | → | y |
| if(true, true, x, y) | → | logIter(x, y) | | f | → | g |
| f | → | h |
Original Signature
Termination of terms over the following signature is verified: f, g, half, true, logZeroError, h, logIter, 0, s, le, inc, logarithm, if, false
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
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(s(x)) | → | s(inc(x)) | | inc(0) | → | s(0) |
| logarithm(x) | → | logIter(x, 0) | | logIter(x, y) | → | if(le(s(0), x), le(s(s(0)), x), half(x), inc(y)) |
| if(false, b, x, y) | → | logZeroError | | if(true, false, x, s(y)) | → | y |
| if(true, true, x, y) | → | logIter(x, y) | | f | → | g |
| f | → | h |
Original Signature
Termination of terms over the following signature is verified: f, g, half, true, logZeroError, h, logIter, 0, s, le, inc, logarithm, if, false
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
Problem 5: BackwardInstantiation
Dependency Pair Problem
Dependency Pairs
| if#(true, true, x, y) | → | logIter#(x, y) | | logIter#(x, y) | → | if#(le(s(0), x), le(s(s(0)), x), half(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(s(x)) | → | s(inc(x)) | | inc(0) | → | s(0) |
| logarithm(x) | → | logIter(x, 0) | | logIter(x, y) | → | if(le(s(0), x), le(s(s(0)), x), half(x), inc(y)) |
| if(false, b, x, y) | → | logZeroError | | if(true, false, x, s(y)) | → | y |
| if(true, true, x, y) | → | logIter(x, y) | | f | → | g |
| f | → | h |
Original Signature
Termination of terms over the following signature is verified: f, g, half, true, logZeroError, h, logIter, 0, s, le, inc, logarithm, if, false
Strategy
Instantiation
For all potential predecessors l → r of the rule logIter
#(
x,
y) → if
#(le(s(0),
x), le(s(s(0)),
x), half(
x), inc(
y)) on dependency pair chains it holds that:
- logIter#(x, y) matches r,
- all variables of logIter#(x, y) are embedded in constructor contexts, i.e., each subterm of logIter#(x, y), containing a variable is rooted by a constructor symbol.
Thus, logIter
#(
x,
y) → if
#(le(s(0),
x), le(s(s(0)),
x), half(
x), inc(
y)) is replaced by instances determined through the above matching. These instances are:
| logIter#(_x, _y) → if#(le(s(0), _x), le(s(s(0)), _x), half(_x), inc(_y)) |
Problem 6: BackwardInstantiation
Dependency Pair Problem
Dependency Pairs
| if#(true, true, x, y) | → | logIter#(x, y) | | logIter#(_x, _y) | → | if#(le(s(0), _x), le(s(s(0)), _x), half(_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(s(x)) | → | s(inc(x)) | | inc(0) | → | s(0) |
| logarithm(x) | → | logIter(x, 0) | | logIter(x, y) | → | if(le(s(0), x), le(s(s(0)), x), half(x), inc(y)) |
| if(false, b, x, y) | → | logZeroError | | if(true, false, x, s(y)) | → | y |
| if(true, true, x, y) | → | logIter(x, y) | | f | → | g |
| f | → | h |
Original Signature
Termination of terms over the following signature is verified: f, g, half, true, logZeroError, h, logIter, 0, s, le, inc, logarithm, if, false
Strategy
Instantiation
For all potential predecessors l → r of the rule logIter
#(
_x,
_y) → if
#(le(s(0),
_x), le(s(s(0)),
_x), half(
_x), inc(
_y)) on dependency pair chains it holds that:
- logIter#(_x, _y) matches r,
- all variables of logIter#(_x, _y) are embedded in constructor contexts, i.e., each subterm of logIter#(_x, _y), containing a variable is rooted by a constructor symbol.
Thus, logIter
#(
_x,
_y) → if
#(le(s(0),
_x), le(s(s(0)),
_x), half(
_x), inc(
_y)) is replaced by instances determined through the above matching. These instances are:
| logIter#(x, y) → if#(le(s(0), x), le(s(s(0)), x), half(x), inc(y)) |
Problem 7: Propagation
Dependency Pair Problem
Dependency Pairs
| if#(true, true, x, y) | → | logIter#(x, y) | | logIter#(x, y) | → | if#(le(s(0), x), le(s(s(0)), x), half(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(s(x)) | → | s(inc(x)) | | inc(0) | → | s(0) |
| logarithm(x) | → | logIter(x, 0) | | logIter(x, y) | → | if(le(s(0), x), le(s(s(0)), x), half(x), inc(y)) |
| if(false, b, x, y) | → | logZeroError | | if(true, false, x, s(y)) | → | y |
| if(true, true, x, y) | → | logIter(x, y) | | f | → | g |
| f | → | h |
Original Signature
Termination of terms over the following signature is verified: f, g, half, true, logZeroError, h, logIter, 0, s, le, inc, logarithm, if, false
Strategy
The dependency pairs if
#(true, true,
x,
y) → logIter
#(
x,
y) and logIter
#(
x,
y) → if
#(le(s(0),
x), le(s(s(0)),
x), half(
x), inc(
y)) are consolidated into the rule if
#(true, true,
x,
y) → if
#(le(s(0),
x), le(s(s(0)),
x), half(
x), inc(
y)) .
This is possible as
- all subterms of logIter#(x, y) containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in logIter#(x, y), but non-replacing in both if#(true, true, x, y) and if#(le(s(0), x), le(s(s(0)), x), half(x), inc(y))
The dependency pairs if
#(true, true,
x,
y) → logIter
#(
x,
y) and logIter
#(
x,
y) → if
#(le(s(0),
x), le(s(s(0)),
x), half(
x), inc(
y)) are consolidated into the rule if
#(true, true,
x,
y) → if
#(le(s(0),
x), le(s(s(0)),
x), half(
x), inc(
y)) .
This is possible as
- all subterms of logIter#(x, y) containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in logIter#(x, y), but non-replacing in both if#(true, true, x, y) and if#(le(s(0), x), le(s(s(0)), x), half(x), inc(y))
Summary
| Removed Dependency Pairs | Added Dependency Pairs |
|---|
| logIter#(x, y) → if#(le(s(0), x), le(s(s(0)), x), half(x), inc(y)) | if#(true, true, x, y) → if#(le(s(0), x), le(s(s(0)), x), half(x), inc(y)) |
| if#(true, true, x, y) → logIter#(x, y) | |