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 (80ms).
| – Problem 2 was processed with processor SubtermCriterion (1ms).
| – Problem 3 was processed with processor SubtermCriterion (1ms).
| – Problem 4 was processed with processor SubtermCriterion (1ms).
| – Problem 5 was processed with processor BackwardInstantiation (2ms).
| | – Problem 7 was processed with processor ForwardInstantiation (3ms).
| | | – Problem 8 was processed with processor Propagation (4ms).
| | | | – Problem 9 remains open; application of the following processors failed [ForwardNarrowing (1ms), BackwardInstantiation (1ms), ForwardInstantiation (3ms), Propagation (1ms)].
| – Problem 6 was processed with processor PolynomialLinearRange4iUR (125ms).
The following open problems remain:
Open Dependency Pair Problem 5
Dependency Pairs
| if2#(false, x, y) | → | log2#(quot(x, s(s(0))), y) | | log2#(x, y) | → | if#(le(x, 0), le(x, s(0)), x, inc(y)) |
| if#(false, b, x, y) | → | if2#(b, x, y) |
Rewrite Rules
| 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)) | | minus(0, y) | → | 0 |
| minus(x, 0) | → | x | | minus(s(x), s(y)) | → | minus(x, y) |
| quot(0, s(y)) | → | 0 | | quot(s(x), s(y)) | → | s(quot(minus(x, y), s(y))) |
| log(x) | → | log2(x, 0) | | log2(x, y) | → | if(le(x, 0), le(x, s(0)), x, inc(y)) |
| if(true, b, x, y) | → | log_undefined | | if(false, b, x, y) | → | if2(b, x, y) |
| if2(true, x, s(y)) | → | y | | if2(false, x, y) | → | log2(quot(x, s(s(0))), y) |
Original Signature
Termination of terms over the following signature is verified: minus, true, log2, if2, log, 0, le, s, inc, if, false, log_undefined, quot
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| log2#(x, y) | → | inc#(y) | | log2#(x, y) | → | le#(x, 0) |
| if2#(false, x, y) | → | log2#(quot(x, s(s(0))), y) | | quot#(s(x), s(y)) | → | minus#(x, y) |
| if2#(false, x, y) | → | quot#(x, s(s(0))) | | le#(s(x), s(y)) | → | le#(x, y) |
| quot#(s(x), s(y)) | → | quot#(minus(x, y), s(y)) | | minus#(s(x), s(y)) | → | minus#(x, y) |
| log2#(x, y) | → | le#(x, s(0)) | | inc#(s(x)) | → | inc#(x) |
| log2#(x, y) | → | if#(le(x, 0), le(x, s(0)), x, inc(y)) | | log#(x) | → | log2#(x, 0) |
| if#(false, b, x, y) | → | if2#(b, x, y) |
Rewrite Rules
| 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)) | | minus(0, y) | → | 0 |
| minus(x, 0) | → | x | | minus(s(x), s(y)) | → | minus(x, y) |
| quot(0, s(y)) | → | 0 | | quot(s(x), s(y)) | → | s(quot(minus(x, y), s(y))) |
| log(x) | → | log2(x, 0) | | log2(x, y) | → | if(le(x, 0), le(x, s(0)), x, inc(y)) |
| if(true, b, x, y) | → | log_undefined | | if(false, b, x, y) | → | if2(b, x, y) |
| if2(true, x, s(y)) | → | y | | if2(false, x, y) | → | log2(quot(x, s(s(0))), y) |
Original Signature
Termination of terms over the following signature is verified: minus, true, log2, if2, log, 0, le, s, inc, if, false, log_undefined, quot
Strategy
The following SCCs where found
| le#(s(x), s(y)) → le#(x, y) |
| quot#(s(x), s(y)) → quot#(minus(x, y), s(y)) |
| minus#(s(x), s(y)) → minus#(x, y) |
| if2#(false, x, y) → log2#(quot(x, s(s(0))), y) | log2#(x, y) → if#(le(x, 0), le(x, s(0)), x, inc(y)) |
| if#(false, b, x, y) → if2#(b, x, y) |
Problem 2: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
Rewrite Rules
| 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)) | | minus(0, y) | → | 0 |
| minus(x, 0) | → | x | | minus(s(x), s(y)) | → | minus(x, y) |
| quot(0, s(y)) | → | 0 | | quot(s(x), s(y)) | → | s(quot(minus(x, y), s(y))) |
| log(x) | → | log2(x, 0) | | log2(x, y) | → | if(le(x, 0), le(x, s(0)), x, inc(y)) |
| if(true, b, x, y) | → | log_undefined | | if(false, b, x, y) | → | if2(b, x, y) |
| if2(true, x, s(y)) | → | y | | if2(false, x, y) | → | log2(quot(x, s(s(0))), y) |
Original Signature
Termination of terms over the following signature is verified: minus, true, log2, if2, log, 0, le, s, inc, if, false, log_undefined, quot
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
| 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)) | | minus(0, y) | → | 0 |
| minus(x, 0) | → | x | | minus(s(x), s(y)) | → | minus(x, y) |
| quot(0, s(y)) | → | 0 | | quot(s(x), s(y)) | → | s(quot(minus(x, y), s(y))) |
| log(x) | → | log2(x, 0) | | log2(x, y) | → | if(le(x, 0), le(x, s(0)), x, inc(y)) |
| if(true, b, x, y) | → | log_undefined | | if(false, b, x, y) | → | if2(b, x, y) |
| if2(true, x, s(y)) | → | y | | if2(false, x, y) | → | log2(quot(x, s(s(0))), y) |
Original Signature
Termination of terms over the following signature is verified: minus, true, log2, if2, log, 0, le, s, inc, if, false, log_undefined, quot
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
| minus#(s(x), s(y)) | → | minus#(x, y) |
Rewrite Rules
| 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)) | | minus(0, y) | → | 0 |
| minus(x, 0) | → | x | | minus(s(x), s(y)) | → | minus(x, y) |
| quot(0, s(y)) | → | 0 | | quot(s(x), s(y)) | → | s(quot(minus(x, y), s(y))) |
| log(x) | → | log2(x, 0) | | log2(x, y) | → | if(le(x, 0), le(x, s(0)), x, inc(y)) |
| if(true, b, x, y) | → | log_undefined | | if(false, b, x, y) | → | if2(b, x, y) |
| if2(true, x, s(y)) | → | y | | if2(false, x, y) | → | log2(quot(x, s(s(0))), y) |
Original Signature
Termination of terms over the following signature is verified: minus, true, log2, if2, log, 0, le, s, inc, if, false, log_undefined, quot
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| minus#(s(x), s(y)) | → | minus#(x, y) |
Problem 5: BackwardInstantiation
Dependency Pair Problem
Dependency Pairs
| if2#(false, x, y) | → | log2#(quot(x, s(s(0))), y) | | log2#(x, y) | → | if#(le(x, 0), le(x, s(0)), x, inc(y)) |
| if#(false, b, x, y) | → | if2#(b, x, y) |
Rewrite Rules
| 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)) | | minus(0, y) | → | 0 |
| minus(x, 0) | → | x | | minus(s(x), s(y)) | → | minus(x, y) |
| quot(0, s(y)) | → | 0 | | quot(s(x), s(y)) | → | s(quot(minus(x, y), s(y))) |
| log(x) | → | log2(x, 0) | | log2(x, y) | → | if(le(x, 0), le(x, s(0)), x, inc(y)) |
| if(true, b, x, y) | → | log_undefined | | if(false, b, x, y) | → | if2(b, x, y) |
| if2(true, x, s(y)) | → | y | | if2(false, x, y) | → | log2(quot(x, s(s(0))), y) |
Original Signature
Termination of terms over the following signature is verified: minus, true, log2, if2, log, 0, le, s, inc, if, false, log_undefined, quot
Strategy
Instantiation
For all potential predecessors l → r of the rule log2
#(
x,
y) → if
#(le(
x, 0), 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, 0), le(
x, s(0)),
x, inc(
y)) is replaced by instances determined through the above matching. These instances are:
| log2#(quot(_x, s(s(0))), _y) → if#(le(quot(_x, s(s(0))), 0), le(quot(_x, s(s(0))), s(0)), quot(_x, s(s(0))), inc(_y)) |
Problem 7: ForwardInstantiation
Dependency Pair Problem
Dependency Pairs
| log2#(quot(_x, s(s(0))), _y) | → | if#(le(quot(_x, s(s(0))), 0), le(quot(_x, s(s(0))), s(0)), quot(_x, s(s(0))), inc(_y)) | | if2#(false, x, y) | → | log2#(quot(x, s(s(0))), y) |
| if#(false, b, x, y) | → | if2#(b, x, y) |
Rewrite Rules
| 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)) | | minus(0, y) | → | 0 |
| minus(x, 0) | → | x | | minus(s(x), s(y)) | → | minus(x, y) |
| quot(0, s(y)) | → | 0 | | quot(s(x), s(y)) | → | s(quot(minus(x, y), s(y))) |
| log(x) | → | log2(x, 0) | | log2(x, y) | → | if(le(x, 0), le(x, s(0)), x, inc(y)) |
| if(true, b, x, y) | → | log_undefined | | if(false, b, x, y) | → | if2(b, x, y) |
| if2(true, x, s(y)) | → | y | | if2(false, x, y) | → | log2(quot(x, s(s(0))), y) |
Original Signature
Termination of terms over the following signature is verified: minus, true, log2, if2, log, 0, le, s, inc, if, false, log_undefined, quot
Strategy
Instantiation
For all potential successors l → r of the rule if
#(false,
b,
x,
y) → if2
#(
b,
x,
y) on dependency pair chains it holds that:
- if2#(b, x, y) matches l,
- all variables of if2#(b, x, y) are embedded in constructor contexts, i.e., each subterm of if2#(b, x, y) containing a variable is rooted by a constructor symbol.
Thus, if
#(false,
b,
x,
y) → if2
#(
b,
x,
y) is replaced by instances determined through the above matching. These instances are:
| if#(false, false, x, y) → if2#(false, x, y) |
Problem 8: Propagation
Dependency Pair Problem
Dependency Pairs
| log2#(quot(_x, s(s(0))), _y) | → | if#(le(quot(_x, s(s(0))), 0), le(quot(_x, s(s(0))), s(0)), quot(_x, s(s(0))), inc(_y)) | | if#(false, false, x, y) | → | if2#(false, x, y) |
| if2#(false, x, y) | → | log2#(quot(x, s(s(0))), y) |
Rewrite Rules
| 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)) | | minus(0, y) | → | 0 |
| minus(x, 0) | → | x | | minus(s(x), s(y)) | → | minus(x, y) |
| quot(0, s(y)) | → | 0 | | quot(s(x), s(y)) | → | s(quot(minus(x, y), s(y))) |
| log(x) | → | log2(x, 0) | | log2(x, y) | → | if(le(x, 0), le(x, s(0)), x, inc(y)) |
| if(true, b, x, y) | → | log_undefined | | if(false, b, x, y) | → | if2(b, x, y) |
| if2(true, x, s(y)) | → | y | | if2(false, x, y) | → | log2(quot(x, s(s(0))), y) |
Original Signature
Termination of terms over the following signature is verified: minus, true, log2, if2, log, 0, le, s, inc, if, false, log_undefined, quot
Strategy
The dependency pairs if
#(false, false,
x,
y) → if2
#(false,
x,
y) and if2
#(false,
x,
y) → log2
#(quot(
x, s(s(0))),
y) are consolidated into the rule if
#(false, false,
x,
y) → log2
#(quot(
x, s(s(0))),
y) .
This is possible as
- all subterms of if2#(false, x, y) containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in if2#(false, x, y), but non-replacing in both if#(false, false, x, y) and log2#(quot(x, s(s(0))), y)
The dependency pairs if
#(false, false,
x,
y) → if2
#(false,
x,
y) and if2
#(false,
x,
y) → log2
#(quot(
x, s(s(0))),
y) are consolidated into the rule if
#(false, false,
x,
y) → log2
#(quot(
x, s(s(0))),
y) .
This is possible as
- all subterms of if2#(false, x, y) containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in if2#(false, x, y), but non-replacing in both if#(false, false, x, y) and log2#(quot(x, s(s(0))), y)
The dependency pairs if
#(false, false,
x,
y) → if2
#(false,
x,
y) and if2
#(false,
x,
y) → log2
#(quot(
x, s(s(0))),
y) are consolidated into the rule if
#(false, false,
x,
y) → log2
#(quot(
x, s(s(0))),
y) .
This is possible as
- all subterms of if2#(false, x, y) containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in if2#(false, x, y), but non-replacing in both if#(false, false, x, y) and log2#(quot(x, s(s(0))), y)
Summary
| Removed Dependency Pairs | Added Dependency Pairs |
|---|
| if#(false, false, x, y) → if2#(false, x, y) | if#(false, false, x, y) → log2#(quot(x, s(s(0))), y) |
| if2#(false, x, y) → log2#(quot(x, s(s(0))), y) | |
Problem 6: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| quot#(s(x), s(y)) | → | quot#(minus(x, y), s(y)) |
Rewrite Rules
| 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)) | | minus(0, y) | → | 0 |
| minus(x, 0) | → | x | | minus(s(x), s(y)) | → | minus(x, y) |
| quot(0, s(y)) | → | 0 | | quot(s(x), s(y)) | → | s(quot(minus(x, y), s(y))) |
| log(x) | → | log2(x, 0) | | log2(x, y) | → | if(le(x, 0), le(x, s(0)), x, inc(y)) |
| if(true, b, x, y) | → | log_undefined | | if(false, b, x, y) | → | if2(b, x, y) |
| if2(true, x, s(y)) | → | y | | if2(false, x, y) | → | log2(quot(x, s(s(0))), y) |
Original Signature
Termination of terms over the following signature is verified: minus, true, log2, if2, log, 0, le, s, inc, if, false, log_undefined, quot
Strategy
Polynomial Interpretation
- 0: 0
- false: 0
- if(x1,x2,x3,x4): 0
- if2(x,y,z): 0
- inc(x): 0
- le(x,y): 0
- log(x): 0
- log2(x,y): 0
- log_undefined: 0
- minus(x,y): x
- quot(x,y): 0
- quot#(x,y): x
- s(x): 2x + 2
- true: 0
Improved Usable rules
| minus(s(x), s(y)) | → | minus(x, y) | | minus(0, y) | → | 0 |
| minus(x, 0) | → | x |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| quot#(s(x), s(y)) | → | quot#(minus(x, y), s(y)) |