(0) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
quot(0, s(y)) → 0
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
inc(s(x)) → s(inc(x))
inc(0) → s(0)
log(x) → logIter(x, 0)
logIter(x, y) → if(le(s(0), x), le(s(s(0)), x), quot(x, s(s(0))), inc(y))
if(false, b, x, y) → logZeroError
if(true, false, x, s(y)) → y
if(true, true, x, y) → logIter(x, 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:
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
quot(0, s(y)) → 0
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
inc(s(x)) → s(inc(x))
inc(0) → s(0)
log(x) → logIter(x, 0)
logIter(x, y) → if(le(s(0), x), le(s(s(0)), x), quot(x, s(s(0))), inc(y))
if(false, b, x, y) → logZeroError
if(true, false, x, s(y)) → y
if(true, true, x, y) → logIter(x, y)
The set Q consists of the following terms:
minus(x0, 0)
minus(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
inc(s(x0))
inc(0)
log(x0)
logIter(x0, x1)
if(false, x0, x1, x2)
if(true, false, x0, s(x1))
if(true, 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:
MINUS(s(x), s(y)) → MINUS(x, y)
QUOT(s(x), s(y)) → QUOT(minus(x, y), s(y))
QUOT(s(x), s(y)) → MINUS(x, y)
LE(s(x), s(y)) → LE(x, y)
INC(s(x)) → INC(x)
LOG(x) → LOGITER(x, 0)
LOGITER(x, y) → IF(le(s(0), x), le(s(s(0)), x), quot(x, s(s(0))), inc(y))
LOGITER(x, y) → LE(s(0), x)
LOGITER(x, y) → LE(s(s(0)), x)
LOGITER(x, y) → QUOT(x, s(s(0)))
LOGITER(x, y) → INC(y)
IF(true, true, x, y) → LOGITER(x, y)
The TRS R consists of the following rules:
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
quot(0, s(y)) → 0
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
inc(s(x)) → s(inc(x))
inc(0) → s(0)
log(x) → logIter(x, 0)
logIter(x, y) → if(le(s(0), x), le(s(s(0)), x), quot(x, s(s(0))), inc(y))
if(false, b, x, y) → logZeroError
if(true, false, x, s(y)) → y
if(true, true, x, y) → logIter(x, y)
The set Q consists of the following terms:
minus(x0, 0)
minus(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
inc(s(x0))
inc(0)
log(x0)
logIter(x0, x1)
if(false, x0, x1, x2)
if(true, false, x0, s(x1))
if(true, 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 5 SCCs with 6 less nodes.
(6) Complex Obligation (AND)
(7) Obligation:
Q DP problem:
The TRS P consists of the following rules:
INC(s(x)) → INC(x)
The TRS R consists of the following rules:
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
quot(0, s(y)) → 0
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
inc(s(x)) → s(inc(x))
inc(0) → s(0)
log(x) → logIter(x, 0)
logIter(x, y) → if(le(s(0), x), le(s(s(0)), x), quot(x, s(s(0))), inc(y))
if(false, b, x, y) → logZeroError
if(true, false, x, s(y)) → y
if(true, true, x, y) → logIter(x, y)
The set Q consists of the following terms:
minus(x0, 0)
minus(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
inc(s(x0))
inc(0)
log(x0)
logIter(x0, x1)
if(false, x0, x1, x2)
if(true, false, x0, s(x1))
if(true, 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:
INC(s(x)) → INC(x)
R is empty.
The set Q consists of the following terms:
minus(x0, 0)
minus(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
inc(s(x0))
inc(0)
log(x0)
logIter(x0, x1)
if(false, x0, x1, x2)
if(true, false, x0, s(x1))
if(true, 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].
minus(x0, 0)
minus(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
inc(s(x0))
inc(0)
log(x0)
logIter(x0, x1)
if(false, x0, x1, x2)
if(true, false, x0, s(x1))
if(true, true, x0, x1)
(11) Obligation:
Q DP problem:
The TRS P consists of the following rules:
INC(s(x)) → INC(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:
- INC(s(x)) → INC(x)
The graph contains the following edges 1 > 1
(13) TRUE
(14) Obligation:
Q DP problem:
The TRS P consists of the following rules:
LE(s(x), s(y)) → LE(x, y)
The TRS R consists of the following rules:
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
quot(0, s(y)) → 0
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
inc(s(x)) → s(inc(x))
inc(0) → s(0)
log(x) → logIter(x, 0)
logIter(x, y) → if(le(s(0), x), le(s(s(0)), x), quot(x, s(s(0))), inc(y))
if(false, b, x, y) → logZeroError
if(true, false, x, s(y)) → y
if(true, true, x, y) → logIter(x, y)
The set Q consists of the following terms:
minus(x0, 0)
minus(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
inc(s(x0))
inc(0)
log(x0)
logIter(x0, x1)
if(false, x0, x1, x2)
if(true, false, x0, s(x1))
if(true, 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:
LE(s(x), s(y)) → LE(x, y)
R is empty.
The set Q consists of the following terms:
minus(x0, 0)
minus(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
inc(s(x0))
inc(0)
log(x0)
logIter(x0, x1)
if(false, x0, x1, x2)
if(true, false, x0, s(x1))
if(true, 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].
minus(x0, 0)
minus(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
inc(s(x0))
inc(0)
log(x0)
logIter(x0, x1)
if(false, x0, x1, x2)
if(true, false, x0, s(x1))
if(true, true, x0, x1)
(18) Obligation:
Q DP problem:
The TRS P consists of the following rules:
LE(s(x), s(y)) → LE(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:
- LE(s(x), s(y)) → LE(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), s(y)) → MINUS(x, y)
The TRS R consists of the following rules:
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
quot(0, s(y)) → 0
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
inc(s(x)) → s(inc(x))
inc(0) → s(0)
log(x) → logIter(x, 0)
logIter(x, y) → if(le(s(0), x), le(s(s(0)), x), quot(x, s(s(0))), inc(y))
if(false, b, x, y) → logZeroError
if(true, false, x, s(y)) → y
if(true, true, x, y) → logIter(x, y)
The set Q consists of the following terms:
minus(x0, 0)
minus(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
inc(s(x0))
inc(0)
log(x0)
logIter(x0, x1)
if(false, x0, x1, x2)
if(true, false, x0, s(x1))
if(true, 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), s(y)) → MINUS(x, y)
R is empty.
The set Q consists of the following terms:
minus(x0, 0)
minus(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
inc(s(x0))
inc(0)
log(x0)
logIter(x0, x1)
if(false, x0, x1, x2)
if(true, false, x0, s(x1))
if(true, 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].
minus(x0, 0)
minus(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
inc(s(x0))
inc(0)
log(x0)
logIter(x0, x1)
if(false, x0, x1, x2)
if(true, false, x0, s(x1))
if(true, true, x0, x1)
(25) 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.
(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), s(y)) → MINUS(x, y)
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:
QUOT(s(x), s(y)) → QUOT(minus(x, y), s(y))
The TRS R consists of the following rules:
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
quot(0, s(y)) → 0
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
inc(s(x)) → s(inc(x))
inc(0) → s(0)
log(x) → logIter(x, 0)
logIter(x, y) → if(le(s(0), x), le(s(s(0)), x), quot(x, s(s(0))), inc(y))
if(false, b, x, y) → logZeroError
if(true, false, x, s(y)) → y
if(true, true, x, y) → logIter(x, y)
The set Q consists of the following terms:
minus(x0, 0)
minus(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
inc(s(x0))
inc(0)
log(x0)
logIter(x0, x1)
if(false, x0, x1, x2)
if(true, false, x0, s(x1))
if(true, 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:
QUOT(s(x), s(y)) → QUOT(minus(x, y), s(y))
The TRS R consists of the following rules:
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
The set Q consists of the following terms:
minus(x0, 0)
minus(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
inc(s(x0))
inc(0)
log(x0)
logIter(x0, x1)
if(false, x0, x1, x2)
if(true, false, x0, s(x1))
if(true, 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].
quot(0, s(x0))
quot(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
inc(s(x0))
inc(0)
log(x0)
logIter(x0, x1)
if(false, x0, x1, x2)
if(true, false, x0, s(x1))
if(true, true, x0, x1)
(32) Obligation:
Q DP problem:
The TRS P consists of the following rules:
QUOT(s(x), s(y)) → QUOT(minus(x, y), s(y))
The TRS R consists of the following rules:
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
The set Q consists of the following terms:
minus(x0, 0)
minus(s(x0), s(x1))
We have to consider all minimal (P,Q,R)-chains.
(33) QDPOrderProof (EQUIVALENT transformation)
We use the reduction pair processor [LPAR04].
The following pairs can be oriented strictly and are deleted.
QUOT(s(x), s(y)) → QUOT(minus(x, y), s(y))
The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO]:
POL(QUOT(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(minus(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
The following usable rules [FROCOS05] were oriented:
minus(s(x), s(y)) → minus(x, y)
minus(x, 0) → x
(34) Obligation:
Q DP problem:
P is empty.
The TRS R consists of the following rules:
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
The set Q consists of the following terms:
minus(x0, 0)
minus(s(x0), s(x1))
We have to consider all minimal (P,Q,R)-chains.
(35) PisEmptyProof (EQUIVALENT transformation)
The TRS P is empty. Hence, there is no (P,Q,R) chain.
(36) TRUE
(37) Obligation:
Q DP problem:
The TRS P consists of the following rules:
LOGITER(x, y) → IF(le(s(0), x), le(s(s(0)), x), quot(x, s(s(0))), inc(y))
IF(true, true, x, y) → LOGITER(x, y)
The TRS R consists of the following rules:
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
quot(0, s(y)) → 0
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
inc(s(x)) → s(inc(x))
inc(0) → s(0)
log(x) → logIter(x, 0)
logIter(x, y) → if(le(s(0), x), le(s(s(0)), x), quot(x, s(s(0))), inc(y))
if(false, b, x, y) → logZeroError
if(true, false, x, s(y)) → y
if(true, true, x, y) → logIter(x, y)
The set Q consists of the following terms:
minus(x0, 0)
minus(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
inc(s(x0))
inc(0)
log(x0)
logIter(x0, x1)
if(false, x0, x1, x2)
if(true, false, x0, s(x1))
if(true, true, x0, x1)
We have to consider all minimal (P,Q,R)-chains.
(38) 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.
(39) Obligation:
Q DP problem:
The TRS P consists of the following rules:
LOGITER(x, y) → IF(le(s(0), x), le(s(s(0)), x), quot(x, s(s(0))), inc(y))
IF(true, true, x, y) → LOGITER(x, y)
The TRS R consists of the following rules:
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
quot(0, s(y)) → 0
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
inc(s(x)) → s(inc(x))
inc(0) → s(0)
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
le(0, y) → true
The set Q consists of the following terms:
minus(x0, 0)
minus(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
inc(s(x0))
inc(0)
log(x0)
logIter(x0, x1)
if(false, x0, x1, x2)
if(true, false, x0, s(x1))
if(true, true, x0, x1)
We have to consider all minimal (P,Q,R)-chains.
(40) 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].
log(x0)
logIter(x0, x1)
if(false, x0, x1, x2)
if(true, false, x0, s(x1))
if(true, true, x0, x1)
(41) Obligation:
Q DP problem:
The TRS P consists of the following rules:
LOGITER(x, y) → IF(le(s(0), x), le(s(s(0)), x), quot(x, s(s(0))), inc(y))
IF(true, true, x, y) → LOGITER(x, y)
The TRS R consists of the following rules:
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
quot(0, s(y)) → 0
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
inc(s(x)) → s(inc(x))
inc(0) → s(0)
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
le(0, y) → true
The set Q consists of the following terms:
minus(x0, 0)
minus(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
inc(s(x0))
inc(0)
We have to consider all minimal (P,Q,R)-chains.
(42) Induction-Processor (SOUND transformation)
This DP could be deleted by the Induction-Processor:LOGITER(
x,
y) →
IF(
le(
s(
0),
x),
le(
s(
s(
0)),
x),
quot(
x,
s(
s(
0))),
inc(
y))
This order was computed:Polynomial interpretation [POLO]:
POL(0) = 0
POL(IF(x1, x2, x3, x4)) = x1 + 2·x2 + x3
POL(LOGITER(x1, x2)) = 3
POL(false) = 0
POL(inc(x1)) = 0
POL(le(x1, x2)) = 1
POL(minus(x1, x2)) = 2 + x1
POL(quot(x1, x2)) = 0
POL(s(x1)) = 2·x1
POL(true) = 1
At least one of these decreasing rules is always used after the deleted DP:le(
s(
x),
0) →
falseThe following formula is valid:z0:sort[a0],x:sort[a0].(((
z0 =
s(
0)→
le'(
z0 ,
x )=
true)∨(
z0 =
s2 (
0)→
le'(
z0 ,
x )=
true))∨
false=
true)
The transformed set:le'(
s(
x),
0) →
truele'(
s(
x5),
s(
y3)) →
le'(
x5,
y3)
le'(
0,
y42) →
falsele(
s(
x),
0) →
falsele(
s(
x5),
s(
y3)) →
le(
x5,
y3)
quot(
0,
s(
y9)) →
0quot(
s(
x18),
s(
y15)) →
s(
quot(
minus(
x18,
y15),
s(
y15)))
inc(
s(
x25)) →
s(
inc(
x25))
inc(
0) →
s(
0)
minus(
x38,
0) →
x38minus(
s(
x45),
s(
y36)) →
minus(
x45,
y36)
le(
0,
y42) →
truequot(
0,
0) →
0quot(
s(
x2),
0) →
0minus(
0,
s(
x0)) →
0equal_bool(
true,
false) →
falseequal_bool(
false,
true) →
falseequal_bool(
true,
true) →
trueequal_bool(
false,
false) →
trueand(
true,
x) →
xand(
false,
x) →
falseor(
true,
x) →
trueor(
false,
x) →
xnot(
false) →
truenot(
true) →
falseisa_true(
true) →
trueisa_true(
false) →
falseisa_false(
true) →
falseisa_false(
false) →
trueequal_sort[a0](
0,
0) →
trueequal_sort[a0](
0,
s(
x0)) →
falseequal_sort[a0](
s(
x0),
0) →
falseequal_sort[a0](
s(
x0),
s(
x1)) →
equal_sort[a0](
x0,
x1)
equal_sort[a32](
witness_sort[a32],
witness_sort[a32]) →
true
(43) Complex Obligation (AND)
(44) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IF(true, true, x, y) → LOGITER(x, y)
The TRS R consists of the following rules:
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
quot(0, s(y)) → 0
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
inc(s(x)) → s(inc(x))
inc(0) → s(0)
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
le(0, y) → true
The set Q consists of the following terms:
minus(x0, 0)
minus(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
inc(s(x0))
inc(0)
We have to consider all minimal (P,Q,R)-chains.
(45) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 1 less node.
(46) TRUE
(47) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
le'(s(x), 0) → true
le'(s(x5), s(y3)) → le'(x5, y3)
le'(0, y42) → false
le(s(x), 0) → false
le(s(x5), s(y3)) → le(x5, y3)
quot(0, s(y9)) → 0
quot(s(x18), s(y15)) → s(quot(minus(x18, y15), s(y15)))
inc(s(x25)) → s(inc(x25))
inc(0) → s(0)
minus(x38, 0) → x38
minus(s(x45), s(y36)) → minus(x45, y36)
le(0, y42) → true
quot(0, 0) → 0
quot(s(x2), 0) → 0
minus(0, s(x0)) → 0
equal_bool(true, false) → false
equal_bool(false, true) → false
equal_bool(true, true) → true
equal_bool(false, false) → true
and(true, x) → x
and(false, x) → false
or(true, x) → true
or(false, x) → x
not(false) → true
not(true) → false
isa_true(true) → true
isa_true(false) → false
isa_false(true) → false
isa_false(false) → true
equal_sort[a0](0, 0) → true
equal_sort[a0](0, s(x0)) → false
equal_sort[a0](s(x0), 0) → false
equal_sort[a0](s(x0), s(x1)) → equal_sort[a0](x0, x1)
equal_sort[a32](witness_sort[a32], witness_sort[a32]) → true
Q is empty.
(48) Overlay + Local Confluence (EQUIVALENT transformation)
The TRS is overlay and locally confluent. By [NOC] we can switch to innermost.
(49) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
le'(s(x), 0) → true
le'(s(x5), s(y3)) → le'(x5, y3)
le'(0, y42) → false
le(s(x), 0) → false
le(s(x5), s(y3)) → le(x5, y3)
quot(0, s(y9)) → 0
quot(s(x18), s(y15)) → s(quot(minus(x18, y15), s(y15)))
inc(s(x25)) → s(inc(x25))
inc(0) → s(0)
minus(x38, 0) → x38
minus(s(x45), s(y36)) → minus(x45, y36)
le(0, y42) → true
quot(0, 0) → 0
quot(s(x2), 0) → 0
minus(0, s(x0)) → 0
equal_bool(true, false) → false
equal_bool(false, true) → false
equal_bool(true, true) → true
equal_bool(false, false) → true
and(true, x) → x
and(false, x) → false
or(true, x) → true
or(false, x) → x
not(false) → true
not(true) → false
isa_true(true) → true
isa_true(false) → false
isa_false(true) → false
isa_false(false) → true
equal_sort[a0](0, 0) → true
equal_sort[a0](0, s(x0)) → false
equal_sort[a0](s(x0), 0) → false
equal_sort[a0](s(x0), s(x1)) → equal_sort[a0](x0, x1)
equal_sort[a32](witness_sort[a32], witness_sort[a32]) → true
The set Q consists of the following terms:
le'(s(x0), 0)
le'(s(x0), s(x1))
le'(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
inc(s(x0))
inc(0)
minus(x0, 0)
minus(s(x0), s(x1))
le(0, x0)
quot(0, 0)
quot(s(x0), 0)
minus(0, s(x0))
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a0](0, 0)
equal_sort[a0](0, s(x0))
equal_sort[a0](s(x0), 0)
equal_sort[a0](s(x0), s(x1))
equal_sort[a32](witness_sort[a32], witness_sort[a32])
(50) DependencyPairsProof (EQUIVALENT transformation)
Using Dependency Pairs [AG00,LPAR04] we result in the following initial DP problem.
(51) Obligation:
Q DP problem:
The TRS P consists of the following rules:
LE'(s(x5), s(y3)) → LE'(x5, y3)
LE(s(x5), s(y3)) → LE(x5, y3)
QUOT(s(x18), s(y15)) → QUOT(minus(x18, y15), s(y15))
QUOT(s(x18), s(y15)) → MINUS(x18, y15)
INC(s(x25)) → INC(x25)
MINUS(s(x45), s(y36)) → MINUS(x45, y36)
EQUAL_SORT[A0](s(x0), s(x1)) → EQUAL_SORT[A0](x0, x1)
The TRS R consists of the following rules:
le'(s(x), 0) → true
le'(s(x5), s(y3)) → le'(x5, y3)
le'(0, y42) → false
le(s(x), 0) → false
le(s(x5), s(y3)) → le(x5, y3)
quot(0, s(y9)) → 0
quot(s(x18), s(y15)) → s(quot(minus(x18, y15), s(y15)))
inc(s(x25)) → s(inc(x25))
inc(0) → s(0)
minus(x38, 0) → x38
minus(s(x45), s(y36)) → minus(x45, y36)
le(0, y42) → true
quot(0, 0) → 0
quot(s(x2), 0) → 0
minus(0, s(x0)) → 0
equal_bool(true, false) → false
equal_bool(false, true) → false
equal_bool(true, true) → true
equal_bool(false, false) → true
and(true, x) → x
and(false, x) → false
or(true, x) → true
or(false, x) → x
not(false) → true
not(true) → false
isa_true(true) → true
isa_true(false) → false
isa_false(true) → false
isa_false(false) → true
equal_sort[a0](0, 0) → true
equal_sort[a0](0, s(x0)) → false
equal_sort[a0](s(x0), 0) → false
equal_sort[a0](s(x0), s(x1)) → equal_sort[a0](x0, x1)
equal_sort[a32](witness_sort[a32], witness_sort[a32]) → true
The set Q consists of the following terms:
le'(s(x0), 0)
le'(s(x0), s(x1))
le'(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
inc(s(x0))
inc(0)
minus(x0, 0)
minus(s(x0), s(x1))
le(0, x0)
quot(0, 0)
quot(s(x0), 0)
minus(0, s(x0))
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a0](0, 0)
equal_sort[a0](0, s(x0))
equal_sort[a0](s(x0), 0)
equal_sort[a0](s(x0), s(x1))
equal_sort[a32](witness_sort[a32], witness_sort[a32])
We have to consider all minimal (P,Q,R)-chains.
(52) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 6 SCCs with 1 less node.
(53) Complex Obligation (AND)
(54) Obligation:
Q DP problem:
The TRS P consists of the following rules:
EQUAL_SORT[A0](s(x0), s(x1)) → EQUAL_SORT[A0](x0, x1)
The TRS R consists of the following rules:
le'(s(x), 0) → true
le'(s(x5), s(y3)) → le'(x5, y3)
le'(0, y42) → false
le(s(x), 0) → false
le(s(x5), s(y3)) → le(x5, y3)
quot(0, s(y9)) → 0
quot(s(x18), s(y15)) → s(quot(minus(x18, y15), s(y15)))
inc(s(x25)) → s(inc(x25))
inc(0) → s(0)
minus(x38, 0) → x38
minus(s(x45), s(y36)) → minus(x45, y36)
le(0, y42) → true
quot(0, 0) → 0
quot(s(x2), 0) → 0
minus(0, s(x0)) → 0
equal_bool(true, false) → false
equal_bool(false, true) → false
equal_bool(true, true) → true
equal_bool(false, false) → true
and(true, x) → x
and(false, x) → false
or(true, x) → true
or(false, x) → x
not(false) → true
not(true) → false
isa_true(true) → true
isa_true(false) → false
isa_false(true) → false
isa_false(false) → true
equal_sort[a0](0, 0) → true
equal_sort[a0](0, s(x0)) → false
equal_sort[a0](s(x0), 0) → false
equal_sort[a0](s(x0), s(x1)) → equal_sort[a0](x0, x1)
equal_sort[a32](witness_sort[a32], witness_sort[a32]) → true
The set Q consists of the following terms:
le'(s(x0), 0)
le'(s(x0), s(x1))
le'(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
inc(s(x0))
inc(0)
minus(x0, 0)
minus(s(x0), s(x1))
le(0, x0)
quot(0, 0)
quot(s(x0), 0)
minus(0, s(x0))
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a0](0, 0)
equal_sort[a0](0, s(x0))
equal_sort[a0](s(x0), 0)
equal_sort[a0](s(x0), s(x1))
equal_sort[a32](witness_sort[a32], witness_sort[a32])
We have to consider all minimal (P,Q,R)-chains.
(55) 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.
(56) Obligation:
Q DP problem:
The TRS P consists of the following rules:
EQUAL_SORT[A0](s(x0), s(x1)) → EQUAL_SORT[A0](x0, x1)
R is empty.
The set Q consists of the following terms:
le'(s(x0), 0)
le'(s(x0), s(x1))
le'(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
inc(s(x0))
inc(0)
minus(x0, 0)
minus(s(x0), s(x1))
le(0, x0)
quot(0, 0)
quot(s(x0), 0)
minus(0, s(x0))
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a0](0, 0)
equal_sort[a0](0, s(x0))
equal_sort[a0](s(x0), 0)
equal_sort[a0](s(x0), s(x1))
equal_sort[a32](witness_sort[a32], witness_sort[a32])
We have to consider all minimal (P,Q,R)-chains.
(57) 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].
le'(s(x0), 0)
le'(s(x0), s(x1))
le'(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
inc(s(x0))
inc(0)
minus(x0, 0)
minus(s(x0), s(x1))
le(0, x0)
quot(0, 0)
quot(s(x0), 0)
minus(0, s(x0))
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a0](0, 0)
equal_sort[a0](0, s(x0))
equal_sort[a0](s(x0), 0)
equal_sort[a0](s(x0), s(x1))
equal_sort[a32](witness_sort[a32], witness_sort[a32])
(58) Obligation:
Q DP problem:
The TRS P consists of the following rules:
EQUAL_SORT[A0](s(x0), s(x1)) → EQUAL_SORT[A0](x0, x1)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(59) 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:
- EQUAL_SORT[A0](s(x0), s(x1)) → EQUAL_SORT[A0](x0, x1)
The graph contains the following edges 1 > 1, 2 > 2
(60) TRUE
(61) Obligation:
Q DP problem:
The TRS P consists of the following rules:
MINUS(s(x45), s(y36)) → MINUS(x45, y36)
The TRS R consists of the following rules:
le'(s(x), 0) → true
le'(s(x5), s(y3)) → le'(x5, y3)
le'(0, y42) → false
le(s(x), 0) → false
le(s(x5), s(y3)) → le(x5, y3)
quot(0, s(y9)) → 0
quot(s(x18), s(y15)) → s(quot(minus(x18, y15), s(y15)))
inc(s(x25)) → s(inc(x25))
inc(0) → s(0)
minus(x38, 0) → x38
minus(s(x45), s(y36)) → minus(x45, y36)
le(0, y42) → true
quot(0, 0) → 0
quot(s(x2), 0) → 0
minus(0, s(x0)) → 0
equal_bool(true, false) → false
equal_bool(false, true) → false
equal_bool(true, true) → true
equal_bool(false, false) → true
and(true, x) → x
and(false, x) → false
or(true, x) → true
or(false, x) → x
not(false) → true
not(true) → false
isa_true(true) → true
isa_true(false) → false
isa_false(true) → false
isa_false(false) → true
equal_sort[a0](0, 0) → true
equal_sort[a0](0, s(x0)) → false
equal_sort[a0](s(x0), 0) → false
equal_sort[a0](s(x0), s(x1)) → equal_sort[a0](x0, x1)
equal_sort[a32](witness_sort[a32], witness_sort[a32]) → true
The set Q consists of the following terms:
le'(s(x0), 0)
le'(s(x0), s(x1))
le'(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
inc(s(x0))
inc(0)
minus(x0, 0)
minus(s(x0), s(x1))
le(0, x0)
quot(0, 0)
quot(s(x0), 0)
minus(0, s(x0))
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a0](0, 0)
equal_sort[a0](0, s(x0))
equal_sort[a0](s(x0), 0)
equal_sort[a0](s(x0), s(x1))
equal_sort[a32](witness_sort[a32], witness_sort[a32])
We have to consider all minimal (P,Q,R)-chains.
(62) 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.
(63) Obligation:
Q DP problem:
The TRS P consists of the following rules:
MINUS(s(x45), s(y36)) → MINUS(x45, y36)
R is empty.
The set Q consists of the following terms:
le'(s(x0), 0)
le'(s(x0), s(x1))
le'(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
inc(s(x0))
inc(0)
minus(x0, 0)
minus(s(x0), s(x1))
le(0, x0)
quot(0, 0)
quot(s(x0), 0)
minus(0, s(x0))
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a0](0, 0)
equal_sort[a0](0, s(x0))
equal_sort[a0](s(x0), 0)
equal_sort[a0](s(x0), s(x1))
equal_sort[a32](witness_sort[a32], witness_sort[a32])
We have to consider all minimal (P,Q,R)-chains.
(64) 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].
le'(s(x0), 0)
le'(s(x0), s(x1))
le'(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
inc(s(x0))
inc(0)
minus(x0, 0)
minus(s(x0), s(x1))
le(0, x0)
quot(0, 0)
quot(s(x0), 0)
minus(0, s(x0))
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a0](0, 0)
equal_sort[a0](0, s(x0))
equal_sort[a0](s(x0), 0)
equal_sort[a0](s(x0), s(x1))
equal_sort[a32](witness_sort[a32], witness_sort[a32])
(65) Obligation:
Q DP problem:
The TRS P consists of the following rules:
MINUS(s(x45), s(y36)) → MINUS(x45, y36)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(66) 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(x45), s(y36)) → MINUS(x45, y36)
The graph contains the following edges 1 > 1, 2 > 2
(67) TRUE
(68) Obligation:
Q DP problem:
The TRS P consists of the following rules:
INC(s(x25)) → INC(x25)
The TRS R consists of the following rules:
le'(s(x), 0) → true
le'(s(x5), s(y3)) → le'(x5, y3)
le'(0, y42) → false
le(s(x), 0) → false
le(s(x5), s(y3)) → le(x5, y3)
quot(0, s(y9)) → 0
quot(s(x18), s(y15)) → s(quot(minus(x18, y15), s(y15)))
inc(s(x25)) → s(inc(x25))
inc(0) → s(0)
minus(x38, 0) → x38
minus(s(x45), s(y36)) → minus(x45, y36)
le(0, y42) → true
quot(0, 0) → 0
quot(s(x2), 0) → 0
minus(0, s(x0)) → 0
equal_bool(true, false) → false
equal_bool(false, true) → false
equal_bool(true, true) → true
equal_bool(false, false) → true
and(true, x) → x
and(false, x) → false
or(true, x) → true
or(false, x) → x
not(false) → true
not(true) → false
isa_true(true) → true
isa_true(false) → false
isa_false(true) → false
isa_false(false) → true
equal_sort[a0](0, 0) → true
equal_sort[a0](0, s(x0)) → false
equal_sort[a0](s(x0), 0) → false
equal_sort[a0](s(x0), s(x1)) → equal_sort[a0](x0, x1)
equal_sort[a32](witness_sort[a32], witness_sort[a32]) → true
The set Q consists of the following terms:
le'(s(x0), 0)
le'(s(x0), s(x1))
le'(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
inc(s(x0))
inc(0)
minus(x0, 0)
minus(s(x0), s(x1))
le(0, x0)
quot(0, 0)
quot(s(x0), 0)
minus(0, s(x0))
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a0](0, 0)
equal_sort[a0](0, s(x0))
equal_sort[a0](s(x0), 0)
equal_sort[a0](s(x0), s(x1))
equal_sort[a32](witness_sort[a32], witness_sort[a32])
We have to consider all minimal (P,Q,R)-chains.
(69) 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.
(70) Obligation:
Q DP problem:
The TRS P consists of the following rules:
INC(s(x25)) → INC(x25)
R is empty.
The set Q consists of the following terms:
le'(s(x0), 0)
le'(s(x0), s(x1))
le'(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
inc(s(x0))
inc(0)
minus(x0, 0)
minus(s(x0), s(x1))
le(0, x0)
quot(0, 0)
quot(s(x0), 0)
minus(0, s(x0))
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a0](0, 0)
equal_sort[a0](0, s(x0))
equal_sort[a0](s(x0), 0)
equal_sort[a0](s(x0), s(x1))
equal_sort[a32](witness_sort[a32], witness_sort[a32])
We have to consider all minimal (P,Q,R)-chains.
(71) 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].
le'(s(x0), 0)
le'(s(x0), s(x1))
le'(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
inc(s(x0))
inc(0)
minus(x0, 0)
minus(s(x0), s(x1))
le(0, x0)
quot(0, 0)
quot(s(x0), 0)
minus(0, s(x0))
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a0](0, 0)
equal_sort[a0](0, s(x0))
equal_sort[a0](s(x0), 0)
equal_sort[a0](s(x0), s(x1))
equal_sort[a32](witness_sort[a32], witness_sort[a32])
(72) Obligation:
Q DP problem:
The TRS P consists of the following rules:
INC(s(x25)) → INC(x25)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(73) 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:
- INC(s(x25)) → INC(x25)
The graph contains the following edges 1 > 1
(74) TRUE
(75) Obligation:
Q DP problem:
The TRS P consists of the following rules:
QUOT(s(x18), s(y15)) → QUOT(minus(x18, y15), s(y15))
The TRS R consists of the following rules:
le'(s(x), 0) → true
le'(s(x5), s(y3)) → le'(x5, y3)
le'(0, y42) → false
le(s(x), 0) → false
le(s(x5), s(y3)) → le(x5, y3)
quot(0, s(y9)) → 0
quot(s(x18), s(y15)) → s(quot(minus(x18, y15), s(y15)))
inc(s(x25)) → s(inc(x25))
inc(0) → s(0)
minus(x38, 0) → x38
minus(s(x45), s(y36)) → minus(x45, y36)
le(0, y42) → true
quot(0, 0) → 0
quot(s(x2), 0) → 0
minus(0, s(x0)) → 0
equal_bool(true, false) → false
equal_bool(false, true) → false
equal_bool(true, true) → true
equal_bool(false, false) → true
and(true, x) → x
and(false, x) → false
or(true, x) → true
or(false, x) → x
not(false) → true
not(true) → false
isa_true(true) → true
isa_true(false) → false
isa_false(true) → false
isa_false(false) → true
equal_sort[a0](0, 0) → true
equal_sort[a0](0, s(x0)) → false
equal_sort[a0](s(x0), 0) → false
equal_sort[a0](s(x0), s(x1)) → equal_sort[a0](x0, x1)
equal_sort[a32](witness_sort[a32], witness_sort[a32]) → true
The set Q consists of the following terms:
le'(s(x0), 0)
le'(s(x0), s(x1))
le'(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
inc(s(x0))
inc(0)
minus(x0, 0)
minus(s(x0), s(x1))
le(0, x0)
quot(0, 0)
quot(s(x0), 0)
minus(0, s(x0))
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a0](0, 0)
equal_sort[a0](0, s(x0))
equal_sort[a0](s(x0), 0)
equal_sort[a0](s(x0), s(x1))
equal_sort[a32](witness_sort[a32], witness_sort[a32])
We have to consider all minimal (P,Q,R)-chains.
(76) 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.
(77) Obligation:
Q DP problem:
The TRS P consists of the following rules:
QUOT(s(x18), s(y15)) → QUOT(minus(x18, y15), s(y15))
The TRS R consists of the following rules:
minus(x38, 0) → x38
minus(s(x45), s(y36)) → minus(x45, y36)
minus(0, s(x0)) → 0
The set Q consists of the following terms:
le'(s(x0), 0)
le'(s(x0), s(x1))
le'(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
inc(s(x0))
inc(0)
minus(x0, 0)
minus(s(x0), s(x1))
le(0, x0)
quot(0, 0)
quot(s(x0), 0)
minus(0, s(x0))
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a0](0, 0)
equal_sort[a0](0, s(x0))
equal_sort[a0](s(x0), 0)
equal_sort[a0](s(x0), s(x1))
equal_sort[a32](witness_sort[a32], witness_sort[a32])
We have to consider all minimal (P,Q,R)-chains.
(78) 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].
le'(s(x0), 0)
le'(s(x0), s(x1))
le'(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
inc(s(x0))
inc(0)
le(0, x0)
quot(0, 0)
quot(s(x0), 0)
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a0](0, 0)
equal_sort[a0](0, s(x0))
equal_sort[a0](s(x0), 0)
equal_sort[a0](s(x0), s(x1))
equal_sort[a32](witness_sort[a32], witness_sort[a32])
(79) Obligation:
Q DP problem:
The TRS P consists of the following rules:
QUOT(s(x18), s(y15)) → QUOT(minus(x18, y15), s(y15))
The TRS R consists of the following rules:
minus(x38, 0) → x38
minus(s(x45), s(y36)) → minus(x45, y36)
minus(0, s(x0)) → 0
The set Q consists of the following terms:
minus(x0, 0)
minus(s(x0), s(x1))
minus(0, s(x0))
We have to consider all minimal (P,Q,R)-chains.
(80) QDPOrderProof (EQUIVALENT transformation)
We use the reduction pair processor [LPAR04].
The following pairs can be oriented strictly and are deleted.
QUOT(s(x18), s(y15)) → QUOT(minus(x18, y15), s(y15))
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:
POL(0) = 0
POL(QUOT(x1, x2)) = x1
POL(minus(x1, x2)) = x1
POL(s(x1)) = 1 + x1
The following usable rules [FROCOS05] were oriented:
minus(x38, 0) → x38
minus(s(x45), s(y36)) → minus(x45, y36)
minus(0, s(x0)) → 0
(81) Obligation:
Q DP problem:
P is empty.
The TRS R consists of the following rules:
minus(x38, 0) → x38
minus(s(x45), s(y36)) → minus(x45, y36)
minus(0, s(x0)) → 0
The set Q consists of the following terms:
minus(x0, 0)
minus(s(x0), s(x1))
minus(0, s(x0))
We have to consider all minimal (P,Q,R)-chains.
(82) PisEmptyProof (EQUIVALENT transformation)
The TRS P is empty. Hence, there is no (P,Q,R) chain.
(83) TRUE
(84) Obligation:
Q DP problem:
The TRS P consists of the following rules:
LE(s(x5), s(y3)) → LE(x5, y3)
The TRS R consists of the following rules:
le'(s(x), 0) → true
le'(s(x5), s(y3)) → le'(x5, y3)
le'(0, y42) → false
le(s(x), 0) → false
le(s(x5), s(y3)) → le(x5, y3)
quot(0, s(y9)) → 0
quot(s(x18), s(y15)) → s(quot(minus(x18, y15), s(y15)))
inc(s(x25)) → s(inc(x25))
inc(0) → s(0)
minus(x38, 0) → x38
minus(s(x45), s(y36)) → minus(x45, y36)
le(0, y42) → true
quot(0, 0) → 0
quot(s(x2), 0) → 0
minus(0, s(x0)) → 0
equal_bool(true, false) → false
equal_bool(false, true) → false
equal_bool(true, true) → true
equal_bool(false, false) → true
and(true, x) → x
and(false, x) → false
or(true, x) → true
or(false, x) → x
not(false) → true
not(true) → false
isa_true(true) → true
isa_true(false) → false
isa_false(true) → false
isa_false(false) → true
equal_sort[a0](0, 0) → true
equal_sort[a0](0, s(x0)) → false
equal_sort[a0](s(x0), 0) → false
equal_sort[a0](s(x0), s(x1)) → equal_sort[a0](x0, x1)
equal_sort[a32](witness_sort[a32], witness_sort[a32]) → true
The set Q consists of the following terms:
le'(s(x0), 0)
le'(s(x0), s(x1))
le'(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
inc(s(x0))
inc(0)
minus(x0, 0)
minus(s(x0), s(x1))
le(0, x0)
quot(0, 0)
quot(s(x0), 0)
minus(0, s(x0))
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a0](0, 0)
equal_sort[a0](0, s(x0))
equal_sort[a0](s(x0), 0)
equal_sort[a0](s(x0), s(x1))
equal_sort[a32](witness_sort[a32], witness_sort[a32])
We have to consider all minimal (P,Q,R)-chains.
(85) 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.
(86) Obligation:
Q DP problem:
The TRS P consists of the following rules:
LE(s(x5), s(y3)) → LE(x5, y3)
R is empty.
The set Q consists of the following terms:
le'(s(x0), 0)
le'(s(x0), s(x1))
le'(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
inc(s(x0))
inc(0)
minus(x0, 0)
minus(s(x0), s(x1))
le(0, x0)
quot(0, 0)
quot(s(x0), 0)
minus(0, s(x0))
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a0](0, 0)
equal_sort[a0](0, s(x0))
equal_sort[a0](s(x0), 0)
equal_sort[a0](s(x0), s(x1))
equal_sort[a32](witness_sort[a32], witness_sort[a32])
We have to consider all minimal (P,Q,R)-chains.
(87) 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].
le'(s(x0), 0)
le'(s(x0), s(x1))
le'(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
inc(s(x0))
inc(0)
minus(x0, 0)
minus(s(x0), s(x1))
le(0, x0)
quot(0, 0)
quot(s(x0), 0)
minus(0, s(x0))
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a0](0, 0)
equal_sort[a0](0, s(x0))
equal_sort[a0](s(x0), 0)
equal_sort[a0](s(x0), s(x1))
equal_sort[a32](witness_sort[a32], witness_sort[a32])
(88) Obligation:
Q DP problem:
The TRS P consists of the following rules:
LE(s(x5), s(y3)) → LE(x5, y3)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(89) 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:
- LE(s(x5), s(y3)) → LE(x5, y3)
The graph contains the following edges 1 > 1, 2 > 2
(90) TRUE
(91) Obligation:
Q DP problem:
The TRS P consists of the following rules:
LE'(s(x5), s(y3)) → LE'(x5, y3)
The TRS R consists of the following rules:
le'(s(x), 0) → true
le'(s(x5), s(y3)) → le'(x5, y3)
le'(0, y42) → false
le(s(x), 0) → false
le(s(x5), s(y3)) → le(x5, y3)
quot(0, s(y9)) → 0
quot(s(x18), s(y15)) → s(quot(minus(x18, y15), s(y15)))
inc(s(x25)) → s(inc(x25))
inc(0) → s(0)
minus(x38, 0) → x38
minus(s(x45), s(y36)) → minus(x45, y36)
le(0, y42) → true
quot(0, 0) → 0
quot(s(x2), 0) → 0
minus(0, s(x0)) → 0
equal_bool(true, false) → false
equal_bool(false, true) → false
equal_bool(true, true) → true
equal_bool(false, false) → true
and(true, x) → x
and(false, x) → false
or(true, x) → true
or(false, x) → x
not(false) → true
not(true) → false
isa_true(true) → true
isa_true(false) → false
isa_false(true) → false
isa_false(false) → true
equal_sort[a0](0, 0) → true
equal_sort[a0](0, s(x0)) → false
equal_sort[a0](s(x0), 0) → false
equal_sort[a0](s(x0), s(x1)) → equal_sort[a0](x0, x1)
equal_sort[a32](witness_sort[a32], witness_sort[a32]) → true
The set Q consists of the following terms:
le'(s(x0), 0)
le'(s(x0), s(x1))
le'(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
inc(s(x0))
inc(0)
minus(x0, 0)
minus(s(x0), s(x1))
le(0, x0)
quot(0, 0)
quot(s(x0), 0)
minus(0, s(x0))
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a0](0, 0)
equal_sort[a0](0, s(x0))
equal_sort[a0](s(x0), 0)
equal_sort[a0](s(x0), s(x1))
equal_sort[a32](witness_sort[a32], witness_sort[a32])
We have to consider all minimal (P,Q,R)-chains.
(92) 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.
(93) Obligation:
Q DP problem:
The TRS P consists of the following rules:
LE'(s(x5), s(y3)) → LE'(x5, y3)
R is empty.
The set Q consists of the following terms:
le'(s(x0), 0)
le'(s(x0), s(x1))
le'(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
inc(s(x0))
inc(0)
minus(x0, 0)
minus(s(x0), s(x1))
le(0, x0)
quot(0, 0)
quot(s(x0), 0)
minus(0, s(x0))
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a0](0, 0)
equal_sort[a0](0, s(x0))
equal_sort[a0](s(x0), 0)
equal_sort[a0](s(x0), s(x1))
equal_sort[a32](witness_sort[a32], witness_sort[a32])
We have to consider all minimal (P,Q,R)-chains.
(94) 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].
le'(s(x0), 0)
le'(s(x0), s(x1))
le'(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
inc(s(x0))
inc(0)
minus(x0, 0)
minus(s(x0), s(x1))
le(0, x0)
quot(0, 0)
quot(s(x0), 0)
minus(0, s(x0))
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a0](0, 0)
equal_sort[a0](0, s(x0))
equal_sort[a0](s(x0), 0)
equal_sort[a0](s(x0), s(x1))
equal_sort[a32](witness_sort[a32], witness_sort[a32])
(95) Obligation:
Q DP problem:
The TRS P consists of the following rules:
LE'(s(x5), s(y3)) → LE'(x5, y3)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(96) 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:
- LE'(s(x5), s(y3)) → LE'(x5, y3)
The graph contains the following edges 1 > 1, 2 > 2
(97) TRUE