(0) Obligation:
Q restricted rewrite system:
The TRS R consists of the following 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)))
Q is empty.
(1) DependencyPairsProof (EQUIVALENT transformation)
Using Dependency Pairs [AG00,LPAR04] we result in the following initial DP problem.
(2) Obligation:
Q DP problem:
The TRS P consists of the following rules:
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)
The TRS R consists of the following 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)))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(3) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 3 SCCs with 2 less nodes.
(4) Complex Obligation (AND)
(5) Obligation:
Q DP problem:
The TRS P consists of the following rules:
PLUS(s(X), Y) → PLUS(X, Y)
The TRS R consists of the following 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)))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(6) UsableRulesProof (EQUIVALENT transformation)
We can use the usable rules and reduction pair processor [LPAR04] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its arguments. Then, we can delete all non-usable rules [FROCOS05] from R.
(7) Obligation:
Q DP problem:
The TRS P consists of the following rules:
PLUS(s(X), Y) → PLUS(X, Y)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(8) QDPSizeChangeProof (EQUIVALENT transformation)
By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.
From the DPs we obtained the following set of size-change graphs:
- PLUS(s(X), Y) → PLUS(X, Y)
The graph contains the following edges 1 > 1, 2 >= 2
(9) YES
(10) Obligation:
Q DP problem:
The TRS P consists of the following rules:
MIN(min(X, Y), Z) → MIN(X, plus(Y, Z))
MIN(s(X), s(Y)) → MIN(X, Y)
The TRS R consists of the following 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)))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(11) UsableRulesProof (EQUIVALENT transformation)
We can use the usable rules and reduction pair processor [LPAR04] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its arguments. Then, we can delete all non-usable rules [FROCOS05] from R.
(12) Obligation:
Q DP problem:
The TRS P consists of the following rules:
MIN(min(X, Y), Z) → MIN(X, plus(Y, Z))
MIN(s(X), s(Y)) → MIN(X, Y)
The TRS R consists of the following rules:
plus(0, Y) → Y
plus(s(X), Y) → s(plus(X, Y))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(13) MNOCProof (EQUIVALENT transformation)
We use the modular non-overlap check [LPAR04] to enlarge Q to all left-hand sides of R.
(14) Obligation:
Q DP problem:
The TRS P consists of the following rules:
MIN(min(X, Y), Z) → MIN(X, plus(Y, Z))
MIN(s(X), s(Y)) → MIN(X, Y)
The TRS R consists of the following rules:
plus(0, Y) → Y
plus(s(X), Y) → s(plus(X, Y))
The set Q consists of the following terms:
plus(0, x0)
plus(s(x0), x1)
We have to consider all minimal (P,Q,R)-chains.
(15) QDPSizeChangeProof (EQUIVALENT transformation)
By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.
From the DPs we obtained the following set of size-change graphs:
- MIN(min(X, Y), Z) → MIN(X, plus(Y, Z))
The graph contains the following edges 1 > 1
- MIN(s(X), s(Y)) → MIN(X, Y)
The graph contains the following edges 1 > 1, 2 > 2
(16) YES
(17) Obligation:
Q DP problem:
The TRS P consists of the following rules:
QUOT(s(X), s(Y)) → QUOT(min(X, Y), s(Y))
The TRS R consists of the following 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)))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(18) QDPOrderProof (EQUIVALENT transformation)
We use the reduction pair processor [LPAR04,JAR06].
The following pairs can be oriented strictly and are deleted.
QUOT(s(X), s(Y)) → QUOT(min(X, Y), s(Y))
The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
QUOT(
x1,
x2) =
x1
s(
x1) =
s(
x1)
min(
x1,
x2) =
x1
Knuth-Bendix order [KBO] with precedence:
trivial
and weight map:
s_1=1
dummyConstant=1
The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:
min(X, 0) → X
min(min(X, Y), Z) → min(X, plus(Y, Z))
min(s(X), s(Y)) → min(X, Y)
(19) Obligation:
Q DP problem:
P is empty.
The TRS R consists of the following 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)))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(20) PisEmptyProof (EQUIVALENT transformation)
The TRS P is empty. Hence, there is no (P,Q,R) chain.
(21) YES