(0) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
empty(nil) → true
empty(cons(x, y)) → false
tail(nil) → nil
tail(cons(x, y)) → y
head(cons(x, y)) → x
zero(0) → true
zero(s(x)) → false
p(0) → 0
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
intlist(x) → if_intlist(empty(x), x)
if_intlist(true, x) → nil
if_intlist(false, x) → cons(s(head(x)), intlist(tail(x)))
int(x, y) → if_int(zero(x), zero(y), x, y)
if_int(true, b, x, y) → if1(b, x, y)
if_int(false, b, x, y) → if2(b, x, y)
if1(true, x, y) → cons(0, nil)
if1(false, x, y) → cons(0, int(s(0), y))
if2(true, x, y) → nil
if2(false, x, y) → intlist(int(p(x), p(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:
empty(nil) → true
empty(cons(x, y)) → false
tail(nil) → nil
tail(cons(x, y)) → y
head(cons(x, y)) → x
zero(0) → true
zero(s(x)) → false
p(0) → 0
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
intlist(x) → if_intlist(empty(x), x)
if_intlist(true, x) → nil
if_intlist(false, x) → cons(s(head(x)), intlist(tail(x)))
int(x, y) → if_int(zero(x), zero(y), x, y)
if_int(true, b, x, y) → if1(b, x, y)
if_int(false, b, x, y) → if2(b, x, y)
if1(true, x, y) → cons(0, nil)
if1(false, x, y) → cons(0, int(s(0), y))
if2(true, x, y) → nil
if2(false, x, y) → intlist(int(p(x), p(y)))
The set Q consists of the following terms:
empty(nil)
empty(cons(x0, x1))
tail(nil)
tail(cons(x0, x1))
head(cons(x0, x1))
zero(0)
zero(s(x0))
p(0)
p(s(0))
p(s(s(x0)))
intlist(x0)
if_intlist(true, x0)
if_intlist(false, x0)
int(x0, x1)
if_int(true, x0, x1, x2)
if_int(false, x0, x1, x2)
if1(true, x0, x1)
if1(false, x0, x1)
if2(true, x0, x1)
if2(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:
P(s(s(x))) → P(s(x))
INTLIST(x) → IF_INTLIST(empty(x), x)
INTLIST(x) → EMPTY(x)
IF_INTLIST(false, x) → HEAD(x)
IF_INTLIST(false, x) → INTLIST(tail(x))
IF_INTLIST(false, x) → TAIL(x)
INT(x, y) → IF_INT(zero(x), zero(y), x, y)
INT(x, y) → ZERO(x)
INT(x, y) → ZERO(y)
IF_INT(true, b, x, y) → IF1(b, x, y)
IF_INT(false, b, x, y) → IF2(b, x, y)
IF1(false, x, y) → INT(s(0), y)
IF2(false, x, y) → INTLIST(int(p(x), p(y)))
IF2(false, x, y) → INT(p(x), p(y))
IF2(false, x, y) → P(x)
IF2(false, x, y) → P(y)
The TRS R consists of the following rules:
empty(nil) → true
empty(cons(x, y)) → false
tail(nil) → nil
tail(cons(x, y)) → y
head(cons(x, y)) → x
zero(0) → true
zero(s(x)) → false
p(0) → 0
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
intlist(x) → if_intlist(empty(x), x)
if_intlist(true, x) → nil
if_intlist(false, x) → cons(s(head(x)), intlist(tail(x)))
int(x, y) → if_int(zero(x), zero(y), x, y)
if_int(true, b, x, y) → if1(b, x, y)
if_int(false, b, x, y) → if2(b, x, y)
if1(true, x, y) → cons(0, nil)
if1(false, x, y) → cons(0, int(s(0), y))
if2(true, x, y) → nil
if2(false, x, y) → intlist(int(p(x), p(y)))
The set Q consists of the following terms:
empty(nil)
empty(cons(x0, x1))
tail(nil)
tail(cons(x0, x1))
head(cons(x0, x1))
zero(0)
zero(s(x0))
p(0)
p(s(0))
p(s(s(x0)))
intlist(x0)
if_intlist(true, x0)
if_intlist(false, x0)
int(x0, x1)
if_int(true, x0, x1, x2)
if_int(false, x0, x1, x2)
if1(true, x0, x1)
if1(false, x0, x1)
if2(true, x0, x1)
if2(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 3 SCCs with 8 less nodes.
(6) Complex Obligation (AND)
(7) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IF_INTLIST(false, x) → INTLIST(tail(x))
INTLIST(x) → IF_INTLIST(empty(x), x)
The TRS R consists of the following rules:
empty(nil) → true
empty(cons(x, y)) → false
tail(nil) → nil
tail(cons(x, y)) → y
head(cons(x, y)) → x
zero(0) → true
zero(s(x)) → false
p(0) → 0
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
intlist(x) → if_intlist(empty(x), x)
if_intlist(true, x) → nil
if_intlist(false, x) → cons(s(head(x)), intlist(tail(x)))
int(x, y) → if_int(zero(x), zero(y), x, y)
if_int(true, b, x, y) → if1(b, x, y)
if_int(false, b, x, y) → if2(b, x, y)
if1(true, x, y) → cons(0, nil)
if1(false, x, y) → cons(0, int(s(0), y))
if2(true, x, y) → nil
if2(false, x, y) → intlist(int(p(x), p(y)))
The set Q consists of the following terms:
empty(nil)
empty(cons(x0, x1))
tail(nil)
tail(cons(x0, x1))
head(cons(x0, x1))
zero(0)
zero(s(x0))
p(0)
p(s(0))
p(s(s(x0)))
intlist(x0)
if_intlist(true, x0)
if_intlist(false, x0)
int(x0, x1)
if_int(true, x0, x1, x2)
if_int(false, x0, x1, x2)
if1(true, x0, x1)
if1(false, x0, x1)
if2(true, x0, x1)
if2(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:
IF_INTLIST(false, x) → INTLIST(tail(x))
INTLIST(x) → IF_INTLIST(empty(x), x)
The TRS R consists of the following rules:
empty(nil) → true
empty(cons(x, y)) → false
tail(nil) → nil
tail(cons(x, y)) → y
The set Q consists of the following terms:
empty(nil)
empty(cons(x0, x1))
tail(nil)
tail(cons(x0, x1))
head(cons(x0, x1))
zero(0)
zero(s(x0))
p(0)
p(s(0))
p(s(s(x0)))
intlist(x0)
if_intlist(true, x0)
if_intlist(false, x0)
int(x0, x1)
if_int(true, x0, x1, x2)
if_int(false, x0, x1, x2)
if1(true, x0, x1)
if1(false, x0, x1)
if2(true, x0, x1)
if2(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].
head(cons(x0, x1))
zero(0)
zero(s(x0))
p(0)
p(s(0))
p(s(s(x0)))
intlist(x0)
if_intlist(true, x0)
if_intlist(false, x0)
int(x0, x1)
if_int(true, x0, x1, x2)
if_int(false, x0, x1, x2)
if1(true, x0, x1)
if1(false, x0, x1)
if2(true, x0, x1)
if2(false, x0, x1)
(11) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IF_INTLIST(false, x) → INTLIST(tail(x))
INTLIST(x) → IF_INTLIST(empty(x), x)
The TRS R consists of the following rules:
empty(nil) → true
empty(cons(x, y)) → false
tail(nil) → nil
tail(cons(x, y)) → y
The set Q consists of the following terms:
empty(nil)
empty(cons(x0, x1))
tail(nil)
tail(cons(x0, x1))
We have to consider all minimal (P,Q,R)-chains.
(12) QDPOrderProof (EQUIVALENT transformation)
We use the reduction pair processor [LPAR04].
The following pairs can be oriented strictly and are deleted.
IF_INTLIST(false, x) → INTLIST(tail(x))
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO,RATPOLO]:
POL(IF_INTLIST(x1, x2)) = (1/4)x1 + (1/4)x2
POL(false) = 1/2
POL(INTLIST(x1)) = x1
POL(tail(x1)) = (1/4)x1
POL(empty(x1)) = (3)x1
POL(cons(x1, x2)) = 7/4 + (4)x2
POL(nil) = 0
POL(true) = 0
The value of delta used in the strict ordering is 1/8.
The following usable rules [FROCOS05] were oriented:
tail(cons(x, y)) → y
empty(cons(x, y)) → false
tail(nil) → nil
empty(nil) → true
(13) Obligation:
Q DP problem:
The TRS P consists of the following rules:
INTLIST(x) → IF_INTLIST(empty(x), x)
The TRS R consists of the following rules:
empty(nil) → true
empty(cons(x, y)) → false
tail(nil) → nil
tail(cons(x, y)) → y
The set Q consists of the following terms:
empty(nil)
empty(cons(x0, x1))
tail(nil)
tail(cons(x0, x1))
We have to consider all minimal (P,Q,R)-chains.
(14) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 1 less node.
(15) TRUE
(16) Obligation:
Q DP problem:
The TRS P consists of the following rules:
P(s(s(x))) → P(s(x))
The TRS R consists of the following rules:
empty(nil) → true
empty(cons(x, y)) → false
tail(nil) → nil
tail(cons(x, y)) → y
head(cons(x, y)) → x
zero(0) → true
zero(s(x)) → false
p(0) → 0
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
intlist(x) → if_intlist(empty(x), x)
if_intlist(true, x) → nil
if_intlist(false, x) → cons(s(head(x)), intlist(tail(x)))
int(x, y) → if_int(zero(x), zero(y), x, y)
if_int(true, b, x, y) → if1(b, x, y)
if_int(false, b, x, y) → if2(b, x, y)
if1(true, x, y) → cons(0, nil)
if1(false, x, y) → cons(0, int(s(0), y))
if2(true, x, y) → nil
if2(false, x, y) → intlist(int(p(x), p(y)))
The set Q consists of the following terms:
empty(nil)
empty(cons(x0, x1))
tail(nil)
tail(cons(x0, x1))
head(cons(x0, x1))
zero(0)
zero(s(x0))
p(0)
p(s(0))
p(s(s(x0)))
intlist(x0)
if_intlist(true, x0)
if_intlist(false, x0)
int(x0, x1)
if_int(true, x0, x1, x2)
if_int(false, x0, x1, x2)
if1(true, x0, x1)
if1(false, x0, x1)
if2(true, x0, x1)
if2(false, x0, x1)
We have to consider all minimal (P,Q,R)-chains.
(17) 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.
(18) Obligation:
Q DP problem:
The TRS P consists of the following rules:
P(s(s(x))) → P(s(x))
R is empty.
The set Q consists of the following terms:
empty(nil)
empty(cons(x0, x1))
tail(nil)
tail(cons(x0, x1))
head(cons(x0, x1))
zero(0)
zero(s(x0))
p(0)
p(s(0))
p(s(s(x0)))
intlist(x0)
if_intlist(true, x0)
if_intlist(false, x0)
int(x0, x1)
if_int(true, x0, x1, x2)
if_int(false, x0, x1, x2)
if1(true, x0, x1)
if1(false, x0, x1)
if2(true, x0, x1)
if2(false, x0, x1)
We have to consider all minimal (P,Q,R)-chains.
(19) 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].
empty(nil)
empty(cons(x0, x1))
tail(nil)
tail(cons(x0, x1))
head(cons(x0, x1))
zero(0)
zero(s(x0))
p(0)
p(s(0))
p(s(s(x0)))
intlist(x0)
if_intlist(true, x0)
if_intlist(false, x0)
int(x0, x1)
if_int(true, x0, x1, x2)
if_int(false, x0, x1, x2)
if1(true, x0, x1)
if1(false, x0, x1)
if2(true, x0, x1)
if2(false, x0, x1)
(20) Obligation:
Q DP problem:
The TRS P consists of the following rules:
P(s(s(x))) → P(s(x))
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(21) 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:
- P(s(s(x))) → P(s(x))
The graph contains the following edges 1 > 1
(22) TRUE
(23) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IF2(false, x, y) → INT(p(x), p(y))
INT(x, y) → IF_INT(zero(x), zero(y), x, y)
IF_INT(true, b, x, y) → IF1(b, x, y)
IF1(false, x, y) → INT(s(0), y)
IF_INT(false, b, x, y) → IF2(b, x, y)
The TRS R consists of the following rules:
empty(nil) → true
empty(cons(x, y)) → false
tail(nil) → nil
tail(cons(x, y)) → y
head(cons(x, y)) → x
zero(0) → true
zero(s(x)) → false
p(0) → 0
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
intlist(x) → if_intlist(empty(x), x)
if_intlist(true, x) → nil
if_intlist(false, x) → cons(s(head(x)), intlist(tail(x)))
int(x, y) → if_int(zero(x), zero(y), x, y)
if_int(true, b, x, y) → if1(b, x, y)
if_int(false, b, x, y) → if2(b, x, y)
if1(true, x, y) → cons(0, nil)
if1(false, x, y) → cons(0, int(s(0), y))
if2(true, x, y) → nil
if2(false, x, y) → intlist(int(p(x), p(y)))
The set Q consists of the following terms:
empty(nil)
empty(cons(x0, x1))
tail(nil)
tail(cons(x0, x1))
head(cons(x0, x1))
zero(0)
zero(s(x0))
p(0)
p(s(0))
p(s(s(x0)))
intlist(x0)
if_intlist(true, x0)
if_intlist(false, x0)
int(x0, x1)
if_int(true, x0, x1, x2)
if_int(false, x0, x1, x2)
if1(true, x0, x1)
if1(false, x0, x1)
if2(true, x0, x1)
if2(false, x0, x1)
We have to consider all minimal (P,Q,R)-chains.
(24) 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.
(25) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IF2(false, x, y) → INT(p(x), p(y))
INT(x, y) → IF_INT(zero(x), zero(y), x, y)
IF_INT(true, b, x, y) → IF1(b, x, y)
IF1(false, x, y) → INT(s(0), y)
IF_INT(false, b, x, y) → IF2(b, x, y)
The TRS R consists of the following rules:
zero(0) → true
zero(s(x)) → false
p(0) → 0
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
The set Q consists of the following terms:
empty(nil)
empty(cons(x0, x1))
tail(nil)
tail(cons(x0, x1))
head(cons(x0, x1))
zero(0)
zero(s(x0))
p(0)
p(s(0))
p(s(s(x0)))
intlist(x0)
if_intlist(true, x0)
if_intlist(false, x0)
int(x0, x1)
if_int(true, x0, x1, x2)
if_int(false, x0, x1, x2)
if1(true, x0, x1)
if1(false, x0, x1)
if2(true, x0, x1)
if2(false, x0, x1)
We have to consider all minimal (P,Q,R)-chains.
(26) 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].
empty(nil)
empty(cons(x0, x1))
tail(nil)
tail(cons(x0, x1))
head(cons(x0, x1))
intlist(x0)
if_intlist(true, x0)
if_intlist(false, x0)
int(x0, x1)
if_int(true, x0, x1, x2)
if_int(false, x0, x1, x2)
if1(true, x0, x1)
if1(false, x0, x1)
if2(true, x0, x1)
if2(false, x0, x1)
(27) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IF2(false, x, y) → INT(p(x), p(y))
INT(x, y) → IF_INT(zero(x), zero(y), x, y)
IF_INT(true, b, x, y) → IF1(b, x, y)
IF1(false, x, y) → INT(s(0), y)
IF_INT(false, b, x, y) → IF2(b, x, y)
The TRS R consists of the following rules:
zero(0) → true
zero(s(x)) → false
p(0) → 0
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
The set Q consists of the following terms:
zero(0)
zero(s(x0))
p(0)
p(s(0))
p(s(s(x0)))
We have to consider all minimal (P,Q,R)-chains.
(28) Narrowing (EQUIVALENT transformation)
By narrowing [LPAR04] the rule
INT(
x,
y) →
IF_INT(
zero(
x),
zero(
y),
x,
y) at position [0] we obtained the following new rules [LPAR04]:
INT(0, y1) → IF_INT(true, zero(y1), 0, y1)
INT(s(x0), y1) → IF_INT(false, zero(y1), s(x0), y1)
(29) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IF2(false, x, y) → INT(p(x), p(y))
IF_INT(true, b, x, y) → IF1(b, x, y)
IF1(false, x, y) → INT(s(0), y)
IF_INT(false, b, x, y) → IF2(b, x, y)
INT(0, y1) → IF_INT(true, zero(y1), 0, y1)
INT(s(x0), y1) → IF_INT(false, zero(y1), s(x0), y1)
The TRS R consists of the following rules:
zero(0) → true
zero(s(x)) → false
p(0) → 0
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
The set Q consists of the following terms:
zero(0)
zero(s(x0))
p(0)
p(s(0))
p(s(s(x0)))
We have to consider all minimal (P,Q,R)-chains.
(30) Instantiation (EQUIVALENT transformation)
By instantiating [LPAR04] the rule
IF_INT(
true,
b,
x,
y) →
IF1(
b,
x,
y) we obtained the following new rules [LPAR04]:
IF_INT(true, y_0, 0, z0) → IF1(y_0, 0, z0)
(31) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IF2(false, x, y) → INT(p(x), p(y))
IF1(false, x, y) → INT(s(0), y)
IF_INT(false, b, x, y) → IF2(b, x, y)
INT(0, y1) → IF_INT(true, zero(y1), 0, y1)
INT(s(x0), y1) → IF_INT(false, zero(y1), s(x0), y1)
IF_INT(true, y_0, 0, z0) → IF1(y_0, 0, z0)
The TRS R consists of the following rules:
zero(0) → true
zero(s(x)) → false
p(0) → 0
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
The set Q consists of the following terms:
zero(0)
zero(s(x0))
p(0)
p(s(0))
p(s(s(x0)))
We have to consider all minimal (P,Q,R)-chains.
(32) Instantiation (EQUIVALENT transformation)
By instantiating [LPAR04] the rule
IF1(
false,
x,
y) →
INT(
s(
0),
y) we obtained the following new rules [LPAR04]:
IF1(false, 0, z1) → INT(s(0), z1)
(33) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IF2(false, x, y) → INT(p(x), p(y))
IF_INT(false, b, x, y) → IF2(b, x, y)
INT(0, y1) → IF_INT(true, zero(y1), 0, y1)
INT(s(x0), y1) → IF_INT(false, zero(y1), s(x0), y1)
IF_INT(true, y_0, 0, z0) → IF1(y_0, 0, z0)
IF1(false, 0, z1) → INT(s(0), z1)
The TRS R consists of the following rules:
zero(0) → true
zero(s(x)) → false
p(0) → 0
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
The set Q consists of the following terms:
zero(0)
zero(s(x0))
p(0)
p(s(0))
p(s(s(x0)))
We have to consider all minimal (P,Q,R)-chains.
(34) Narrowing (EQUIVALENT transformation)
By narrowing [LPAR04] the rule
IF2(
false,
x,
y) →
INT(
p(
x),
p(
y)) at position [0] we obtained the following new rules [LPAR04]:
IF2(false, 0, y1) → INT(0, p(y1))
IF2(false, s(0), y1) → INT(0, p(y1))
IF2(false, s(s(x0)), y1) → INT(s(p(s(x0))), p(y1))
(35) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IF_INT(false, b, x, y) → IF2(b, x, y)
INT(0, y1) → IF_INT(true, zero(y1), 0, y1)
INT(s(x0), y1) → IF_INT(false, zero(y1), s(x0), y1)
IF_INT(true, y_0, 0, z0) → IF1(y_0, 0, z0)
IF1(false, 0, z1) → INT(s(0), z1)
IF2(false, 0, y1) → INT(0, p(y1))
IF2(false, s(0), y1) → INT(0, p(y1))
IF2(false, s(s(x0)), y1) → INT(s(p(s(x0))), p(y1))
The TRS R consists of the following rules:
zero(0) → true
zero(s(x)) → false
p(0) → 0
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
The set Q consists of the following terms:
zero(0)
zero(s(x0))
p(0)
p(s(0))
p(s(s(x0)))
We have to consider all minimal (P,Q,R)-chains.
(36) Instantiation (EQUIVALENT transformation)
By instantiating [LPAR04] the rule
IF_INT(
false,
b,
x,
y) →
IF2(
b,
x,
y) we obtained the following new rules [LPAR04]:
IF_INT(false, y_0, s(z0), z1) → IF2(y_0, s(z0), z1)
(37) Obligation:
Q DP problem:
The TRS P consists of the following rules:
INT(0, y1) → IF_INT(true, zero(y1), 0, y1)
INT(s(x0), y1) → IF_INT(false, zero(y1), s(x0), y1)
IF_INT(true, y_0, 0, z0) → IF1(y_0, 0, z0)
IF1(false, 0, z1) → INT(s(0), z1)
IF2(false, 0, y1) → INT(0, p(y1))
IF2(false, s(0), y1) → INT(0, p(y1))
IF2(false, s(s(x0)), y1) → INT(s(p(s(x0))), p(y1))
IF_INT(false, y_0, s(z0), z1) → IF2(y_0, s(z0), z1)
The TRS R consists of the following rules:
zero(0) → true
zero(s(x)) → false
p(0) → 0
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
The set Q consists of the following terms:
zero(0)
zero(s(x0))
p(0)
p(s(0))
p(s(s(x0)))
We have to consider all minimal (P,Q,R)-chains.
(38) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.
(39) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IF_INT(true, y_0, 0, z0) → IF1(y_0, 0, z0)
IF1(false, 0, z1) → INT(s(0), z1)
INT(s(x0), y1) → IF_INT(false, zero(y1), s(x0), y1)
IF_INT(false, y_0, s(z0), z1) → IF2(y_0, s(z0), z1)
IF2(false, s(0), y1) → INT(0, p(y1))
INT(0, y1) → IF_INT(true, zero(y1), 0, y1)
IF2(false, s(s(x0)), y1) → INT(s(p(s(x0))), p(y1))
The TRS R consists of the following rules:
zero(0) → true
zero(s(x)) → false
p(0) → 0
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
The set Q consists of the following terms:
zero(0)
zero(s(x0))
p(0)
p(s(0))
p(s(s(x0)))
We have to consider all minimal (P,Q,R)-chains.
(40) ForwardInstantiation (EQUIVALENT transformation)
By forward instantiating [JAR06] the rule
IF_INT(
true,
y_0,
0,
z0) →
IF1(
y_0,
0,
z0) we obtained the following new rules [LPAR04]:
IF_INT(true, false, 0, x1) → IF1(false, 0, x1)
(41) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IF1(false, 0, z1) → INT(s(0), z1)
INT(s(x0), y1) → IF_INT(false, zero(y1), s(x0), y1)
IF_INT(false, y_0, s(z0), z1) → IF2(y_0, s(z0), z1)
IF2(false, s(0), y1) → INT(0, p(y1))
INT(0, y1) → IF_INT(true, zero(y1), 0, y1)
IF2(false, s(s(x0)), y1) → INT(s(p(s(x0))), p(y1))
IF_INT(true, false, 0, x1) → IF1(false, 0, x1)
The TRS R consists of the following rules:
zero(0) → true
zero(s(x)) → false
p(0) → 0
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
The set Q consists of the following terms:
zero(0)
zero(s(x0))
p(0)
p(s(0))
p(s(s(x0)))
We have to consider all minimal (P,Q,R)-chains.
(42) Narrowing (EQUIVALENT transformation)
By narrowing [LPAR04] the rule
INT(
0,
y1) →
IF_INT(
true,
zero(
y1),
0,
y1) at position [1] we obtained the following new rules [LPAR04]:
INT(0, 0) → IF_INT(true, true, 0, 0)
INT(0, s(x0)) → IF_INT(true, false, 0, s(x0))
(43) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IF1(false, 0, z1) → INT(s(0), z1)
INT(s(x0), y1) → IF_INT(false, zero(y1), s(x0), y1)
IF_INT(false, y_0, s(z0), z1) → IF2(y_0, s(z0), z1)
IF2(false, s(0), y1) → INT(0, p(y1))
IF2(false, s(s(x0)), y1) → INT(s(p(s(x0))), p(y1))
IF_INT(true, false, 0, x1) → IF1(false, 0, x1)
INT(0, 0) → IF_INT(true, true, 0, 0)
INT(0, s(x0)) → IF_INT(true, false, 0, s(x0))
The TRS R consists of the following rules:
zero(0) → true
zero(s(x)) → false
p(0) → 0
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
The set Q consists of the following terms:
zero(0)
zero(s(x0))
p(0)
p(s(0))
p(s(s(x0)))
We have to consider all minimal (P,Q,R)-chains.
(44) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.
(45) Obligation:
Q DP problem:
The TRS P consists of the following rules:
INT(s(x0), y1) → IF_INT(false, zero(y1), s(x0), y1)
IF_INT(false, y_0, s(z0), z1) → IF2(y_0, s(z0), z1)
IF2(false, s(0), y1) → INT(0, p(y1))
INT(0, s(x0)) → IF_INT(true, false, 0, s(x0))
IF_INT(true, false, 0, x1) → IF1(false, 0, x1)
IF1(false, 0, z1) → INT(s(0), z1)
IF2(false, s(s(x0)), y1) → INT(s(p(s(x0))), p(y1))
The TRS R consists of the following rules:
zero(0) → true
zero(s(x)) → false
p(0) → 0
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
The set Q consists of the following terms:
zero(0)
zero(s(x0))
p(0)
p(s(0))
p(s(s(x0)))
We have to consider all minimal (P,Q,R)-chains.
(46) Narrowing (EQUIVALENT transformation)
By narrowing [LPAR04] the rule
IF2(
false,
s(
0),
y1) →
INT(
0,
p(
y1)) at position [1] we obtained the following new rules [LPAR04]:
IF2(false, s(0), 0) → INT(0, 0)
IF2(false, s(0), s(0)) → INT(0, 0)
IF2(false, s(0), s(s(x0))) → INT(0, s(p(s(x0))))
(47) Obligation:
Q DP problem:
The TRS P consists of the following rules:
INT(s(x0), y1) → IF_INT(false, zero(y1), s(x0), y1)
IF_INT(false, y_0, s(z0), z1) → IF2(y_0, s(z0), z1)
INT(0, s(x0)) → IF_INT(true, false, 0, s(x0))
IF_INT(true, false, 0, x1) → IF1(false, 0, x1)
IF1(false, 0, z1) → INT(s(0), z1)
IF2(false, s(s(x0)), y1) → INT(s(p(s(x0))), p(y1))
IF2(false, s(0), 0) → INT(0, 0)
IF2(false, s(0), s(0)) → INT(0, 0)
IF2(false, s(0), s(s(x0))) → INT(0, s(p(s(x0))))
The TRS R consists of the following rules:
zero(0) → true
zero(s(x)) → false
p(0) → 0
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
The set Q consists of the following terms:
zero(0)
zero(s(x0))
p(0)
p(s(0))
p(s(s(x0)))
We have to consider all minimal (P,Q,R)-chains.
(48) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 2 less nodes.
(49) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IF_INT(false, y_0, s(z0), z1) → IF2(y_0, s(z0), z1)
IF2(false, s(s(x0)), y1) → INT(s(p(s(x0))), p(y1))
INT(s(x0), y1) → IF_INT(false, zero(y1), s(x0), y1)
IF2(false, s(0), s(s(x0))) → INT(0, s(p(s(x0))))
INT(0, s(x0)) → IF_INT(true, false, 0, s(x0))
IF_INT(true, false, 0, x1) → IF1(false, 0, x1)
IF1(false, 0, z1) → INT(s(0), z1)
The TRS R consists of the following rules:
zero(0) → true
zero(s(x)) → false
p(0) → 0
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
The set Q consists of the following terms:
zero(0)
zero(s(x0))
p(0)
p(s(0))
p(s(s(x0)))
We have to consider all minimal (P,Q,R)-chains.
(50) Instantiation (EQUIVALENT transformation)
By instantiating [LPAR04] the rule
IF_INT(
true,
false,
0,
x1) →
IF1(
false,
0,
x1) we obtained the following new rules [LPAR04]:
IF_INT(true, false, 0, s(z0)) → IF1(false, 0, s(z0))
(51) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IF_INT(false, y_0, s(z0), z1) → IF2(y_0, s(z0), z1)
IF2(false, s(s(x0)), y1) → INT(s(p(s(x0))), p(y1))
INT(s(x0), y1) → IF_INT(false, zero(y1), s(x0), y1)
IF2(false, s(0), s(s(x0))) → INT(0, s(p(s(x0))))
INT(0, s(x0)) → IF_INT(true, false, 0, s(x0))
IF1(false, 0, z1) → INT(s(0), z1)
IF_INT(true, false, 0, s(z0)) → IF1(false, 0, s(z0))
The TRS R consists of the following rules:
zero(0) → true
zero(s(x)) → false
p(0) → 0
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
The set Q consists of the following terms:
zero(0)
zero(s(x0))
p(0)
p(s(0))
p(s(s(x0)))
We have to consider all minimal (P,Q,R)-chains.
(52) Instantiation (EQUIVALENT transformation)
By instantiating [LPAR04] the rule
IF1(
false,
0,
z1) →
INT(
s(
0),
z1) we obtained the following new rules [LPAR04]:
IF1(false, 0, s(z0)) → INT(s(0), s(z0))
(53) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IF_INT(false, y_0, s(z0), z1) → IF2(y_0, s(z0), z1)
IF2(false, s(s(x0)), y1) → INT(s(p(s(x0))), p(y1))
INT(s(x0), y1) → IF_INT(false, zero(y1), s(x0), y1)
IF2(false, s(0), s(s(x0))) → INT(0, s(p(s(x0))))
INT(0, s(x0)) → IF_INT(true, false, 0, s(x0))
IF_INT(true, false, 0, s(z0)) → IF1(false, 0, s(z0))
IF1(false, 0, s(z0)) → INT(s(0), s(z0))
The TRS R consists of the following rules:
zero(0) → true
zero(s(x)) → false
p(0) → 0
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
The set Q consists of the following terms:
zero(0)
zero(s(x0))
p(0)
p(s(0))
p(s(s(x0)))
We have to consider all minimal (P,Q,R)-chains.
(54) ForwardInstantiation (EQUIVALENT transformation)
By forward instantiating [JAR06] the rule
IF_INT(
false,
y_0,
s(
z0),
z1) →
IF2(
y_0,
s(
z0),
z1) we obtained the following new rules [LPAR04]:
IF_INT(false, false, s(s(y_0)), x2) → IF2(false, s(s(y_0)), x2)
IF_INT(false, false, s(0), s(s(y_0))) → IF2(false, s(0), s(s(y_0)))
(55) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IF2(false, s(s(x0)), y1) → INT(s(p(s(x0))), p(y1))
INT(s(x0), y1) → IF_INT(false, zero(y1), s(x0), y1)
IF2(false, s(0), s(s(x0))) → INT(0, s(p(s(x0))))
INT(0, s(x0)) → IF_INT(true, false, 0, s(x0))
IF_INT(true, false, 0, s(z0)) → IF1(false, 0, s(z0))
IF1(false, 0, s(z0)) → INT(s(0), s(z0))
IF_INT(false, false, s(s(y_0)), x2) → IF2(false, s(s(y_0)), x2)
IF_INT(false, false, s(0), s(s(y_0))) → IF2(false, s(0), s(s(y_0)))
The TRS R consists of the following rules:
zero(0) → true
zero(s(x)) → false
p(0) → 0
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
The set Q consists of the following terms:
zero(0)
zero(s(x0))
p(0)
p(s(0))
p(s(s(x0)))
We have to consider all minimal (P,Q,R)-chains.
(56) Narrowing (EQUIVALENT transformation)
By narrowing [LPAR04] the rule
INT(
s(
x0),
y1) →
IF_INT(
false,
zero(
y1),
s(
x0),
y1) at position [1] we obtained the following new rules [LPAR04]:
INT(s(y0), 0) → IF_INT(false, true, s(y0), 0)
INT(s(y0), s(x0)) → IF_INT(false, false, s(y0), s(x0))
(57) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IF2(false, s(s(x0)), y1) → INT(s(p(s(x0))), p(y1))
IF2(false, s(0), s(s(x0))) → INT(0, s(p(s(x0))))
INT(0, s(x0)) → IF_INT(true, false, 0, s(x0))
IF_INT(true, false, 0, s(z0)) → IF1(false, 0, s(z0))
IF1(false, 0, s(z0)) → INT(s(0), s(z0))
IF_INT(false, false, s(s(y_0)), x2) → IF2(false, s(s(y_0)), x2)
IF_INT(false, false, s(0), s(s(y_0))) → IF2(false, s(0), s(s(y_0)))
INT(s(y0), 0) → IF_INT(false, true, s(y0), 0)
INT(s(y0), s(x0)) → IF_INT(false, false, s(y0), s(x0))
The TRS R consists of the following rules:
zero(0) → true
zero(s(x)) → false
p(0) → 0
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
The set Q consists of the following terms:
zero(0)
zero(s(x0))
p(0)
p(s(0))
p(s(s(x0)))
We have to consider all minimal (P,Q,R)-chains.
(58) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.
(59) Obligation:
Q DP problem:
The TRS P consists of the following rules:
INT(s(y0), s(x0)) → IF_INT(false, false, s(y0), s(x0))
IF_INT(false, false, s(s(y_0)), x2) → IF2(false, s(s(y_0)), x2)
IF2(false, s(s(x0)), y1) → INT(s(p(s(x0))), p(y1))
IF_INT(false, false, s(0), s(s(y_0))) → IF2(false, s(0), s(s(y_0)))
IF2(false, s(0), s(s(x0))) → INT(0, s(p(s(x0))))
INT(0, s(x0)) → IF_INT(true, false, 0, s(x0))
IF_INT(true, false, 0, s(z0)) → IF1(false, 0, s(z0))
IF1(false, 0, s(z0)) → INT(s(0), s(z0))
The TRS R consists of the following rules:
zero(0) → true
zero(s(x)) → false
p(0) → 0
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
The set Q consists of the following terms:
zero(0)
zero(s(x0))
p(0)
p(s(0))
p(s(s(x0)))
We have to consider all minimal (P,Q,R)-chains.
(60) 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.
(61) Obligation:
Q DP problem:
The TRS P consists of the following rules:
INT(s(y0), s(x0)) → IF_INT(false, false, s(y0), s(x0))
IF_INT(false, false, s(s(y_0)), x2) → IF2(false, s(s(y_0)), x2)
IF2(false, s(s(x0)), y1) → INT(s(p(s(x0))), p(y1))
IF_INT(false, false, s(0), s(s(y_0))) → IF2(false, s(0), s(s(y_0)))
IF2(false, s(0), s(s(x0))) → INT(0, s(p(s(x0))))
INT(0, s(x0)) → IF_INT(true, false, 0, s(x0))
IF_INT(true, false, 0, s(z0)) → IF1(false, 0, s(z0))
IF1(false, 0, s(z0)) → INT(s(0), s(z0))
The TRS R consists of the following rules:
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
p(0) → 0
The set Q consists of the following terms:
zero(0)
zero(s(x0))
p(0)
p(s(0))
p(s(s(x0)))
We have to consider all minimal (P,Q,R)-chains.
(62) 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))
(63) Obligation:
Q DP problem:
The TRS P consists of the following rules:
INT(s(y0), s(x0)) → IF_INT(false, false, s(y0), s(x0))
IF_INT(false, false, s(s(y_0)), x2) → IF2(false, s(s(y_0)), x2)
IF2(false, s(s(x0)), y1) → INT(s(p(s(x0))), p(y1))
IF_INT(false, false, s(0), s(s(y_0))) → IF2(false, s(0), s(s(y_0)))
IF2(false, s(0), s(s(x0))) → INT(0, s(p(s(x0))))
INT(0, s(x0)) → IF_INT(true, false, 0, s(x0))
IF_INT(true, false, 0, s(z0)) → IF1(false, 0, s(z0))
IF1(false, 0, s(z0)) → INT(s(0), s(z0))
The TRS R consists of the following rules:
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
p(0) → 0
The set Q consists of the following terms:
p(0)
p(s(0))
p(s(s(x0)))
We have to consider all minimal (P,Q,R)-chains.
(64) Narrowing (EQUIVALENT transformation)
By narrowing [LPAR04] the rule
IF2(
false,
s(
s(
x0)),
y1) →
INT(
s(
p(
s(
x0))),
p(
y1)) at position [1] we obtained the following new rules [LPAR04]:
IF2(false, s(s(y0)), s(0)) → INT(s(p(s(y0))), 0)
IF2(false, s(s(y0)), s(s(x0))) → INT(s(p(s(y0))), s(p(s(x0))))
IF2(false, s(s(y0)), 0) → INT(s(p(s(y0))), 0)
(65) Obligation:
Q DP problem:
The TRS P consists of the following rules:
INT(s(y0), s(x0)) → IF_INT(false, false, s(y0), s(x0))
IF_INT(false, false, s(s(y_0)), x2) → IF2(false, s(s(y_0)), x2)
IF_INT(false, false, s(0), s(s(y_0))) → IF2(false, s(0), s(s(y_0)))
IF2(false, s(0), s(s(x0))) → INT(0, s(p(s(x0))))
INT(0, s(x0)) → IF_INT(true, false, 0, s(x0))
IF_INT(true, false, 0, s(z0)) → IF1(false, 0, s(z0))
IF1(false, 0, s(z0)) → INT(s(0), s(z0))
IF2(false, s(s(y0)), s(0)) → INT(s(p(s(y0))), 0)
IF2(false, s(s(y0)), s(s(x0))) → INT(s(p(s(y0))), s(p(s(x0))))
IF2(false, s(s(y0)), 0) → INT(s(p(s(y0))), 0)
The TRS R consists of the following rules:
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
p(0) → 0
The set Q consists of the following terms:
p(0)
p(s(0))
p(s(s(x0)))
We have to consider all minimal (P,Q,R)-chains.
(66) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 2 less nodes.
(67) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IF_INT(false, false, s(s(y_0)), x2) → IF2(false, s(s(y_0)), x2)
IF2(false, s(s(y0)), s(s(x0))) → INT(s(p(s(y0))), s(p(s(x0))))
INT(s(y0), s(x0)) → IF_INT(false, false, s(y0), s(x0))
IF_INT(false, false, s(0), s(s(y_0))) → IF2(false, s(0), s(s(y_0)))
IF2(false, s(0), s(s(x0))) → INT(0, s(p(s(x0))))
INT(0, s(x0)) → IF_INT(true, false, 0, s(x0))
IF_INT(true, false, 0, s(z0)) → IF1(false, 0, s(z0))
IF1(false, 0, s(z0)) → INT(s(0), s(z0))
The TRS R consists of the following rules:
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
p(0) → 0
The set Q consists of the following terms:
p(0)
p(s(0))
p(s(s(x0)))
We have to consider all minimal (P,Q,R)-chains.
(68) 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.
(69) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IF_INT(false, false, s(s(y_0)), x2) → IF2(false, s(s(y_0)), x2)
IF2(false, s(s(y0)), s(s(x0))) → INT(s(p(s(y0))), s(p(s(x0))))
INT(s(y0), s(x0)) → IF_INT(false, false, s(y0), s(x0))
IF_INT(false, false, s(0), s(s(y_0))) → IF2(false, s(0), s(s(y_0)))
IF2(false, s(0), s(s(x0))) → INT(0, s(p(s(x0))))
INT(0, s(x0)) → IF_INT(true, false, 0, s(x0))
IF_INT(true, false, 0, s(z0)) → IF1(false, 0, s(z0))
IF1(false, 0, s(z0)) → INT(s(0), s(z0))
The TRS R consists of the following rules:
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
The set Q consists of the following terms:
p(0)
p(s(0))
p(s(s(x0)))
We have to consider all minimal (P,Q,R)-chains.
(70) Instantiation (EQUIVALENT transformation)
By instantiating [LPAR04] the rule
IF_INT(
false,
false,
s(
s(
y_0)),
x2) →
IF2(
false,
s(
s(
y_0)),
x2) we obtained the following new rules [LPAR04]:
IF_INT(false, false, s(s(x0)), s(z1)) → IF2(false, s(s(x0)), s(z1))
(71) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IF2(false, s(s(y0)), s(s(x0))) → INT(s(p(s(y0))), s(p(s(x0))))
INT(s(y0), s(x0)) → IF_INT(false, false, s(y0), s(x0))
IF_INT(false, false, s(0), s(s(y_0))) → IF2(false, s(0), s(s(y_0)))
IF2(false, s(0), s(s(x0))) → INT(0, s(p(s(x0))))
INT(0, s(x0)) → IF_INT(true, false, 0, s(x0))
IF_INT(true, false, 0, s(z0)) → IF1(false, 0, s(z0))
IF1(false, 0, s(z0)) → INT(s(0), s(z0))
IF_INT(false, false, s(s(x0)), s(z1)) → IF2(false, s(s(x0)), s(z1))
The TRS R consists of the following rules:
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
The set Q consists of the following terms:
p(0)
p(s(0))
p(s(s(x0)))
We have to consider all minimal (P,Q,R)-chains.
(72) ForwardInstantiation (EQUIVALENT transformation)
By forward instantiating [JAR06] the rule
INT(
s(
y0),
s(
x0)) →
IF_INT(
false,
false,
s(
y0),
s(
x0)) we obtained the following new rules [LPAR04]:
INT(s(0), s(s(y_0))) → IF_INT(false, false, s(0), s(s(y_0)))
INT(s(s(y_0)), s(x1)) → IF_INT(false, false, s(s(y_0)), s(x1))
(73) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IF2(false, s(s(y0)), s(s(x0))) → INT(s(p(s(y0))), s(p(s(x0))))
IF_INT(false, false, s(0), s(s(y_0))) → IF2(false, s(0), s(s(y_0)))
IF2(false, s(0), s(s(x0))) → INT(0, s(p(s(x0))))
INT(0, s(x0)) → IF_INT(true, false, 0, s(x0))
IF_INT(true, false, 0, s(z0)) → IF1(false, 0, s(z0))
IF1(false, 0, s(z0)) → INT(s(0), s(z0))
IF_INT(false, false, s(s(x0)), s(z1)) → IF2(false, s(s(x0)), s(z1))
INT(s(0), s(s(y_0))) → IF_INT(false, false, s(0), s(s(y_0)))
INT(s(s(y_0)), s(x1)) → IF_INT(false, false, s(s(y_0)), s(x1))
The TRS R consists of the following rules:
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
The set Q consists of the following terms:
p(0)
p(s(0))
p(s(s(x0)))
We have to consider all minimal (P,Q,R)-chains.
(74) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 2 SCCs.
(75) Complex Obligation (AND)
(76) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IF2(false, s(0), s(s(x0))) → INT(0, s(p(s(x0))))
INT(0, s(x0)) → IF_INT(true, false, 0, s(x0))
IF_INT(true, false, 0, s(z0)) → IF1(false, 0, s(z0))
IF1(false, 0, s(z0)) → INT(s(0), s(z0))
INT(s(0), s(s(y_0))) → IF_INT(false, false, s(0), s(s(y_0)))
IF_INT(false, false, s(0), s(s(y_0))) → IF2(false, s(0), s(s(y_0)))
The TRS R consists of the following rules:
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
The set Q consists of the following terms:
p(0)
p(s(0))
p(s(s(x0)))
We have to consider all minimal (P,Q,R)-chains.
(77) ForwardInstantiation (EQUIVALENT transformation)
By forward instantiating [JAR06] the rule
IF1(
false,
0,
s(
z0)) →
INT(
s(
0),
s(
z0)) we obtained the following new rules [LPAR04]:
IF1(false, 0, s(s(y_0))) → INT(s(0), s(s(y_0)))
(78) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IF2(false, s(0), s(s(x0))) → INT(0, s(p(s(x0))))
INT(0, s(x0)) → IF_INT(true, false, 0, s(x0))
IF_INT(true, false, 0, s(z0)) → IF1(false, 0, s(z0))
INT(s(0), s(s(y_0))) → IF_INT(false, false, s(0), s(s(y_0)))
IF_INT(false, false, s(0), s(s(y_0))) → IF2(false, s(0), s(s(y_0)))
IF1(false, 0, s(s(y_0))) → INT(s(0), s(s(y_0)))
The TRS R consists of the following rules:
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
The set Q consists of the following terms:
p(0)
p(s(0))
p(s(s(x0)))
We have to consider all minimal (P,Q,R)-chains.
(79) QDPOrderProof (EQUIVALENT transformation)
We use the reduction pair processor [LPAR04].
The following pairs can be oriented strictly and are deleted.
IF2(false, s(0), s(s(x0))) → INT(0, s(p(s(x0))))
The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO]:
POL(IF2(x1, x2, x3)) = | | + | | · | x1 | + | | · | x2 | + | | · | x3 |
POL(INT(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(IF_INT(x1, x2, x3, x4)) = | | + | | · | x1 | + | | · | x2 | + | | · | x3 | + | | · | x4 |
POL(IF1(x1, x2, x3)) = | | + | | · | x1 | + | | · | x2 | + | | · | x3 |
The following usable rules [FROCOS05] were oriented:
p(s(s(x))) → s(p(s(x)))
p(s(0)) → 0
(80) Obligation:
Q DP problem:
The TRS P consists of the following rules:
INT(0, s(x0)) → IF_INT(true, false, 0, s(x0))
IF_INT(true, false, 0, s(z0)) → IF1(false, 0, s(z0))
INT(s(0), s(s(y_0))) → IF_INT(false, false, s(0), s(s(y_0)))
IF_INT(false, false, s(0), s(s(y_0))) → IF2(false, s(0), s(s(y_0)))
IF1(false, 0, s(s(y_0))) → INT(s(0), s(s(y_0)))
The TRS R consists of the following rules:
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
The set Q consists of the following terms:
p(0)
p(s(0))
p(s(s(x0)))
We have to consider all minimal (P,Q,R)-chains.
(81) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 5 less nodes.
(82) TRUE
(83) Obligation:
Q DP problem:
The TRS P consists of the following rules:
INT(s(s(y_0)), s(x1)) → IF_INT(false, false, s(s(y_0)), s(x1))
IF_INT(false, false, s(s(x0)), s(z1)) → IF2(false, s(s(x0)), s(z1))
IF2(false, s(s(y0)), s(s(x0))) → INT(s(p(s(y0))), s(p(s(x0))))
The TRS R consists of the following rules:
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
The set Q consists of the following terms:
p(0)
p(s(0))
p(s(s(x0)))
We have to consider all minimal (P,Q,R)-chains.
(84) MRRProof (EQUIVALENT transformation)
By using the rule removal processor [LPAR04] with the following ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.
Strictly oriented rules of the TRS R:
p(s(0)) → 0
Used ordering: Polynomial interpretation [POLO]:
POL(0) = 0
POL(IF2(x1, x2, x3)) = x1 + x2 + x3
POL(IF_INT(x1, x2, x3, x4)) = x1 + x2 + x3 + x4
POL(INT(x1, x2)) = x1 + x2
POL(false) = 0
POL(p(x1)) = x1
POL(s(x1)) = 1 + x1
(85) Obligation:
Q DP problem:
The TRS P consists of the following rules:
INT(s(s(y_0)), s(x1)) → IF_INT(false, false, s(s(y_0)), s(x1))
IF_INT(false, false, s(s(x0)), s(z1)) → IF2(false, s(s(x0)), s(z1))
IF2(false, s(s(y0)), s(s(x0))) → INT(s(p(s(y0))), s(p(s(x0))))
The TRS R consists of the following rules:
p(s(s(x))) → s(p(s(x)))
The set Q consists of the following terms:
p(0)
p(s(0))
p(s(s(x0)))
We have to consider all minimal (P,Q,R)-chains.
(86) QDPOrderProof (EQUIVALENT transformation)
We use the reduction pair processor [LPAR04].
The following pairs can be oriented strictly and are deleted.
INT(s(s(y_0)), s(x1)) → IF_INT(false, false, s(s(y_0)), s(x1))
The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO]:
POL(INT(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(IF_INT(x1, x2, x3, x4)) = | | + | | · | x1 | + | | · | x2 | + | | · | x3 | + | | · | x4 |
POL(IF2(x1, x2, x3)) = | | + | | · | x1 | + | | · | x2 | + | | · | x3 |
The following usable rules [FROCOS05] were oriented:
p(s(s(x))) → s(p(s(x)))
(87) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IF_INT(false, false, s(s(x0)), s(z1)) → IF2(false, s(s(x0)), s(z1))
IF2(false, s(s(y0)), s(s(x0))) → INT(s(p(s(y0))), s(p(s(x0))))
The TRS R consists of the following rules:
p(s(s(x))) → s(p(s(x)))
The set Q consists of the following terms:
p(0)
p(s(0))
p(s(s(x0)))
We have to consider all minimal (P,Q,R)-chains.
(88) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 2 less nodes.
(89) TRUE