(0) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
times(x, y) → sum(generate(x, y))
generate(x, y) → gen(x, y, 0)
gen(x, y, z) → if(ge(z, x), x, y, z)
if(true, x, y, z) → nil
if(false, x, y, z) → cons(y, gen(x, y, s(z)))
sum(xs) → sum2(xs, 0)
sum2(xs, y) → ifsum(isNil(xs), isZero(head(xs)), xs, y)
ifsum(true, b, xs, y) → y
ifsum(false, b, xs, y) → ifsum2(b, xs, y)
ifsum2(true, xs, y) → sum2(tail(xs), y)
ifsum2(false, xs, y) → sum2(cons(p(head(xs)), tail(xs)), s(y))
isNil(nil) → true
isNil(cons(x, xs)) → false
tail(nil) → nil
tail(cons(x, xs)) → xs
head(cons(x, xs)) → x
head(nil) → error
isZero(0) → true
isZero(s(0)) → false
isZero(s(s(x))) → isZero(s(x))
p(0) → s(s(0))
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
ge(x, 0) → true
ge(0, s(y)) → false
ge(s(x), s(y)) → ge(x, y)
a → c
a → d
Q is empty.
(1) AAECC Innermost (EQUIVALENT transformation)
We have applied [NOC,AAECCNOC] to switch to innermost. The TRS R 1 is
generate(x, y) → gen(x, y, 0)
gen(x, y, z) → if(ge(z, x), x, y, z)
if(true, x, y, z) → nil
if(false, x, y, z) → cons(y, gen(x, y, s(z)))
ifsum(true, b, xs, y) → y
ifsum(false, b, xs, y) → ifsum2(b, xs, y)
ifsum2(true, xs, y) → sum2(tail(xs), y)
ifsum2(false, xs, y) → sum2(cons(p(head(xs)), tail(xs)), s(y))
isNil(nil) → true
isNil(cons(x, xs)) → false
tail(nil) → nil
tail(cons(x, xs)) → xs
head(cons(x, xs)) → x
head(nil) → error
isZero(0) → true
isZero(s(0)) → false
isZero(s(s(x))) → isZero(s(x))
p(0) → s(s(0))
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
ge(x, 0) → true
ge(0, s(y)) → false
ge(s(x), s(y)) → ge(x, y)
sum(xs) → sum2(xs, 0)
sum2(xs, y) → ifsum(isNil(xs), isZero(head(xs)), xs, y)
times(x, y) → sum(generate(x, y))
The TRS R 2 is
a → c
a → d
The signature Sigma is {
c,
a,
d}
(2) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
times(x, y) → sum(generate(x, y))
generate(x, y) → gen(x, y, 0)
gen(x, y, z) → if(ge(z, x), x, y, z)
if(true, x, y, z) → nil
if(false, x, y, z) → cons(y, gen(x, y, s(z)))
sum(xs) → sum2(xs, 0)
sum2(xs, y) → ifsum(isNil(xs), isZero(head(xs)), xs, y)
ifsum(true, b, xs, y) → y
ifsum(false, b, xs, y) → ifsum2(b, xs, y)
ifsum2(true, xs, y) → sum2(tail(xs), y)
ifsum2(false, xs, y) → sum2(cons(p(head(xs)), tail(xs)), s(y))
isNil(nil) → true
isNil(cons(x, xs)) → false
tail(nil) → nil
tail(cons(x, xs)) → xs
head(cons(x, xs)) → x
head(nil) → error
isZero(0) → true
isZero(s(0)) → false
isZero(s(s(x))) → isZero(s(x))
p(0) → s(s(0))
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
ge(x, 0) → true
ge(0, s(y)) → false
ge(s(x), s(y)) → ge(x, y)
a → c
a → d
The set Q consists of the following terms:
times(x0, x1)
generate(x0, x1)
gen(x0, x1, x2)
if(true, x0, x1, x2)
if(false, x0, x1, x2)
sum(x0)
sum2(x0, x1)
ifsum(true, x0, x1, x2)
ifsum(false, x0, x1, x2)
ifsum2(true, x0, x1)
ifsum2(false, x0, x1)
isNil(nil)
isNil(cons(x0, x1))
tail(nil)
tail(cons(x0, x1))
head(cons(x0, x1))
head(nil)
isZero(0)
isZero(s(0))
isZero(s(s(x0)))
p(0)
p(s(0))
p(s(s(x0)))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
a
(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:
TIMES(x, y) → SUM(generate(x, y))
TIMES(x, y) → GENERATE(x, y)
GENERATE(x, y) → GEN(x, y, 0)
GEN(x, y, z) → IF(ge(z, x), x, y, z)
GEN(x, y, z) → GE(z, x)
IF(false, x, y, z) → GEN(x, y, s(z))
SUM(xs) → SUM2(xs, 0)
SUM2(xs, y) → IFSUM(isNil(xs), isZero(head(xs)), xs, y)
SUM2(xs, y) → ISNIL(xs)
SUM2(xs, y) → ISZERO(head(xs))
SUM2(xs, y) → HEAD(xs)
IFSUM(false, b, xs, y) → IFSUM2(b, xs, y)
IFSUM2(true, xs, y) → SUM2(tail(xs), y)
IFSUM2(true, xs, y) → TAIL(xs)
IFSUM2(false, xs, y) → SUM2(cons(p(head(xs)), tail(xs)), s(y))
IFSUM2(false, xs, y) → P(head(xs))
IFSUM2(false, xs, y) → HEAD(xs)
IFSUM2(false, xs, y) → TAIL(xs)
ISZERO(s(s(x))) → ISZERO(s(x))
P(s(s(x))) → P(s(x))
GE(s(x), s(y)) → GE(x, y)
The TRS R consists of the following rules:
times(x, y) → sum(generate(x, y))
generate(x, y) → gen(x, y, 0)
gen(x, y, z) → if(ge(z, x), x, y, z)
if(true, x, y, z) → nil
if(false, x, y, z) → cons(y, gen(x, y, s(z)))
sum(xs) → sum2(xs, 0)
sum2(xs, y) → ifsum(isNil(xs), isZero(head(xs)), xs, y)
ifsum(true, b, xs, y) → y
ifsum(false, b, xs, y) → ifsum2(b, xs, y)
ifsum2(true, xs, y) → sum2(tail(xs), y)
ifsum2(false, xs, y) → sum2(cons(p(head(xs)), tail(xs)), s(y))
isNil(nil) → true
isNil(cons(x, xs)) → false
tail(nil) → nil
tail(cons(x, xs)) → xs
head(cons(x, xs)) → x
head(nil) → error
isZero(0) → true
isZero(s(0)) → false
isZero(s(s(x))) → isZero(s(x))
p(0) → s(s(0))
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
ge(x, 0) → true
ge(0, s(y)) → false
ge(s(x), s(y)) → ge(x, y)
a → c
a → d
The set Q consists of the following terms:
times(x0, x1)
generate(x0, x1)
gen(x0, x1, x2)
if(true, x0, x1, x2)
if(false, x0, x1, x2)
sum(x0)
sum2(x0, x1)
ifsum(true, x0, x1, x2)
ifsum(false, x0, x1, x2)
ifsum2(true, x0, x1)
ifsum2(false, x0, x1)
isNil(nil)
isNil(cons(x0, x1))
tail(nil)
tail(cons(x0, x1))
head(cons(x0, x1))
head(nil)
isZero(0)
isZero(s(0))
isZero(s(s(x0)))
p(0)
p(s(0))
p(s(s(x0)))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
a
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 12 less nodes.
(6) Complex Obligation (AND)
(7) Obligation:
Q DP problem:
The TRS P consists of the following rules:
GE(s(x), s(y)) → GE(x, y)
The TRS R consists of the following rules:
times(x, y) → sum(generate(x, y))
generate(x, y) → gen(x, y, 0)
gen(x, y, z) → if(ge(z, x), x, y, z)
if(true, x, y, z) → nil
if(false, x, y, z) → cons(y, gen(x, y, s(z)))
sum(xs) → sum2(xs, 0)
sum2(xs, y) → ifsum(isNil(xs), isZero(head(xs)), xs, y)
ifsum(true, b, xs, y) → y
ifsum(false, b, xs, y) → ifsum2(b, xs, y)
ifsum2(true, xs, y) → sum2(tail(xs), y)
ifsum2(false, xs, y) → sum2(cons(p(head(xs)), tail(xs)), s(y))
isNil(nil) → true
isNil(cons(x, xs)) → false
tail(nil) → nil
tail(cons(x, xs)) → xs
head(cons(x, xs)) → x
head(nil) → error
isZero(0) → true
isZero(s(0)) → false
isZero(s(s(x))) → isZero(s(x))
p(0) → s(s(0))
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
ge(x, 0) → true
ge(0, s(y)) → false
ge(s(x), s(y)) → ge(x, y)
a → c
a → d
The set Q consists of the following terms:
times(x0, x1)
generate(x0, x1)
gen(x0, x1, x2)
if(true, x0, x1, x2)
if(false, x0, x1, x2)
sum(x0)
sum2(x0, x1)
ifsum(true, x0, x1, x2)
ifsum(false, x0, x1, x2)
ifsum2(true, x0, x1)
ifsum2(false, x0, x1)
isNil(nil)
isNil(cons(x0, x1))
tail(nil)
tail(cons(x0, x1))
head(cons(x0, x1))
head(nil)
isZero(0)
isZero(s(0))
isZero(s(s(x0)))
p(0)
p(s(0))
p(s(s(x0)))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
a
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:
GE(s(x), s(y)) → GE(x, y)
R is empty.
The set Q consists of the following terms:
times(x0, x1)
generate(x0, x1)
gen(x0, x1, x2)
if(true, x0, x1, x2)
if(false, x0, x1, x2)
sum(x0)
sum2(x0, x1)
ifsum(true, x0, x1, x2)
ifsum(false, x0, x1, x2)
ifsum2(true, x0, x1)
ifsum2(false, x0, x1)
isNil(nil)
isNil(cons(x0, x1))
tail(nil)
tail(cons(x0, x1))
head(cons(x0, x1))
head(nil)
isZero(0)
isZero(s(0))
isZero(s(s(x0)))
p(0)
p(s(0))
p(s(s(x0)))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
a
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].
times(x0, x1)
generate(x0, x1)
gen(x0, x1, x2)
if(true, x0, x1, x2)
if(false, x0, x1, x2)
sum(x0)
sum2(x0, x1)
ifsum(true, x0, x1, x2)
ifsum(false, x0, x1, x2)
ifsum2(true, x0, x1)
ifsum2(false, x0, x1)
isNil(nil)
isNil(cons(x0, x1))
tail(nil)
tail(cons(x0, x1))
head(cons(x0, x1))
head(nil)
isZero(0)
isZero(s(0))
isZero(s(s(x0)))
p(0)
p(s(0))
p(s(s(x0)))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
a
(11) Obligation:
Q DP problem:
The TRS P consists of the following rules:
GE(s(x), s(y)) → GE(x, y)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(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:
- GE(s(x), s(y)) → GE(x, y)
The graph contains the following edges 1 > 1, 2 > 2
(13) TRUE
(14) Obligation:
Q DP problem:
The TRS P consists of the following rules:
P(s(s(x))) → P(s(x))
The TRS R consists of the following rules:
times(x, y) → sum(generate(x, y))
generate(x, y) → gen(x, y, 0)
gen(x, y, z) → if(ge(z, x), x, y, z)
if(true, x, y, z) → nil
if(false, x, y, z) → cons(y, gen(x, y, s(z)))
sum(xs) → sum2(xs, 0)
sum2(xs, y) → ifsum(isNil(xs), isZero(head(xs)), xs, y)
ifsum(true, b, xs, y) → y
ifsum(false, b, xs, y) → ifsum2(b, xs, y)
ifsum2(true, xs, y) → sum2(tail(xs), y)
ifsum2(false, xs, y) → sum2(cons(p(head(xs)), tail(xs)), s(y))
isNil(nil) → true
isNil(cons(x, xs)) → false
tail(nil) → nil
tail(cons(x, xs)) → xs
head(cons(x, xs)) → x
head(nil) → error
isZero(0) → true
isZero(s(0)) → false
isZero(s(s(x))) → isZero(s(x))
p(0) → s(s(0))
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
ge(x, 0) → true
ge(0, s(y)) → false
ge(s(x), s(y)) → ge(x, y)
a → c
a → d
The set Q consists of the following terms:
times(x0, x1)
generate(x0, x1)
gen(x0, x1, x2)
if(true, x0, x1, x2)
if(false, x0, x1, x2)
sum(x0)
sum2(x0, x1)
ifsum(true, x0, x1, x2)
ifsum(false, x0, x1, x2)
ifsum2(true, x0, x1)
ifsum2(false, x0, x1)
isNil(nil)
isNil(cons(x0, x1))
tail(nil)
tail(cons(x0, x1))
head(cons(x0, x1))
head(nil)
isZero(0)
isZero(s(0))
isZero(s(s(x0)))
p(0)
p(s(0))
p(s(s(x0)))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
a
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:
P(s(s(x))) → P(s(x))
R is empty.
The set Q consists of the following terms:
times(x0, x1)
generate(x0, x1)
gen(x0, x1, x2)
if(true, x0, x1, x2)
if(false, x0, x1, x2)
sum(x0)
sum2(x0, x1)
ifsum(true, x0, x1, x2)
ifsum(false, x0, x1, x2)
ifsum2(true, x0, x1)
ifsum2(false, x0, x1)
isNil(nil)
isNil(cons(x0, x1))
tail(nil)
tail(cons(x0, x1))
head(cons(x0, x1))
head(nil)
isZero(0)
isZero(s(0))
isZero(s(s(x0)))
p(0)
p(s(0))
p(s(s(x0)))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
a
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].
times(x0, x1)
generate(x0, x1)
gen(x0, x1, x2)
if(true, x0, x1, x2)
if(false, x0, x1, x2)
sum(x0)
sum2(x0, x1)
ifsum(true, x0, x1, x2)
ifsum(false, x0, x1, x2)
ifsum2(true, x0, x1)
ifsum2(false, x0, x1)
isNil(nil)
isNil(cons(x0, x1))
tail(nil)
tail(cons(x0, x1))
head(cons(x0, x1))
head(nil)
isZero(0)
isZero(s(0))
isZero(s(s(x0)))
p(0)
p(s(0))
p(s(s(x0)))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
a
(18) 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.
(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:
- P(s(s(x))) → P(s(x))
The graph contains the following edges 1 > 1
(20) TRUE
(21) Obligation:
Q DP problem:
The TRS P consists of the following rules:
ISZERO(s(s(x))) → ISZERO(s(x))
The TRS R consists of the following rules:
times(x, y) → sum(generate(x, y))
generate(x, y) → gen(x, y, 0)
gen(x, y, z) → if(ge(z, x), x, y, z)
if(true, x, y, z) → nil
if(false, x, y, z) → cons(y, gen(x, y, s(z)))
sum(xs) → sum2(xs, 0)
sum2(xs, y) → ifsum(isNil(xs), isZero(head(xs)), xs, y)
ifsum(true, b, xs, y) → y
ifsum(false, b, xs, y) → ifsum2(b, xs, y)
ifsum2(true, xs, y) → sum2(tail(xs), y)
ifsum2(false, xs, y) → sum2(cons(p(head(xs)), tail(xs)), s(y))
isNil(nil) → true
isNil(cons(x, xs)) → false
tail(nil) → nil
tail(cons(x, xs)) → xs
head(cons(x, xs)) → x
head(nil) → error
isZero(0) → true
isZero(s(0)) → false
isZero(s(s(x))) → isZero(s(x))
p(0) → s(s(0))
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
ge(x, 0) → true
ge(0, s(y)) → false
ge(s(x), s(y)) → ge(x, y)
a → c
a → d
The set Q consists of the following terms:
times(x0, x1)
generate(x0, x1)
gen(x0, x1, x2)
if(true, x0, x1, x2)
if(false, x0, x1, x2)
sum(x0)
sum2(x0, x1)
ifsum(true, x0, x1, x2)
ifsum(false, x0, x1, x2)
ifsum2(true, x0, x1)
ifsum2(false, x0, x1)
isNil(nil)
isNil(cons(x0, x1))
tail(nil)
tail(cons(x0, x1))
head(cons(x0, x1))
head(nil)
isZero(0)
isZero(s(0))
isZero(s(s(x0)))
p(0)
p(s(0))
p(s(s(x0)))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
a
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:
ISZERO(s(s(x))) → ISZERO(s(x))
R is empty.
The set Q consists of the following terms:
times(x0, x1)
generate(x0, x1)
gen(x0, x1, x2)
if(true, x0, x1, x2)
if(false, x0, x1, x2)
sum(x0)
sum2(x0, x1)
ifsum(true, x0, x1, x2)
ifsum(false, x0, x1, x2)
ifsum2(true, x0, x1)
ifsum2(false, x0, x1)
isNil(nil)
isNil(cons(x0, x1))
tail(nil)
tail(cons(x0, x1))
head(cons(x0, x1))
head(nil)
isZero(0)
isZero(s(0))
isZero(s(s(x0)))
p(0)
p(s(0))
p(s(s(x0)))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
a
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].
times(x0, x1)
generate(x0, x1)
gen(x0, x1, x2)
if(true, x0, x1, x2)
if(false, x0, x1, x2)
sum(x0)
sum2(x0, x1)
ifsum(true, x0, x1, x2)
ifsum(false, x0, x1, x2)
ifsum2(true, x0, x1)
ifsum2(false, x0, x1)
isNil(nil)
isNil(cons(x0, x1))
tail(nil)
tail(cons(x0, x1))
head(cons(x0, x1))
head(nil)
isZero(0)
isZero(s(0))
isZero(s(s(x0)))
p(0)
p(s(0))
p(s(s(x0)))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
a
(25) Obligation:
Q DP problem:
The TRS P consists of the following rules:
ISZERO(s(s(x))) → ISZERO(s(x))
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:
- ISZERO(s(s(x))) → ISZERO(s(x))
The graph contains the following edges 1 > 1
(27) TRUE
(28) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IFSUM(false, b, xs, y) → IFSUM2(b, xs, y)
IFSUM2(true, xs, y) → SUM2(tail(xs), y)
SUM2(xs, y) → IFSUM(isNil(xs), isZero(head(xs)), xs, y)
IFSUM2(false, xs, y) → SUM2(cons(p(head(xs)), tail(xs)), s(y))
The TRS R consists of the following rules:
times(x, y) → sum(generate(x, y))
generate(x, y) → gen(x, y, 0)
gen(x, y, z) → if(ge(z, x), x, y, z)
if(true, x, y, z) → nil
if(false, x, y, z) → cons(y, gen(x, y, s(z)))
sum(xs) → sum2(xs, 0)
sum2(xs, y) → ifsum(isNil(xs), isZero(head(xs)), xs, y)
ifsum(true, b, xs, y) → y
ifsum(false, b, xs, y) → ifsum2(b, xs, y)
ifsum2(true, xs, y) → sum2(tail(xs), y)
ifsum2(false, xs, y) → sum2(cons(p(head(xs)), tail(xs)), s(y))
isNil(nil) → true
isNil(cons(x, xs)) → false
tail(nil) → nil
tail(cons(x, xs)) → xs
head(cons(x, xs)) → x
head(nil) → error
isZero(0) → true
isZero(s(0)) → false
isZero(s(s(x))) → isZero(s(x))
p(0) → s(s(0))
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
ge(x, 0) → true
ge(0, s(y)) → false
ge(s(x), s(y)) → ge(x, y)
a → c
a → d
The set Q consists of the following terms:
times(x0, x1)
generate(x0, x1)
gen(x0, x1, x2)
if(true, x0, x1, x2)
if(false, x0, x1, x2)
sum(x0)
sum2(x0, x1)
ifsum(true, x0, x1, x2)
ifsum(false, x0, x1, x2)
ifsum2(true, x0, x1)
ifsum2(false, x0, x1)
isNil(nil)
isNil(cons(x0, x1))
tail(nil)
tail(cons(x0, x1))
head(cons(x0, x1))
head(nil)
isZero(0)
isZero(s(0))
isZero(s(s(x0)))
p(0)
p(s(0))
p(s(s(x0)))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
a
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:
IFSUM(false, b, xs, y) → IFSUM2(b, xs, y)
IFSUM2(true, xs, y) → SUM2(tail(xs), y)
SUM2(xs, y) → IFSUM(isNil(xs), isZero(head(xs)), xs, y)
IFSUM2(false, xs, y) → SUM2(cons(p(head(xs)), tail(xs)), s(y))
The TRS R consists of the following rules:
head(cons(x, xs)) → x
head(nil) → error
p(0) → s(s(0))
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
tail(nil) → nil
tail(cons(x, xs)) → xs
isNil(nil) → true
isNil(cons(x, xs)) → false
isZero(0) → true
isZero(s(0)) → false
isZero(s(s(x))) → isZero(s(x))
The set Q consists of the following terms:
times(x0, x1)
generate(x0, x1)
gen(x0, x1, x2)
if(true, x0, x1, x2)
if(false, x0, x1, x2)
sum(x0)
sum2(x0, x1)
ifsum(true, x0, x1, x2)
ifsum(false, x0, x1, x2)
ifsum2(true, x0, x1)
ifsum2(false, x0, x1)
isNil(nil)
isNil(cons(x0, x1))
tail(nil)
tail(cons(x0, x1))
head(cons(x0, x1))
head(nil)
isZero(0)
isZero(s(0))
isZero(s(s(x0)))
p(0)
p(s(0))
p(s(s(x0)))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
a
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].
times(x0, x1)
generate(x0, x1)
gen(x0, x1, x2)
if(true, x0, x1, x2)
if(false, x0, x1, x2)
sum(x0)
sum2(x0, x1)
ifsum(true, x0, x1, x2)
ifsum(false, x0, x1, x2)
ifsum2(true, x0, x1)
ifsum2(false, x0, x1)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
a
(32) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IFSUM(false, b, xs, y) → IFSUM2(b, xs, y)
IFSUM2(true, xs, y) → SUM2(tail(xs), y)
SUM2(xs, y) → IFSUM(isNil(xs), isZero(head(xs)), xs, y)
IFSUM2(false, xs, y) → SUM2(cons(p(head(xs)), tail(xs)), s(y))
The TRS R consists of the following rules:
head(cons(x, xs)) → x
head(nil) → error
p(0) → s(s(0))
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
tail(nil) → nil
tail(cons(x, xs)) → xs
isNil(nil) → true
isNil(cons(x, xs)) → false
isZero(0) → true
isZero(s(0)) → false
isZero(s(s(x))) → isZero(s(x))
The set Q consists of the following terms:
isNil(nil)
isNil(cons(x0, x1))
tail(nil)
tail(cons(x0, x1))
head(cons(x0, x1))
head(nil)
isZero(0)
isZero(s(0))
isZero(s(s(x0)))
p(0)
p(s(0))
p(s(s(x0)))
We have to consider all minimal (P,Q,R)-chains.
(33) Narrowing (EQUIVALENT transformation)
By narrowing [LPAR04] the rule
SUM2(
xs,
y) →
IFSUM(
isNil(
xs),
isZero(
head(
xs)),
xs,
y) at position [0] we obtained the following new rules [LPAR04]:
SUM2(nil, y1) → IFSUM(true, isZero(head(nil)), nil, y1)
SUM2(cons(x0, x1), y1) → IFSUM(false, isZero(head(cons(x0, x1))), cons(x0, x1), y1)
(34) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IFSUM(false, b, xs, y) → IFSUM2(b, xs, y)
IFSUM2(true, xs, y) → SUM2(tail(xs), y)
IFSUM2(false, xs, y) → SUM2(cons(p(head(xs)), tail(xs)), s(y))
SUM2(nil, y1) → IFSUM(true, isZero(head(nil)), nil, y1)
SUM2(cons(x0, x1), y1) → IFSUM(false, isZero(head(cons(x0, x1))), cons(x0, x1), y1)
The TRS R consists of the following rules:
head(cons(x, xs)) → x
head(nil) → error
p(0) → s(s(0))
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
tail(nil) → nil
tail(cons(x, xs)) → xs
isNil(nil) → true
isNil(cons(x, xs)) → false
isZero(0) → true
isZero(s(0)) → false
isZero(s(s(x))) → isZero(s(x))
The set Q consists of the following terms:
isNil(nil)
isNil(cons(x0, x1))
tail(nil)
tail(cons(x0, x1))
head(cons(x0, x1))
head(nil)
isZero(0)
isZero(s(0))
isZero(s(s(x0)))
p(0)
p(s(0))
p(s(s(x0)))
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:
IFSUM2(true, xs, y) → SUM2(tail(xs), y)
SUM2(cons(x0, x1), y1) → IFSUM(false, isZero(head(cons(x0, x1))), cons(x0, x1), y1)
IFSUM(false, b, xs, y) → IFSUM2(b, xs, y)
IFSUM2(false, xs, y) → SUM2(cons(p(head(xs)), tail(xs)), s(y))
The TRS R consists of the following rules:
head(cons(x, xs)) → x
head(nil) → error
p(0) → s(s(0))
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
tail(nil) → nil
tail(cons(x, xs)) → xs
isNil(nil) → true
isNil(cons(x, xs)) → false
isZero(0) → true
isZero(s(0)) → false
isZero(s(s(x))) → isZero(s(x))
The set Q consists of the following terms:
isNil(nil)
isNil(cons(x0, x1))
tail(nil)
tail(cons(x0, x1))
head(cons(x0, x1))
head(nil)
isZero(0)
isZero(s(0))
isZero(s(s(x0)))
p(0)
p(s(0))
p(s(s(x0)))
We have to consider all minimal (P,Q,R)-chains.
(37) 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.
(38) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IFSUM2(true, xs, y) → SUM2(tail(xs), y)
SUM2(cons(x0, x1), y1) → IFSUM(false, isZero(head(cons(x0, x1))), cons(x0, x1), y1)
IFSUM(false, b, xs, y) → IFSUM2(b, xs, y)
IFSUM2(false, xs, y) → SUM2(cons(p(head(xs)), tail(xs)), s(y))
The TRS R consists of the following rules:
head(cons(x, xs)) → x
head(nil) → error
p(0) → s(s(0))
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
tail(nil) → nil
tail(cons(x, xs)) → xs
isZero(0) → true
isZero(s(0)) → false
isZero(s(s(x))) → isZero(s(x))
The set Q consists of the following terms:
isNil(nil)
isNil(cons(x0, x1))
tail(nil)
tail(cons(x0, x1))
head(cons(x0, x1))
head(nil)
isZero(0)
isZero(s(0))
isZero(s(s(x0)))
p(0)
p(s(0))
p(s(s(x0)))
We have to consider all minimal (P,Q,R)-chains.
(39) 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].
isNil(nil)
isNil(cons(x0, x1))
(40) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IFSUM2(true, xs, y) → SUM2(tail(xs), y)
SUM2(cons(x0, x1), y1) → IFSUM(false, isZero(head(cons(x0, x1))), cons(x0, x1), y1)
IFSUM(false, b, xs, y) → IFSUM2(b, xs, y)
IFSUM2(false, xs, y) → SUM2(cons(p(head(xs)), tail(xs)), s(y))
The TRS R consists of the following rules:
head(cons(x, xs)) → x
head(nil) → error
p(0) → s(s(0))
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
tail(nil) → nil
tail(cons(x, xs)) → xs
isZero(0) → true
isZero(s(0)) → false
isZero(s(s(x))) → isZero(s(x))
The set Q consists of the following terms:
tail(nil)
tail(cons(x0, x1))
head(cons(x0, x1))
head(nil)
isZero(0)
isZero(s(0))
isZero(s(s(x0)))
p(0)
p(s(0))
p(s(s(x0)))
We have to consider all minimal (P,Q,R)-chains.
(41) Rewriting (EQUIVALENT transformation)
By rewriting [LPAR04] the rule
SUM2(
cons(
x0,
x1),
y1) →
IFSUM(
false,
isZero(
head(
cons(
x0,
x1))),
cons(
x0,
x1),
y1) at position [1,0] we obtained the following new rules [LPAR04]:
SUM2(cons(x0, x1), y1) → IFSUM(false, isZero(x0), cons(x0, x1), y1)
(42) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IFSUM2(true, xs, y) → SUM2(tail(xs), y)
IFSUM(false, b, xs, y) → IFSUM2(b, xs, y)
IFSUM2(false, xs, y) → SUM2(cons(p(head(xs)), tail(xs)), s(y))
SUM2(cons(x0, x1), y1) → IFSUM(false, isZero(x0), cons(x0, x1), y1)
The TRS R consists of the following rules:
head(cons(x, xs)) → x
head(nil) → error
p(0) → s(s(0))
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
tail(nil) → nil
tail(cons(x, xs)) → xs
isZero(0) → true
isZero(s(0)) → false
isZero(s(s(x))) → isZero(s(x))
The set Q consists of the following terms:
tail(nil)
tail(cons(x0, x1))
head(cons(x0, x1))
head(nil)
isZero(0)
isZero(s(0))
isZero(s(s(x0)))
p(0)
p(s(0))
p(s(s(x0)))
We have to consider all minimal (P,Q,R)-chains.
(43) Narrowing (EQUIVALENT transformation)
By narrowing [LPAR04] the rule
IFSUM2(
true,
xs,
y) →
SUM2(
tail(
xs),
y) at position [0] we obtained the following new rules [LPAR04]:
IFSUM2(true, nil, y1) → SUM2(nil, y1)
IFSUM2(true, cons(x0, x1), y1) → SUM2(x1, y1)
(44) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IFSUM(false, b, xs, y) → IFSUM2(b, xs, y)
IFSUM2(false, xs, y) → SUM2(cons(p(head(xs)), tail(xs)), s(y))
SUM2(cons(x0, x1), y1) → IFSUM(false, isZero(x0), cons(x0, x1), y1)
IFSUM2(true, nil, y1) → SUM2(nil, y1)
IFSUM2(true, cons(x0, x1), y1) → SUM2(x1, y1)
The TRS R consists of the following rules:
head(cons(x, xs)) → x
head(nil) → error
p(0) → s(s(0))
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
tail(nil) → nil
tail(cons(x, xs)) → xs
isZero(0) → true
isZero(s(0)) → false
isZero(s(s(x))) → isZero(s(x))
The set Q consists of the following terms:
tail(nil)
tail(cons(x0, x1))
head(cons(x0, x1))
head(nil)
isZero(0)
isZero(s(0))
isZero(s(s(x0)))
p(0)
p(s(0))
p(s(s(x0)))
We have to consider all minimal (P,Q,R)-chains.
(45) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.
(46) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IFSUM2(false, xs, y) → SUM2(cons(p(head(xs)), tail(xs)), s(y))
SUM2(cons(x0, x1), y1) → IFSUM(false, isZero(x0), cons(x0, x1), y1)
IFSUM(false, b, xs, y) → IFSUM2(b, xs, y)
IFSUM2(true, cons(x0, x1), y1) → SUM2(x1, y1)
The TRS R consists of the following rules:
head(cons(x, xs)) → x
head(nil) → error
p(0) → s(s(0))
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
tail(nil) → nil
tail(cons(x, xs)) → xs
isZero(0) → true
isZero(s(0)) → false
isZero(s(s(x))) → isZero(s(x))
The set Q consists of the following terms:
tail(nil)
tail(cons(x0, x1))
head(cons(x0, x1))
head(nil)
isZero(0)
isZero(s(0))
isZero(s(s(x0)))
p(0)
p(s(0))
p(s(s(x0)))
We have to consider all minimal (P,Q,R)-chains.
(47) Instantiation (EQUIVALENT transformation)
By instantiating [LPAR04] the rule
IFSUM(
false,
b,
xs,
y) →
IFSUM2(
b,
xs,
y) we obtained the following new rules [LPAR04]:
IFSUM(false, y_0, cons(z0, z1), z2) → IFSUM2(y_0, cons(z0, z1), z2)
(48) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IFSUM2(false, xs, y) → SUM2(cons(p(head(xs)), tail(xs)), s(y))
SUM2(cons(x0, x1), y1) → IFSUM(false, isZero(x0), cons(x0, x1), y1)
IFSUM2(true, cons(x0, x1), y1) → SUM2(x1, y1)
IFSUM(false, y_0, cons(z0, z1), z2) → IFSUM2(y_0, cons(z0, z1), z2)
The TRS R consists of the following rules:
head(cons(x, xs)) → x
head(nil) → error
p(0) → s(s(0))
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
tail(nil) → nil
tail(cons(x, xs)) → xs
isZero(0) → true
isZero(s(0)) → false
isZero(s(s(x))) → isZero(s(x))
The set Q consists of the following terms:
tail(nil)
tail(cons(x0, x1))
head(cons(x0, x1))
head(nil)
isZero(0)
isZero(s(0))
isZero(s(s(x0)))
p(0)
p(s(0))
p(s(s(x0)))
We have to consider all minimal (P,Q,R)-chains.
(49) Instantiation (EQUIVALENT transformation)
By instantiating [LPAR04] the rule
IFSUM(
false,
b,
xs,
y) →
IFSUM2(
b,
xs,
y) we obtained the following new rules [LPAR04]:
IFSUM(false, y_0, cons(z0, z1), z2) → IFSUM2(y_0, cons(z0, z1), z2)
(50) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IFSUM2(false, xs, y) → SUM2(cons(p(head(xs)), tail(xs)), s(y))
SUM2(cons(x0, x1), y1) → IFSUM(false, isZero(x0), cons(x0, x1), y1)
IFSUM2(true, cons(x0, x1), y1) → SUM2(x1, y1)
IFSUM(false, y_0, cons(z0, z1), z2) → IFSUM2(y_0, cons(z0, z1), z2)
The TRS R consists of the following rules:
head(cons(x, xs)) → x
head(nil) → error
p(0) → s(s(0))
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
tail(nil) → nil
tail(cons(x, xs)) → xs
isZero(0) → true
isZero(s(0)) → false
isZero(s(s(x))) → isZero(s(x))
The set Q consists of the following terms:
tail(nil)
tail(cons(x0, x1))
head(cons(x0, x1))
head(nil)
isZero(0)
isZero(s(0))
isZero(s(s(x0)))
p(0)
p(s(0))
p(s(s(x0)))
We have to consider all minimal (P,Q,R)-chains.
(51) Instantiation (EQUIVALENT transformation)
By instantiating [LPAR04] the rule
IFSUM2(
false,
xs,
y) →
SUM2(
cons(
p(
head(
xs)),
tail(
xs)),
s(
y)) we obtained the following new rules [LPAR04]:
IFSUM2(false, cons(z1, z2), z3) → SUM2(cons(p(head(cons(z1, z2))), tail(cons(z1, z2))), s(z3))
(52) Obligation:
Q DP problem:
The TRS P consists of the following rules:
SUM2(cons(x0, x1), y1) → IFSUM(false, isZero(x0), cons(x0, x1), y1)
IFSUM2(true, cons(x0, x1), y1) → SUM2(x1, y1)
IFSUM(false, y_0, cons(z0, z1), z2) → IFSUM2(y_0, cons(z0, z1), z2)
IFSUM2(false, cons(z1, z2), z3) → SUM2(cons(p(head(cons(z1, z2))), tail(cons(z1, z2))), s(z3))
The TRS R consists of the following rules:
head(cons(x, xs)) → x
head(nil) → error
p(0) → s(s(0))
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
tail(nil) → nil
tail(cons(x, xs)) → xs
isZero(0) → true
isZero(s(0)) → false
isZero(s(s(x))) → isZero(s(x))
The set Q consists of the following terms:
tail(nil)
tail(cons(x0, x1))
head(cons(x0, x1))
head(nil)
isZero(0)
isZero(s(0))
isZero(s(s(x0)))
p(0)
p(s(0))
p(s(s(x0)))
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:
SUM2(cons(x0, x1), y1) → IFSUM(false, isZero(x0), cons(x0, x1), y1)
IFSUM2(true, cons(x0, x1), y1) → SUM2(x1, y1)
IFSUM(false, y_0, cons(z0, z1), z2) → IFSUM2(y_0, cons(z0, z1), z2)
IFSUM2(false, cons(z1, z2), z3) → SUM2(cons(p(head(cons(z1, z2))), tail(cons(z1, z2))), s(z3))
The TRS R consists of the following rules:
head(cons(x, xs)) → x
p(0) → s(s(0))
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
tail(cons(x, xs)) → xs
isZero(0) → true
isZero(s(0)) → false
isZero(s(s(x))) → isZero(s(x))
The set Q consists of the following terms:
tail(nil)
tail(cons(x0, x1))
head(cons(x0, x1))
head(nil)
isZero(0)
isZero(s(0))
isZero(s(s(x0)))
p(0)
p(s(0))
p(s(s(x0)))
We have to consider all minimal (P,Q,R)-chains.
(55) Rewriting (EQUIVALENT transformation)
By rewriting [LPAR04] the rule
IFSUM2(
false,
cons(
z1,
z2),
z3) →
SUM2(
cons(
p(
head(
cons(
z1,
z2))),
tail(
cons(
z1,
z2))),
s(
z3)) at position [0,0,0] we obtained the following new rules [LPAR04]:
IFSUM2(false, cons(z1, z2), z3) → SUM2(cons(p(z1), tail(cons(z1, z2))), s(z3))
(56) Obligation:
Q DP problem:
The TRS P consists of the following rules:
SUM2(cons(x0, x1), y1) → IFSUM(false, isZero(x0), cons(x0, x1), y1)
IFSUM2(true, cons(x0, x1), y1) → SUM2(x1, y1)
IFSUM(false, y_0, cons(z0, z1), z2) → IFSUM2(y_0, cons(z0, z1), z2)
IFSUM2(false, cons(z1, z2), z3) → SUM2(cons(p(z1), tail(cons(z1, z2))), s(z3))
The TRS R consists of the following rules:
head(cons(x, xs)) → x
p(0) → s(s(0))
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
tail(cons(x, xs)) → xs
isZero(0) → true
isZero(s(0)) → false
isZero(s(s(x))) → isZero(s(x))
The set Q consists of the following terms:
tail(nil)
tail(cons(x0, x1))
head(cons(x0, x1))
head(nil)
isZero(0)
isZero(s(0))
isZero(s(s(x0)))
p(0)
p(s(0))
p(s(s(x0)))
We have to consider all minimal (P,Q,R)-chains.
(57) UsableRulesProof (EQUIVALENT transformation)
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.
(58) Obligation:
Q DP problem:
The TRS P consists of the following rules:
SUM2(cons(x0, x1), y1) → IFSUM(false, isZero(x0), cons(x0, x1), y1)
IFSUM2(true, cons(x0, x1), y1) → SUM2(x1, y1)
IFSUM(false, y_0, cons(z0, z1), z2) → IFSUM2(y_0, cons(z0, z1), z2)
IFSUM2(false, cons(z1, z2), z3) → SUM2(cons(p(z1), tail(cons(z1, z2))), s(z3))
The TRS R consists of the following rules:
p(0) → s(s(0))
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
tail(cons(x, xs)) → xs
isZero(0) → true
isZero(s(0)) → false
isZero(s(s(x))) → isZero(s(x))
The set Q consists of the following terms:
tail(nil)
tail(cons(x0, x1))
head(cons(x0, x1))
head(nil)
isZero(0)
isZero(s(0))
isZero(s(s(x0)))
p(0)
p(s(0))
p(s(s(x0)))
We have to consider all minimal (P,Q,R)-chains.
(59) QReductionProof (EQUIVALENT transformation)
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].
head(cons(x0, x1))
head(nil)
(60) Obligation:
Q DP problem:
The TRS P consists of the following rules:
SUM2(cons(x0, x1), y1) → IFSUM(false, isZero(x0), cons(x0, x1), y1)
IFSUM2(true, cons(x0, x1), y1) → SUM2(x1, y1)
IFSUM(false, y_0, cons(z0, z1), z2) → IFSUM2(y_0, cons(z0, z1), z2)
IFSUM2(false, cons(z1, z2), z3) → SUM2(cons(p(z1), tail(cons(z1, z2))), s(z3))
The TRS R consists of the following rules:
p(0) → s(s(0))
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
tail(cons(x, xs)) → xs
isZero(0) → true
isZero(s(0)) → false
isZero(s(s(x))) → isZero(s(x))
The set Q consists of the following terms:
tail(nil)
tail(cons(x0, x1))
isZero(0)
isZero(s(0))
isZero(s(s(x0)))
p(0)
p(s(0))
p(s(s(x0)))
We have to consider all minimal (P,Q,R)-chains.
(61) Rewriting (EQUIVALENT transformation)
By rewriting [LPAR04] the rule
IFSUM2(
false,
cons(
z1,
z2),
z3) →
SUM2(
cons(
p(
z1),
tail(
cons(
z1,
z2))),
s(
z3)) at position [0,1] we obtained the following new rules [LPAR04]:
IFSUM2(false, cons(z1, z2), z3) → SUM2(cons(p(z1), z2), s(z3))
(62) Obligation:
Q DP problem:
The TRS P consists of the following rules:
SUM2(cons(x0, x1), y1) → IFSUM(false, isZero(x0), cons(x0, x1), y1)
IFSUM2(true, cons(x0, x1), y1) → SUM2(x1, y1)
IFSUM(false, y_0, cons(z0, z1), z2) → IFSUM2(y_0, cons(z0, z1), z2)
IFSUM2(false, cons(z1, z2), z3) → SUM2(cons(p(z1), z2), s(z3))
The TRS R consists of the following rules:
p(0) → s(s(0))
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
tail(cons(x, xs)) → xs
isZero(0) → true
isZero(s(0)) → false
isZero(s(s(x))) → isZero(s(x))
The set Q consists of the following terms:
tail(nil)
tail(cons(x0, x1))
isZero(0)
isZero(s(0))
isZero(s(s(x0)))
p(0)
p(s(0))
p(s(s(x0)))
We have to consider all minimal (P,Q,R)-chains.
(63) 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.
(64) Obligation:
Q DP problem:
The TRS P consists of the following rules:
SUM2(cons(x0, x1), y1) → IFSUM(false, isZero(x0), cons(x0, x1), y1)
IFSUM2(true, cons(x0, x1), y1) → SUM2(x1, y1)
IFSUM(false, y_0, cons(z0, z1), z2) → IFSUM2(y_0, cons(z0, z1), z2)
IFSUM2(false, cons(z1, z2), z3) → SUM2(cons(p(z1), z2), s(z3))
The TRS R consists of the following rules:
p(0) → s(s(0))
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
isZero(0) → true
isZero(s(0)) → false
isZero(s(s(x))) → isZero(s(x))
The set Q consists of the following terms:
tail(nil)
tail(cons(x0, x1))
isZero(0)
isZero(s(0))
isZero(s(s(x0)))
p(0)
p(s(0))
p(s(s(x0)))
We have to consider all minimal (P,Q,R)-chains.
(65) 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].
tail(nil)
tail(cons(x0, x1))
(66) Obligation:
Q DP problem:
The TRS P consists of the following rules:
SUM2(cons(x0, x1), y1) → IFSUM(false, isZero(x0), cons(x0, x1), y1)
IFSUM2(true, cons(x0, x1), y1) → SUM2(x1, y1)
IFSUM(false, y_0, cons(z0, z1), z2) → IFSUM2(y_0, cons(z0, z1), z2)
IFSUM2(false, cons(z1, z2), z3) → SUM2(cons(p(z1), z2), s(z3))
The TRS R consists of the following rules:
p(0) → s(s(0))
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
isZero(0) → true
isZero(s(0)) → false
isZero(s(s(x))) → isZero(s(x))
The set Q consists of the following terms:
isZero(0)
isZero(s(0))
isZero(s(s(x0)))
p(0)
p(s(0))
p(s(s(x0)))
We have to consider all minimal (P,Q,R)-chains.
(67) ForwardInstantiation (EQUIVALENT transformation)
By forward instantiating [JAR06] the rule
IFSUM2(
true,
cons(
x0,
x1),
y1) →
SUM2(
x1,
y1) we obtained the following new rules [LPAR04]:
IFSUM2(true, cons(x0, cons(y_0, y_1)), x2) → SUM2(cons(y_0, y_1), x2)
(68) Obligation:
Q DP problem:
The TRS P consists of the following rules:
SUM2(cons(x0, x1), y1) → IFSUM(false, isZero(x0), cons(x0, x1), y1)
IFSUM(false, y_0, cons(z0, z1), z2) → IFSUM2(y_0, cons(z0, z1), z2)
IFSUM2(false, cons(z1, z2), z3) → SUM2(cons(p(z1), z2), s(z3))
IFSUM2(true, cons(x0, cons(y_0, y_1)), x2) → SUM2(cons(y_0, y_1), x2)
The TRS R consists of the following rules:
p(0) → s(s(0))
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
isZero(0) → true
isZero(s(0)) → false
isZero(s(s(x))) → isZero(s(x))
The set Q consists of the following terms:
isZero(0)
isZero(s(0))
isZero(s(s(x0)))
p(0)
p(s(0))
p(s(s(x0)))
We have to consider all minimal (P,Q,R)-chains.
(69) ForwardInstantiation (EQUIVALENT transformation)
By forward instantiating [JAR06] the rule
IFSUM(
false,
y_0,
cons(
z0,
z1),
z2) →
IFSUM2(
y_0,
cons(
z0,
z1),
z2) we obtained the following new rules [LPAR04]:
IFSUM(false, false, cons(x1, x2), x3) → IFSUM2(false, cons(x1, x2), x3)
IFSUM(false, true, cons(x1, cons(y_1, y_2)), x3) → IFSUM2(true, cons(x1, cons(y_1, y_2)), x3)
(70) Obligation:
Q DP problem:
The TRS P consists of the following rules:
SUM2(cons(x0, x1), y1) → IFSUM(false, isZero(x0), cons(x0, x1), y1)
IFSUM2(false, cons(z1, z2), z3) → SUM2(cons(p(z1), z2), s(z3))
IFSUM2(true, cons(x0, cons(y_0, y_1)), x2) → SUM2(cons(y_0, y_1), x2)
IFSUM(false, false, cons(x1, x2), x3) → IFSUM2(false, cons(x1, x2), x3)
IFSUM(false, true, cons(x1, cons(y_1, y_2)), x3) → IFSUM2(true, cons(x1, cons(y_1, y_2)), x3)
The TRS R consists of the following rules:
p(0) → s(s(0))
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
isZero(0) → true
isZero(s(0)) → false
isZero(s(s(x))) → isZero(s(x))
The set Q consists of the following terms:
isZero(0)
isZero(s(0))
isZero(s(s(x0)))
p(0)
p(s(0))
p(s(s(x0)))
We have to consider all minimal (P,Q,R)-chains.
(71) Narrowing (EQUIVALENT transformation)
By narrowing [LPAR04] the rule
SUM2(
cons(
x0,
x1),
y1) →
IFSUM(
false,
isZero(
x0),
cons(
x0,
x1),
y1) at position [1] we obtained the following new rules [LPAR04]:
SUM2(cons(0, y1), y2) → IFSUM(false, true, cons(0, y1), y2)
SUM2(cons(s(0), y1), y2) → IFSUM(false, false, cons(s(0), y1), y2)
SUM2(cons(s(s(x0)), y1), y2) → IFSUM(false, isZero(s(x0)), cons(s(s(x0)), y1), y2)
(72) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IFSUM2(false, cons(z1, z2), z3) → SUM2(cons(p(z1), z2), s(z3))
IFSUM2(true, cons(x0, cons(y_0, y_1)), x2) → SUM2(cons(y_0, y_1), x2)
IFSUM(false, false, cons(x1, x2), x3) → IFSUM2(false, cons(x1, x2), x3)
IFSUM(false, true, cons(x1, cons(y_1, y_2)), x3) → IFSUM2(true, cons(x1, cons(y_1, y_2)), x3)
SUM2(cons(0, y1), y2) → IFSUM(false, true, cons(0, y1), y2)
SUM2(cons(s(0), y1), y2) → IFSUM(false, false, cons(s(0), y1), y2)
SUM2(cons(s(s(x0)), y1), y2) → IFSUM(false, isZero(s(x0)), cons(s(s(x0)), y1), y2)
The TRS R consists of the following rules:
p(0) → s(s(0))
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
isZero(0) → true
isZero(s(0)) → false
isZero(s(s(x))) → isZero(s(x))
The set Q consists of the following terms:
isZero(0)
isZero(s(0))
isZero(s(s(x0)))
p(0)
p(s(0))
p(s(s(x0)))
We have to consider all minimal (P,Q,R)-chains.
(73) 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.
(74) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IFSUM2(false, cons(z1, z2), z3) → SUM2(cons(p(z1), z2), s(z3))
IFSUM2(true, cons(x0, cons(y_0, y_1)), x2) → SUM2(cons(y_0, y_1), x2)
IFSUM(false, false, cons(x1, x2), x3) → IFSUM2(false, cons(x1, x2), x3)
IFSUM(false, true, cons(x1, cons(y_1, y_2)), x3) → IFSUM2(true, cons(x1, cons(y_1, y_2)), x3)
SUM2(cons(0, y1), y2) → IFSUM(false, true, cons(0, y1), y2)
SUM2(cons(s(0), y1), y2) → IFSUM(false, false, cons(s(0), y1), y2)
SUM2(cons(s(s(x0)), y1), y2) → IFSUM(false, isZero(s(x0)), cons(s(s(x0)), y1), y2)
The TRS R consists of the following rules:
isZero(s(0)) → false
isZero(s(s(x))) → isZero(s(x))
p(0) → s(s(0))
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
The set Q consists of the following terms:
isZero(0)
isZero(s(0))
isZero(s(s(x0)))
p(0)
p(s(0))
p(s(s(x0)))
We have to consider all minimal (P,Q,R)-chains.
(75) Narrowing (EQUIVALENT transformation)
By narrowing [LPAR04] the rule
IFSUM2(
false,
cons(
z1,
z2),
z3) →
SUM2(
cons(
p(
z1),
z2),
s(
z3)) at position [0,0] we obtained the following new rules [LPAR04]:
IFSUM2(false, cons(0, y1), y2) → SUM2(cons(s(s(0)), y1), s(y2))
IFSUM2(false, cons(s(0), y1), y2) → SUM2(cons(0, y1), s(y2))
IFSUM2(false, cons(s(s(x0)), y1), y2) → SUM2(cons(s(p(s(x0))), y1), s(y2))
(76) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IFSUM2(true, cons(x0, cons(y_0, y_1)), x2) → SUM2(cons(y_0, y_1), x2)
IFSUM(false, false, cons(x1, x2), x3) → IFSUM2(false, cons(x1, x2), x3)
IFSUM(false, true, cons(x1, cons(y_1, y_2)), x3) → IFSUM2(true, cons(x1, cons(y_1, y_2)), x3)
SUM2(cons(0, y1), y2) → IFSUM(false, true, cons(0, y1), y2)
SUM2(cons(s(0), y1), y2) → IFSUM(false, false, cons(s(0), y1), y2)
SUM2(cons(s(s(x0)), y1), y2) → IFSUM(false, isZero(s(x0)), cons(s(s(x0)), y1), y2)
IFSUM2(false, cons(0, y1), y2) → SUM2(cons(s(s(0)), y1), s(y2))
IFSUM2(false, cons(s(0), y1), y2) → SUM2(cons(0, y1), s(y2))
IFSUM2(false, cons(s(s(x0)), y1), y2) → SUM2(cons(s(p(s(x0))), y1), s(y2))
The TRS R consists of the following rules:
isZero(s(0)) → false
isZero(s(s(x))) → isZero(s(x))
p(0) → s(s(0))
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
The set Q consists of the following terms:
isZero(0)
isZero(s(0))
isZero(s(s(x0)))
p(0)
p(s(0))
p(s(s(x0)))
We have to consider all minimal (P,Q,R)-chains.
(77) 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.
(78) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IFSUM2(true, cons(x0, cons(y_0, y_1)), x2) → SUM2(cons(y_0, y_1), x2)
IFSUM(false, false, cons(x1, x2), x3) → IFSUM2(false, cons(x1, x2), x3)
IFSUM(false, true, cons(x1, cons(y_1, y_2)), x3) → IFSUM2(true, cons(x1, cons(y_1, y_2)), x3)
SUM2(cons(0, y1), y2) → IFSUM(false, true, cons(0, y1), y2)
SUM2(cons(s(0), y1), y2) → IFSUM(false, false, cons(s(0), y1), y2)
SUM2(cons(s(s(x0)), y1), y2) → IFSUM(false, isZero(s(x0)), cons(s(s(x0)), y1), y2)
IFSUM2(false, cons(0, y1), y2) → SUM2(cons(s(s(0)), y1), s(y2))
IFSUM2(false, cons(s(0), y1), y2) → SUM2(cons(0, y1), s(y2))
IFSUM2(false, cons(s(s(x0)), y1), y2) → SUM2(cons(s(p(s(x0))), y1), s(y2))
The TRS R consists of the following rules:
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
isZero(s(0)) → false
isZero(s(s(x))) → isZero(s(x))
The set Q consists of the following terms:
isZero(0)
isZero(s(0))
isZero(s(s(x0)))
p(0)
p(s(0))
p(s(s(x0)))
We have to consider all minimal (P,Q,R)-chains.
(79) Instantiation (EQUIVALENT transformation)
By instantiating [LPAR04] the rule
IFSUM(
false,
false,
cons(
x1,
x2),
x3) →
IFSUM2(
false,
cons(
x1,
x2),
x3) we obtained the following new rules [LPAR04]:
IFSUM(false, false, cons(s(0), z0), z1) → IFSUM2(false, cons(s(0), z0), z1)
IFSUM(false, false, cons(s(s(z0)), z1), z2) → IFSUM2(false, cons(s(s(z0)), z1), z2)
(80) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IFSUM2(true, cons(x0, cons(y_0, y_1)), x2) → SUM2(cons(y_0, y_1), x2)
IFSUM(false, true, cons(x1, cons(y_1, y_2)), x3) → IFSUM2(true, cons(x1, cons(y_1, y_2)), x3)
SUM2(cons(0, y1), y2) → IFSUM(false, true, cons(0, y1), y2)
SUM2(cons(s(0), y1), y2) → IFSUM(false, false, cons(s(0), y1), y2)
SUM2(cons(s(s(x0)), y1), y2) → IFSUM(false, isZero(s(x0)), cons(s(s(x0)), y1), y2)
IFSUM2(false, cons(0, y1), y2) → SUM2(cons(s(s(0)), y1), s(y2))
IFSUM2(false, cons(s(0), y1), y2) → SUM2(cons(0, y1), s(y2))
IFSUM2(false, cons(s(s(x0)), y1), y2) → SUM2(cons(s(p(s(x0))), y1), s(y2))
IFSUM(false, false, cons(s(0), z0), z1) → IFSUM2(false, cons(s(0), z0), z1)
IFSUM(false, false, cons(s(s(z0)), z1), z2) → IFSUM2(false, cons(s(s(z0)), z1), z2)
The TRS R consists of the following rules:
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
isZero(s(0)) → false
isZero(s(s(x))) → isZero(s(x))
The set Q consists of the following terms:
isZero(0)
isZero(s(0))
isZero(s(s(x0)))
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 1 SCC with 1 less node.
(82) Obligation:
Q DP problem:
The TRS P consists of the following rules:
SUM2(cons(0, y1), y2) → IFSUM(false, true, cons(0, y1), y2)
IFSUM(false, true, cons(x1, cons(y_1, y_2)), x3) → IFSUM2(true, cons(x1, cons(y_1, y_2)), x3)
IFSUM2(true, cons(x0, cons(y_0, y_1)), x2) → SUM2(cons(y_0, y_1), x2)
SUM2(cons(s(0), y1), y2) → IFSUM(false, false, cons(s(0), y1), y2)
IFSUM(false, false, cons(s(0), z0), z1) → IFSUM2(false, cons(s(0), z0), z1)
IFSUM2(false, cons(s(0), y1), y2) → SUM2(cons(0, y1), s(y2))
SUM2(cons(s(s(x0)), y1), y2) → IFSUM(false, isZero(s(x0)), cons(s(s(x0)), y1), y2)
IFSUM(false, false, cons(s(s(z0)), z1), z2) → IFSUM2(false, cons(s(s(z0)), z1), z2)
IFSUM2(false, cons(s(s(x0)), y1), y2) → SUM2(cons(s(p(s(x0))), y1), s(y2))
The TRS R consists of the following rules:
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
isZero(s(0)) → false
isZero(s(s(x))) → isZero(s(x))
The set Q consists of the following terms:
isZero(0)
isZero(s(0))
isZero(s(s(x0)))
p(0)
p(s(0))
p(s(s(x0)))
We have to consider all minimal (P,Q,R)-chains.
(83) Instantiation (EQUIVALENT transformation)
By instantiating [LPAR04] the rule
IFSUM(
false,
true,
cons(
x1,
cons(
y_1,
y_2)),
x3) →
IFSUM2(
true,
cons(
x1,
cons(
y_1,
y_2)),
x3) we obtained the following new rules [LPAR04]:
IFSUM(false, true, cons(0, cons(x1, x2)), z1) → IFSUM2(true, cons(0, cons(x1, x2)), z1)
(84) Obligation:
Q DP problem:
The TRS P consists of the following rules:
SUM2(cons(0, y1), y2) → IFSUM(false, true, cons(0, y1), y2)
IFSUM2(true, cons(x0, cons(y_0, y_1)), x2) → SUM2(cons(y_0, y_1), x2)
SUM2(cons(s(0), y1), y2) → IFSUM(false, false, cons(s(0), y1), y2)
IFSUM(false, false, cons(s(0), z0), z1) → IFSUM2(false, cons(s(0), z0), z1)
IFSUM2(false, cons(s(0), y1), y2) → SUM2(cons(0, y1), s(y2))
SUM2(cons(s(s(x0)), y1), y2) → IFSUM(false, isZero(s(x0)), cons(s(s(x0)), y1), y2)
IFSUM(false, false, cons(s(s(z0)), z1), z2) → IFSUM2(false, cons(s(s(z0)), z1), z2)
IFSUM2(false, cons(s(s(x0)), y1), y2) → SUM2(cons(s(p(s(x0))), y1), s(y2))
IFSUM(false, true, cons(0, cons(x1, x2)), z1) → IFSUM2(true, cons(0, cons(x1, x2)), z1)
The TRS R consists of the following rules:
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
isZero(s(0)) → false
isZero(s(s(x))) → isZero(s(x))
The set Q consists of the following terms:
isZero(0)
isZero(s(0))
isZero(s(s(x0)))
p(0)
p(s(0))
p(s(s(x0)))
We have to consider all minimal (P,Q,R)-chains.
(85) Instantiation (EQUIVALENT transformation)
By instantiating [LPAR04] the rule
IFSUM2(
true,
cons(
x0,
cons(
y_0,
y_1)),
x2) →
SUM2(
cons(
y_0,
y_1),
x2) we obtained the following new rules [LPAR04]:
IFSUM2(true, cons(0, cons(z0, z1)), z2) → SUM2(cons(z0, z1), z2)
(86) Obligation:
Q DP problem:
The TRS P consists of the following rules:
SUM2(cons(0, y1), y2) → IFSUM(false, true, cons(0, y1), y2)
SUM2(cons(s(0), y1), y2) → IFSUM(false, false, cons(s(0), y1), y2)
IFSUM(false, false, cons(s(0), z0), z1) → IFSUM2(false, cons(s(0), z0), z1)
IFSUM2(false, cons(s(0), y1), y2) → SUM2(cons(0, y1), s(y2))
SUM2(cons(s(s(x0)), y1), y2) → IFSUM(false, isZero(s(x0)), cons(s(s(x0)), y1), y2)
IFSUM(false, false, cons(s(s(z0)), z1), z2) → IFSUM2(false, cons(s(s(z0)), z1), z2)
IFSUM2(false, cons(s(s(x0)), y1), y2) → SUM2(cons(s(p(s(x0))), y1), s(y2))
IFSUM(false, true, cons(0, cons(x1, x2)), z1) → IFSUM2(true, cons(0, cons(x1, x2)), z1)
IFSUM2(true, cons(0, cons(z0, z1)), z2) → SUM2(cons(z0, z1), z2)
The TRS R consists of the following rules:
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
isZero(s(0)) → false
isZero(s(s(x))) → isZero(s(x))
The set Q consists of the following terms:
isZero(0)
isZero(s(0))
isZero(s(s(x0)))
p(0)
p(s(0))
p(s(s(x0)))
We have to consider all minimal (P,Q,R)-chains.
(87) ForwardInstantiation (EQUIVALENT transformation)
By forward instantiating [JAR06] the rule
SUM2(
cons(
0,
y1),
y2) →
IFSUM(
false,
true,
cons(
0,
y1),
y2) we obtained the following new rules [LPAR04]:
SUM2(cons(0, cons(y_0, y_1)), x1) → IFSUM(false, true, cons(0, cons(y_0, y_1)), x1)
(88) Obligation:
Q DP problem:
The TRS P consists of the following rules:
SUM2(cons(s(0), y1), y2) → IFSUM(false, false, cons(s(0), y1), y2)
IFSUM(false, false, cons(s(0), z0), z1) → IFSUM2(false, cons(s(0), z0), z1)
IFSUM2(false, cons(s(0), y1), y2) → SUM2(cons(0, y1), s(y2))
SUM2(cons(s(s(x0)), y1), y2) → IFSUM(false, isZero(s(x0)), cons(s(s(x0)), y1), y2)
IFSUM(false, false, cons(s(s(z0)), z1), z2) → IFSUM2(false, cons(s(s(z0)), z1), z2)
IFSUM2(false, cons(s(s(x0)), y1), y2) → SUM2(cons(s(p(s(x0))), y1), s(y2))
IFSUM(false, true, cons(0, cons(x1, x2)), z1) → IFSUM2(true, cons(0, cons(x1, x2)), z1)
IFSUM2(true, cons(0, cons(z0, z1)), z2) → SUM2(cons(z0, z1), z2)
SUM2(cons(0, cons(y_0, y_1)), x1) → IFSUM(false, true, cons(0, cons(y_0, y_1)), x1)
The TRS R consists of the following rules:
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
isZero(s(0)) → false
isZero(s(s(x))) → isZero(s(x))
The set Q consists of the following terms:
isZero(0)
isZero(s(0))
isZero(s(s(x0)))
p(0)
p(s(0))
p(s(s(x0)))
We have to consider all minimal (P,Q,R)-chains.
(89) ForwardInstantiation (EQUIVALENT transformation)
By forward instantiating [JAR06] the rule
IFSUM2(
false,
cons(
s(
0),
y1),
y2) →
SUM2(
cons(
0,
y1),
s(
y2)) we obtained the following new rules [LPAR04]:
IFSUM2(false, cons(s(0), cons(y_0, y_1)), x1) → SUM2(cons(0, cons(y_0, y_1)), s(x1))
(90) Obligation:
Q DP problem:
The TRS P consists of the following rules:
SUM2(cons(s(0), y1), y2) → IFSUM(false, false, cons(s(0), y1), y2)
IFSUM(false, false, cons(s(0), z0), z1) → IFSUM2(false, cons(s(0), z0), z1)
SUM2(cons(s(s(x0)), y1), y2) → IFSUM(false, isZero(s(x0)), cons(s(s(x0)), y1), y2)
IFSUM(false, false, cons(s(s(z0)), z1), z2) → IFSUM2(false, cons(s(s(z0)), z1), z2)
IFSUM2(false, cons(s(s(x0)), y1), y2) → SUM2(cons(s(p(s(x0))), y1), s(y2))
IFSUM(false, true, cons(0, cons(x1, x2)), z1) → IFSUM2(true, cons(0, cons(x1, x2)), z1)
IFSUM2(true, cons(0, cons(z0, z1)), z2) → SUM2(cons(z0, z1), z2)
SUM2(cons(0, cons(y_0, y_1)), x1) → IFSUM(false, true, cons(0, cons(y_0, y_1)), x1)
IFSUM2(false, cons(s(0), cons(y_0, y_1)), x1) → SUM2(cons(0, cons(y_0, y_1)), s(x1))
The TRS R consists of the following rules:
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
isZero(s(0)) → false
isZero(s(s(x))) → isZero(s(x))
The set Q consists of the following terms:
isZero(0)
isZero(s(0))
isZero(s(s(x0)))
p(0)
p(s(0))
p(s(s(x0)))
We have to consider all minimal (P,Q,R)-chains.
(91) QDPOrderProof (EQUIVALENT transformation)
We use the reduction pair processor [LPAR04].
The following pairs can be oriented strictly and are deleted.
IFSUM2(false, cons(s(0), cons(y_0, y_1)), x1) → SUM2(cons(0, cons(y_0, y_1)), s(x1))
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:
POL(0) = 0
POL(IFSUM(x1, x2, x3, x4)) = x3
POL(IFSUM2(x1, x2, x3)) = x2
POL(SUM2(x1, x2)) = x1
POL(cons(x1, x2)) = x1 + x2
POL(false) = 0
POL(isZero(x1)) = 0
POL(p(x1)) = 1 + x1
POL(s(x1)) = 1
POL(true) = 0
The following usable rules [FROCOS05] were oriented:
none
(92) Obligation:
Q DP problem:
The TRS P consists of the following rules:
SUM2(cons(s(0), y1), y2) → IFSUM(false, false, cons(s(0), y1), y2)
IFSUM(false, false, cons(s(0), z0), z1) → IFSUM2(false, cons(s(0), z0), z1)
SUM2(cons(s(s(x0)), y1), y2) → IFSUM(false, isZero(s(x0)), cons(s(s(x0)), y1), y2)
IFSUM(false, false, cons(s(s(z0)), z1), z2) → IFSUM2(false, cons(s(s(z0)), z1), z2)
IFSUM2(false, cons(s(s(x0)), y1), y2) → SUM2(cons(s(p(s(x0))), y1), s(y2))
IFSUM(false, true, cons(0, cons(x1, x2)), z1) → IFSUM2(true, cons(0, cons(x1, x2)), z1)
IFSUM2(true, cons(0, cons(z0, z1)), z2) → SUM2(cons(z0, z1), z2)
SUM2(cons(0, cons(y_0, y_1)), x1) → IFSUM(false, true, cons(0, cons(y_0, y_1)), x1)
The TRS R consists of the following rules:
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
isZero(s(0)) → false
isZero(s(s(x))) → isZero(s(x))
The set Q consists of the following terms:
isZero(0)
isZero(s(0))
isZero(s(s(x0)))
p(0)
p(s(0))
p(s(s(x0)))
We have to consider all minimal (P,Q,R)-chains.
(93) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 2 SCCs with 2 less nodes.
(94) Complex Obligation (AND)
(95) Obligation:
Q DP problem:
The TRS P consists of the following rules:
SUM2(cons(s(s(x0)), y1), y2) → IFSUM(false, isZero(s(x0)), cons(s(s(x0)), y1), y2)
IFSUM(false, false, cons(s(s(z0)), z1), z2) → IFSUM2(false, cons(s(s(z0)), z1), z2)
IFSUM2(false, cons(s(s(x0)), y1), y2) → SUM2(cons(s(p(s(x0))), y1), s(y2))
The TRS R consists of the following rules:
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
isZero(s(0)) → false
isZero(s(s(x))) → isZero(s(x))
The set Q consists of the following terms:
isZero(0)
isZero(s(0))
isZero(s(s(x0)))
p(0)
p(s(0))
p(s(s(x0)))
We have to consider all minimal (P,Q,R)-chains.
(96) QDPOrderProof (EQUIVALENT transformation)
We use the reduction pair processor [LPAR04].
The following pairs can be oriented strictly and are deleted.
IFSUM2(false, cons(s(s(x0)), y1), y2) → SUM2(cons(s(p(s(x0))), y1), s(y2))
The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO]:
POL(SUM2(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(cons(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(IFSUM(x1, x2, x3, x4)) = | | + | | · | x1 | + | | · | x2 | + | | · | x3 | + | | · | x4 |
POL(IFSUM2(x1, x2, x3)) = | | + | | · | x1 | + | | · | x2 | + | | · | x3 |
The following usable rules [FROCOS05] were oriented:
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
(97) Obligation:
Q DP problem:
The TRS P consists of the following rules:
SUM2(cons(s(s(x0)), y1), y2) → IFSUM(false, isZero(s(x0)), cons(s(s(x0)), y1), y2)
IFSUM(false, false, cons(s(s(z0)), z1), z2) → IFSUM2(false, cons(s(s(z0)), z1), z2)
The TRS R consists of the following rules:
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
isZero(s(0)) → false
isZero(s(s(x))) → isZero(s(x))
The set Q consists of the following terms:
isZero(0)
isZero(s(0))
isZero(s(s(x0)))
p(0)
p(s(0))
p(s(s(x0)))
We have to consider all minimal (P,Q,R)-chains.
(98) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 2 less nodes.
(99) TRUE
(100) Obligation:
Q DP problem:
The TRS P consists of the following rules:
SUM2(cons(0, cons(y_0, y_1)), x1) → IFSUM(false, true, cons(0, cons(y_0, y_1)), x1)
IFSUM(false, true, cons(0, cons(x1, x2)), z1) → IFSUM2(true, cons(0, cons(x1, x2)), z1)
IFSUM2(true, cons(0, cons(z0, z1)), z2) → SUM2(cons(z0, z1), z2)
The TRS R consists of the following rules:
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
isZero(s(0)) → false
isZero(s(s(x))) → isZero(s(x))
The set Q consists of the following terms:
isZero(0)
isZero(s(0))
isZero(s(s(x0)))
p(0)
p(s(0))
p(s(s(x0)))
We have to consider all minimal (P,Q,R)-chains.
(101) 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.
(102) Obligation:
Q DP problem:
The TRS P consists of the following rules:
SUM2(cons(0, cons(y_0, y_1)), x1) → IFSUM(false, true, cons(0, cons(y_0, y_1)), x1)
IFSUM(false, true, cons(0, cons(x1, x2)), z1) → IFSUM2(true, cons(0, cons(x1, x2)), z1)
IFSUM2(true, cons(0, cons(z0, z1)), z2) → SUM2(cons(z0, z1), z2)
R is empty.
The set Q consists of the following terms:
isZero(0)
isZero(s(0))
isZero(s(s(x0)))
p(0)
p(s(0))
p(s(s(x0)))
We have to consider all minimal (P,Q,R)-chains.
(103) 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].
isZero(0)
isZero(s(0))
isZero(s(s(x0)))
p(0)
p(s(0))
p(s(s(x0)))
(104) Obligation:
Q DP problem:
The TRS P consists of the following rules:
SUM2(cons(0, cons(y_0, y_1)), x1) → IFSUM(false, true, cons(0, cons(y_0, y_1)), x1)
IFSUM(false, true, cons(0, cons(x1, x2)), z1) → IFSUM2(true, cons(0, cons(x1, x2)), z1)
IFSUM2(true, cons(0, cons(z0, z1)), z2) → SUM2(cons(z0, z1), z2)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(105) 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:
- IFSUM(false, true, cons(0, cons(x1, x2)), z1) → IFSUM2(true, cons(0, cons(x1, x2)), z1)
The graph contains the following edges 2 >= 1, 3 >= 2, 4 >= 3
- IFSUM2(true, cons(0, cons(z0, z1)), z2) → SUM2(cons(z0, z1), z2)
The graph contains the following edges 2 > 1, 3 >= 2
- SUM2(cons(0, cons(y_0, y_1)), x1) → IFSUM(false, true, cons(0, cons(y_0, y_1)), x1)
The graph contains the following edges 1 >= 3, 2 >= 4
(106) TRUE
(107) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IF(false, x, y, z) → GEN(x, y, s(z))
GEN(x, y, z) → IF(ge(z, x), x, y, z)
The TRS R consists of the following rules:
times(x, y) → sum(generate(x, y))
generate(x, y) → gen(x, y, 0)
gen(x, y, z) → if(ge(z, x), x, y, z)
if(true, x, y, z) → nil
if(false, x, y, z) → cons(y, gen(x, y, s(z)))
sum(xs) → sum2(xs, 0)
sum2(xs, y) → ifsum(isNil(xs), isZero(head(xs)), xs, y)
ifsum(true, b, xs, y) → y
ifsum(false, b, xs, y) → ifsum2(b, xs, y)
ifsum2(true, xs, y) → sum2(tail(xs), y)
ifsum2(false, xs, y) → sum2(cons(p(head(xs)), tail(xs)), s(y))
isNil(nil) → true
isNil(cons(x, xs)) → false
tail(nil) → nil
tail(cons(x, xs)) → xs
head(cons(x, xs)) → x
head(nil) → error
isZero(0) → true
isZero(s(0)) → false
isZero(s(s(x))) → isZero(s(x))
p(0) → s(s(0))
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
ge(x, 0) → true
ge(0, s(y)) → false
ge(s(x), s(y)) → ge(x, y)
a → c
a → d
The set Q consists of the following terms:
times(x0, x1)
generate(x0, x1)
gen(x0, x1, x2)
if(true, x0, x1, x2)
if(false, x0, x1, x2)
sum(x0)
sum2(x0, x1)
ifsum(true, x0, x1, x2)
ifsum(false, x0, x1, x2)
ifsum2(true, x0, x1)
ifsum2(false, x0, x1)
isNil(nil)
isNil(cons(x0, x1))
tail(nil)
tail(cons(x0, x1))
head(cons(x0, x1))
head(nil)
isZero(0)
isZero(s(0))
isZero(s(s(x0)))
p(0)
p(s(0))
p(s(s(x0)))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
a
We have to consider all minimal (P,Q,R)-chains.
(108) 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.
(109) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IF(false, x, y, z) → GEN(x, y, s(z))
GEN(x, y, z) → IF(ge(z, x), x, y, z)
The TRS R consists of the following rules:
ge(x, 0) → true
ge(0, s(y)) → false
ge(s(x), s(y)) → ge(x, y)
The set Q consists of the following terms:
times(x0, x1)
generate(x0, x1)
gen(x0, x1, x2)
if(true, x0, x1, x2)
if(false, x0, x1, x2)
sum(x0)
sum2(x0, x1)
ifsum(true, x0, x1, x2)
ifsum(false, x0, x1, x2)
ifsum2(true, x0, x1)
ifsum2(false, x0, x1)
isNil(nil)
isNil(cons(x0, x1))
tail(nil)
tail(cons(x0, x1))
head(cons(x0, x1))
head(nil)
isZero(0)
isZero(s(0))
isZero(s(s(x0)))
p(0)
p(s(0))
p(s(s(x0)))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
a
We have to consider all minimal (P,Q,R)-chains.
(110) 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].
times(x0, x1)
generate(x0, x1)
gen(x0, x1, x2)
if(true, x0, x1, x2)
if(false, x0, x1, x2)
sum(x0)
sum2(x0, x1)
ifsum(true, x0, x1, x2)
ifsum(false, x0, x1, x2)
ifsum2(true, x0, x1)
ifsum2(false, x0, x1)
isNil(nil)
isNil(cons(x0, x1))
tail(nil)
tail(cons(x0, x1))
head(cons(x0, x1))
head(nil)
isZero(0)
isZero(s(0))
isZero(s(s(x0)))
p(0)
p(s(0))
p(s(s(x0)))
a
(111) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IF(false, x, y, z) → GEN(x, y, s(z))
GEN(x, y, z) → IF(ge(z, x), x, y, z)
The TRS R consists of the following rules:
ge(x, 0) → true
ge(0, s(y)) → false
ge(s(x), s(y)) → ge(x, y)
The set Q consists of the following terms:
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
We have to consider all minimal (P,Q,R)-chains.
(112) Instantiation (EQUIVALENT transformation)
By instantiating [LPAR04] the rule
GEN(
x,
y,
z) →
IF(
ge(
z,
x),
x,
y,
z) we obtained the following new rules [LPAR04]:
GEN(z0, z1, s(z2)) → IF(ge(s(z2), z0), z0, z1, s(z2))
(113) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IF(false, x, y, z) → GEN(x, y, s(z))
GEN(z0, z1, s(z2)) → IF(ge(s(z2), z0), z0, z1, s(z2))
The TRS R consists of the following rules:
ge(x, 0) → true
ge(0, s(y)) → false
ge(s(x), s(y)) → ge(x, y)
The set Q consists of the following terms:
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
We have to consider all minimal (P,Q,R)-chains.
(114) NonInfProof (EQUIVALENT transformation)
The DP Problem is simplified using the Induction Calculus [NONINF] with the following steps:
Note that
final constraints are written in
bold face.
For Pair
IF(
false,
x,
y,
z) →
GEN(
x,
y,
s(
z)) the following chains were created:
- We consider the chain GEN(x, y, z) → IF(ge(z, x), x, y, z), IF(false, x, y, z) → GEN(x, y, s(z)) which results in the following constraint:
(1) (IF(ge(x5, x3), x3, x4, x5)=IF(false, x6, x7, x8) ⇒ IF(false, x6, x7, x8)≥GEN(x6, x7, s(x8)))
We simplified constraint (1) using rules (I), (II), (III) which results in the following new constraint:
(2) (ge(x5, x3)=false ⇒ IF(false, x3, x4, x5)≥GEN(x3, x4, s(x5)))
We simplified constraint (2) using rule (V) (with possible (I) afterwards) using induction on ge(x5, x3)=false which results in the following new constraints:
(3) (false=false ⇒ IF(false, s(x19), x4, 0)≥GEN(s(x19), x4, s(0)))
(4) (ge(x21, x20)=false∧(∀x22:ge(x21, x20)=false ⇒ IF(false, x20, x22, x21)≥GEN(x20, x22, s(x21))) ⇒ IF(false, s(x20), x4, s(x21))≥GEN(s(x20), x4, s(s(x21))))
We simplified constraint (3) using rules (I), (II) which results in the following new constraint:
(5) (IF(false, s(x19), x4, 0)≥GEN(s(x19), x4, s(0)))
We simplified constraint (4) using rule (VI) where we applied the induction hypothesis (∀x22:ge(x21, x20)=false ⇒ IF(false, x20, x22, x21)≥GEN(x20, x22, s(x21))) with σ = [x22 / x4] which results in the following new constraint:
(6) (IF(false, x20, x4, x21)≥GEN(x20, x4, s(x21)) ⇒ IF(false, s(x20), x4, s(x21))≥GEN(s(x20), x4, s(s(x21))))
For Pair
GEN(
x,
y,
z) →
IF(
ge(
z,
x),
x,
y,
z) the following chains were created:
- We consider the chain IF(false, x, y, z) → GEN(x, y, s(z)), GEN(x, y, z) → IF(ge(z, x), x, y, z) which results in the following constraint:
(7) (GEN(x9, x10, s(x11))=GEN(x12, x13, x14) ⇒ GEN(x12, x13, x14)≥IF(ge(x14, x12), x12, x13, x14))
We simplified constraint (7) using rules (I), (II), (III) which results in the following new constraint:
(8) (GEN(x9, x10, s(x11))≥IF(ge(s(x11), x9), x9, x10, s(x11)))
To summarize, we get the following constraints P
≥ for the following pairs.
- IF(false, x, y, z) → GEN(x, y, s(z))
- (IF(false, s(x19), x4, 0)≥GEN(s(x19), x4, s(0)))
- (IF(false, x20, x4, x21)≥GEN(x20, x4, s(x21)) ⇒ IF(false, s(x20), x4, s(x21))≥GEN(s(x20), x4, s(s(x21))))
- GEN(x, y, z) → IF(ge(z, x), x, y, z)
- (GEN(x9, x10, s(x11))≥IF(ge(s(x11), x9), x9, x10, s(x11)))
The constraints for P
> respective P
bound are constructed from P
≥ where we just replace every occurence of "t ≥ s" in P
≥ by "t > s" respective "t ≥
c". Here
c stands for the fresh constant used for P
bound.
Using the following integer polynomial ordering the resulting constraints can be solved
Polynomial interpretation [NONINF]:
POL(0) = 1
POL(GEN(x1, x2, x3)) = -1 + x1 - x3
POL(IF(x1, x2, x3, x4)) = -1 + x2 - x4
POL(c) = -2
POL(false) = 1
POL(ge(x1, x2)) = 0
POL(s(x1)) = 1 + x1
POL(true) = 0
The following pairs are in P
>:
IF(false, x, y, z) → GEN(x, y, s(z))
The following pairs are in P
bound:
IF(false, x, y, z) → GEN(x, y, s(z))
There are no usable rules
(115) Obligation:
Q DP problem:
The TRS P consists of the following rules:
GEN(x, y, z) → IF(ge(z, x), x, y, z)
The TRS R consists of the following rules:
ge(x, 0) → true
ge(0, s(y)) → false
ge(s(x), s(y)) → ge(x, y)
The set Q consists of the following terms:
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
We have to consider all minimal (P,Q,R)-chains.
(116) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 1 less node.
(117) TRUE