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