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