TIMEOUT
The TRS could not be proven terminating. The proof attempt took 60003 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (61ms).
| – Problem 2 was processed with processor SubtermCriterion (1ms).
| – Problem 3 was processed with processor SubtermCriterion (1ms).
| – Problem 4 was processed with processor BackwardInstantiation (2ms).
| | – Problem 6 was processed with processor BackwardInstantiation (1ms).
| | | – Problem 7 was processed with processor Propagation (3ms).
| | | | – Problem 8 remains open; application of the following processors failed [ForwardNarrowing (0ms), BackwardInstantiation (1ms), ForwardInstantiation (1ms), Propagation (1ms)].
| – Problem 5 was processed with processor SubtermCriterion (0ms).
The following open problems remain:
Open Dependency Pair Problem 4
Dependency Pairs
| if#(false, x, y, z) | → | facIter#(x, z) | | facIter#(x, y) | → | if#(isZero(x), minus(x, s(0)), y, times(y, x)) |
Rewrite Rules
| plus(0, x) | → | x | | plus(s(x), y) | → | s(plus(x, y)) |
| times(0, y) | → | 0 | | times(s(x), y) | → | plus(y, times(x, y)) |
| p(s(x)) | → | x | | p(0) | → | 0 |
| minus(x, 0) | → | x | | minus(0, x) | → | 0 |
| minus(x, s(y)) | → | p(minus(x, y)) | | isZero(0) | → | true |
| isZero(s(x)) | → | false | | facIter(x, y) | → | if(isZero(x), minus(x, s(0)), y, times(y, x)) |
| if(true, x, y, z) | → | y | | if(false, x, y, z) | → | facIter(x, z) |
| factorial(x) | → | facIter(x, s(0)) |
Original Signature
Termination of terms over the following signature is verified: plus, minus, 0, s, times, if, p, false, true, factorial, facIter, isZero
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| times#(s(x), y) | → | plus#(y, times(x, y)) | | facIter#(x, y) | → | minus#(x, s(0)) |
| times#(s(x), y) | → | times#(x, y) | | if#(false, x, y, z) | → | facIter#(x, z) |
| plus#(s(x), y) | → | plus#(x, y) | | minus#(x, s(y)) | → | minus#(x, y) |
| facIter#(x, y) | → | isZero#(x) | | minus#(x, s(y)) | → | p#(minus(x, y)) |
| facIter#(x, y) | → | times#(y, x) | | factorial#(x) | → | facIter#(x, s(0)) |
| facIter#(x, y) | → | if#(isZero(x), minus(x, s(0)), y, times(y, x)) |
Rewrite Rules
| plus(0, x) | → | x | | plus(s(x), y) | → | s(plus(x, y)) |
| times(0, y) | → | 0 | | times(s(x), y) | → | plus(y, times(x, y)) |
| p(s(x)) | → | x | | p(0) | → | 0 |
| minus(x, 0) | → | x | | minus(0, x) | → | 0 |
| minus(x, s(y)) | → | p(minus(x, y)) | | isZero(0) | → | true |
| isZero(s(x)) | → | false | | facIter(x, y) | → | if(isZero(x), minus(x, s(0)), y, times(y, x)) |
| if(true, x, y, z) | → | y | | if(false, x, y, z) | → | facIter(x, z) |
| factorial(x) | → | facIter(x, s(0)) |
Original Signature
Termination of terms over the following signature is verified: plus, 0, minus, s, times, if, p, true, false, facIter, factorial, isZero
Strategy
The following SCCs where found
| if#(false, x, y, z) → facIter#(x, z) | facIter#(x, y) → if#(isZero(x), minus(x, s(0)), y, times(y, x)) |
| times#(s(x), y) → times#(x, y) |
| plus#(s(x), y) → plus#(x, y) |
| minus#(x, s(y)) → minus#(x, y) |
Problem 2: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| minus#(x, s(y)) | → | minus#(x, y) |
Rewrite Rules
| plus(0, x) | → | x | | plus(s(x), y) | → | s(plus(x, y)) |
| times(0, y) | → | 0 | | times(s(x), y) | → | plus(y, times(x, y)) |
| p(s(x)) | → | x | | p(0) | → | 0 |
| minus(x, 0) | → | x | | minus(0, x) | → | 0 |
| minus(x, s(y)) | → | p(minus(x, y)) | | isZero(0) | → | true |
| isZero(s(x)) | → | false | | facIter(x, y) | → | if(isZero(x), minus(x, s(0)), y, times(y, x)) |
| if(true, x, y, z) | → | y | | if(false, x, y, z) | → | facIter(x, z) |
| factorial(x) | → | facIter(x, s(0)) |
Original Signature
Termination of terms over the following signature is verified: plus, 0, minus, s, times, if, p, true, false, facIter, factorial, isZero
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| minus#(x, s(y)) | → | minus#(x, y) |
Problem 3: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| plus#(s(x), y) | → | plus#(x, y) |
Rewrite Rules
| plus(0, x) | → | x | | plus(s(x), y) | → | s(plus(x, y)) |
| times(0, y) | → | 0 | | times(s(x), y) | → | plus(y, times(x, y)) |
| p(s(x)) | → | x | | p(0) | → | 0 |
| minus(x, 0) | → | x | | minus(0, x) | → | 0 |
| minus(x, s(y)) | → | p(minus(x, y)) | | isZero(0) | → | true |
| isZero(s(x)) | → | false | | facIter(x, y) | → | if(isZero(x), minus(x, s(0)), y, times(y, x)) |
| if(true, x, y, z) | → | y | | if(false, x, y, z) | → | facIter(x, z) |
| factorial(x) | → | facIter(x, s(0)) |
Original Signature
Termination of terms over the following signature is verified: plus, 0, minus, s, times, if, p, true, false, facIter, factorial, isZero
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| plus#(s(x), y) | → | plus#(x, y) |
Problem 4: BackwardInstantiation
Dependency Pair Problem
Dependency Pairs
| if#(false, x, y, z) | → | facIter#(x, z) | | facIter#(x, y) | → | if#(isZero(x), minus(x, s(0)), y, times(y, x)) |
Rewrite Rules
| plus(0, x) | → | x | | plus(s(x), y) | → | s(plus(x, y)) |
| times(0, y) | → | 0 | | times(s(x), y) | → | plus(y, times(x, y)) |
| p(s(x)) | → | x | | p(0) | → | 0 |
| minus(x, 0) | → | x | | minus(0, x) | → | 0 |
| minus(x, s(y)) | → | p(minus(x, y)) | | isZero(0) | → | true |
| isZero(s(x)) | → | false | | facIter(x, y) | → | if(isZero(x), minus(x, s(0)), y, times(y, x)) |
| if(true, x, y, z) | → | y | | if(false, x, y, z) | → | facIter(x, z) |
| factorial(x) | → | facIter(x, s(0)) |
Original Signature
Termination of terms over the following signature is verified: plus, 0, minus, s, times, if, p, true, false, facIter, factorial, isZero
Strategy
Instantiation
For all potential predecessors l → r of the rule facIter
#(
x,
y) → if
#(isZero(
x), minus(
x, s(0)),
y, times(
y,
x)) on dependency pair chains it holds that:
- facIter#(x, y) matches r,
- all variables of facIter#(x, y) are embedded in constructor contexts, i.e., each subterm of facIter#(x, y), containing a variable is rooted by a constructor symbol.
Thus, facIter
#(
x,
y) → if
#(isZero(
x), minus(
x, s(0)),
y, times(
y,
x)) is replaced by instances determined through the above matching. These instances are:
| facIter#(_x, _z) → if#(isZero(_x), minus(_x, s(0)), _z, times(_z, _x)) |
Problem 6: BackwardInstantiation
Dependency Pair Problem
Dependency Pairs
| facIter#(_x, _z) | → | if#(isZero(_x), minus(_x, s(0)), _z, times(_z, _x)) | | if#(false, x, y, z) | → | facIter#(x, z) |
Rewrite Rules
| plus(0, x) | → | x | | plus(s(x), y) | → | s(plus(x, y)) |
| times(0, y) | → | 0 | | times(s(x), y) | → | plus(y, times(x, y)) |
| p(s(x)) | → | x | | p(0) | → | 0 |
| minus(x, 0) | → | x | | minus(0, x) | → | 0 |
| minus(x, s(y)) | → | p(minus(x, y)) | | isZero(0) | → | true |
| isZero(s(x)) | → | false | | facIter(x, y) | → | if(isZero(x), minus(x, s(0)), y, times(y, x)) |
| if(true, x, y, z) | → | y | | if(false, x, y, z) | → | facIter(x, z) |
| factorial(x) | → | facIter(x, s(0)) |
Original Signature
Termination of terms over the following signature is verified: plus, minus, 0, s, times, if, p, false, true, factorial, facIter, isZero
Strategy
Instantiation
For all potential predecessors l → r of the rule facIter
#(
_x,
_z) → if
#(isZero(
_x), minus(
_x, s(0)),
_z, times(
_z,
_x)) on dependency pair chains it holds that:
- facIter#(_x, _z) matches r,
- all variables of facIter#(_x, _z) are embedded in constructor contexts, i.e., each subterm of facIter#(_x, _z), containing a variable is rooted by a constructor symbol.
Thus, facIter
#(
_x,
_z) → if
#(isZero(
_x), minus(
_x, s(0)),
_z, times(
_z,
_x)) is replaced by instances determined through the above matching. These instances are:
| facIter#(x, z) → if#(isZero(x), minus(x, s(0)), z, times(z, x)) |
Problem 7: Propagation
Dependency Pair Problem
Dependency Pairs
| if#(false, x, y, z) | → | facIter#(x, z) | | facIter#(x, z) | → | if#(isZero(x), minus(x, s(0)), z, times(z, x)) |
Rewrite Rules
| plus(0, x) | → | x | | plus(s(x), y) | → | s(plus(x, y)) |
| times(0, y) | → | 0 | | times(s(x), y) | → | plus(y, times(x, y)) |
| p(s(x)) | → | x | | p(0) | → | 0 |
| minus(x, 0) | → | x | | minus(0, x) | → | 0 |
| minus(x, s(y)) | → | p(minus(x, y)) | | isZero(0) | → | true |
| isZero(s(x)) | → | false | | facIter(x, y) | → | if(isZero(x), minus(x, s(0)), y, times(y, x)) |
| if(true, x, y, z) | → | y | | if(false, x, y, z) | → | facIter(x, z) |
| factorial(x) | → | facIter(x, s(0)) |
Original Signature
Termination of terms over the following signature is verified: plus, 0, minus, s, times, if, p, true, false, facIter, factorial, isZero
Strategy
The dependency pairs if
#(false,
x,
y,
z) → facIter
#(
x,
z) and facIter
#(
x,
z) → if
#(isZero(
x), minus(
x, s(0)),
z, times(
z,
x)) are consolidated into the rule if
#(false,
x,
y,
z) → if
#(isZero(
x), minus(
x, s(0)),
z, times(
z,
x)) .
This is possible as
- all subterms of facIter#(x, z) containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in facIter#(x, z), but non-replacing in both if#(false, x, y, z) and if#(isZero(x), minus(x, s(0)), z, times(z, x))
The dependency pairs if
#(false,
x,
y,
z) → facIter
#(
x,
z) and facIter
#(
x,
z) → if
#(isZero(
x), minus(
x, s(0)),
z, times(
z,
x)) are consolidated into the rule if
#(false,
x,
y,
z) → if
#(isZero(
x), minus(
x, s(0)),
z, times(
z,
x)) .
This is possible as
- all subterms of facIter#(x, z) containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in facIter#(x, z), but non-replacing in both if#(false, x, y, z) and if#(isZero(x), minus(x, s(0)), z, times(z, x))
Summary
| Removed Dependency Pairs | Added Dependency Pairs |
|---|
| if#(false, x, y, z) → facIter#(x, z) | if#(false, x, y, z) → if#(isZero(x), minus(x, s(0)), z, times(z, x)) |
| facIter#(x, z) → if#(isZero(x), minus(x, s(0)), z, times(z, x)) | |
Problem 5: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| times#(s(x), y) | → | times#(x, y) |
Rewrite Rules
| plus(0, x) | → | x | | plus(s(x), y) | → | s(plus(x, y)) |
| times(0, y) | → | 0 | | times(s(x), y) | → | plus(y, times(x, y)) |
| p(s(x)) | → | x | | p(0) | → | 0 |
| minus(x, 0) | → | x | | minus(0, x) | → | 0 |
| minus(x, s(y)) | → | p(minus(x, y)) | | isZero(0) | → | true |
| isZero(s(x)) | → | false | | facIter(x, y) | → | if(isZero(x), minus(x, s(0)), y, times(y, x)) |
| if(true, x, y, z) | → | y | | if(false, x, y, z) | → | facIter(x, z) |
| factorial(x) | → | facIter(x, s(0)) |
Original Signature
Termination of terms over the following signature is verified: plus, 0, minus, s, times, if, p, true, false, facIter, factorial, isZero
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| times#(s(x), y) | → | times#(x, y) |