(0) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
ge(0, 0) → true
ge(s(x), 0) → ge(x, 0)
ge(0, s(0)) → false
ge(0, s(s(x))) → ge(0, s(x))
ge(s(x), s(y)) → ge(x, y)
minus(0, 0) → 0
minus(0, s(x)) → minus(0, x)
minus(s(x), 0) → s(minus(x, 0))
minus(s(x), s(y)) → minus(x, y)
plus(0, 0) → 0
plus(0, s(x)) → s(plus(0, x))
plus(s(x), y) → s(plus(x, y))
div(x, y) → ify(ge(y, s(0)), x, y)
ify(false, x, y) → divByZeroError
ify(true, x, y) → if(ge(x, y), x, y)
if(false, x, y) → 0
if(true, x, y) → s(div(minus(x, y), y))
Q is empty.
(1) Overlay + Local Confluence (EQUIVALENT transformation)
The TRS is overlay and locally confluent. By [NOC] we can switch to innermost.
(2) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
ge(0, 0) → true
ge(s(x), 0) → ge(x, 0)
ge(0, s(0)) → false
ge(0, s(s(x))) → ge(0, s(x))
ge(s(x), s(y)) → ge(x, y)
minus(0, 0) → 0
minus(0, s(x)) → minus(0, x)
minus(s(x), 0) → s(minus(x, 0))
minus(s(x), s(y)) → minus(x, y)
plus(0, 0) → 0
plus(0, s(x)) → s(plus(0, x))
plus(s(x), y) → s(plus(x, y))
div(x, y) → ify(ge(y, s(0)), x, y)
ify(false, x, y) → divByZeroError
ify(true, x, y) → if(ge(x, y), x, y)
if(false, x, y) → 0
if(true, x, y) → s(div(minus(x, y), y))
The set Q consists of the following terms:
ge(0, 0)
ge(s(x0), 0)
ge(0, s(0))
ge(0, s(s(x0)))
ge(s(x0), s(x1))
minus(0, 0)
minus(0, s(x0))
minus(s(x0), 0)
minus(s(x0), s(x1))
plus(0, 0)
plus(0, s(x0))
plus(s(x0), x1)
div(x0, x1)
ify(false, x0, x1)
ify(true, x0, x1)
if(false, x0, x1)
if(true, x0, x1)
(3) DependencyPairsProof (EQUIVALENT transformation)
Using Dependency Pairs [AG00,LPAR04] we result in the following initial DP problem.
(4) Obligation:
Q DP problem:
The TRS P consists of the following rules:
GE(s(x), 0) → GE(x, 0)
GE(0, s(s(x))) → GE(0, s(x))
GE(s(x), s(y)) → GE(x, y)
MINUS(0, s(x)) → MINUS(0, x)
MINUS(s(x), 0) → MINUS(x, 0)
MINUS(s(x), s(y)) → MINUS(x, y)
PLUS(0, s(x)) → PLUS(0, x)
PLUS(s(x), y) → PLUS(x, y)
DIV(x, y) → IFY(ge(y, s(0)), x, y)
DIV(x, y) → GE(y, s(0))
IFY(true, x, y) → IF(ge(x, y), x, y)
IFY(true, x, y) → GE(x, y)
IF(true, x, y) → DIV(minus(x, y), y)
IF(true, x, y) → MINUS(x, y)
The TRS R consists of the following rules:
ge(0, 0) → true
ge(s(x), 0) → ge(x, 0)
ge(0, s(0)) → false
ge(0, s(s(x))) → ge(0, s(x))
ge(s(x), s(y)) → ge(x, y)
minus(0, 0) → 0
minus(0, s(x)) → minus(0, x)
minus(s(x), 0) → s(minus(x, 0))
minus(s(x), s(y)) → minus(x, y)
plus(0, 0) → 0
plus(0, s(x)) → s(plus(0, x))
plus(s(x), y) → s(plus(x, y))
div(x, y) → ify(ge(y, s(0)), x, y)
ify(false, x, y) → divByZeroError
ify(true, x, y) → if(ge(x, y), x, y)
if(false, x, y) → 0
if(true, x, y) → s(div(minus(x, y), y))
The set Q consists of the following terms:
ge(0, 0)
ge(s(x0), 0)
ge(0, s(0))
ge(0, s(s(x0)))
ge(s(x0), s(x1))
minus(0, 0)
minus(0, s(x0))
minus(s(x0), 0)
minus(s(x0), s(x1))
plus(0, 0)
plus(0, s(x0))
plus(s(x0), x1)
div(x0, x1)
ify(false, x0, x1)
ify(true, x0, x1)
if(false, x0, x1)
if(true, x0, x1)
We have to consider all minimal (P,Q,R)-chains.
(5) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 9 SCCs with 3 less nodes.
(6) Complex Obligation (AND)
(7) Obligation:
Q DP problem:
The TRS P consists of the following rules:
PLUS(0, s(x)) → PLUS(0, x)
The TRS R consists of the following rules:
ge(0, 0) → true
ge(s(x), 0) → ge(x, 0)
ge(0, s(0)) → false
ge(0, s(s(x))) → ge(0, s(x))
ge(s(x), s(y)) → ge(x, y)
minus(0, 0) → 0
minus(0, s(x)) → minus(0, x)
minus(s(x), 0) → s(minus(x, 0))
minus(s(x), s(y)) → minus(x, y)
plus(0, 0) → 0
plus(0, s(x)) → s(plus(0, x))
plus(s(x), y) → s(plus(x, y))
div(x, y) → ify(ge(y, s(0)), x, y)
ify(false, x, y) → divByZeroError
ify(true, x, y) → if(ge(x, y), x, y)
if(false, x, y) → 0
if(true, x, y) → s(div(minus(x, y), y))
The set Q consists of the following terms:
ge(0, 0)
ge(s(x0), 0)
ge(0, s(0))
ge(0, s(s(x0)))
ge(s(x0), s(x1))
minus(0, 0)
minus(0, s(x0))
minus(s(x0), 0)
minus(s(x0), s(x1))
plus(0, 0)
plus(0, s(x0))
plus(s(x0), x1)
div(x0, x1)
ify(false, x0, x1)
ify(true, x0, x1)
if(false, x0, x1)
if(true, x0, x1)
We have to consider all minimal (P,Q,R)-chains.
(8) UsableRulesProof (EQUIVALENT transformation)
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.
(9) Obligation:
Q DP problem:
The TRS P consists of the following rules:
PLUS(0, s(x)) → PLUS(0, x)
R is empty.
The set Q consists of the following terms:
ge(0, 0)
ge(s(x0), 0)
ge(0, s(0))
ge(0, s(s(x0)))
ge(s(x0), s(x1))
minus(0, 0)
minus(0, s(x0))
minus(s(x0), 0)
minus(s(x0), s(x1))
plus(0, 0)
plus(0, s(x0))
plus(s(x0), x1)
div(x0, x1)
ify(false, x0, x1)
ify(true, x0, x1)
if(false, x0, x1)
if(true, x0, x1)
We have to consider all minimal (P,Q,R)-chains.
(10) QReductionProof (EQUIVALENT transformation)
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].
ge(0, 0)
ge(s(x0), 0)
ge(0, s(0))
ge(0, s(s(x0)))
ge(s(x0), s(x1))
minus(0, 0)
minus(0, s(x0))
minus(s(x0), 0)
minus(s(x0), s(x1))
plus(0, 0)
plus(0, s(x0))
plus(s(x0), x1)
div(x0, x1)
ify(false, x0, x1)
ify(true, x0, x1)
if(false, x0, x1)
if(true, x0, x1)
(11) Obligation:
Q DP problem:
The TRS P consists of the following rules:
PLUS(0, s(x)) → PLUS(0, x)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(12) 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(0, s(x)) → PLUS(0, x)
The graph contains the following edges 1 >= 1, 2 > 2
(13) TRUE
(14) 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:
ge(0, 0) → true
ge(s(x), 0) → ge(x, 0)
ge(0, s(0)) → false
ge(0, s(s(x))) → ge(0, s(x))
ge(s(x), s(y)) → ge(x, y)
minus(0, 0) → 0
minus(0, s(x)) → minus(0, x)
minus(s(x), 0) → s(minus(x, 0))
minus(s(x), s(y)) → minus(x, y)
plus(0, 0) → 0
plus(0, s(x)) → s(plus(0, x))
plus(s(x), y) → s(plus(x, y))
div(x, y) → ify(ge(y, s(0)), x, y)
ify(false, x, y) → divByZeroError
ify(true, x, y) → if(ge(x, y), x, y)
if(false, x, y) → 0
if(true, x, y) → s(div(minus(x, y), y))
The set Q consists of the following terms:
ge(0, 0)
ge(s(x0), 0)
ge(0, s(0))
ge(0, s(s(x0)))
ge(s(x0), s(x1))
minus(0, 0)
minus(0, s(x0))
minus(s(x0), 0)
minus(s(x0), s(x1))
plus(0, 0)
plus(0, s(x0))
plus(s(x0), x1)
div(x0, x1)
ify(false, x0, x1)
ify(true, x0, x1)
if(false, x0, x1)
if(true, x0, x1)
We have to consider all minimal (P,Q,R)-chains.
(15) UsableRulesProof (EQUIVALENT transformation)
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.
(16) Obligation:
Q DP problem:
The TRS P consists of the following rules:
PLUS(s(x), y) → PLUS(x, y)
R is empty.
The set Q consists of the following terms:
ge(0, 0)
ge(s(x0), 0)
ge(0, s(0))
ge(0, s(s(x0)))
ge(s(x0), s(x1))
minus(0, 0)
minus(0, s(x0))
minus(s(x0), 0)
minus(s(x0), s(x1))
plus(0, 0)
plus(0, s(x0))
plus(s(x0), x1)
div(x0, x1)
ify(false, x0, x1)
ify(true, x0, x1)
if(false, x0, x1)
if(true, x0, x1)
We have to consider all minimal (P,Q,R)-chains.
(17) QReductionProof (EQUIVALENT transformation)
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].
ge(0, 0)
ge(s(x0), 0)
ge(0, s(0))
ge(0, s(s(x0)))
ge(s(x0), s(x1))
minus(0, 0)
minus(0, s(x0))
minus(s(x0), 0)
minus(s(x0), s(x1))
plus(0, 0)
plus(0, s(x0))
plus(s(x0), x1)
div(x0, x1)
ify(false, x0, x1)
ify(true, x0, x1)
if(false, x0, x1)
if(true, x0, x1)
(18) 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.
(19) 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
(20) TRUE
(21) Obligation:
Q DP problem:
The TRS P consists of the following rules:
MINUS(s(x), 0) → MINUS(x, 0)
The TRS R consists of the following rules:
ge(0, 0) → true
ge(s(x), 0) → ge(x, 0)
ge(0, s(0)) → false
ge(0, s(s(x))) → ge(0, s(x))
ge(s(x), s(y)) → ge(x, y)
minus(0, 0) → 0
minus(0, s(x)) → minus(0, x)
minus(s(x), 0) → s(minus(x, 0))
minus(s(x), s(y)) → minus(x, y)
plus(0, 0) → 0
plus(0, s(x)) → s(plus(0, x))
plus(s(x), y) → s(plus(x, y))
div(x, y) → ify(ge(y, s(0)), x, y)
ify(false, x, y) → divByZeroError
ify(true, x, y) → if(ge(x, y), x, y)
if(false, x, y) → 0
if(true, x, y) → s(div(minus(x, y), y))
The set Q consists of the following terms:
ge(0, 0)
ge(s(x0), 0)
ge(0, s(0))
ge(0, s(s(x0)))
ge(s(x0), s(x1))
minus(0, 0)
minus(0, s(x0))
minus(s(x0), 0)
minus(s(x0), s(x1))
plus(0, 0)
plus(0, s(x0))
plus(s(x0), x1)
div(x0, x1)
ify(false, x0, x1)
ify(true, x0, x1)
if(false, x0, x1)
if(true, x0, x1)
We have to consider all minimal (P,Q,R)-chains.
(22) UsableRulesProof (EQUIVALENT transformation)
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.
(23) Obligation:
Q DP problem:
The TRS P consists of the following rules:
MINUS(s(x), 0) → MINUS(x, 0)
R is empty.
The set Q consists of the following terms:
ge(0, 0)
ge(s(x0), 0)
ge(0, s(0))
ge(0, s(s(x0)))
ge(s(x0), s(x1))
minus(0, 0)
minus(0, s(x0))
minus(s(x0), 0)
minus(s(x0), s(x1))
plus(0, 0)
plus(0, s(x0))
plus(s(x0), x1)
div(x0, x1)
ify(false, x0, x1)
ify(true, x0, x1)
if(false, x0, x1)
if(true, x0, x1)
We have to consider all minimal (P,Q,R)-chains.
(24) QReductionProof (EQUIVALENT transformation)
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].
ge(0, 0)
ge(s(x0), 0)
ge(0, s(0))
ge(0, s(s(x0)))
ge(s(x0), s(x1))
minus(0, 0)
minus(0, s(x0))
minus(s(x0), 0)
minus(s(x0), s(x1))
plus(0, 0)
plus(0, s(x0))
plus(s(x0), x1)
div(x0, x1)
ify(false, x0, x1)
ify(true, x0, x1)
if(false, x0, x1)
if(true, x0, x1)
(25) Obligation:
Q DP problem:
The TRS P consists of the following rules:
MINUS(s(x), 0) → MINUS(x, 0)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(26) 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:
- MINUS(s(x), 0) → MINUS(x, 0)
The graph contains the following edges 1 > 1, 2 >= 2
(27) TRUE
(28) Obligation:
Q DP problem:
The TRS P consists of the following rules:
MINUS(0, s(x)) → MINUS(0, x)
The TRS R consists of the following rules:
ge(0, 0) → true
ge(s(x), 0) → ge(x, 0)
ge(0, s(0)) → false
ge(0, s(s(x))) → ge(0, s(x))
ge(s(x), s(y)) → ge(x, y)
minus(0, 0) → 0
minus(0, s(x)) → minus(0, x)
minus(s(x), 0) → s(minus(x, 0))
minus(s(x), s(y)) → minus(x, y)
plus(0, 0) → 0
plus(0, s(x)) → s(plus(0, x))
plus(s(x), y) → s(plus(x, y))
div(x, y) → ify(ge(y, s(0)), x, y)
ify(false, x, y) → divByZeroError
ify(true, x, y) → if(ge(x, y), x, y)
if(false, x, y) → 0
if(true, x, y) → s(div(minus(x, y), y))
The set Q consists of the following terms:
ge(0, 0)
ge(s(x0), 0)
ge(0, s(0))
ge(0, s(s(x0)))
ge(s(x0), s(x1))
minus(0, 0)
minus(0, s(x0))
minus(s(x0), 0)
minus(s(x0), s(x1))
plus(0, 0)
plus(0, s(x0))
plus(s(x0), x1)
div(x0, x1)
ify(false, x0, x1)
ify(true, x0, x1)
if(false, x0, x1)
if(true, x0, x1)
We have to consider all minimal (P,Q,R)-chains.
(29) UsableRulesProof (EQUIVALENT transformation)
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.
(30) Obligation:
Q DP problem:
The TRS P consists of the following rules:
MINUS(0, s(x)) → MINUS(0, x)
R is empty.
The set Q consists of the following terms:
ge(0, 0)
ge(s(x0), 0)
ge(0, s(0))
ge(0, s(s(x0)))
ge(s(x0), s(x1))
minus(0, 0)
minus(0, s(x0))
minus(s(x0), 0)
minus(s(x0), s(x1))
plus(0, 0)
plus(0, s(x0))
plus(s(x0), x1)
div(x0, x1)
ify(false, x0, x1)
ify(true, x0, x1)
if(false, x0, x1)
if(true, x0, x1)
We have to consider all minimal (P,Q,R)-chains.
(31) QReductionProof (EQUIVALENT transformation)
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].
ge(0, 0)
ge(s(x0), 0)
ge(0, s(0))
ge(0, s(s(x0)))
ge(s(x0), s(x1))
minus(0, 0)
minus(0, s(x0))
minus(s(x0), 0)
minus(s(x0), s(x1))
plus(0, 0)
plus(0, s(x0))
plus(s(x0), x1)
div(x0, x1)
ify(false, x0, x1)
ify(true, x0, x1)
if(false, x0, x1)
if(true, x0, x1)
(32) Obligation:
Q DP problem:
The TRS P consists of the following rules:
MINUS(0, s(x)) → MINUS(0, x)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(33) 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:
- MINUS(0, s(x)) → MINUS(0, x)
The graph contains the following edges 1 >= 1, 2 > 2
(34) TRUE
(35) Obligation:
Q DP problem:
The TRS P consists of the following rules:
MINUS(s(x), s(y)) → MINUS(x, y)
The TRS R consists of the following rules:
ge(0, 0) → true
ge(s(x), 0) → ge(x, 0)
ge(0, s(0)) → false
ge(0, s(s(x))) → ge(0, s(x))
ge(s(x), s(y)) → ge(x, y)
minus(0, 0) → 0
minus(0, s(x)) → minus(0, x)
minus(s(x), 0) → s(minus(x, 0))
minus(s(x), s(y)) → minus(x, y)
plus(0, 0) → 0
plus(0, s(x)) → s(plus(0, x))
plus(s(x), y) → s(plus(x, y))
div(x, y) → ify(ge(y, s(0)), x, y)
ify(false, x, y) → divByZeroError
ify(true, x, y) → if(ge(x, y), x, y)
if(false, x, y) → 0
if(true, x, y) → s(div(minus(x, y), y))
The set Q consists of the following terms:
ge(0, 0)
ge(s(x0), 0)
ge(0, s(0))
ge(0, s(s(x0)))
ge(s(x0), s(x1))
minus(0, 0)
minus(0, s(x0))
minus(s(x0), 0)
minus(s(x0), s(x1))
plus(0, 0)
plus(0, s(x0))
plus(s(x0), x1)
div(x0, x1)
ify(false, x0, x1)
ify(true, x0, x1)
if(false, x0, x1)
if(true, x0, x1)
We have to consider all minimal (P,Q,R)-chains.
(36) UsableRulesProof (EQUIVALENT transformation)
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.
(37) Obligation:
Q DP problem:
The TRS P consists of the following rules:
MINUS(s(x), s(y)) → MINUS(x, y)
R is empty.
The set Q consists of the following terms:
ge(0, 0)
ge(s(x0), 0)
ge(0, s(0))
ge(0, s(s(x0)))
ge(s(x0), s(x1))
minus(0, 0)
minus(0, s(x0))
minus(s(x0), 0)
minus(s(x0), s(x1))
plus(0, 0)
plus(0, s(x0))
plus(s(x0), x1)
div(x0, x1)
ify(false, x0, x1)
ify(true, x0, x1)
if(false, x0, x1)
if(true, x0, x1)
We have to consider all minimal (P,Q,R)-chains.
(38) QReductionProof (EQUIVALENT transformation)
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].
ge(0, 0)
ge(s(x0), 0)
ge(0, s(0))
ge(0, s(s(x0)))
ge(s(x0), s(x1))
minus(0, 0)
minus(0, s(x0))
minus(s(x0), 0)
minus(s(x0), s(x1))
plus(0, 0)
plus(0, s(x0))
plus(s(x0), x1)
div(x0, x1)
ify(false, x0, x1)
ify(true, x0, x1)
if(false, x0, x1)
if(true, x0, x1)
(39) Obligation:
Q DP problem:
The TRS P consists of the following rules:
MINUS(s(x), s(y)) → MINUS(x, y)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(40) 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:
- MINUS(s(x), s(y)) → MINUS(x, y)
The graph contains the following edges 1 > 1, 2 > 2
(41) TRUE
(42) Obligation:
Q DP problem:
The TRS P consists of the following rules:
GE(0, s(s(x))) → GE(0, s(x))
The TRS R consists of the following rules:
ge(0, 0) → true
ge(s(x), 0) → ge(x, 0)
ge(0, s(0)) → false
ge(0, s(s(x))) → ge(0, s(x))
ge(s(x), s(y)) → ge(x, y)
minus(0, 0) → 0
minus(0, s(x)) → minus(0, x)
minus(s(x), 0) → s(minus(x, 0))
minus(s(x), s(y)) → minus(x, y)
plus(0, 0) → 0
plus(0, s(x)) → s(plus(0, x))
plus(s(x), y) → s(plus(x, y))
div(x, y) → ify(ge(y, s(0)), x, y)
ify(false, x, y) → divByZeroError
ify(true, x, y) → if(ge(x, y), x, y)
if(false, x, y) → 0
if(true, x, y) → s(div(minus(x, y), y))
The set Q consists of the following terms:
ge(0, 0)
ge(s(x0), 0)
ge(0, s(0))
ge(0, s(s(x0)))
ge(s(x0), s(x1))
minus(0, 0)
minus(0, s(x0))
minus(s(x0), 0)
minus(s(x0), s(x1))
plus(0, 0)
plus(0, s(x0))
plus(s(x0), x1)
div(x0, x1)
ify(false, x0, x1)
ify(true, x0, x1)
if(false, x0, x1)
if(true, x0, x1)
We have to consider all minimal (P,Q,R)-chains.
(43) UsableRulesProof (EQUIVALENT transformation)
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.
(44) Obligation:
Q DP problem:
The TRS P consists of the following rules:
GE(0, s(s(x))) → GE(0, s(x))
R is empty.
The set Q consists of the following terms:
ge(0, 0)
ge(s(x0), 0)
ge(0, s(0))
ge(0, s(s(x0)))
ge(s(x0), s(x1))
minus(0, 0)
minus(0, s(x0))
minus(s(x0), 0)
minus(s(x0), s(x1))
plus(0, 0)
plus(0, s(x0))
plus(s(x0), x1)
div(x0, x1)
ify(false, x0, x1)
ify(true, x0, x1)
if(false, x0, x1)
if(true, x0, x1)
We have to consider all minimal (P,Q,R)-chains.
(45) QReductionProof (EQUIVALENT transformation)
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].
ge(0, 0)
ge(s(x0), 0)
ge(0, s(0))
ge(0, s(s(x0)))
ge(s(x0), s(x1))
minus(0, 0)
minus(0, s(x0))
minus(s(x0), 0)
minus(s(x0), s(x1))
plus(0, 0)
plus(0, s(x0))
plus(s(x0), x1)
div(x0, x1)
ify(false, x0, x1)
ify(true, x0, x1)
if(false, x0, x1)
if(true, x0, x1)
(46) Obligation:
Q DP problem:
The TRS P consists of the following rules:
GE(0, s(s(x))) → GE(0, s(x))
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(47) 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:
- GE(0, s(s(x))) → GE(0, s(x))
The graph contains the following edges 1 >= 1, 2 > 2
(48) TRUE
(49) Obligation:
Q DP problem:
The TRS P consists of the following rules:
GE(s(x), 0) → GE(x, 0)
The TRS R consists of the following rules:
ge(0, 0) → true
ge(s(x), 0) → ge(x, 0)
ge(0, s(0)) → false
ge(0, s(s(x))) → ge(0, s(x))
ge(s(x), s(y)) → ge(x, y)
minus(0, 0) → 0
minus(0, s(x)) → minus(0, x)
minus(s(x), 0) → s(minus(x, 0))
minus(s(x), s(y)) → minus(x, y)
plus(0, 0) → 0
plus(0, s(x)) → s(plus(0, x))
plus(s(x), y) → s(plus(x, y))
div(x, y) → ify(ge(y, s(0)), x, y)
ify(false, x, y) → divByZeroError
ify(true, x, y) → if(ge(x, y), x, y)
if(false, x, y) → 0
if(true, x, y) → s(div(minus(x, y), y))
The set Q consists of the following terms:
ge(0, 0)
ge(s(x0), 0)
ge(0, s(0))
ge(0, s(s(x0)))
ge(s(x0), s(x1))
minus(0, 0)
minus(0, s(x0))
minus(s(x0), 0)
minus(s(x0), s(x1))
plus(0, 0)
plus(0, s(x0))
plus(s(x0), x1)
div(x0, x1)
ify(false, x0, x1)
ify(true, x0, x1)
if(false, x0, x1)
if(true, x0, x1)
We have to consider all minimal (P,Q,R)-chains.
(50) UsableRulesProof (EQUIVALENT transformation)
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.
(51) Obligation:
Q DP problem:
The TRS P consists of the following rules:
GE(s(x), 0) → GE(x, 0)
R is empty.
The set Q consists of the following terms:
ge(0, 0)
ge(s(x0), 0)
ge(0, s(0))
ge(0, s(s(x0)))
ge(s(x0), s(x1))
minus(0, 0)
minus(0, s(x0))
minus(s(x0), 0)
minus(s(x0), s(x1))
plus(0, 0)
plus(0, s(x0))
plus(s(x0), x1)
div(x0, x1)
ify(false, x0, x1)
ify(true, x0, x1)
if(false, x0, x1)
if(true, x0, x1)
We have to consider all minimal (P,Q,R)-chains.
(52) QReductionProof (EQUIVALENT transformation)
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].
ge(0, 0)
ge(s(x0), 0)
ge(0, s(0))
ge(0, s(s(x0)))
ge(s(x0), s(x1))
minus(0, 0)
minus(0, s(x0))
minus(s(x0), 0)
minus(s(x0), s(x1))
plus(0, 0)
plus(0, s(x0))
plus(s(x0), x1)
div(x0, x1)
ify(false, x0, x1)
ify(true, x0, x1)
if(false, x0, x1)
if(true, x0, x1)
(53) Obligation:
Q DP problem:
The TRS P consists of the following rules:
GE(s(x), 0) → GE(x, 0)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(54) 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:
- GE(s(x), 0) → GE(x, 0)
The graph contains the following edges 1 > 1, 2 >= 2
(55) TRUE
(56) Obligation:
Q DP problem:
The TRS P consists of the following rules:
GE(s(x), s(y)) → GE(x, y)
The TRS R consists of the following rules:
ge(0, 0) → true
ge(s(x), 0) → ge(x, 0)
ge(0, s(0)) → false
ge(0, s(s(x))) → ge(0, s(x))
ge(s(x), s(y)) → ge(x, y)
minus(0, 0) → 0
minus(0, s(x)) → minus(0, x)
minus(s(x), 0) → s(minus(x, 0))
minus(s(x), s(y)) → minus(x, y)
plus(0, 0) → 0
plus(0, s(x)) → s(plus(0, x))
plus(s(x), y) → s(plus(x, y))
div(x, y) → ify(ge(y, s(0)), x, y)
ify(false, x, y) → divByZeroError
ify(true, x, y) → if(ge(x, y), x, y)
if(false, x, y) → 0
if(true, x, y) → s(div(minus(x, y), y))
The set Q consists of the following terms:
ge(0, 0)
ge(s(x0), 0)
ge(0, s(0))
ge(0, s(s(x0)))
ge(s(x0), s(x1))
minus(0, 0)
minus(0, s(x0))
minus(s(x0), 0)
minus(s(x0), s(x1))
plus(0, 0)
plus(0, s(x0))
plus(s(x0), x1)
div(x0, x1)
ify(false, x0, x1)
ify(true, x0, x1)
if(false, x0, x1)
if(true, x0, x1)
We have to consider all minimal (P,Q,R)-chains.
(57) UsableRulesProof (EQUIVALENT transformation)
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.
(58) Obligation:
Q DP problem:
The TRS P consists of the following rules:
GE(s(x), s(y)) → GE(x, y)
R is empty.
The set Q consists of the following terms:
ge(0, 0)
ge(s(x0), 0)
ge(0, s(0))
ge(0, s(s(x0)))
ge(s(x0), s(x1))
minus(0, 0)
minus(0, s(x0))
minus(s(x0), 0)
minus(s(x0), s(x1))
plus(0, 0)
plus(0, s(x0))
plus(s(x0), x1)
div(x0, x1)
ify(false, x0, x1)
ify(true, x0, x1)
if(false, x0, x1)
if(true, x0, x1)
We have to consider all minimal (P,Q,R)-chains.
(59) QReductionProof (EQUIVALENT transformation)
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].
ge(0, 0)
ge(s(x0), 0)
ge(0, s(0))
ge(0, s(s(x0)))
ge(s(x0), s(x1))
minus(0, 0)
minus(0, s(x0))
minus(s(x0), 0)
minus(s(x0), s(x1))
plus(0, 0)
plus(0, s(x0))
plus(s(x0), x1)
div(x0, x1)
ify(false, x0, x1)
ify(true, x0, x1)
if(false, x0, x1)
if(true, x0, x1)
(60) Obligation:
Q DP problem:
The TRS P consists of the following rules:
GE(s(x), s(y)) → GE(x, y)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(61) 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:
- GE(s(x), s(y)) → GE(x, y)
The graph contains the following edges 1 > 1, 2 > 2
(62) TRUE
(63) Obligation:
Q DP problem:
The TRS P consists of the following rules:
DIV(x, y) → IFY(ge(y, s(0)), x, y)
IFY(true, x, y) → IF(ge(x, y), x, y)
IF(true, x, y) → DIV(minus(x, y), y)
The TRS R consists of the following rules:
ge(0, 0) → true
ge(s(x), 0) → ge(x, 0)
ge(0, s(0)) → false
ge(0, s(s(x))) → ge(0, s(x))
ge(s(x), s(y)) → ge(x, y)
minus(0, 0) → 0
minus(0, s(x)) → minus(0, x)
minus(s(x), 0) → s(minus(x, 0))
minus(s(x), s(y)) → minus(x, y)
plus(0, 0) → 0
plus(0, s(x)) → s(plus(0, x))
plus(s(x), y) → s(plus(x, y))
div(x, y) → ify(ge(y, s(0)), x, y)
ify(false, x, y) → divByZeroError
ify(true, x, y) → if(ge(x, y), x, y)
if(false, x, y) → 0
if(true, x, y) → s(div(minus(x, y), y))
The set Q consists of the following terms:
ge(0, 0)
ge(s(x0), 0)
ge(0, s(0))
ge(0, s(s(x0)))
ge(s(x0), s(x1))
minus(0, 0)
minus(0, s(x0))
minus(s(x0), 0)
minus(s(x0), s(x1))
plus(0, 0)
plus(0, s(x0))
plus(s(x0), x1)
div(x0, x1)
ify(false, x0, x1)
ify(true, x0, x1)
if(false, x0, x1)
if(true, x0, x1)
We have to consider all minimal (P,Q,R)-chains.
(64) UsableRulesProof (EQUIVALENT transformation)
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.
(65) Obligation:
Q DP problem:
The TRS P consists of the following rules:
DIV(x, y) → IFY(ge(y, s(0)), x, y)
IFY(true, x, y) → IF(ge(x, y), x, y)
IF(true, x, y) → DIV(minus(x, y), y)
The TRS R consists of the following rules:
minus(0, 0) → 0
minus(0, s(x)) → minus(0, x)
minus(s(x), 0) → s(minus(x, 0))
minus(s(x), s(y)) → minus(x, y)
ge(0, 0) → true
ge(s(x), 0) → ge(x, 0)
ge(0, s(0)) → false
ge(0, s(s(x))) → ge(0, s(x))
ge(s(x), s(y)) → ge(x, y)
The set Q consists of the following terms:
ge(0, 0)
ge(s(x0), 0)
ge(0, s(0))
ge(0, s(s(x0)))
ge(s(x0), s(x1))
minus(0, 0)
minus(0, s(x0))
minus(s(x0), 0)
minus(s(x0), s(x1))
plus(0, 0)
plus(0, s(x0))
plus(s(x0), x1)
div(x0, x1)
ify(false, x0, x1)
ify(true, x0, x1)
if(false, x0, x1)
if(true, x0, x1)
We have to consider all minimal (P,Q,R)-chains.
(66) QReductionProof (EQUIVALENT transformation)
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].
plus(0, 0)
plus(0, s(x0))
plus(s(x0), x1)
div(x0, x1)
ify(false, x0, x1)
ify(true, x0, x1)
if(false, x0, x1)
if(true, x0, x1)
(67) Obligation:
Q DP problem:
The TRS P consists of the following rules:
DIV(x, y) → IFY(ge(y, s(0)), x, y)
IFY(true, x, y) → IF(ge(x, y), x, y)
IF(true, x, y) → DIV(minus(x, y), y)
The TRS R consists of the following rules:
minus(0, 0) → 0
minus(0, s(x)) → minus(0, x)
minus(s(x), 0) → s(minus(x, 0))
minus(s(x), s(y)) → minus(x, y)
ge(0, 0) → true
ge(s(x), 0) → ge(x, 0)
ge(0, s(0)) → false
ge(0, s(s(x))) → ge(0, s(x))
ge(s(x), s(y)) → ge(x, y)
The set Q consists of the following terms:
ge(0, 0)
ge(s(x0), 0)
ge(0, s(0))
ge(0, s(s(x0)))
ge(s(x0), s(x1))
minus(0, 0)
minus(0, s(x0))
minus(s(x0), 0)
minus(s(x0), s(x1))
We have to consider all minimal (P,Q,R)-chains.
(68) Narrowing (EQUIVALENT transformation)
By narrowing [LPAR04] the rule
DIV(
x,
y) →
IFY(
ge(
y,
s(
0)),
x,
y) at position [0] we obtained the following new rules [LPAR04]:
DIV(y0, 0) → IFY(false, y0, 0)
DIV(y0, s(x0)) → IFY(ge(x0, 0), y0, s(x0))
(69) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IFY(true, x, y) → IF(ge(x, y), x, y)
IF(true, x, y) → DIV(minus(x, y), y)
DIV(y0, 0) → IFY(false, y0, 0)
DIV(y0, s(x0)) → IFY(ge(x0, 0), y0, s(x0))
The TRS R consists of the following rules:
minus(0, 0) → 0
minus(0, s(x)) → minus(0, x)
minus(s(x), 0) → s(minus(x, 0))
minus(s(x), s(y)) → minus(x, y)
ge(0, 0) → true
ge(s(x), 0) → ge(x, 0)
ge(0, s(0)) → false
ge(0, s(s(x))) → ge(0, s(x))
ge(s(x), s(y)) → ge(x, y)
The set Q consists of the following terms:
ge(0, 0)
ge(s(x0), 0)
ge(0, s(0))
ge(0, s(s(x0)))
ge(s(x0), s(x1))
minus(0, 0)
minus(0, s(x0))
minus(s(x0), 0)
minus(s(x0), s(x1))
We have to consider all minimal (P,Q,R)-chains.
(70) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.
(71) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IF(true, x, y) → DIV(minus(x, y), y)
DIV(y0, s(x0)) → IFY(ge(x0, 0), y0, s(x0))
IFY(true, x, y) → IF(ge(x, y), x, y)
The TRS R consists of the following rules:
minus(0, 0) → 0
minus(0, s(x)) → minus(0, x)
minus(s(x), 0) → s(minus(x, 0))
minus(s(x), s(y)) → minus(x, y)
ge(0, 0) → true
ge(s(x), 0) → ge(x, 0)
ge(0, s(0)) → false
ge(0, s(s(x))) → ge(0, s(x))
ge(s(x), s(y)) → ge(x, y)
The set Q consists of the following terms:
ge(0, 0)
ge(s(x0), 0)
ge(0, s(0))
ge(0, s(s(x0)))
ge(s(x0), s(x1))
minus(0, 0)
minus(0, s(x0))
minus(s(x0), 0)
minus(s(x0), s(x1))
We have to consider all minimal (P,Q,R)-chains.
(72) Narrowing (EQUIVALENT transformation)
By narrowing [LPAR04] the rule
IFY(
true,
x,
y) →
IF(
ge(
x,
y),
x,
y) at position [0] we obtained the following new rules [LPAR04]:
IFY(true, 0, 0) → IF(true, 0, 0)
IFY(true, s(x0), 0) → IF(ge(x0, 0), s(x0), 0)
IFY(true, 0, s(0)) → IF(false, 0, s(0))
IFY(true, 0, s(s(x0))) → IF(ge(0, s(x0)), 0, s(s(x0)))
IFY(true, s(x0), s(x1)) → IF(ge(x0, x1), s(x0), s(x1))
(73) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IF(true, x, y) → DIV(minus(x, y), y)
DIV(y0, s(x0)) → IFY(ge(x0, 0), y0, s(x0))
IFY(true, 0, 0) → IF(true, 0, 0)
IFY(true, s(x0), 0) → IF(ge(x0, 0), s(x0), 0)
IFY(true, 0, s(0)) → IF(false, 0, s(0))
IFY(true, 0, s(s(x0))) → IF(ge(0, s(x0)), 0, s(s(x0)))
IFY(true, s(x0), s(x1)) → IF(ge(x0, x1), s(x0), s(x1))
The TRS R consists of the following rules:
minus(0, 0) → 0
minus(0, s(x)) → minus(0, x)
minus(s(x), 0) → s(minus(x, 0))
minus(s(x), s(y)) → minus(x, y)
ge(0, 0) → true
ge(s(x), 0) → ge(x, 0)
ge(0, s(0)) → false
ge(0, s(s(x))) → ge(0, s(x))
ge(s(x), s(y)) → ge(x, y)
The set Q consists of the following terms:
ge(0, 0)
ge(s(x0), 0)
ge(0, s(0))
ge(0, s(s(x0)))
ge(s(x0), s(x1))
minus(0, 0)
minus(0, s(x0))
minus(s(x0), 0)
minus(s(x0), s(x1))
We have to consider all minimal (P,Q,R)-chains.
(74) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 4 less nodes.
(75) Obligation:
Q DP problem:
The TRS P consists of the following rules:
DIV(y0, s(x0)) → IFY(ge(x0, 0), y0, s(x0))
IFY(true, s(x0), s(x1)) → IF(ge(x0, x1), s(x0), s(x1))
IF(true, x, y) → DIV(minus(x, y), y)
The TRS R consists of the following rules:
minus(0, 0) → 0
minus(0, s(x)) → minus(0, x)
minus(s(x), 0) → s(minus(x, 0))
minus(s(x), s(y)) → minus(x, y)
ge(0, 0) → true
ge(s(x), 0) → ge(x, 0)
ge(0, s(0)) → false
ge(0, s(s(x))) → ge(0, s(x))
ge(s(x), s(y)) → ge(x, y)
The set Q consists of the following terms:
ge(0, 0)
ge(s(x0), 0)
ge(0, s(0))
ge(0, s(s(x0)))
ge(s(x0), s(x1))
minus(0, 0)
minus(0, s(x0))
minus(s(x0), 0)
minus(s(x0), s(x1))
We have to consider all minimal (P,Q,R)-chains.
(76) Instantiation (EQUIVALENT transformation)
By instantiating [LPAR04] the rule
IF(
true,
x,
y) →
DIV(
minus(
x,
y),
y) we obtained the following new rules [LPAR04]:
IF(true, s(z0), s(z1)) → DIV(minus(s(z0), s(z1)), s(z1))
(77) Obligation:
Q DP problem:
The TRS P consists of the following rules:
DIV(y0, s(x0)) → IFY(ge(x0, 0), y0, s(x0))
IFY(true, s(x0), s(x1)) → IF(ge(x0, x1), s(x0), s(x1))
IF(true, s(z0), s(z1)) → DIV(minus(s(z0), s(z1)), s(z1))
The TRS R consists of the following rules:
minus(0, 0) → 0
minus(0, s(x)) → minus(0, x)
minus(s(x), 0) → s(minus(x, 0))
minus(s(x), s(y)) → minus(x, y)
ge(0, 0) → true
ge(s(x), 0) → ge(x, 0)
ge(0, s(0)) → false
ge(0, s(s(x))) → ge(0, s(x))
ge(s(x), s(y)) → ge(x, y)
The set Q consists of the following terms:
ge(0, 0)
ge(s(x0), 0)
ge(0, s(0))
ge(0, s(s(x0)))
ge(s(x0), s(x1))
minus(0, 0)
minus(0, s(x0))
minus(s(x0), 0)
minus(s(x0), s(x1))
We have to consider all minimal (P,Q,R)-chains.
(78) Rewriting (EQUIVALENT transformation)
By rewriting [LPAR04] the rule
IF(
true,
s(
z0),
s(
z1)) →
DIV(
minus(
s(
z0),
s(
z1)),
s(
z1)) at position [0] we obtained the following new rules [LPAR04]:
IF(true, s(z0), s(z1)) → DIV(minus(z0, z1), s(z1))
(79) Obligation:
Q DP problem:
The TRS P consists of the following rules:
DIV(y0, s(x0)) → IFY(ge(x0, 0), y0, s(x0))
IFY(true, s(x0), s(x1)) → IF(ge(x0, x1), s(x0), s(x1))
IF(true, s(z0), s(z1)) → DIV(minus(z0, z1), s(z1))
The TRS R consists of the following rules:
minus(0, 0) → 0
minus(0, s(x)) → minus(0, x)
minus(s(x), 0) → s(minus(x, 0))
minus(s(x), s(y)) → minus(x, y)
ge(0, 0) → true
ge(s(x), 0) → ge(x, 0)
ge(0, s(0)) → false
ge(0, s(s(x))) → ge(0, s(x))
ge(s(x), s(y)) → ge(x, y)
The set Q consists of the following terms:
ge(0, 0)
ge(s(x0), 0)
ge(0, s(0))
ge(0, s(s(x0)))
ge(s(x0), s(x1))
minus(0, 0)
minus(0, s(x0))
minus(s(x0), 0)
minus(s(x0), s(x1))
We have to consider all minimal (P,Q,R)-chains.
(80) ForwardInstantiation (EQUIVALENT transformation)
By forward instantiating [JAR06] the rule
DIV(
y0,
s(
x0)) →
IFY(
ge(
x0,
0),
y0,
s(
x0)) we obtained the following new rules [LPAR04]:
DIV(s(y_1), s(x1)) → IFY(ge(x1, 0), s(y_1), s(x1))
(81) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IFY(true, s(x0), s(x1)) → IF(ge(x0, x1), s(x0), s(x1))
IF(true, s(z0), s(z1)) → DIV(minus(z0, z1), s(z1))
DIV(s(y_1), s(x1)) → IFY(ge(x1, 0), s(y_1), s(x1))
The TRS R consists of the following rules:
minus(0, 0) → 0
minus(0, s(x)) → minus(0, x)
minus(s(x), 0) → s(minus(x, 0))
minus(s(x), s(y)) → minus(x, y)
ge(0, 0) → true
ge(s(x), 0) → ge(x, 0)
ge(0, s(0)) → false
ge(0, s(s(x))) → ge(0, s(x))
ge(s(x), s(y)) → ge(x, y)
The set Q consists of the following terms:
ge(0, 0)
ge(s(x0), 0)
ge(0, s(0))
ge(0, s(s(x0)))
ge(s(x0), s(x1))
minus(0, 0)
minus(0, s(x0))
minus(s(x0), 0)
minus(s(x0), s(x1))
We have to consider all minimal (P,Q,R)-chains.
(82) Narrowing (EQUIVALENT transformation)
By narrowing [LPAR04] the rule
IF(
true,
s(
z0),
s(
z1)) →
DIV(
minus(
z0,
z1),
s(
z1)) at position [0] we obtained the following new rules [LPAR04]:
IF(true, s(0), s(0)) → DIV(0, s(0))
IF(true, s(0), s(s(x0))) → DIV(minus(0, x0), s(s(x0)))
IF(true, s(s(x0)), s(0)) → DIV(s(minus(x0, 0)), s(0))
IF(true, s(s(x0)), s(s(x1))) → DIV(minus(x0, x1), s(s(x1)))
(83) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IFY(true, s(x0), s(x1)) → IF(ge(x0, x1), s(x0), s(x1))
DIV(s(y_1), s(x1)) → IFY(ge(x1, 0), s(y_1), s(x1))
IF(true, s(0), s(0)) → DIV(0, s(0))
IF(true, s(0), s(s(x0))) → DIV(minus(0, x0), s(s(x0)))
IF(true, s(s(x0)), s(0)) → DIV(s(minus(x0, 0)), s(0))
IF(true, s(s(x0)), s(s(x1))) → DIV(minus(x0, x1), s(s(x1)))
The TRS R consists of the following rules:
minus(0, 0) → 0
minus(0, s(x)) → minus(0, x)
minus(s(x), 0) → s(minus(x, 0))
minus(s(x), s(y)) → minus(x, y)
ge(0, 0) → true
ge(s(x), 0) → ge(x, 0)
ge(0, s(0)) → false
ge(0, s(s(x))) → ge(0, s(x))
ge(s(x), s(y)) → ge(x, y)
The set Q consists of the following terms:
ge(0, 0)
ge(s(x0), 0)
ge(0, s(0))
ge(0, s(s(x0)))
ge(s(x0), s(x1))
minus(0, 0)
minus(0, s(x0))
minus(s(x0), 0)
minus(s(x0), s(x1))
We have to consider all minimal (P,Q,R)-chains.
(84) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 2 less nodes.
(85) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IF(true, s(s(x0)), s(0)) → DIV(s(minus(x0, 0)), s(0))
DIV(s(y_1), s(x1)) → IFY(ge(x1, 0), s(y_1), s(x1))
IFY(true, s(x0), s(x1)) → IF(ge(x0, x1), s(x0), s(x1))
IF(true, s(s(x0)), s(s(x1))) → DIV(minus(x0, x1), s(s(x1)))
The TRS R consists of the following rules:
minus(0, 0) → 0
minus(0, s(x)) → minus(0, x)
minus(s(x), 0) → s(minus(x, 0))
minus(s(x), s(y)) → minus(x, y)
ge(0, 0) → true
ge(s(x), 0) → ge(x, 0)
ge(0, s(0)) → false
ge(0, s(s(x))) → ge(0, s(x))
ge(s(x), s(y)) → ge(x, y)
The set Q consists of the following terms:
ge(0, 0)
ge(s(x0), 0)
ge(0, s(0))
ge(0, s(s(x0)))
ge(s(x0), s(x1))
minus(0, 0)
minus(0, s(x0))
minus(s(x0), 0)
minus(s(x0), s(x1))
We have to consider all minimal (P,Q,R)-chains.
(86) Instantiation (EQUIVALENT transformation)
By instantiating [LPAR04] the rule
DIV(
s(
y_1),
s(
x1)) →
IFY(
ge(
x1,
0),
s(
y_1),
s(
x1)) we obtained the following new rules [LPAR04]:
DIV(s(y_0), s(0)) → IFY(ge(0, 0), s(y_0), s(0))
DIV(s(x0), s(s(z1))) → IFY(ge(s(z1), 0), s(x0), s(s(z1)))
(87) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IF(true, s(s(x0)), s(0)) → DIV(s(minus(x0, 0)), s(0))
IFY(true, s(x0), s(x1)) → IF(ge(x0, x1), s(x0), s(x1))
IF(true, s(s(x0)), s(s(x1))) → DIV(minus(x0, x1), s(s(x1)))
DIV(s(y_0), s(0)) → IFY(ge(0, 0), s(y_0), s(0))
DIV(s(x0), s(s(z1))) → IFY(ge(s(z1), 0), s(x0), s(s(z1)))
The TRS R consists of the following rules:
minus(0, 0) → 0
minus(0, s(x)) → minus(0, x)
minus(s(x), 0) → s(minus(x, 0))
minus(s(x), s(y)) → minus(x, y)
ge(0, 0) → true
ge(s(x), 0) → ge(x, 0)
ge(0, s(0)) → false
ge(0, s(s(x))) → ge(0, s(x))
ge(s(x), s(y)) → ge(x, y)
The set Q consists of the following terms:
ge(0, 0)
ge(s(x0), 0)
ge(0, s(0))
ge(0, s(s(x0)))
ge(s(x0), s(x1))
minus(0, 0)
minus(0, s(x0))
minus(s(x0), 0)
minus(s(x0), s(x1))
We have to consider all minimal (P,Q,R)-chains.
(88) Rewriting (EQUIVALENT transformation)
By rewriting [LPAR04] the rule
DIV(
s(
y_0),
s(
0)) →
IFY(
ge(
0,
0),
s(
y_0),
s(
0)) at position [0] we obtained the following new rules [LPAR04]:
DIV(s(y_0), s(0)) → IFY(true, s(y_0), s(0))
(89) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IF(true, s(s(x0)), s(0)) → DIV(s(minus(x0, 0)), s(0))
IFY(true, s(x0), s(x1)) → IF(ge(x0, x1), s(x0), s(x1))
IF(true, s(s(x0)), s(s(x1))) → DIV(minus(x0, x1), s(s(x1)))
DIV(s(x0), s(s(z1))) → IFY(ge(s(z1), 0), s(x0), s(s(z1)))
DIV(s(y_0), s(0)) → IFY(true, s(y_0), s(0))
The TRS R consists of the following rules:
minus(0, 0) → 0
minus(0, s(x)) → minus(0, x)
minus(s(x), 0) → s(minus(x, 0))
minus(s(x), s(y)) → minus(x, y)
ge(0, 0) → true
ge(s(x), 0) → ge(x, 0)
ge(0, s(0)) → false
ge(0, s(s(x))) → ge(0, s(x))
ge(s(x), s(y)) → ge(x, y)
The set Q consists of the following terms:
ge(0, 0)
ge(s(x0), 0)
ge(0, s(0))
ge(0, s(s(x0)))
ge(s(x0), s(x1))
minus(0, 0)
minus(0, s(x0))
minus(s(x0), 0)
minus(s(x0), s(x1))
We have to consider all minimal (P,Q,R)-chains.
(90) Rewriting (EQUIVALENT transformation)
By rewriting [LPAR04] the rule
DIV(
s(
x0),
s(
s(
z1))) →
IFY(
ge(
s(
z1),
0),
s(
x0),
s(
s(
z1))) at position [0] we obtained the following new rules [LPAR04]:
DIV(s(x0), s(s(z1))) → IFY(ge(z1, 0), s(x0), s(s(z1)))
(91) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IF(true, s(s(x0)), s(0)) → DIV(s(minus(x0, 0)), s(0))
IFY(true, s(x0), s(x1)) → IF(ge(x0, x1), s(x0), s(x1))
IF(true, s(s(x0)), s(s(x1))) → DIV(minus(x0, x1), s(s(x1)))
DIV(s(y_0), s(0)) → IFY(true, s(y_0), s(0))
DIV(s(x0), s(s(z1))) → IFY(ge(z1, 0), s(x0), s(s(z1)))
The TRS R consists of the following rules:
minus(0, 0) → 0
minus(0, s(x)) → minus(0, x)
minus(s(x), 0) → s(minus(x, 0))
minus(s(x), s(y)) → minus(x, y)
ge(0, 0) → true
ge(s(x), 0) → ge(x, 0)
ge(0, s(0)) → false
ge(0, s(s(x))) → ge(0, s(x))
ge(s(x), s(y)) → ge(x, y)
The set Q consists of the following terms:
ge(0, 0)
ge(s(x0), 0)
ge(0, s(0))
ge(0, s(s(x0)))
ge(s(x0), s(x1))
minus(0, 0)
minus(0, s(x0))
minus(s(x0), 0)
minus(s(x0), s(x1))
We have to consider all minimal (P,Q,R)-chains.
(92) Instantiation (EQUIVALENT transformation)
By instantiating [LPAR04] the rule
IFY(
true,
s(
x0),
s(
x1)) →
IF(
ge(
x0,
x1),
s(
x0),
s(
x1)) we obtained the following new rules [LPAR04]:
IFY(true, s(z0), s(0)) → IF(ge(z0, 0), s(z0), s(0))
IFY(true, s(z0), s(s(z1))) → IF(ge(z0, s(z1)), s(z0), s(s(z1)))
(93) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IF(true, s(s(x0)), s(0)) → DIV(s(minus(x0, 0)), s(0))
IF(true, s(s(x0)), s(s(x1))) → DIV(minus(x0, x1), s(s(x1)))
DIV(s(y_0), s(0)) → IFY(true, s(y_0), s(0))
DIV(s(x0), s(s(z1))) → IFY(ge(z1, 0), s(x0), s(s(z1)))
IFY(true, s(z0), s(0)) → IF(ge(z0, 0), s(z0), s(0))
IFY(true, s(z0), s(s(z1))) → IF(ge(z0, s(z1)), s(z0), s(s(z1)))
The TRS R consists of the following rules:
minus(0, 0) → 0
minus(0, s(x)) → minus(0, x)
minus(s(x), 0) → s(minus(x, 0))
minus(s(x), s(y)) → minus(x, y)
ge(0, 0) → true
ge(s(x), 0) → ge(x, 0)
ge(0, s(0)) → false
ge(0, s(s(x))) → ge(0, s(x))
ge(s(x), s(y)) → ge(x, y)
The set Q consists of the following terms:
ge(0, 0)
ge(s(x0), 0)
ge(0, s(0))
ge(0, s(s(x0)))
ge(s(x0), s(x1))
minus(0, 0)
minus(0, s(x0))
minus(s(x0), 0)
minus(s(x0), s(x1))
We have to consider all minimal (P,Q,R)-chains.
(94) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 2 SCCs.
(95) Complex Obligation (AND)
(96) Obligation:
Q DP problem:
The TRS P consists of the following rules:
DIV(s(x0), s(s(z1))) → IFY(ge(z1, 0), s(x0), s(s(z1)))
IFY(true, s(z0), s(s(z1))) → IF(ge(z0, s(z1)), s(z0), s(s(z1)))
IF(true, s(s(x0)), s(s(x1))) → DIV(minus(x0, x1), s(s(x1)))
The TRS R consists of the following rules:
minus(0, 0) → 0
minus(0, s(x)) → minus(0, x)
minus(s(x), 0) → s(minus(x, 0))
minus(s(x), s(y)) → minus(x, y)
ge(0, 0) → true
ge(s(x), 0) → ge(x, 0)
ge(0, s(0)) → false
ge(0, s(s(x))) → ge(0, s(x))
ge(s(x), s(y)) → ge(x, y)
The set Q consists of the following terms:
ge(0, 0)
ge(s(x0), 0)
ge(0, s(0))
ge(0, s(s(x0)))
ge(s(x0), s(x1))
minus(0, 0)
minus(0, s(x0))
minus(s(x0), 0)
minus(s(x0), s(x1))
We have to consider all minimal (P,Q,R)-chains.
(97) ForwardInstantiation (EQUIVALENT transformation)
By forward instantiating [JAR06] the rule
IFY(
true,
s(
z0),
s(
s(
z1))) →
IF(
ge(
z0,
s(
z1)),
s(
z0),
s(
s(
z1))) we obtained the following new rules [LPAR04]:
IFY(true, s(s(y_1)), s(s(x1))) → IF(ge(s(y_1), s(x1)), s(s(y_1)), s(s(x1)))
(98) Obligation:
Q DP problem:
The TRS P consists of the following rules:
DIV(s(x0), s(s(z1))) → IFY(ge(z1, 0), s(x0), s(s(z1)))
IF(true, s(s(x0)), s(s(x1))) → DIV(minus(x0, x1), s(s(x1)))
IFY(true, s(s(y_1)), s(s(x1))) → IF(ge(s(y_1), s(x1)), s(s(y_1)), s(s(x1)))
The TRS R consists of the following rules:
minus(0, 0) → 0
minus(0, s(x)) → minus(0, x)
minus(s(x), 0) → s(minus(x, 0))
minus(s(x), s(y)) → minus(x, y)
ge(0, 0) → true
ge(s(x), 0) → ge(x, 0)
ge(0, s(0)) → false
ge(0, s(s(x))) → ge(0, s(x))
ge(s(x), s(y)) → ge(x, y)
The set Q consists of the following terms:
ge(0, 0)
ge(s(x0), 0)
ge(0, s(0))
ge(0, s(s(x0)))
ge(s(x0), s(x1))
minus(0, 0)
minus(0, s(x0))
minus(s(x0), 0)
minus(s(x0), s(x1))
We have to consider all minimal (P,Q,R)-chains.
(99) Rewriting (EQUIVALENT transformation)
By rewriting [LPAR04] the rule
IFY(
true,
s(
s(
y_1)),
s(
s(
x1))) →
IF(
ge(
s(
y_1),
s(
x1)),
s(
s(
y_1)),
s(
s(
x1))) at position [0] we obtained the following new rules [LPAR04]:
IFY(true, s(s(y_1)), s(s(x1))) → IF(ge(y_1, x1), s(s(y_1)), s(s(x1)))
(100) Obligation:
Q DP problem:
The TRS P consists of the following rules:
DIV(s(x0), s(s(z1))) → IFY(ge(z1, 0), s(x0), s(s(z1)))
IF(true, s(s(x0)), s(s(x1))) → DIV(minus(x0, x1), s(s(x1)))
IFY(true, s(s(y_1)), s(s(x1))) → IF(ge(y_1, x1), s(s(y_1)), s(s(x1)))
The TRS R consists of the following rules:
minus(0, 0) → 0
minus(0, s(x)) → minus(0, x)
minus(s(x), 0) → s(minus(x, 0))
minus(s(x), s(y)) → minus(x, y)
ge(0, 0) → true
ge(s(x), 0) → ge(x, 0)
ge(0, s(0)) → false
ge(0, s(s(x))) → ge(0, s(x))
ge(s(x), s(y)) → ge(x, y)
The set Q consists of the following terms:
ge(0, 0)
ge(s(x0), 0)
ge(0, s(0))
ge(0, s(s(x0)))
ge(s(x0), s(x1))
minus(0, 0)
minus(0, s(x0))
minus(s(x0), 0)
minus(s(x0), s(x1))
We have to consider all minimal (P,Q,R)-chains.
(101) QDPOrderProof (EQUIVALENT transformation)
We use the reduction pair processor [LPAR04].
The following pairs can be oriented strictly and are deleted.
IF(true, s(s(x0)), s(s(x1))) → DIV(minus(x0, x1), s(s(x1)))
The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO]:
POL(DIV(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(IFY(x1, x2, x3)) = | | + | | · | x1 | + | | · | x2 | + | | · | x3 |
POL(ge(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(IF(x1, x2, x3)) = | | + | | · | x1 | + | | · | x2 | + | | · | x3 |
POL(minus(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
The following usable rules [FROCOS05] were oriented:
ge(s(x), s(y)) → ge(x, y)
ge(0, s(s(x))) → ge(0, s(x))
ge(0, s(0)) → false
ge(s(x), 0) → ge(x, 0)
ge(0, 0) → true
minus(s(x), s(y)) → minus(x, y)
minus(s(x), 0) → s(minus(x, 0))
minus(0, s(x)) → minus(0, x)
minus(0, 0) → 0
(102) Obligation:
Q DP problem:
The TRS P consists of the following rules:
DIV(s(x0), s(s(z1))) → IFY(ge(z1, 0), s(x0), s(s(z1)))
IFY(true, s(s(y_1)), s(s(x1))) → IF(ge(y_1, x1), s(s(y_1)), s(s(x1)))
The TRS R consists of the following rules:
minus(0, 0) → 0
minus(0, s(x)) → minus(0, x)
minus(s(x), 0) → s(minus(x, 0))
minus(s(x), s(y)) → minus(x, y)
ge(0, 0) → true
ge(s(x), 0) → ge(x, 0)
ge(0, s(0)) → false
ge(0, s(s(x))) → ge(0, s(x))
ge(s(x), s(y)) → ge(x, y)
The set Q consists of the following terms:
ge(0, 0)
ge(s(x0), 0)
ge(0, s(0))
ge(0, s(s(x0)))
ge(s(x0), s(x1))
minus(0, 0)
minus(0, s(x0))
minus(s(x0), 0)
minus(s(x0), s(x1))
We have to consider all minimal (P,Q,R)-chains.
(103) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 2 less nodes.
(104) TRUE
(105) Obligation:
Q DP problem:
The TRS P consists of the following rules:
DIV(s(y_0), s(0)) → IFY(true, s(y_0), s(0))
IFY(true, s(z0), s(0)) → IF(ge(z0, 0), s(z0), s(0))
IF(true, s(s(x0)), s(0)) → DIV(s(minus(x0, 0)), s(0))
The TRS R consists of the following rules:
minus(0, 0) → 0
minus(0, s(x)) → minus(0, x)
minus(s(x), 0) → s(minus(x, 0))
minus(s(x), s(y)) → minus(x, y)
ge(0, 0) → true
ge(s(x), 0) → ge(x, 0)
ge(0, s(0)) → false
ge(0, s(s(x))) → ge(0, s(x))
ge(s(x), s(y)) → ge(x, y)
The set Q consists of the following terms:
ge(0, 0)
ge(s(x0), 0)
ge(0, s(0))
ge(0, s(s(x0)))
ge(s(x0), s(x1))
minus(0, 0)
minus(0, s(x0))
minus(s(x0), 0)
minus(s(x0), s(x1))
We have to consider all minimal (P,Q,R)-chains.
(106) UsableRulesProof (EQUIVALENT transformation)
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.
(107) Obligation:
Q DP problem:
The TRS P consists of the following rules:
DIV(s(y_0), s(0)) → IFY(true, s(y_0), s(0))
IFY(true, s(z0), s(0)) → IF(ge(z0, 0), s(z0), s(0))
IF(true, s(s(x0)), s(0)) → DIV(s(minus(x0, 0)), s(0))
The TRS R consists of the following rules:
minus(0, 0) → 0
minus(s(x), 0) → s(minus(x, 0))
ge(0, 0) → true
ge(s(x), 0) → ge(x, 0)
The set Q consists of the following terms:
ge(0, 0)
ge(s(x0), 0)
ge(0, s(0))
ge(0, s(s(x0)))
ge(s(x0), s(x1))
minus(0, 0)
minus(0, s(x0))
minus(s(x0), 0)
minus(s(x0), s(x1))
We have to consider all minimal (P,Q,R)-chains.
(108) ForwardInstantiation (EQUIVALENT transformation)
By forward instantiating [JAR06] the rule
IFY(
true,
s(
z0),
s(
0)) →
IF(
ge(
z0,
0),
s(
z0),
s(
0)) we obtained the following new rules [LPAR04]:
IFY(true, s(s(y_1)), s(0)) → IF(ge(s(y_1), 0), s(s(y_1)), s(0))
(109) Obligation:
Q DP problem:
The TRS P consists of the following rules:
DIV(s(y_0), s(0)) → IFY(true, s(y_0), s(0))
IF(true, s(s(x0)), s(0)) → DIV(s(minus(x0, 0)), s(0))
IFY(true, s(s(y_1)), s(0)) → IF(ge(s(y_1), 0), s(s(y_1)), s(0))
The TRS R consists of the following rules:
minus(0, 0) → 0
minus(s(x), 0) → s(minus(x, 0))
ge(0, 0) → true
ge(s(x), 0) → ge(x, 0)
The set Q consists of the following terms:
ge(0, 0)
ge(s(x0), 0)
ge(0, s(0))
ge(0, s(s(x0)))
ge(s(x0), s(x1))
minus(0, 0)
minus(0, s(x0))
minus(s(x0), 0)
minus(s(x0), s(x1))
We have to consider all minimal (P,Q,R)-chains.
(110) Rewriting (EQUIVALENT transformation)
By rewriting [LPAR04] the rule
IFY(
true,
s(
s(
y_1)),
s(
0)) →
IF(
ge(
s(
y_1),
0),
s(
s(
y_1)),
s(
0)) at position [0] we obtained the following new rules [LPAR04]:
IFY(true, s(s(y_1)), s(0)) → IF(ge(y_1, 0), s(s(y_1)), s(0))
(111) Obligation:
Q DP problem:
The TRS P consists of the following rules:
DIV(s(y_0), s(0)) → IFY(true, s(y_0), s(0))
IF(true, s(s(x0)), s(0)) → DIV(s(minus(x0, 0)), s(0))
IFY(true, s(s(y_1)), s(0)) → IF(ge(y_1, 0), s(s(y_1)), s(0))
The TRS R consists of the following rules:
minus(0, 0) → 0
minus(s(x), 0) → s(minus(x, 0))
ge(0, 0) → true
ge(s(x), 0) → ge(x, 0)
The set Q consists of the following terms:
ge(0, 0)
ge(s(x0), 0)
ge(0, s(0))
ge(0, s(s(x0)))
ge(s(x0), s(x1))
minus(0, 0)
minus(0, s(x0))
minus(s(x0), 0)
minus(s(x0), s(x1))
We have to consider all minimal (P,Q,R)-chains.
(112) MRRProof (EQUIVALENT transformation)
By using the rule removal processor [LPAR04] with the following ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.
Strictly oriented dependency pairs:
IF(true, s(s(x0)), s(0)) → DIV(s(minus(x0, 0)), s(0))
Strictly oriented rules of the TRS R:
ge(s(x), 0) → ge(x, 0)
Used ordering: Polynomial interpretation [POLO]:
POL(0) = 0
POL(DIV(x1, x2)) = 1 + 2·x1 + 2·x2
POL(IF(x1, x2, x3)) = 2 + x1 + x2 + 2·x3
POL(IFY(x1, x2, x3)) = x1 + 2·x2 + x3
POL(ge(x1, x2)) = 2 + x1 + 2·x2
POL(minus(x1, x2)) = x1 + x2
POL(s(x1)) = 1 + 2·x1
POL(true) = 2
(113) Obligation:
Q DP problem:
The TRS P consists of the following rules:
DIV(s(y_0), s(0)) → IFY(true, s(y_0), s(0))
IFY(true, s(s(y_1)), s(0)) → IF(ge(y_1, 0), s(s(y_1)), s(0))
The TRS R consists of the following rules:
minus(0, 0) → 0
minus(s(x), 0) → s(minus(x, 0))
ge(0, 0) → true
The set Q consists of the following terms:
ge(0, 0)
ge(s(x0), 0)
ge(0, s(0))
ge(0, s(s(x0)))
ge(s(x0), s(x1))
minus(0, 0)
minus(0, s(x0))
minus(s(x0), 0)
minus(s(x0), s(x1))
We have to consider all minimal (P,Q,R)-chains.
(114) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 2 less nodes.
(115) TRUE