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