Term Rewriting System R:
[Y, X]
plus(0, Y) -> Y
plus(s(X), Y) -> s(plus(X, Y))
min(X, 0) -> X
min(s(X), s(Y)) -> min(X, Y)
min(min(X, Y), Z) -> min(X, plus(Y, Z))
quot(0, s(Y)) -> 0
quot(s(X), s(Y)) -> s(quot(min(X, Y), s(Y)))
Termination of R to be shown.
R
↳Dependency Pair Analysis
R contains the following Dependency Pairs:
PLUS(s(X), Y) -> PLUS(X, Y)
MIN(s(X), s(Y)) -> MIN(X, Y)
MIN(min(X, Y), Z) -> MIN(X, plus(Y, Z))
MIN(min(X, Y), Z) -> PLUS(Y, Z)
QUOT(s(X), s(Y)) -> QUOT(min(X, Y), s(Y))
QUOT(s(X), s(Y)) -> MIN(X, Y)
Furthermore, R contains three SCCs.
R
↳DPs
→DP Problem 1
↳Size-Change Principle
→DP Problem 2
↳SCP
→DP Problem 3
↳Neg POLO
Dependency Pair:
PLUS(s(X), Y) -> PLUS(X, Y)
Rules:
plus(0, Y) -> Y
plus(s(X), Y) -> s(plus(X, Y))
min(X, 0) -> X
min(s(X), s(Y)) -> min(X, Y)
min(min(X, Y), Z) -> min(X, plus(Y, Z))
quot(0, s(Y)) -> 0
quot(s(X), s(Y)) -> s(quot(min(X, Y), s(Y)))
We number the DPs as follows:
- PLUS(s(X), Y) -> PLUS(X, Y)
and get the following Size-Change Graph(s):
which lead(s) to this/these maximal multigraph(s):
D_{P}: empty set
Oriented Rules: none
We used the order Homeomorphic Embedding Order with Non-Strict Precedence.
trivial
with Argument Filtering System:
s(x_{1}) -> s(x_{1})
We obtain no new DP problems.
R
↳DPs
→DP Problem 1
↳SCP
→DP Problem 2
↳Size-Change Principle
→DP Problem 3
↳Neg POLO
Dependency Pairs:
MIN(min(X, Y), Z) -> MIN(X, plus(Y, Z))
MIN(s(X), s(Y)) -> MIN(X, Y)
Rules:
plus(0, Y) -> Y
plus(s(X), Y) -> s(plus(X, Y))
min(X, 0) -> X
min(s(X), s(Y)) -> min(X, Y)
min(min(X, Y), Z) -> min(X, plus(Y, Z))
quot(0, s(Y)) -> 0
quot(s(X), s(Y)) -> s(quot(min(X, Y), s(Y)))
We number the DPs as follows:
- MIN(min(X, Y), Z) -> MIN(X, plus(Y, Z))
- MIN(s(X), s(Y)) -> MIN(X, Y)
and get the following Size-Change Graph(s):
which lead(s) to this/these maximal multigraph(s):
D_{P}: empty set
Oriented Rules: none
We used the order Homeomorphic Embedding Order with Non-Strict Precedence.
trivial
with Argument Filtering System:
min(x_{1}, x_{2}) -> min(x_{1}, x_{2})
s(x_{1}) -> s(x_{1})
We obtain no new DP problems.
R
↳DPs
→DP Problem 1
↳SCP
→DP Problem 2
↳SCP
→DP Problem 3
↳Negative Polynomial Order
Dependency Pair:
QUOT(s(X), s(Y)) -> QUOT(min(X, Y), s(Y))
Rules:
plus(0, Y) -> Y
plus(s(X), Y) -> s(plus(X, Y))
min(X, 0) -> X
min(s(X), s(Y)) -> min(X, Y)
min(min(X, Y), Z) -> min(X, plus(Y, Z))
quot(0, s(Y)) -> 0
quot(s(X), s(Y)) -> s(quot(min(X, Y), s(Y)))
The following Dependency Pair can be strictly oriented using the given order.
QUOT(s(X), s(Y)) -> QUOT(min(X, Y), s(Y))
Moreover, the following usable rules (regarding the implicit AFS) are oriented.
min(X, 0) -> X
min(s(X), s(Y)) -> min(X, Y)
min(min(X, Y), Z) -> min(X, plus(Y, Z))
plus(0, Y) -> Y
plus(s(X), Y) -> s(plus(X, Y))
Used ordering:
Polynomial Order with Interpretation:
POL( QUOT(x_{1}, x_{2}) ) = x_{1}
POL( s(x_{1}) ) = x_{1} + 1
POL( min(x_{1}, x_{2}) ) = x_{1}
POL( plus(x_{1}, x_{2}) ) = x_{1} + x_{2}
This results in one new DP problem.
R
↳DPs
→DP Problem 1
↳SCP
→DP Problem 2
↳SCP
→DP Problem 3
↳Neg POLO
→DP Problem 4
↳Dependency Graph
Dependency Pair:
Rules:
plus(0, Y) -> Y
plus(s(X), Y) -> s(plus(X, Y))
min(X, 0) -> X
min(s(X), s(Y)) -> min(X, Y)
min(min(X, Y), Z) -> min(X, plus(Y, Z))
quot(0, s(Y)) -> 0
quot(s(X), s(Y)) -> s(quot(min(X, Y), s(Y)))
Using the Dependency Graph resulted in no new DP problems.
Termination of R successfully shown.
Duration:
0:00 minutes