(0) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
zero(0) → true
zero(s(x)) → false
id(0) → 0
id(s(x)) → s(id(x))
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
mod(x, y) → if_mod(zero(x), zero(y), le(y, x), id(x), id(y))
if_mod(true, b1, b2, x, y) → 0
if_mod(false, b1, b2, x, y) → if2(b1, b2, x, y)
if2(true, b2, x, y) → 0
if2(false, b2, x, y) → if3(b2, x, y)
if3(true, x, y) → mod(minus(x, y), s(y))
if3(false, x, y) → x
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:
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
zero(0) → true
zero(s(x)) → false
id(0) → 0
id(s(x)) → s(id(x))
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
mod(x, y) → if_mod(zero(x), zero(y), le(y, x), id(x), id(y))
if_mod(true, b1, b2, x, y) → 0
if_mod(false, b1, b2, x, y) → if2(b1, b2, x, y)
if2(true, b2, x, y) → 0
if2(false, b2, x, y) → if3(b2, x, y)
if3(true, x, y) → mod(minus(x, y), s(y))
if3(false, x, y) → x
The set Q consists of the following terms:
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
zero(0)
zero(s(x0))
id(0)
id(s(x0))
minus(x0, 0)
minus(s(x0), s(x1))
mod(x0, x1)
if_mod(true, x0, x1, x2, x3)
if_mod(false, x0, x1, x2, x3)
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
if3(true, x0, x1)
if3(false, 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:
LE(s(x), s(y)) → LE(x, y)
ID(s(x)) → ID(x)
MINUS(s(x), s(y)) → MINUS(x, y)
MOD(x, y) → IF_MOD(zero(x), zero(y), le(y, x), id(x), id(y))
MOD(x, y) → ZERO(x)
MOD(x, y) → ZERO(y)
MOD(x, y) → LE(y, x)
MOD(x, y) → ID(x)
MOD(x, y) → ID(y)
IF_MOD(false, b1, b2, x, y) → IF2(b1, b2, x, y)
IF2(false, b2, x, y) → IF3(b2, x, y)
IF3(true, x, y) → MOD(minus(x, y), s(y))
IF3(true, x, y) → MINUS(x, y)
The TRS R consists of the following rules:
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
zero(0) → true
zero(s(x)) → false
id(0) → 0
id(s(x)) → s(id(x))
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
mod(x, y) → if_mod(zero(x), zero(y), le(y, x), id(x), id(y))
if_mod(true, b1, b2, x, y) → 0
if_mod(false, b1, b2, x, y) → if2(b1, b2, x, y)
if2(true, b2, x, y) → 0
if2(false, b2, x, y) → if3(b2, x, y)
if3(true, x, y) → mod(minus(x, y), s(y))
if3(false, x, y) → x
The set Q consists of the following terms:
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
zero(0)
zero(s(x0))
id(0)
id(s(x0))
minus(x0, 0)
minus(s(x0), s(x1))
mod(x0, x1)
if_mod(true, x0, x1, x2, x3)
if_mod(false, x0, x1, x2, x3)
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
if3(true, x0, x1)
if3(false, 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 4 SCCs with 6 less nodes.
(6) Complex Obligation (AND)
(7) 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:
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
zero(0) → true
zero(s(x)) → false
id(0) → 0
id(s(x)) → s(id(x))
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
mod(x, y) → if_mod(zero(x), zero(y), le(y, x), id(x), id(y))
if_mod(true, b1, b2, x, y) → 0
if_mod(false, b1, b2, x, y) → if2(b1, b2, x, y)
if2(true, b2, x, y) → 0
if2(false, b2, x, y) → if3(b2, x, y)
if3(true, x, y) → mod(minus(x, y), s(y))
if3(false, x, y) → x
The set Q consists of the following terms:
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
zero(0)
zero(s(x0))
id(0)
id(s(x0))
minus(x0, 0)
minus(s(x0), s(x1))
mod(x0, x1)
if_mod(true, x0, x1, x2, x3)
if_mod(false, x0, x1, x2, x3)
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
if3(true, x0, x1)
if3(false, 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:
MINUS(s(x), s(y)) → MINUS(x, y)
R is empty.
The set Q consists of the following terms:
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
zero(0)
zero(s(x0))
id(0)
id(s(x0))
minus(x0, 0)
minus(s(x0), s(x1))
mod(x0, x1)
if_mod(true, x0, x1, x2, x3)
if_mod(false, x0, x1, x2, x3)
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
if3(true, x0, x1)
if3(false, 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].
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
zero(0)
zero(s(x0))
id(0)
id(s(x0))
minus(x0, 0)
minus(s(x0), s(x1))
mod(x0, x1)
if_mod(true, x0, x1, x2, x3)
if_mod(false, x0, x1, x2, x3)
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
if3(true, x0, x1)
if3(false, x0, x1)
(11) 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.
(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:
- MINUS(s(x), s(y)) → MINUS(x, y)
The graph contains the following edges 1 > 1, 2 > 2
(13) YES
(14) Obligation:
Q DP problem:
The TRS P consists of the following rules:
ID(s(x)) → ID(x)
The TRS R consists of the following rules:
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
zero(0) → true
zero(s(x)) → false
id(0) → 0
id(s(x)) → s(id(x))
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
mod(x, y) → if_mod(zero(x), zero(y), le(y, x), id(x), id(y))
if_mod(true, b1, b2, x, y) → 0
if_mod(false, b1, b2, x, y) → if2(b1, b2, x, y)
if2(true, b2, x, y) → 0
if2(false, b2, x, y) → if3(b2, x, y)
if3(true, x, y) → mod(minus(x, y), s(y))
if3(false, x, y) → x
The set Q consists of the following terms:
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
zero(0)
zero(s(x0))
id(0)
id(s(x0))
minus(x0, 0)
minus(s(x0), s(x1))
mod(x0, x1)
if_mod(true, x0, x1, x2, x3)
if_mod(false, x0, x1, x2, x3)
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
if3(true, x0, x1)
if3(false, 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:
ID(s(x)) → ID(x)
R is empty.
The set Q consists of the following terms:
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
zero(0)
zero(s(x0))
id(0)
id(s(x0))
minus(x0, 0)
minus(s(x0), s(x1))
mod(x0, x1)
if_mod(true, x0, x1, x2, x3)
if_mod(false, x0, x1, x2, x3)
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
if3(true, x0, x1)
if3(false, 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].
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
zero(0)
zero(s(x0))
id(0)
id(s(x0))
minus(x0, 0)
minus(s(x0), s(x1))
mod(x0, x1)
if_mod(true, x0, x1, x2, x3)
if_mod(false, x0, x1, x2, x3)
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
if3(true, x0, x1)
if3(false, x0, x1)
(18) Obligation:
Q DP problem:
The TRS P consists of the following rules:
ID(s(x)) → ID(x)
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:
- ID(s(x)) → ID(x)
The graph contains the following edges 1 > 1
(20) YES
(21) 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:
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
zero(0) → true
zero(s(x)) → false
id(0) → 0
id(s(x)) → s(id(x))
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
mod(x, y) → if_mod(zero(x), zero(y), le(y, x), id(x), id(y))
if_mod(true, b1, b2, x, y) → 0
if_mod(false, b1, b2, x, y) → if2(b1, b2, x, y)
if2(true, b2, x, y) → 0
if2(false, b2, x, y) → if3(b2, x, y)
if3(true, x, y) → mod(minus(x, y), s(y))
if3(false, x, y) → x
The set Q consists of the following terms:
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
zero(0)
zero(s(x0))
id(0)
id(s(x0))
minus(x0, 0)
minus(s(x0), s(x1))
mod(x0, x1)
if_mod(true, x0, x1, x2, x3)
if_mod(false, x0, x1, x2, x3)
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
if3(true, x0, x1)
if3(false, 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:
LE(s(x), s(y)) → LE(x, y)
R is empty.
The set Q consists of the following terms:
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
zero(0)
zero(s(x0))
id(0)
id(s(x0))
minus(x0, 0)
minus(s(x0), s(x1))
mod(x0, x1)
if_mod(true, x0, x1, x2, x3)
if_mod(false, x0, x1, x2, x3)
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
if3(true, x0, x1)
if3(false, 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].
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
zero(0)
zero(s(x0))
id(0)
id(s(x0))
minus(x0, 0)
minus(s(x0), s(x1))
mod(x0, x1)
if_mod(true, x0, x1, x2, x3)
if_mod(false, x0, x1, x2, x3)
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
if3(true, x0, x1)
if3(false, x0, x1)
(25) 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.
(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:
- LE(s(x), s(y)) → LE(x, y)
The graph contains the following edges 1 > 1, 2 > 2
(27) YES
(28) Obligation:
Q DP problem:
The TRS P consists of the following rules:
MOD(x, y) → IF_MOD(zero(x), zero(y), le(y, x), id(x), id(y))
IF_MOD(false, b1, b2, x, y) → IF2(b1, b2, x, y)
IF2(false, b2, x, y) → IF3(b2, x, y)
IF3(true, x, y) → MOD(minus(x, y), s(y))
The TRS R consists of the following rules:
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
zero(0) → true
zero(s(x)) → false
id(0) → 0
id(s(x)) → s(id(x))
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
mod(x, y) → if_mod(zero(x), zero(y), le(y, x), id(x), id(y))
if_mod(true, b1, b2, x, y) → 0
if_mod(false, b1, b2, x, y) → if2(b1, b2, x, y)
if2(true, b2, x, y) → 0
if2(false, b2, x, y) → if3(b2, x, y)
if3(true, x, y) → mod(minus(x, y), s(y))
if3(false, x, y) → x
The set Q consists of the following terms:
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
zero(0)
zero(s(x0))
id(0)
id(s(x0))
minus(x0, 0)
minus(s(x0), s(x1))
mod(x0, x1)
if_mod(true, x0, x1, x2, x3)
if_mod(false, x0, x1, x2, x3)
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
if3(true, x0, x1)
if3(false, 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:
MOD(x, y) → IF_MOD(zero(x), zero(y), le(y, x), id(x), id(y))
IF_MOD(false, b1, b2, x, y) → IF2(b1, b2, x, y)
IF2(false, b2, x, y) → IF3(b2, x, y)
IF3(true, x, y) → MOD(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)
zero(0) → true
zero(s(x)) → false
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
id(0) → 0
id(s(x)) → s(id(x))
The set Q consists of the following terms:
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
zero(0)
zero(s(x0))
id(0)
id(s(x0))
minus(x0, 0)
minus(s(x0), s(x1))
mod(x0, x1)
if_mod(true, x0, x1, x2, x3)
if_mod(false, x0, x1, x2, x3)
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
if3(true, x0, x1)
if3(false, 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].
mod(x0, x1)
if_mod(true, x0, x1, x2, x3)
if_mod(false, x0, x1, x2, x3)
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
if3(true, x0, x1)
if3(false, x0, x1)
(32) Obligation:
Q DP problem:
The TRS P consists of the following rules:
MOD(x, y) → IF_MOD(zero(x), zero(y), le(y, x), id(x), id(y))
IF_MOD(false, b1, b2, x, y) → IF2(b1, b2, x, y)
IF2(false, b2, x, y) → IF3(b2, x, y)
IF3(true, x, y) → MOD(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)
zero(0) → true
zero(s(x)) → false
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
id(0) → 0
id(s(x)) → s(id(x))
The set Q consists of the following terms:
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
zero(0)
zero(s(x0))
id(0)
id(s(x0))
minus(x0, 0)
minus(s(x0), s(x1))
We have to consider all minimal (P,Q,R)-chains.
(33) TransformationProof (EQUIVALENT transformation)
By narrowing [LPAR04] the rule
MOD(
x,
y) →
IF_MOD(
zero(
x),
zero(
y),
le(
y,
x),
id(
x),
id(
y)) at position [0] we obtained the following new rules [LPAR04]:
MOD(0, y1) → IF_MOD(true, zero(y1), le(y1, 0), id(0), id(y1)) → MOD(0, y1) → IF_MOD(true, zero(y1), le(y1, 0), id(0), id(y1))
MOD(s(x0), y1) → IF_MOD(false, zero(y1), le(y1, s(x0)), id(s(x0)), id(y1)) → MOD(s(x0), y1) → IF_MOD(false, zero(y1), le(y1, s(x0)), id(s(x0)), id(y1))
(34) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IF_MOD(false, b1, b2, x, y) → IF2(b1, b2, x, y)
IF2(false, b2, x, y) → IF3(b2, x, y)
IF3(true, x, y) → MOD(minus(x, y), s(y))
MOD(0, y1) → IF_MOD(true, zero(y1), le(y1, 0), id(0), id(y1))
MOD(s(x0), y1) → IF_MOD(false, zero(y1), le(y1, s(x0)), id(s(x0)), id(y1))
The TRS R consists of the following rules:
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
zero(0) → true
zero(s(x)) → false
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
id(0) → 0
id(s(x)) → s(id(x))
The set Q consists of the following terms:
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
zero(0)
zero(s(x0))
id(0)
id(s(x0))
minus(x0, 0)
minus(s(x0), s(x1))
We have to consider all minimal (P,Q,R)-chains.
(35) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.
(36) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IF2(false, b2, x, y) → IF3(b2, x, y)
IF3(true, x, y) → MOD(minus(x, y), s(y))
MOD(s(x0), y1) → IF_MOD(false, zero(y1), le(y1, s(x0)), id(s(x0)), id(y1))
IF_MOD(false, b1, b2, x, y) → IF2(b1, b2, x, y)
The TRS R consists of the following rules:
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
zero(0) → true
zero(s(x)) → false
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
id(0) → 0
id(s(x)) → s(id(x))
The set Q consists of the following terms:
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
zero(0)
zero(s(x0))
id(0)
id(s(x0))
minus(x0, 0)
minus(s(x0), s(x1))
We have to consider all minimal (P,Q,R)-chains.
(37) TransformationProof (EQUIVALENT transformation)
By rewriting [LPAR04] the rule
MOD(
s(
x0),
y1) →
IF_MOD(
false,
zero(
y1),
le(
y1,
s(
x0)),
id(
s(
x0)),
id(
y1)) at position [3] we obtained the following new rules [LPAR04]:
MOD(s(x0), y1) → IF_MOD(false, zero(y1), le(y1, s(x0)), s(id(x0)), id(y1)) → MOD(s(x0), y1) → IF_MOD(false, zero(y1), le(y1, s(x0)), s(id(x0)), id(y1))
(38) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IF2(false, b2, x, y) → IF3(b2, x, y)
IF3(true, x, y) → MOD(minus(x, y), s(y))
IF_MOD(false, b1, b2, x, y) → IF2(b1, b2, x, y)
MOD(s(x0), y1) → IF_MOD(false, zero(y1), le(y1, s(x0)), s(id(x0)), id(y1))
The TRS R consists of the following rules:
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
zero(0) → true
zero(s(x)) → false
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
id(0) → 0
id(s(x)) → s(id(x))
The set Q consists of the following terms:
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
zero(0)
zero(s(x0))
id(0)
id(s(x0))
minus(x0, 0)
minus(s(x0), s(x1))
We have to consider all minimal (P,Q,R)-chains.
(39) TransformationProof (EQUIVALENT transformation)
By narrowing [LPAR04] the rule
IF3(
true,
x,
y) →
MOD(
minus(
x,
y),
s(
y)) at position [0] we obtained the following new rules [LPAR04]:
IF3(true, x0, 0) → MOD(x0, s(0)) → IF3(true, x0, 0) → MOD(x0, s(0))
IF3(true, s(x0), s(x1)) → MOD(minus(x0, x1), s(s(x1))) → IF3(true, s(x0), s(x1)) → MOD(minus(x0, x1), s(s(x1)))
(40) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IF2(false, b2, x, y) → IF3(b2, x, y)
IF_MOD(false, b1, b2, x, y) → IF2(b1, b2, x, y)
MOD(s(x0), y1) → IF_MOD(false, zero(y1), le(y1, s(x0)), s(id(x0)), id(y1))
IF3(true, x0, 0) → MOD(x0, s(0))
IF3(true, s(x0), s(x1)) → MOD(minus(x0, x1), s(s(x1)))
The TRS R consists of the following rules:
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
zero(0) → true
zero(s(x)) → false
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
id(0) → 0
id(s(x)) → s(id(x))
The set Q consists of the following terms:
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
zero(0)
zero(s(x0))
id(0)
id(s(x0))
minus(x0, 0)
minus(s(x0), s(x1))
We have to consider all minimal (P,Q,R)-chains.
(41) TransformationProof (EQUIVALENT transformation)
By instantiating [LPAR04] the rule
IF_MOD(
false,
b1,
b2,
x,
y) →
IF2(
b1,
b2,
x,
y) we obtained the following new rules [LPAR04]:
IF_MOD(false, y_0, y_1, s(y_2), y_3) → IF2(y_0, y_1, s(y_2), y_3) → IF_MOD(false, y_0, y_1, s(y_2), y_3) → IF2(y_0, y_1, s(y_2), y_3)
(42) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IF2(false, b2, x, y) → IF3(b2, x, y)
MOD(s(x0), y1) → IF_MOD(false, zero(y1), le(y1, s(x0)), s(id(x0)), id(y1))
IF3(true, x0, 0) → MOD(x0, s(0))
IF3(true, s(x0), s(x1)) → MOD(minus(x0, x1), s(s(x1)))
IF_MOD(false, y_0, y_1, s(y_2), y_3) → IF2(y_0, y_1, s(y_2), y_3)
The TRS R consists of the following rules:
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
zero(0) → true
zero(s(x)) → false
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
id(0) → 0
id(s(x)) → s(id(x))
The set Q consists of the following terms:
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
zero(0)
zero(s(x0))
id(0)
id(s(x0))
minus(x0, 0)
minus(s(x0), s(x1))
We have to consider all minimal (P,Q,R)-chains.
(43) TransformationProof (EQUIVALENT transformation)
By instantiating [LPAR04] the rule
IF2(
false,
b2,
x,
y) →
IF3(
b2,
x,
y) we obtained the following new rules [LPAR04]:
IF2(false, z1, s(z2), z3) → IF3(z1, s(z2), z3) → IF2(false, z1, s(z2), z3) → IF3(z1, s(z2), z3)
(44) Obligation:
Q DP problem:
The TRS P consists of the following rules:
MOD(s(x0), y1) → IF_MOD(false, zero(y1), le(y1, s(x0)), s(id(x0)), id(y1))
IF3(true, x0, 0) → MOD(x0, s(0))
IF3(true, s(x0), s(x1)) → MOD(minus(x0, x1), s(s(x1)))
IF_MOD(false, y_0, y_1, s(y_2), y_3) → IF2(y_0, y_1, s(y_2), y_3)
IF2(false, z1, s(z2), z3) → IF3(z1, s(z2), z3)
The TRS R consists of the following rules:
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
zero(0) → true
zero(s(x)) → false
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
id(0) → 0
id(s(x)) → s(id(x))
The set Q consists of the following terms:
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
zero(0)
zero(s(x0))
id(0)
id(s(x0))
minus(x0, 0)
minus(s(x0), s(x1))
We have to consider all minimal (P,Q,R)-chains.
(45) TransformationProof (EQUIVALENT transformation)
By instantiating [LPAR04] the rule
MOD(
s(
x0),
y1) →
IF_MOD(
false,
zero(
y1),
le(
y1,
s(
x0)),
s(
id(
x0)),
id(
y1)) we obtained the following new rules [LPAR04]:
MOD(s(x0), s(0)) → IF_MOD(false, zero(s(0)), le(s(0), s(x0)), s(id(x0)), id(s(0))) → MOD(s(x0), s(0)) → IF_MOD(false, zero(s(0)), le(s(0), s(x0)), s(id(x0)), id(s(0)))
MOD(s(x0), s(s(z1))) → IF_MOD(false, zero(s(s(z1))), le(s(s(z1)), s(x0)), s(id(x0)), id(s(s(z1)))) → MOD(s(x0), s(s(z1))) → IF_MOD(false, zero(s(s(z1))), le(s(s(z1)), s(x0)), s(id(x0)), id(s(s(z1))))
(46) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IF3(true, x0, 0) → MOD(x0, s(0))
IF3(true, s(x0), s(x1)) → MOD(minus(x0, x1), s(s(x1)))
IF_MOD(false, y_0, y_1, s(y_2), y_3) → IF2(y_0, y_1, s(y_2), y_3)
IF2(false, z1, s(z2), z3) → IF3(z1, s(z2), z3)
MOD(s(x0), s(0)) → IF_MOD(false, zero(s(0)), le(s(0), s(x0)), s(id(x0)), id(s(0)))
MOD(s(x0), s(s(z1))) → IF_MOD(false, zero(s(s(z1))), le(s(s(z1)), s(x0)), s(id(x0)), id(s(s(z1))))
The TRS R consists of the following rules:
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
zero(0) → true
zero(s(x)) → false
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
id(0) → 0
id(s(x)) → s(id(x))
The set Q consists of the following terms:
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
zero(0)
zero(s(x0))
id(0)
id(s(x0))
minus(x0, 0)
minus(s(x0), s(x1))
We have to consider all minimal (P,Q,R)-chains.
(47) 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.
(48) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IF3(true, x0, 0) → MOD(x0, s(0))
IF3(true, s(x0), s(x1)) → MOD(minus(x0, x1), s(s(x1)))
IF_MOD(false, y_0, y_1, s(y_2), y_3) → IF2(y_0, y_1, s(y_2), y_3)
IF2(false, z1, s(z2), z3) → IF3(z1, s(z2), z3)
MOD(s(x0), s(0)) → IF_MOD(false, zero(s(0)), le(s(0), s(x0)), s(id(x0)), id(s(0)))
MOD(s(x0), s(s(z1))) → IF_MOD(false, zero(s(s(z1))), le(s(s(z1)), s(x0)), s(id(x0)), id(s(s(z1))))
The TRS R consists of the following rules:
zero(s(x)) → false
le(s(x), s(y)) → le(x, y)
id(0) → 0
id(s(x)) → s(id(x))
le(0, y) → true
le(s(x), 0) → false
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
The set Q consists of the following terms:
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
zero(0)
zero(s(x0))
id(0)
id(s(x0))
minus(x0, 0)
minus(s(x0), s(x1))
We have to consider all minimal (P,Q,R)-chains.
(49) TransformationProof (EQUIVALENT transformation)
By rewriting [LPAR04] the rule
MOD(
s(
x0),
s(
0)) →
IF_MOD(
false,
zero(
s(
0)),
le(
s(
0),
s(
x0)),
s(
id(
x0)),
id(
s(
0))) at position [1] we obtained the following new rules [LPAR04]:
MOD(s(x0), s(0)) → IF_MOD(false, false, le(s(0), s(x0)), s(id(x0)), id(s(0))) → MOD(s(x0), s(0)) → IF_MOD(false, false, le(s(0), s(x0)), s(id(x0)), id(s(0)))
(50) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IF3(true, x0, 0) → MOD(x0, s(0))
IF3(true, s(x0), s(x1)) → MOD(minus(x0, x1), s(s(x1)))
IF_MOD(false, y_0, y_1, s(y_2), y_3) → IF2(y_0, y_1, s(y_2), y_3)
IF2(false, z1, s(z2), z3) → IF3(z1, s(z2), z3)
MOD(s(x0), s(s(z1))) → IF_MOD(false, zero(s(s(z1))), le(s(s(z1)), s(x0)), s(id(x0)), id(s(s(z1))))
MOD(s(x0), s(0)) → IF_MOD(false, false, le(s(0), s(x0)), s(id(x0)), id(s(0)))
The TRS R consists of the following rules:
zero(s(x)) → false
le(s(x), s(y)) → le(x, y)
id(0) → 0
id(s(x)) → s(id(x))
le(0, y) → true
le(s(x), 0) → false
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
The set Q consists of the following terms:
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
zero(0)
zero(s(x0))
id(0)
id(s(x0))
minus(x0, 0)
minus(s(x0), s(x1))
We have to consider all minimal (P,Q,R)-chains.
(51) TransformationProof (EQUIVALENT transformation)
By rewriting [LPAR04] the rule
MOD(
s(
x0),
s(
s(
z1))) →
IF_MOD(
false,
zero(
s(
s(
z1))),
le(
s(
s(
z1)),
s(
x0)),
s(
id(
x0)),
id(
s(
s(
z1)))) at position [1] we obtained the following new rules [LPAR04]:
MOD(s(x0), s(s(z1))) → IF_MOD(false, false, le(s(s(z1)), s(x0)), s(id(x0)), id(s(s(z1)))) → MOD(s(x0), s(s(z1))) → IF_MOD(false, false, le(s(s(z1)), s(x0)), s(id(x0)), id(s(s(z1))))
(52) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IF3(true, x0, 0) → MOD(x0, s(0))
IF3(true, s(x0), s(x1)) → MOD(minus(x0, x1), s(s(x1)))
IF_MOD(false, y_0, y_1, s(y_2), y_3) → IF2(y_0, y_1, s(y_2), y_3)
IF2(false, z1, s(z2), z3) → IF3(z1, s(z2), z3)
MOD(s(x0), s(0)) → IF_MOD(false, false, le(s(0), s(x0)), s(id(x0)), id(s(0)))
MOD(s(x0), s(s(z1))) → IF_MOD(false, false, le(s(s(z1)), s(x0)), s(id(x0)), id(s(s(z1))))
The TRS R consists of the following rules:
zero(s(x)) → false
le(s(x), s(y)) → le(x, y)
id(0) → 0
id(s(x)) → s(id(x))
le(0, y) → true
le(s(x), 0) → false
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
The set Q consists of the following terms:
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
zero(0)
zero(s(x0))
id(0)
id(s(x0))
minus(x0, 0)
minus(s(x0), s(x1))
We have to consider all minimal (P,Q,R)-chains.
(53) 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.
(54) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IF3(true, x0, 0) → MOD(x0, s(0))
IF3(true, s(x0), s(x1)) → MOD(minus(x0, x1), s(s(x1)))
IF_MOD(false, y_0, y_1, s(y_2), y_3) → IF2(y_0, y_1, s(y_2), y_3)
IF2(false, z1, s(z2), z3) → IF3(z1, s(z2), z3)
MOD(s(x0), s(0)) → IF_MOD(false, false, le(s(0), s(x0)), s(id(x0)), id(s(0)))
MOD(s(x0), s(s(z1))) → IF_MOD(false, false, le(s(s(z1)), s(x0)), s(id(x0)), id(s(s(z1))))
The TRS R consists of the following rules:
le(s(x), s(y)) → le(x, y)
id(0) → 0
id(s(x)) → s(id(x))
le(0, y) → true
le(s(x), 0) → false
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
The set Q consists of the following terms:
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
zero(0)
zero(s(x0))
id(0)
id(s(x0))
minus(x0, 0)
minus(s(x0), s(x1))
We have to consider all minimal (P,Q,R)-chains.
(55) 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].
zero(0)
zero(s(x0))
(56) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IF3(true, x0, 0) → MOD(x0, s(0))
IF3(true, s(x0), s(x1)) → MOD(minus(x0, x1), s(s(x1)))
IF_MOD(false, y_0, y_1, s(y_2), y_3) → IF2(y_0, y_1, s(y_2), y_3)
IF2(false, z1, s(z2), z3) → IF3(z1, s(z2), z3)
MOD(s(x0), s(0)) → IF_MOD(false, false, le(s(0), s(x0)), s(id(x0)), id(s(0)))
MOD(s(x0), s(s(z1))) → IF_MOD(false, false, le(s(s(z1)), s(x0)), s(id(x0)), id(s(s(z1))))
The TRS R consists of the following rules:
le(s(x), s(y)) → le(x, y)
id(0) → 0
id(s(x)) → s(id(x))
le(0, y) → true
le(s(x), 0) → false
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
The set Q consists of the following terms:
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
id(0)
id(s(x0))
minus(x0, 0)
minus(s(x0), s(x1))
We have to consider all minimal (P,Q,R)-chains.
(57) TransformationProof (EQUIVALENT transformation)
By rewriting [LPAR04] the rule
MOD(
s(
x0),
s(
0)) →
IF_MOD(
false,
false,
le(
s(
0),
s(
x0)),
s(
id(
x0)),
id(
s(
0))) at position [2] we obtained the following new rules [LPAR04]:
MOD(s(x0), s(0)) → IF_MOD(false, false, le(0, x0), s(id(x0)), id(s(0))) → MOD(s(x0), s(0)) → IF_MOD(false, false, le(0, x0), s(id(x0)), id(s(0)))
(58) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IF3(true, x0, 0) → MOD(x0, s(0))
IF3(true, s(x0), s(x1)) → MOD(minus(x0, x1), s(s(x1)))
IF_MOD(false, y_0, y_1, s(y_2), y_3) → IF2(y_0, y_1, s(y_2), y_3)
IF2(false, z1, s(z2), z3) → IF3(z1, s(z2), z3)
MOD(s(x0), s(s(z1))) → IF_MOD(false, false, le(s(s(z1)), s(x0)), s(id(x0)), id(s(s(z1))))
MOD(s(x0), s(0)) → IF_MOD(false, false, le(0, x0), s(id(x0)), id(s(0)))
The TRS R consists of the following rules:
le(s(x), s(y)) → le(x, y)
id(0) → 0
id(s(x)) → s(id(x))
le(0, y) → true
le(s(x), 0) → false
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
The set Q consists of the following terms:
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
id(0)
id(s(x0))
minus(x0, 0)
minus(s(x0), s(x1))
We have to consider all minimal (P,Q,R)-chains.
(59) TransformationProof (EQUIVALENT transformation)
By rewriting [LPAR04] the rule
MOD(
s(
x0),
s(
s(
z1))) →
IF_MOD(
false,
false,
le(
s(
s(
z1)),
s(
x0)),
s(
id(
x0)),
id(
s(
s(
z1)))) at position [2] we obtained the following new rules [LPAR04]:
MOD(s(x0), s(s(z1))) → IF_MOD(false, false, le(s(z1), x0), s(id(x0)), id(s(s(z1)))) → MOD(s(x0), s(s(z1))) → IF_MOD(false, false, le(s(z1), x0), s(id(x0)), id(s(s(z1))))
(60) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IF3(true, x0, 0) → MOD(x0, s(0))
IF3(true, s(x0), s(x1)) → MOD(minus(x0, x1), s(s(x1)))
IF_MOD(false, y_0, y_1, s(y_2), y_3) → IF2(y_0, y_1, s(y_2), y_3)
IF2(false, z1, s(z2), z3) → IF3(z1, s(z2), z3)
MOD(s(x0), s(0)) → IF_MOD(false, false, le(0, x0), s(id(x0)), id(s(0)))
MOD(s(x0), s(s(z1))) → IF_MOD(false, false, le(s(z1), x0), s(id(x0)), id(s(s(z1))))
The TRS R consists of the following rules:
le(s(x), s(y)) → le(x, y)
id(0) → 0
id(s(x)) → s(id(x))
le(0, y) → true
le(s(x), 0) → false
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
The set Q consists of the following terms:
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
id(0)
id(s(x0))
minus(x0, 0)
minus(s(x0), s(x1))
We have to consider all minimal (P,Q,R)-chains.
(61) TransformationProof (EQUIVALENT transformation)
By rewriting [LPAR04] the rule
MOD(
s(
x0),
s(
0)) →
IF_MOD(
false,
false,
le(
0,
x0),
s(
id(
x0)),
id(
s(
0))) at position [2] we obtained the following new rules [LPAR04]:
MOD(s(x0), s(0)) → IF_MOD(false, false, true, s(id(x0)), id(s(0))) → MOD(s(x0), s(0)) → IF_MOD(false, false, true, s(id(x0)), id(s(0)))
(62) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IF3(true, x0, 0) → MOD(x0, s(0))
IF3(true, s(x0), s(x1)) → MOD(minus(x0, x1), s(s(x1)))
IF_MOD(false, y_0, y_1, s(y_2), y_3) → IF2(y_0, y_1, s(y_2), y_3)
IF2(false, z1, s(z2), z3) → IF3(z1, s(z2), z3)
MOD(s(x0), s(s(z1))) → IF_MOD(false, false, le(s(z1), x0), s(id(x0)), id(s(s(z1))))
MOD(s(x0), s(0)) → IF_MOD(false, false, true, s(id(x0)), id(s(0)))
The TRS R consists of the following rules:
le(s(x), s(y)) → le(x, y)
id(0) → 0
id(s(x)) → s(id(x))
le(0, y) → true
le(s(x), 0) → false
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
The set Q consists of the following terms:
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
id(0)
id(s(x0))
minus(x0, 0)
minus(s(x0), s(x1))
We have to consider all minimal (P,Q,R)-chains.
(63) TransformationProof (EQUIVALENT transformation)
By rewriting [LPAR04] the rule
MOD(
s(
x0),
s(
s(
z1))) →
IF_MOD(
false,
false,
le(
s(
z1),
x0),
s(
id(
x0)),
id(
s(
s(
z1)))) at position [4] we obtained the following new rules [LPAR04]:
MOD(s(x0), s(s(z1))) → IF_MOD(false, false, le(s(z1), x0), s(id(x0)), s(id(s(z1)))) → MOD(s(x0), s(s(z1))) → IF_MOD(false, false, le(s(z1), x0), s(id(x0)), s(id(s(z1))))
(64) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IF3(true, x0, 0) → MOD(x0, s(0))
IF3(true, s(x0), s(x1)) → MOD(minus(x0, x1), s(s(x1)))
IF_MOD(false, y_0, y_1, s(y_2), y_3) → IF2(y_0, y_1, s(y_2), y_3)
IF2(false, z1, s(z2), z3) → IF3(z1, s(z2), z3)
MOD(s(x0), s(0)) → IF_MOD(false, false, true, s(id(x0)), id(s(0)))
MOD(s(x0), s(s(z1))) → IF_MOD(false, false, le(s(z1), x0), s(id(x0)), s(id(s(z1))))
The TRS R consists of the following rules:
le(s(x), s(y)) → le(x, y)
id(0) → 0
id(s(x)) → s(id(x))
le(0, y) → true
le(s(x), 0) → false
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
The set Q consists of the following terms:
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
id(0)
id(s(x0))
minus(x0, 0)
minus(s(x0), s(x1))
We have to consider all minimal (P,Q,R)-chains.
(65) TransformationProof (EQUIVALENT transformation)
By rewriting [LPAR04] the rule
MOD(
s(
x0),
s(
0)) →
IF_MOD(
false,
false,
true,
s(
id(
x0)),
id(
s(
0))) at position [4] we obtained the following new rules [LPAR04]:
MOD(s(x0), s(0)) → IF_MOD(false, false, true, s(id(x0)), s(id(0))) → MOD(s(x0), s(0)) → IF_MOD(false, false, true, s(id(x0)), s(id(0)))
(66) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IF3(true, x0, 0) → MOD(x0, s(0))
IF3(true, s(x0), s(x1)) → MOD(minus(x0, x1), s(s(x1)))
IF_MOD(false, y_0, y_1, s(y_2), y_3) → IF2(y_0, y_1, s(y_2), y_3)
IF2(false, z1, s(z2), z3) → IF3(z1, s(z2), z3)
MOD(s(x0), s(s(z1))) → IF_MOD(false, false, le(s(z1), x0), s(id(x0)), s(id(s(z1))))
MOD(s(x0), s(0)) → IF_MOD(false, false, true, s(id(x0)), s(id(0)))
The TRS R consists of the following rules:
le(s(x), s(y)) → le(x, y)
id(0) → 0
id(s(x)) → s(id(x))
le(0, y) → true
le(s(x), 0) → false
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
The set Q consists of the following terms:
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
id(0)
id(s(x0))
minus(x0, 0)
minus(s(x0), s(x1))
We have to consider all minimal (P,Q,R)-chains.
(67) TransformationProof (EQUIVALENT transformation)
By rewriting [LPAR04] the rule
MOD(
s(
x0),
s(
s(
z1))) →
IF_MOD(
false,
false,
le(
s(
z1),
x0),
s(
id(
x0)),
s(
id(
s(
z1)))) at position [4,0] we obtained the following new rules [LPAR04]:
MOD(s(x0), s(s(z1))) → IF_MOD(false, false, le(s(z1), x0), s(id(x0)), s(s(id(z1)))) → MOD(s(x0), s(s(z1))) → IF_MOD(false, false, le(s(z1), x0), s(id(x0)), s(s(id(z1))))
(68) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IF3(true, x0, 0) → MOD(x0, s(0))
IF3(true, s(x0), s(x1)) → MOD(minus(x0, x1), s(s(x1)))
IF_MOD(false, y_0, y_1, s(y_2), y_3) → IF2(y_0, y_1, s(y_2), y_3)
IF2(false, z1, s(z2), z3) → IF3(z1, s(z2), z3)
MOD(s(x0), s(0)) → IF_MOD(false, false, true, s(id(x0)), s(id(0)))
MOD(s(x0), s(s(z1))) → IF_MOD(false, false, le(s(z1), x0), s(id(x0)), s(s(id(z1))))
The TRS R consists of the following rules:
le(s(x), s(y)) → le(x, y)
id(0) → 0
id(s(x)) → s(id(x))
le(0, y) → true
le(s(x), 0) → false
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
The set Q consists of the following terms:
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
id(0)
id(s(x0))
minus(x0, 0)
minus(s(x0), s(x1))
We have to consider all minimal (P,Q,R)-chains.
(69) TransformationProof (EQUIVALENT transformation)
By rewriting [LPAR04] the rule
MOD(
s(
x0),
s(
0)) →
IF_MOD(
false,
false,
true,
s(
id(
x0)),
s(
id(
0))) at position [4,0] we obtained the following new rules [LPAR04]:
MOD(s(x0), s(0)) → IF_MOD(false, false, true, s(id(x0)), s(0)) → MOD(s(x0), s(0)) → IF_MOD(false, false, true, s(id(x0)), s(0))
(70) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IF3(true, x0, 0) → MOD(x0, s(0))
IF3(true, s(x0), s(x1)) → MOD(minus(x0, x1), s(s(x1)))
IF_MOD(false, y_0, y_1, s(y_2), y_3) → IF2(y_0, y_1, s(y_2), y_3)
IF2(false, z1, s(z2), z3) → IF3(z1, s(z2), z3)
MOD(s(x0), s(s(z1))) → IF_MOD(false, false, le(s(z1), x0), s(id(x0)), s(s(id(z1))))
MOD(s(x0), s(0)) → IF_MOD(false, false, true, s(id(x0)), s(0))
The TRS R consists of the following rules:
le(s(x), s(y)) → le(x, y)
id(0) → 0
id(s(x)) → s(id(x))
le(0, y) → true
le(s(x), 0) → false
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
The set Q consists of the following terms:
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
id(0)
id(s(x0))
minus(x0, 0)
minus(s(x0), s(x1))
We have to consider all minimal (P,Q,R)-chains.
(71) TransformationProof (EQUIVALENT transformation)
By instantiating [LPAR04] the rule
IF3(
true,
x0,
0) →
MOD(
x0,
s(
0)) we obtained the following new rules [LPAR04]:
IF3(true, s(z1), 0) → MOD(s(z1), s(0)) → IF3(true, s(z1), 0) → MOD(s(z1), s(0))
(72) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IF3(true, s(x0), s(x1)) → MOD(minus(x0, x1), s(s(x1)))
IF_MOD(false, y_0, y_1, s(y_2), y_3) → IF2(y_0, y_1, s(y_2), y_3)
IF2(false, z1, s(z2), z3) → IF3(z1, s(z2), z3)
MOD(s(x0), s(s(z1))) → IF_MOD(false, false, le(s(z1), x0), s(id(x0)), s(s(id(z1))))
MOD(s(x0), s(0)) → IF_MOD(false, false, true, s(id(x0)), s(0))
IF3(true, s(z1), 0) → MOD(s(z1), s(0))
The TRS R consists of the following rules:
le(s(x), s(y)) → le(x, y)
id(0) → 0
id(s(x)) → s(id(x))
le(0, y) → true
le(s(x), 0) → false
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
The set Q consists of the following terms:
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
id(0)
id(s(x0))
minus(x0, 0)
minus(s(x0), s(x1))
We have to consider all minimal (P,Q,R)-chains.
(73) TransformationProof (EQUIVALENT transformation)
By instantiating [LPAR04] the rule
IF_MOD(
false,
y_0,
y_1,
s(
y_2),
y_3) →
IF2(
y_0,
y_1,
s(
y_2),
y_3) we obtained the following new rules [LPAR04]:
IF_MOD(false, false, y_0, s(y_1), s(s(y_2))) → IF2(false, y_0, s(y_1), s(s(y_2))) → IF_MOD(false, false, y_0, s(y_1), s(s(y_2))) → IF2(false, y_0, s(y_1), s(s(y_2)))
IF_MOD(false, false, true, s(y_0), s(0)) → IF2(false, true, s(y_0), s(0)) → IF_MOD(false, false, true, s(y_0), s(0)) → IF2(false, true, s(y_0), s(0))
(74) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IF3(true, s(x0), s(x1)) → MOD(minus(x0, x1), s(s(x1)))
IF2(false, z1, s(z2), z3) → IF3(z1, s(z2), z3)
MOD(s(x0), s(s(z1))) → IF_MOD(false, false, le(s(z1), x0), s(id(x0)), s(s(id(z1))))
MOD(s(x0), s(0)) → IF_MOD(false, false, true, s(id(x0)), s(0))
IF3(true, s(z1), 0) → MOD(s(z1), s(0))
IF_MOD(false, false, y_0, s(y_1), s(s(y_2))) → IF2(false, y_0, s(y_1), s(s(y_2)))
IF_MOD(false, false, true, s(y_0), s(0)) → IF2(false, true, s(y_0), s(0))
The TRS R consists of the following rules:
le(s(x), s(y)) → le(x, y)
id(0) → 0
id(s(x)) → s(id(x))
le(0, y) → true
le(s(x), 0) → false
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
The set Q consists of the following terms:
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
id(0)
id(s(x0))
minus(x0, 0)
minus(s(x0), s(x1))
We have to consider all minimal (P,Q,R)-chains.
(75) TransformationProof (EQUIVALENT transformation)
By instantiating [LPAR04] the rule
IF2(
false,
z1,
s(
z2),
z3) →
IF3(
z1,
s(
z2),
z3) we obtained the following new rules [LPAR04]:
IF2(false, z0, s(z1), s(s(z2))) → IF3(z0, s(z1), s(s(z2))) → IF2(false, z0, s(z1), s(s(z2))) → IF3(z0, s(z1), s(s(z2)))
IF2(false, true, s(z0), s(0)) → IF3(true, s(z0), s(0)) → IF2(false, true, s(z0), s(0)) → IF3(true, s(z0), s(0))
(76) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IF3(true, s(x0), s(x1)) → MOD(minus(x0, x1), s(s(x1)))
MOD(s(x0), s(s(z1))) → IF_MOD(false, false, le(s(z1), x0), s(id(x0)), s(s(id(z1))))
MOD(s(x0), s(0)) → IF_MOD(false, false, true, s(id(x0)), s(0))
IF3(true, s(z1), 0) → MOD(s(z1), s(0))
IF_MOD(false, false, y_0, s(y_1), s(s(y_2))) → IF2(false, y_0, s(y_1), s(s(y_2)))
IF_MOD(false, false, true, s(y_0), s(0)) → IF2(false, true, s(y_0), s(0))
IF2(false, z0, s(z1), s(s(z2))) → IF3(z0, s(z1), s(s(z2)))
IF2(false, true, s(z0), s(0)) → IF3(true, s(z0), s(0))
The TRS R consists of the following rules:
le(s(x), s(y)) → le(x, y)
id(0) → 0
id(s(x)) → s(id(x))
le(0, y) → true
le(s(x), 0) → false
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
The set Q consists of the following terms:
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
id(0)
id(s(x0))
minus(x0, 0)
minus(s(x0), s(x1))
We have to consider all minimal (P,Q,R)-chains.
(77) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 4 less nodes.
(78) Obligation:
Q DP problem:
The TRS P consists of the following rules:
MOD(s(x0), s(s(z1))) → IF_MOD(false, false, le(s(z1), x0), s(id(x0)), s(s(id(z1))))
IF_MOD(false, false, y_0, s(y_1), s(s(y_2))) → IF2(false, y_0, s(y_1), s(s(y_2)))
IF2(false, z0, s(z1), s(s(z2))) → IF3(z0, s(z1), s(s(z2)))
IF3(true, s(x0), s(x1)) → MOD(minus(x0, x1), s(s(x1)))
The TRS R consists of the following rules:
le(s(x), s(y)) → le(x, y)
id(0) → 0
id(s(x)) → s(id(x))
le(0, y) → true
le(s(x), 0) → false
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
The set Q consists of the following terms:
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
id(0)
id(s(x0))
minus(x0, 0)
minus(s(x0), s(x1))
We have to consider all minimal (P,Q,R)-chains.
(79) TransformationProof (EQUIVALENT transformation)
By instantiating [LPAR04] the rule
IF3(
true,
s(
x0),
s(
x1)) →
MOD(
minus(
x0,
x1),
s(
s(
x1))) we obtained the following new rules [LPAR04]:
IF3(true, s(z1), s(s(z2))) → MOD(minus(z1, s(z2)), s(s(s(z2)))) → IF3(true, s(z1), s(s(z2))) → MOD(minus(z1, s(z2)), s(s(s(z2))))
(80) Obligation:
Q DP problem:
The TRS P consists of the following rules:
MOD(s(x0), s(s(z1))) → IF_MOD(false, false, le(s(z1), x0), s(id(x0)), s(s(id(z1))))
IF_MOD(false, false, y_0, s(y_1), s(s(y_2))) → IF2(false, y_0, s(y_1), s(s(y_2)))
IF2(false, z0, s(z1), s(s(z2))) → IF3(z0, s(z1), s(s(z2)))
IF3(true, s(z1), s(s(z2))) → MOD(minus(z1, s(z2)), s(s(s(z2))))
The TRS R consists of the following rules:
le(s(x), s(y)) → le(x, y)
id(0) → 0
id(s(x)) → s(id(x))
le(0, y) → true
le(s(x), 0) → false
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
The set Q consists of the following terms:
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
id(0)
id(s(x0))
minus(x0, 0)
minus(s(x0), s(x1))
We have to consider all minimal (P,Q,R)-chains.
(81) TransformationProof (EQUIVALENT transformation)
By instantiating [LPAR04] the rule
MOD(
s(
x0),
s(
s(
z1))) →
IF_MOD(
false,
false,
le(
s(
z1),
x0),
s(
id(
x0)),
s(
s(
id(
z1)))) we obtained the following new rules [LPAR04]:
MOD(s(x0), s(s(s(z1)))) → IF_MOD(false, false, le(s(s(z1)), x0), s(id(x0)), s(s(id(s(z1))))) → MOD(s(x0), s(s(s(z1)))) → IF_MOD(false, false, le(s(s(z1)), x0), s(id(x0)), s(s(id(s(z1)))))
(82) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IF_MOD(false, false, y_0, s(y_1), s(s(y_2))) → IF2(false, y_0, s(y_1), s(s(y_2)))
IF2(false, z0, s(z1), s(s(z2))) → IF3(z0, s(z1), s(s(z2)))
IF3(true, s(z1), s(s(z2))) → MOD(minus(z1, s(z2)), s(s(s(z2))))
MOD(s(x0), s(s(s(z1)))) → IF_MOD(false, false, le(s(s(z1)), x0), s(id(x0)), s(s(id(s(z1)))))
The TRS R consists of the following rules:
le(s(x), s(y)) → le(x, y)
id(0) → 0
id(s(x)) → s(id(x))
le(0, y) → true
le(s(x), 0) → false
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
The set Q consists of the following terms:
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
id(0)
id(s(x0))
minus(x0, 0)
minus(s(x0), s(x1))
We have to consider all minimal (P,Q,R)-chains.
(83) TransformationProof (EQUIVALENT transformation)
By rewriting [LPAR04] the rule
MOD(
s(
x0),
s(
s(
s(
z1)))) →
IF_MOD(
false,
false,
le(
s(
s(
z1)),
x0),
s(
id(
x0)),
s(
s(
id(
s(
z1))))) at position [4,0,0] we obtained the following new rules [LPAR04]:
MOD(s(x0), s(s(s(z1)))) → IF_MOD(false, false, le(s(s(z1)), x0), s(id(x0)), s(s(s(id(z1))))) → MOD(s(x0), s(s(s(z1)))) → IF_MOD(false, false, le(s(s(z1)), x0), s(id(x0)), s(s(s(id(z1)))))
(84) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IF_MOD(false, false, y_0, s(y_1), s(s(y_2))) → IF2(false, y_0, s(y_1), s(s(y_2)))
IF2(false, z0, s(z1), s(s(z2))) → IF3(z0, s(z1), s(s(z2)))
IF3(true, s(z1), s(s(z2))) → MOD(minus(z1, s(z2)), s(s(s(z2))))
MOD(s(x0), s(s(s(z1)))) → IF_MOD(false, false, le(s(s(z1)), x0), s(id(x0)), s(s(s(id(z1)))))
The TRS R consists of the following rules:
le(s(x), s(y)) → le(x, y)
id(0) → 0
id(s(x)) → s(id(x))
le(0, y) → true
le(s(x), 0) → false
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
The set Q consists of the following terms:
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
id(0)
id(s(x0))
minus(x0, 0)
minus(s(x0), s(x1))
We have to consider all minimal (P,Q,R)-chains.
(85) TransformationProof (EQUIVALENT transformation)
By forward instantiating [JAR06] the rule
IF2(
false,
z0,
s(
z1),
s(
s(
z2))) →
IF3(
z0,
s(
z1),
s(
s(
z2))) we obtained the following new rules [LPAR04]:
IF2(false, true, s(x1), s(s(x2))) → IF3(true, s(x1), s(s(x2))) → IF2(false, true, s(x1), s(s(x2))) → IF3(true, s(x1), s(s(x2)))
(86) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IF_MOD(false, false, y_0, s(y_1), s(s(y_2))) → IF2(false, y_0, s(y_1), s(s(y_2)))
IF3(true, s(z1), s(s(z2))) → MOD(minus(z1, s(z2)), s(s(s(z2))))
MOD(s(x0), s(s(s(z1)))) → IF_MOD(false, false, le(s(s(z1)), x0), s(id(x0)), s(s(s(id(z1)))))
IF2(false, true, s(x1), s(s(x2))) → IF3(true, s(x1), s(s(x2)))
The TRS R consists of the following rules:
le(s(x), s(y)) → le(x, y)
id(0) → 0
id(s(x)) → s(id(x))
le(0, y) → true
le(s(x), 0) → false
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
The set Q consists of the following terms:
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
id(0)
id(s(x0))
minus(x0, 0)
minus(s(x0), s(x1))
We have to consider all minimal (P,Q,R)-chains.
(87) TransformationProof (EQUIVALENT transformation)
By forward instantiating [JAR06] the rule
IF_MOD(
false,
false,
y_0,
s(
y_1),
s(
s(
y_2))) →
IF2(
false,
y_0,
s(
y_1),
s(
s(
y_2))) we obtained the following new rules [LPAR04]:
IF_MOD(false, false, true, s(x1), s(s(x2))) → IF2(false, true, s(x1), s(s(x2))) → IF_MOD(false, false, true, s(x1), s(s(x2))) → IF2(false, true, s(x1), s(s(x2)))
(88) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IF3(true, s(z1), s(s(z2))) → MOD(minus(z1, s(z2)), s(s(s(z2))))
MOD(s(x0), s(s(s(z1)))) → IF_MOD(false, false, le(s(s(z1)), x0), s(id(x0)), s(s(s(id(z1)))))
IF2(false, true, s(x1), s(s(x2))) → IF3(true, s(x1), s(s(x2)))
IF_MOD(false, false, true, s(x1), s(s(x2))) → IF2(false, true, s(x1), s(s(x2)))
The TRS R consists of the following rules:
le(s(x), s(y)) → le(x, y)
id(0) → 0
id(s(x)) → s(id(x))
le(0, y) → true
le(s(x), 0) → false
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
The set Q consists of the following terms:
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
id(0)
id(s(x0))
minus(x0, 0)
minus(s(x0), s(x1))
We have to consider all minimal (P,Q,R)-chains.
(89) TransformationProof (EQUIVALENT transformation)
By narrowing [LPAR04] the rule
MOD(
s(
x0),
s(
s(
s(
z1)))) →
IF_MOD(
false,
false,
le(
s(
s(
z1)),
x0),
s(
id(
x0)),
s(
s(
s(
id(
z1))))) at position [2] we obtained the following new rules [LPAR04]:
MOD(s(s(x1)), s(s(s(y1)))) → IF_MOD(false, false, le(s(y1), x1), s(id(s(x1))), s(s(s(id(y1))))) → MOD(s(s(x1)), s(s(s(y1)))) → IF_MOD(false, false, le(s(y1), x1), s(id(s(x1))), s(s(s(id(y1)))))
MOD(s(0), s(s(s(y1)))) → IF_MOD(false, false, false, s(id(0)), s(s(s(id(y1))))) → MOD(s(0), s(s(s(y1)))) → IF_MOD(false, false, false, s(id(0)), s(s(s(id(y1)))))
(90) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IF3(true, s(z1), s(s(z2))) → MOD(minus(z1, s(z2)), s(s(s(z2))))
IF2(false, true, s(x1), s(s(x2))) → IF3(true, s(x1), s(s(x2)))
IF_MOD(false, false, true, s(x1), s(s(x2))) → IF2(false, true, s(x1), s(s(x2)))
MOD(s(s(x1)), s(s(s(y1)))) → IF_MOD(false, false, le(s(y1), x1), s(id(s(x1))), s(s(s(id(y1)))))
MOD(s(0), s(s(s(y1)))) → IF_MOD(false, false, false, s(id(0)), s(s(s(id(y1)))))
The TRS R consists of the following rules:
le(s(x), s(y)) → le(x, y)
id(0) → 0
id(s(x)) → s(id(x))
le(0, y) → true
le(s(x), 0) → false
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
The set Q consists of the following terms:
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
id(0)
id(s(x0))
minus(x0, 0)
minus(s(x0), s(x1))
We have to consider all minimal (P,Q,R)-chains.
(91) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.
(92) Obligation:
Q DP problem:
The TRS P consists of the following rules:
MOD(s(s(x1)), s(s(s(y1)))) → IF_MOD(false, false, le(s(y1), x1), s(id(s(x1))), s(s(s(id(y1)))))
IF_MOD(false, false, true, s(x1), s(s(x2))) → IF2(false, true, s(x1), s(s(x2)))
IF2(false, true, s(x1), s(s(x2))) → IF3(true, s(x1), s(s(x2)))
IF3(true, s(z1), s(s(z2))) → MOD(minus(z1, s(z2)), s(s(s(z2))))
The TRS R consists of the following rules:
le(s(x), s(y)) → le(x, y)
id(0) → 0
id(s(x)) → s(id(x))
le(0, y) → true
le(s(x), 0) → false
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
The set Q consists of the following terms:
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
id(0)
id(s(x0))
minus(x0, 0)
minus(s(x0), s(x1))
We have to consider all minimal (P,Q,R)-chains.
(93) TransformationProof (EQUIVALENT transformation)
By rewriting [LPAR04] the rule
MOD(
s(
s(
x1)),
s(
s(
s(
y1)))) →
IF_MOD(
false,
false,
le(
s(
y1),
x1),
s(
id(
s(
x1))),
s(
s(
s(
id(
y1))))) at position [3,0] we obtained the following new rules [LPAR04]:
MOD(s(s(x1)), s(s(s(y1)))) → IF_MOD(false, false, le(s(y1), x1), s(s(id(x1))), s(s(s(id(y1))))) → MOD(s(s(x1)), s(s(s(y1)))) → IF_MOD(false, false, le(s(y1), x1), s(s(id(x1))), s(s(s(id(y1)))))
(94) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IF_MOD(false, false, true, s(x1), s(s(x2))) → IF2(false, true, s(x1), s(s(x2)))
IF2(false, true, s(x1), s(s(x2))) → IF3(true, s(x1), s(s(x2)))
IF3(true, s(z1), s(s(z2))) → MOD(minus(z1, s(z2)), s(s(s(z2))))
MOD(s(s(x1)), s(s(s(y1)))) → IF_MOD(false, false, le(s(y1), x1), s(s(id(x1))), s(s(s(id(y1)))))
The TRS R consists of the following rules:
le(s(x), s(y)) → le(x, y)
id(0) → 0
id(s(x)) → s(id(x))
le(0, y) → true
le(s(x), 0) → false
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
The set Q consists of the following terms:
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
id(0)
id(s(x0))
minus(x0, 0)
minus(s(x0), s(x1))
We have to consider all minimal (P,Q,R)-chains.
(95) QDPOrderProof (EQUIVALENT transformation)
We use the reduction pair processor [LPAR04,JAR06].
The following pairs can be oriented strictly and are deleted.
IF2(false, true, s(x1), s(s(x2))) → IF3(true, s(x1), s(s(x2)))
IF3(true, s(z1), s(s(z2))) → MOD(minus(z1, s(z2)), s(s(s(z2))))
MOD(s(s(x1)), s(s(s(y1)))) → IF_MOD(false, false, le(s(y1), x1), s(s(id(x1))), s(s(s(id(y1)))))
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial Order [NEGPOLO,POLO] with Interpretation:
| POL( MOD(x1, x2) ) = 2x1 + 1 |
| POL( minus(x1, x2) ) = x1 |
| POL( IF_MOD(x1, ..., x5) ) = max{0, x2 + x3 + 2x4 - 2} |
| POL( IF2(x1, ..., x4) ) = max{0, x2 + 2x3 - 2} |
| POL( IF3(x1, ..., x3) ) = max{0, 2x2 - 2} |
The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:
minus(s(x), s(y)) → minus(x, y)
le(s(x), s(y)) → le(x, y)
le(s(x), 0) → false
id(0) → 0
id(s(x)) → s(id(x))
le(0, y) → true
minus(x, 0) → x
(96) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IF_MOD(false, false, true, s(x1), s(s(x2))) → IF2(false, true, s(x1), s(s(x2)))
The TRS R consists of the following rules:
le(s(x), s(y)) → le(x, y)
id(0) → 0
id(s(x)) → s(id(x))
le(0, y) → true
le(s(x), 0) → false
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
The set Q consists of the following terms:
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
id(0)
id(s(x0))
minus(x0, 0)
minus(s(x0), s(x1))
We have to consider all minimal (P,Q,R)-chains.
(97) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 1 less node.
(98) TRUE