(0) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
plus(x, y) → ifPlus(isZero(x), x, inc(y))
ifPlus(true, x, y) → p(y)
ifPlus(false, x, y) → plus(p(x), y)
times(x, y) → timesIter(0, x, y, 0)
timesIter(i, x, y, z) → ifTimes(ge(i, x), i, x, y, z)
ifTimes(true, i, x, y, z) → z
ifTimes(false, i, x, y, z) → timesIter(inc(i), x, y, plus(z, y))
isZero(0) → true
isZero(s(0)) → false
isZero(s(s(x))) → isZero(s(x))
inc(0) → s(0)
inc(s(x)) → s(inc(x))
inc(x) → s(x)
p(0) → 0
p(s(x)) → x
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)
f0(0, y, x) → f1(x, y, x)
f1(x, y, z) → f2(x, y, z)
f2(x, 1, z) → f0(x, z, z)
f0(x, y, z) → d
f1(x, y, z) → c
Q is empty.
(1) AAECC Innermost (EQUIVALENT transformation)
We have applied [NOC,AAECCNOC] to switch to innermost. The TRS R 1 is
ifTimes(true, i, x, y, z) → z
ifTimes(false, i, x, y, z) → timesIter(inc(i), x, y, plus(z, y))
isZero(0) → true
isZero(s(0)) → false
isZero(s(s(x))) → isZero(s(x))
inc(0) → s(0)
inc(s(x)) → s(inc(x))
inc(x) → s(x)
p(0) → 0
p(s(x)) → x
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)
plus(x, y) → ifPlus(isZero(x), x, inc(y))
ifPlus(true, x, y) → p(y)
ifPlus(false, x, y) → plus(p(x), y)
times(x, y) → timesIter(0, x, y, 0)
timesIter(i, x, y, z) → ifTimes(ge(i, x), i, x, y, z)
The TRS R 2 is
f0(0, y, x) → f1(x, y, x)
f1(x, y, z) → f2(x, y, z)
f2(x, 1, z) → f0(x, z, z)
f0(x, y, z) → d
f1(x, y, z) → c
The signature Sigma is {
c,
f2,
d,
f0,
f1}
(2) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
plus(x, y) → ifPlus(isZero(x), x, inc(y))
ifPlus(true, x, y) → p(y)
ifPlus(false, x, y) → plus(p(x), y)
times(x, y) → timesIter(0, x, y, 0)
timesIter(i, x, y, z) → ifTimes(ge(i, x), i, x, y, z)
ifTimes(true, i, x, y, z) → z
ifTimes(false, i, x, y, z) → timesIter(inc(i), x, y, plus(z, y))
isZero(0) → true
isZero(s(0)) → false
isZero(s(s(x))) → isZero(s(x))
inc(0) → s(0)
inc(s(x)) → s(inc(x))
inc(x) → s(x)
p(0) → 0
p(s(x)) → x
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)
f0(0, y, x) → f1(x, y, x)
f1(x, y, z) → f2(x, y, z)
f2(x, 1, z) → f0(x, z, z)
f0(x, y, z) → d
f1(x, y, z) → c
The set Q consists of the following terms:
plus(x0, x1)
ifPlus(true, x0, x1)
ifPlus(false, x0, x1)
times(x0, x1)
timesIter(x0, x1, x2, x3)
ifTimes(true, x0, x1, x2, x3)
ifTimes(false, x0, x1, x2, x3)
isZero(0)
isZero(s(0))
isZero(s(s(x0)))
inc(x0)
p(0)
p(s(x0))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
f1(x0, x1, x2)
f2(x0, 1, x1)
f0(x0, x1, x2)
(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:
PLUS(x, y) → IFPLUS(isZero(x), x, inc(y))
PLUS(x, y) → ISZERO(x)
PLUS(x, y) → INC(y)
IFPLUS(true, x, y) → P(y)
IFPLUS(false, x, y) → PLUS(p(x), y)
IFPLUS(false, x, y) → P(x)
TIMES(x, y) → TIMESITER(0, x, y, 0)
TIMESITER(i, x, y, z) → IFTIMES(ge(i, x), i, x, y, z)
TIMESITER(i, x, y, z) → GE(i, x)
IFTIMES(false, i, x, y, z) → TIMESITER(inc(i), x, y, plus(z, y))
IFTIMES(false, i, x, y, z) → INC(i)
IFTIMES(false, i, x, y, z) → PLUS(z, y)
ISZERO(s(s(x))) → ISZERO(s(x))
INC(s(x)) → INC(x)
P(s(s(x))) → P(s(x))
GE(s(x), s(y)) → GE(x, y)
F0(0, y, x) → F1(x, y, x)
F1(x, y, z) → F2(x, y, z)
F2(x, 1, z) → F0(x, z, z)
The TRS R consists of the following rules:
plus(x, y) → ifPlus(isZero(x), x, inc(y))
ifPlus(true, x, y) → p(y)
ifPlus(false, x, y) → plus(p(x), y)
times(x, y) → timesIter(0, x, y, 0)
timesIter(i, x, y, z) → ifTimes(ge(i, x), i, x, y, z)
ifTimes(true, i, x, y, z) → z
ifTimes(false, i, x, y, z) → timesIter(inc(i), x, y, plus(z, y))
isZero(0) → true
isZero(s(0)) → false
isZero(s(s(x))) → isZero(s(x))
inc(0) → s(0)
inc(s(x)) → s(inc(x))
inc(x) → s(x)
p(0) → 0
p(s(x)) → x
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)
f0(0, y, x) → f1(x, y, x)
f1(x, y, z) → f2(x, y, z)
f2(x, 1, z) → f0(x, z, z)
f0(x, y, z) → d
f1(x, y, z) → c
The set Q consists of the following terms:
plus(x0, x1)
ifPlus(true, x0, x1)
ifPlus(false, x0, x1)
times(x0, x1)
timesIter(x0, x1, x2, x3)
ifTimes(true, x0, x1, x2, x3)
ifTimes(false, x0, x1, x2, x3)
isZero(0)
isZero(s(0))
isZero(s(s(x0)))
inc(x0)
p(0)
p(s(x0))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
f1(x0, x1, x2)
f2(x0, 1, x1)
f0(x0, x1, x2)
We have to consider all minimal (P,Q,R)-chains.
(5) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 7 SCCs with 8 less nodes.
(6) Complex Obligation (AND)
(7) Obligation:
Q DP problem:
The TRS P consists of the following rules:
F1(x, y, z) → F2(x, y, z)
F2(x, 1, z) → F0(x, z, z)
F0(0, y, x) → F1(x, y, x)
The TRS R consists of the following rules:
plus(x, y) → ifPlus(isZero(x), x, inc(y))
ifPlus(true, x, y) → p(y)
ifPlus(false, x, y) → plus(p(x), y)
times(x, y) → timesIter(0, x, y, 0)
timesIter(i, x, y, z) → ifTimes(ge(i, x), i, x, y, z)
ifTimes(true, i, x, y, z) → z
ifTimes(false, i, x, y, z) → timesIter(inc(i), x, y, plus(z, y))
isZero(0) → true
isZero(s(0)) → false
isZero(s(s(x))) → isZero(s(x))
inc(0) → s(0)
inc(s(x)) → s(inc(x))
inc(x) → s(x)
p(0) → 0
p(s(x)) → x
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)
f0(0, y, x) → f1(x, y, x)
f1(x, y, z) → f2(x, y, z)
f2(x, 1, z) → f0(x, z, z)
f0(x, y, z) → d
f1(x, y, z) → c
The set Q consists of the following terms:
plus(x0, x1)
ifPlus(true, x0, x1)
ifPlus(false, x0, x1)
times(x0, x1)
timesIter(x0, x1, x2, x3)
ifTimes(true, x0, x1, x2, x3)
ifTimes(false, x0, x1, x2, x3)
isZero(0)
isZero(s(0))
isZero(s(s(x0)))
inc(x0)
p(0)
p(s(x0))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
f1(x0, x1, x2)
f2(x0, 1, x1)
f0(x0, x1, x2)
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:
F1(x, y, z) → F2(x, y, z)
F2(x, 1, z) → F0(x, z, z)
F0(0, y, x) → F1(x, y, x)
R is empty.
The set Q consists of the following terms:
plus(x0, x1)
ifPlus(true, x0, x1)
ifPlus(false, x0, x1)
times(x0, x1)
timesIter(x0, x1, x2, x3)
ifTimes(true, x0, x1, x2, x3)
ifTimes(false, x0, x1, x2, x3)
isZero(0)
isZero(s(0))
isZero(s(s(x0)))
inc(x0)
p(0)
p(s(x0))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
f1(x0, x1, x2)
f2(x0, 1, x1)
f0(x0, x1, x2)
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].
plus(x0, x1)
ifPlus(true, x0, x1)
ifPlus(false, x0, x1)
times(x0, x1)
timesIter(x0, x1, x2, x3)
ifTimes(true, x0, x1, x2, x3)
ifTimes(false, x0, x1, x2, x3)
isZero(0)
isZero(s(0))
isZero(s(s(x0)))
inc(x0)
p(0)
p(s(x0))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
f1(x0, x1, x2)
f2(x0, 1, x1)
f0(x0, x1, x2)
(11) Obligation:
Q DP problem:
The TRS P consists of the following rules:
F1(x, y, z) → F2(x, y, z)
F2(x, 1, z) → F0(x, z, z)
F0(0, y, x) → F1(x, y, x)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(12) Instantiation (EQUIVALENT transformation)
By instantiating [LPAR04] the rule
F1(
x,
y,
z) →
F2(
x,
y,
z) we obtained the following new rules [LPAR04]:
F1(z1, z0, z1) → F2(z1, z0, z1)
(13) Obligation:
Q DP problem:
The TRS P consists of the following rules:
F2(x, 1, z) → F0(x, z, z)
F0(0, y, x) → F1(x, y, x)
F1(z1, z0, z1) → F2(z1, z0, z1)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(14) Instantiation (EQUIVALENT transformation)
By instantiating [LPAR04] the rule
F1(
x,
y,
z) →
F2(
x,
y,
z) we obtained the following new rules [LPAR04]:
F1(z1, z0, z1) → F2(z1, z0, z1)
(15) Obligation:
Q DP problem:
The TRS P consists of the following rules:
F2(x, 1, z) → F0(x, z, z)
F0(0, y, x) → F1(x, y, x)
F1(z1, z0, z1) → F2(z1, z0, z1)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(16) Instantiation (EQUIVALENT transformation)
By instantiating [LPAR04] the rule
F2(
x,
1,
z) →
F0(
x,
z,
z) we obtained the following new rules [LPAR04]:
F2(z0, 1, z0) → F0(z0, z0, z0)
(17) Obligation:
Q DP problem:
The TRS P consists of the following rules:
F0(0, y, x) → F1(x, y, x)
F1(z1, z0, z1) → F2(z1, z0, z1)
F2(z0, 1, z0) → F0(z0, z0, z0)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(18) Instantiation (EQUIVALENT transformation)
By instantiating [LPAR04] the rule
F0(
0,
y,
x) →
F1(
x,
y,
x) we obtained the following new rules [LPAR04]:
F0(0, 0, 0) → F1(0, 0, 0)
(19) Obligation:
Q DP problem:
The TRS P consists of the following rules:
F1(z1, z0, z1) → F2(z1, z0, z1)
F2(z0, 1, z0) → F0(z0, z0, z0)
F0(0, 0, 0) → F1(0, 0, 0)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(20) Instantiation (EQUIVALENT transformation)
By instantiating [LPAR04] the rule
F1(
z1,
z0,
z1) →
F2(
z1,
z0,
z1) we obtained the following new rules [LPAR04]:
F1(0, 0, 0) → F2(0, 0, 0)
(21) Obligation:
Q DP problem:
The TRS P consists of the following rules:
F2(z0, 1, z0) → F0(z0, z0, z0)
F0(0, 0, 0) → F1(0, 0, 0)
F1(0, 0, 0) → F2(0, 0, 0)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(22) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 3 less nodes.
(23) TRUE
(24) 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:
plus(x, y) → ifPlus(isZero(x), x, inc(y))
ifPlus(true, x, y) → p(y)
ifPlus(false, x, y) → plus(p(x), y)
times(x, y) → timesIter(0, x, y, 0)
timesIter(i, x, y, z) → ifTimes(ge(i, x), i, x, y, z)
ifTimes(true, i, x, y, z) → z
ifTimes(false, i, x, y, z) → timesIter(inc(i), x, y, plus(z, y))
isZero(0) → true
isZero(s(0)) → false
isZero(s(s(x))) → isZero(s(x))
inc(0) → s(0)
inc(s(x)) → s(inc(x))
inc(x) → s(x)
p(0) → 0
p(s(x)) → x
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)
f0(0, y, x) → f1(x, y, x)
f1(x, y, z) → f2(x, y, z)
f2(x, 1, z) → f0(x, z, z)
f0(x, y, z) → d
f1(x, y, z) → c
The set Q consists of the following terms:
plus(x0, x1)
ifPlus(true, x0, x1)
ifPlus(false, x0, x1)
times(x0, x1)
timesIter(x0, x1, x2, x3)
ifTimes(true, x0, x1, x2, x3)
ifTimes(false, x0, x1, x2, x3)
isZero(0)
isZero(s(0))
isZero(s(s(x0)))
inc(x0)
p(0)
p(s(x0))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
f1(x0, x1, x2)
f2(x0, 1, x1)
f0(x0, x1, x2)
We have to consider all minimal (P,Q,R)-chains.
(25) 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.
(26) 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:
plus(x0, x1)
ifPlus(true, x0, x1)
ifPlus(false, x0, x1)
times(x0, x1)
timesIter(x0, x1, x2, x3)
ifTimes(true, x0, x1, x2, x3)
ifTimes(false, x0, x1, x2, x3)
isZero(0)
isZero(s(0))
isZero(s(s(x0)))
inc(x0)
p(0)
p(s(x0))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
f1(x0, x1, x2)
f2(x0, 1, x1)
f0(x0, x1, x2)
We have to consider all minimal (P,Q,R)-chains.
(27) QReductionProof (EQUIVALENT transformation)
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].
plus(x0, x1)
ifPlus(true, x0, x1)
ifPlus(false, x0, x1)
times(x0, x1)
timesIter(x0, x1, x2, x3)
ifTimes(true, x0, x1, x2, x3)
ifTimes(false, x0, x1, x2, x3)
isZero(0)
isZero(s(0))
isZero(s(s(x0)))
inc(x0)
p(0)
p(s(x0))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
f1(x0, x1, x2)
f2(x0, 1, x1)
f0(x0, x1, x2)
(28) 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.
(29) 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
(30) TRUE
(31) 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:
plus(x, y) → ifPlus(isZero(x), x, inc(y))
ifPlus(true, x, y) → p(y)
ifPlus(false, x, y) → plus(p(x), y)
times(x, y) → timesIter(0, x, y, 0)
timesIter(i, x, y, z) → ifTimes(ge(i, x), i, x, y, z)
ifTimes(true, i, x, y, z) → z
ifTimes(false, i, x, y, z) → timesIter(inc(i), x, y, plus(z, y))
isZero(0) → true
isZero(s(0)) → false
isZero(s(s(x))) → isZero(s(x))
inc(0) → s(0)
inc(s(x)) → s(inc(x))
inc(x) → s(x)
p(0) → 0
p(s(x)) → x
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)
f0(0, y, x) → f1(x, y, x)
f1(x, y, z) → f2(x, y, z)
f2(x, 1, z) → f0(x, z, z)
f0(x, y, z) → d
f1(x, y, z) → c
The set Q consists of the following terms:
plus(x0, x1)
ifPlus(true, x0, x1)
ifPlus(false, x0, x1)
times(x0, x1)
timesIter(x0, x1, x2, x3)
ifTimes(true, x0, x1, x2, x3)
ifTimes(false, x0, x1, x2, x3)
isZero(0)
isZero(s(0))
isZero(s(s(x0)))
inc(x0)
p(0)
p(s(x0))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
f1(x0, x1, x2)
f2(x0, 1, x1)
f0(x0, x1, x2)
We have to consider all minimal (P,Q,R)-chains.
(32) 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.
(33) 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:
plus(x0, x1)
ifPlus(true, x0, x1)
ifPlus(false, x0, x1)
times(x0, x1)
timesIter(x0, x1, x2, x3)
ifTimes(true, x0, x1, x2, x3)
ifTimes(false, x0, x1, x2, x3)
isZero(0)
isZero(s(0))
isZero(s(s(x0)))
inc(x0)
p(0)
p(s(x0))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
f1(x0, x1, x2)
f2(x0, 1, x1)
f0(x0, x1, x2)
We have to consider all minimal (P,Q,R)-chains.
(34) QReductionProof (EQUIVALENT transformation)
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].
plus(x0, x1)
ifPlus(true, x0, x1)
ifPlus(false, x0, x1)
times(x0, x1)
timesIter(x0, x1, x2, x3)
ifTimes(true, x0, x1, x2, x3)
ifTimes(false, x0, x1, x2, x3)
isZero(0)
isZero(s(0))
isZero(s(s(x0)))
inc(x0)
p(0)
p(s(x0))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
f1(x0, x1, x2)
f2(x0, 1, x1)
f0(x0, x1, x2)
(35) 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.
(36) 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
(37) TRUE
(38) Obligation:
Q DP problem:
The TRS P consists of the following rules:
INC(s(x)) → INC(x)
The TRS R consists of the following rules:
plus(x, y) → ifPlus(isZero(x), x, inc(y))
ifPlus(true, x, y) → p(y)
ifPlus(false, x, y) → plus(p(x), y)
times(x, y) → timesIter(0, x, y, 0)
timesIter(i, x, y, z) → ifTimes(ge(i, x), i, x, y, z)
ifTimes(true, i, x, y, z) → z
ifTimes(false, i, x, y, z) → timesIter(inc(i), x, y, plus(z, y))
isZero(0) → true
isZero(s(0)) → false
isZero(s(s(x))) → isZero(s(x))
inc(0) → s(0)
inc(s(x)) → s(inc(x))
inc(x) → s(x)
p(0) → 0
p(s(x)) → x
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)
f0(0, y, x) → f1(x, y, x)
f1(x, y, z) → f2(x, y, z)
f2(x, 1, z) → f0(x, z, z)
f0(x, y, z) → d
f1(x, y, z) → c
The set Q consists of the following terms:
plus(x0, x1)
ifPlus(true, x0, x1)
ifPlus(false, x0, x1)
times(x0, x1)
timesIter(x0, x1, x2, x3)
ifTimes(true, x0, x1, x2, x3)
ifTimes(false, x0, x1, x2, x3)
isZero(0)
isZero(s(0))
isZero(s(s(x0)))
inc(x0)
p(0)
p(s(x0))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
f1(x0, x1, x2)
f2(x0, 1, x1)
f0(x0, x1, x2)
We have to consider all minimal (P,Q,R)-chains.
(39) 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.
(40) Obligation:
Q DP problem:
The TRS P consists of the following rules:
INC(s(x)) → INC(x)
R is empty.
The set Q consists of the following terms:
plus(x0, x1)
ifPlus(true, x0, x1)
ifPlus(false, x0, x1)
times(x0, x1)
timesIter(x0, x1, x2, x3)
ifTimes(true, x0, x1, x2, x3)
ifTimes(false, x0, x1, x2, x3)
isZero(0)
isZero(s(0))
isZero(s(s(x0)))
inc(x0)
p(0)
p(s(x0))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
f1(x0, x1, x2)
f2(x0, 1, x1)
f0(x0, x1, x2)
We have to consider all minimal (P,Q,R)-chains.
(41) QReductionProof (EQUIVALENT transformation)
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].
plus(x0, x1)
ifPlus(true, x0, x1)
ifPlus(false, x0, x1)
times(x0, x1)
timesIter(x0, x1, x2, x3)
ifTimes(true, x0, x1, x2, x3)
ifTimes(false, x0, x1, x2, x3)
isZero(0)
isZero(s(0))
isZero(s(s(x0)))
inc(x0)
p(0)
p(s(x0))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
f1(x0, x1, x2)
f2(x0, 1, x1)
f0(x0, x1, x2)
(42) Obligation:
Q DP problem:
The TRS P consists of the following rules:
INC(s(x)) → INC(x)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(43) QDPSizeChangeProof (EQUIVALENT transformation)
By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.
From the DPs we obtained the following set of size-change graphs:
- INC(s(x)) → INC(x)
The graph contains the following edges 1 > 1
(44) TRUE
(45) 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:
plus(x, y) → ifPlus(isZero(x), x, inc(y))
ifPlus(true, x, y) → p(y)
ifPlus(false, x, y) → plus(p(x), y)
times(x, y) → timesIter(0, x, y, 0)
timesIter(i, x, y, z) → ifTimes(ge(i, x), i, x, y, z)
ifTimes(true, i, x, y, z) → z
ifTimes(false, i, x, y, z) → timesIter(inc(i), x, y, plus(z, y))
isZero(0) → true
isZero(s(0)) → false
isZero(s(s(x))) → isZero(s(x))
inc(0) → s(0)
inc(s(x)) → s(inc(x))
inc(x) → s(x)
p(0) → 0
p(s(x)) → x
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)
f0(0, y, x) → f1(x, y, x)
f1(x, y, z) → f2(x, y, z)
f2(x, 1, z) → f0(x, z, z)
f0(x, y, z) → d
f1(x, y, z) → c
The set Q consists of the following terms:
plus(x0, x1)
ifPlus(true, x0, x1)
ifPlus(false, x0, x1)
times(x0, x1)
timesIter(x0, x1, x2, x3)
ifTimes(true, x0, x1, x2, x3)
ifTimes(false, x0, x1, x2, x3)
isZero(0)
isZero(s(0))
isZero(s(s(x0)))
inc(x0)
p(0)
p(s(x0))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
f1(x0, x1, x2)
f2(x0, 1, x1)
f0(x0, x1, x2)
We have to consider all minimal (P,Q,R)-chains.
(46) 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.
(47) 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:
plus(x0, x1)
ifPlus(true, x0, x1)
ifPlus(false, x0, x1)
times(x0, x1)
timesIter(x0, x1, x2, x3)
ifTimes(true, x0, x1, x2, x3)
ifTimes(false, x0, x1, x2, x3)
isZero(0)
isZero(s(0))
isZero(s(s(x0)))
inc(x0)
p(0)
p(s(x0))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
f1(x0, x1, x2)
f2(x0, 1, x1)
f0(x0, x1, x2)
We have to consider all minimal (P,Q,R)-chains.
(48) QReductionProof (EQUIVALENT transformation)
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].
plus(x0, x1)
ifPlus(true, x0, x1)
ifPlus(false, x0, x1)
times(x0, x1)
timesIter(x0, x1, x2, x3)
ifTimes(true, x0, x1, x2, x3)
ifTimes(false, x0, x1, x2, x3)
isZero(0)
isZero(s(0))
isZero(s(s(x0)))
inc(x0)
p(0)
p(s(x0))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
f1(x0, x1, x2)
f2(x0, 1, x1)
f0(x0, x1, x2)
(49) 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.
(50) 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
(51) TRUE
(52) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IFPLUS(false, x, y) → PLUS(p(x), y)
PLUS(x, y) → IFPLUS(isZero(x), x, inc(y))
The TRS R consists of the following rules:
plus(x, y) → ifPlus(isZero(x), x, inc(y))
ifPlus(true, x, y) → p(y)
ifPlus(false, x, y) → plus(p(x), y)
times(x, y) → timesIter(0, x, y, 0)
timesIter(i, x, y, z) → ifTimes(ge(i, x), i, x, y, z)
ifTimes(true, i, x, y, z) → z
ifTimes(false, i, x, y, z) → timesIter(inc(i), x, y, plus(z, y))
isZero(0) → true
isZero(s(0)) → false
isZero(s(s(x))) → isZero(s(x))
inc(0) → s(0)
inc(s(x)) → s(inc(x))
inc(x) → s(x)
p(0) → 0
p(s(x)) → x
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)
f0(0, y, x) → f1(x, y, x)
f1(x, y, z) → f2(x, y, z)
f2(x, 1, z) → f0(x, z, z)
f0(x, y, z) → d
f1(x, y, z) → c
The set Q consists of the following terms:
plus(x0, x1)
ifPlus(true, x0, x1)
ifPlus(false, x0, x1)
times(x0, x1)
timesIter(x0, x1, x2, x3)
ifTimes(true, x0, x1, x2, x3)
ifTimes(false, x0, x1, x2, x3)
isZero(0)
isZero(s(0))
isZero(s(s(x0)))
inc(x0)
p(0)
p(s(x0))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
f1(x0, x1, x2)
f2(x0, 1, x1)
f0(x0, x1, x2)
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:
IFPLUS(false, x, y) → PLUS(p(x), y)
PLUS(x, y) → IFPLUS(isZero(x), x, inc(y))
The TRS R consists of the following rules:
isZero(0) → true
isZero(s(0)) → false
isZero(s(s(x))) → isZero(s(x))
inc(0) → s(0)
inc(s(x)) → s(inc(x))
inc(x) → s(x)
p(0) → 0
p(s(x)) → x
p(s(s(x))) → s(p(s(x)))
The set Q consists of the following terms:
plus(x0, x1)
ifPlus(true, x0, x1)
ifPlus(false, x0, x1)
times(x0, x1)
timesIter(x0, x1, x2, x3)
ifTimes(true, x0, x1, x2, x3)
ifTimes(false, x0, x1, x2, x3)
isZero(0)
isZero(s(0))
isZero(s(s(x0)))
inc(x0)
p(0)
p(s(x0))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
f1(x0, x1, x2)
f2(x0, 1, x1)
f0(x0, x1, x2)
We have to consider all minimal (P,Q,R)-chains.
(55) QReductionProof (EQUIVALENT transformation)
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].
plus(x0, x1)
ifPlus(true, x0, x1)
ifPlus(false, x0, x1)
times(x0, x1)
timesIter(x0, x1, x2, x3)
ifTimes(true, x0, x1, x2, x3)
ifTimes(false, x0, x1, x2, x3)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
f1(x0, x1, x2)
f2(x0, 1, x1)
f0(x0, x1, x2)
(56) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IFPLUS(false, x, y) → PLUS(p(x), y)
PLUS(x, y) → IFPLUS(isZero(x), x, inc(y))
The TRS R consists of the following rules:
isZero(0) → true
isZero(s(0)) → false
isZero(s(s(x))) → isZero(s(x))
inc(0) → s(0)
inc(s(x)) → s(inc(x))
inc(x) → s(x)
p(0) → 0
p(s(x)) → x
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)))
inc(x0)
p(0)
p(s(x0))
We have to consider all minimal (P,Q,R)-chains.
(57) Narrowing (EQUIVALENT transformation)
By narrowing [LPAR04] the rule
PLUS(
x,
y) →
IFPLUS(
isZero(
x),
x,
inc(
y)) at position [0] we obtained the following new rules [LPAR04]:
PLUS(0, y1) → IFPLUS(true, 0, inc(y1))
PLUS(s(0), y1) → IFPLUS(false, s(0), inc(y1))
PLUS(s(s(x0)), y1) → IFPLUS(isZero(s(x0)), s(s(x0)), inc(y1))
(58) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IFPLUS(false, x, y) → PLUS(p(x), y)
PLUS(0, y1) → IFPLUS(true, 0, inc(y1))
PLUS(s(0), y1) → IFPLUS(false, s(0), inc(y1))
PLUS(s(s(x0)), y1) → IFPLUS(isZero(s(x0)), s(s(x0)), inc(y1))
The TRS R consists of the following rules:
isZero(0) → true
isZero(s(0)) → false
isZero(s(s(x))) → isZero(s(x))
inc(0) → s(0)
inc(s(x)) → s(inc(x))
inc(x) → s(x)
p(0) → 0
p(s(x)) → x
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)))
inc(x0)
p(0)
p(s(x0))
We have to consider all minimal (P,Q,R)-chains.
(59) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.
(60) Obligation:
Q DP problem:
The TRS P consists of the following rules:
PLUS(s(0), y1) → IFPLUS(false, s(0), inc(y1))
IFPLUS(false, x, y) → PLUS(p(x), y)
PLUS(s(s(x0)), y1) → IFPLUS(isZero(s(x0)), s(s(x0)), inc(y1))
The TRS R consists of the following rules:
isZero(0) → true
isZero(s(0)) → false
isZero(s(s(x))) → isZero(s(x))
inc(0) → s(0)
inc(s(x)) → s(inc(x))
inc(x) → s(x)
p(0) → 0
p(s(x)) → x
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)))
inc(x0)
p(0)
p(s(x0))
We have to consider all minimal (P,Q,R)-chains.
(61) 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.
(62) Obligation:
Q DP problem:
The TRS P consists of the following rules:
PLUS(s(0), y1) → IFPLUS(false, s(0), inc(y1))
IFPLUS(false, x, y) → PLUS(p(x), y)
PLUS(s(s(x0)), y1) → IFPLUS(isZero(s(x0)), s(s(x0)), inc(y1))
The TRS R consists of the following rules:
isZero(s(0)) → false
isZero(s(s(x))) → isZero(s(x))
inc(0) → s(0)
inc(s(x)) → s(inc(x))
inc(x) → s(x)
p(0) → 0
p(s(x)) → x
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)))
inc(x0)
p(0)
p(s(x0))
We have to consider all minimal (P,Q,R)-chains.
(63) Narrowing (EQUIVALENT transformation)
By narrowing [LPAR04] the rule
PLUS(
s(
0),
y1) →
IFPLUS(
false,
s(
0),
inc(
y1)) at position [2] we obtained the following new rules [LPAR04]:
PLUS(s(0), 0) → IFPLUS(false, s(0), s(0))
PLUS(s(0), s(x0)) → IFPLUS(false, s(0), s(inc(x0)))
PLUS(s(0), x0) → IFPLUS(false, s(0), s(x0))
(64) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IFPLUS(false, x, y) → PLUS(p(x), y)
PLUS(s(s(x0)), y1) → IFPLUS(isZero(s(x0)), s(s(x0)), inc(y1))
PLUS(s(0), 0) → IFPLUS(false, s(0), s(0))
PLUS(s(0), s(x0)) → IFPLUS(false, s(0), s(inc(x0)))
PLUS(s(0), x0) → IFPLUS(false, s(0), s(x0))
The TRS R consists of the following rules:
isZero(s(0)) → false
isZero(s(s(x))) → isZero(s(x))
inc(0) → s(0)
inc(s(x)) → s(inc(x))
inc(x) → s(x)
p(0) → 0
p(s(x)) → x
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)))
inc(x0)
p(0)
p(s(x0))
We have to consider all minimal (P,Q,R)-chains.
(65) Narrowing (EQUIVALENT transformation)
By narrowing [LPAR04] the rule
IFPLUS(
false,
x,
y) →
PLUS(
p(
x),
y) at position [0] we obtained the following new rules [LPAR04]:
IFPLUS(false, 0, y1) → PLUS(0, y1)
IFPLUS(false, s(x0), y1) → PLUS(x0, y1)
IFPLUS(false, s(s(x0)), y1) → PLUS(s(p(s(x0))), y1)
(66) Obligation:
Q DP problem:
The TRS P consists of the following rules:
PLUS(s(s(x0)), y1) → IFPLUS(isZero(s(x0)), s(s(x0)), inc(y1))
PLUS(s(0), 0) → IFPLUS(false, s(0), s(0))
PLUS(s(0), s(x0)) → IFPLUS(false, s(0), s(inc(x0)))
PLUS(s(0), x0) → IFPLUS(false, s(0), s(x0))
IFPLUS(false, 0, y1) → PLUS(0, y1)
IFPLUS(false, s(x0), y1) → PLUS(x0, y1)
IFPLUS(false, s(s(x0)), y1) → PLUS(s(p(s(x0))), y1)
The TRS R consists of the following rules:
isZero(s(0)) → false
isZero(s(s(x))) → isZero(s(x))
inc(0) → s(0)
inc(s(x)) → s(inc(x))
inc(x) → s(x)
p(0) → 0
p(s(x)) → x
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)))
inc(x0)
p(0)
p(s(x0))
We have to consider all minimal (P,Q,R)-chains.
(67) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.
(68) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IFPLUS(false, s(x0), y1) → PLUS(x0, y1)
PLUS(s(s(x0)), y1) → IFPLUS(isZero(s(x0)), s(s(x0)), inc(y1))
IFPLUS(false, s(s(x0)), y1) → PLUS(s(p(s(x0))), y1)
PLUS(s(0), 0) → IFPLUS(false, s(0), s(0))
PLUS(s(0), s(x0)) → IFPLUS(false, s(0), s(inc(x0)))
PLUS(s(0), x0) → IFPLUS(false, s(0), s(x0))
The TRS R consists of the following rules:
isZero(s(0)) → false
isZero(s(s(x))) → isZero(s(x))
inc(0) → s(0)
inc(s(x)) → s(inc(x))
inc(x) → s(x)
p(0) → 0
p(s(x)) → x
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)))
inc(x0)
p(0)
p(s(x0))
We have to consider all minimal (P,Q,R)-chains.
(69) UsableRulesProof (EQUIVALENT transformation)
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.
(70) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IFPLUS(false, s(x0), y1) → PLUS(x0, y1)
PLUS(s(s(x0)), y1) → IFPLUS(isZero(s(x0)), s(s(x0)), inc(y1))
IFPLUS(false, s(s(x0)), y1) → PLUS(s(p(s(x0))), y1)
PLUS(s(0), 0) → IFPLUS(false, s(0), s(0))
PLUS(s(0), s(x0)) → IFPLUS(false, s(0), s(inc(x0)))
PLUS(s(0), x0) → IFPLUS(false, s(0), s(x0))
The TRS R consists of the following rules:
inc(0) → s(0)
inc(s(x)) → s(inc(x))
inc(x) → s(x)
p(s(x)) → x
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)))
inc(x0)
p(0)
p(s(x0))
We have to consider all minimal (P,Q,R)-chains.
(71) Narrowing (EQUIVALENT transformation)
By narrowing [LPAR04] the rule
PLUS(
s(
s(
x0)),
y1) →
IFPLUS(
isZero(
s(
x0)),
s(
s(
x0)),
inc(
y1)) at position [2] we obtained the following new rules [LPAR04]:
PLUS(s(s(y0)), 0) → IFPLUS(isZero(s(y0)), s(s(y0)), s(0))
PLUS(s(s(y0)), s(x0)) → IFPLUS(isZero(s(y0)), s(s(y0)), s(inc(x0)))
PLUS(s(s(y0)), x0) → IFPLUS(isZero(s(y0)), s(s(y0)), s(x0))
(72) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IFPLUS(false, s(x0), y1) → PLUS(x0, y1)
IFPLUS(false, s(s(x0)), y1) → PLUS(s(p(s(x0))), y1)
PLUS(s(0), 0) → IFPLUS(false, s(0), s(0))
PLUS(s(0), s(x0)) → IFPLUS(false, s(0), s(inc(x0)))
PLUS(s(0), x0) → IFPLUS(false, s(0), s(x0))
PLUS(s(s(y0)), 0) → IFPLUS(isZero(s(y0)), s(s(y0)), s(0))
PLUS(s(s(y0)), s(x0)) → IFPLUS(isZero(s(y0)), s(s(y0)), s(inc(x0)))
PLUS(s(s(y0)), x0) → IFPLUS(isZero(s(y0)), s(s(y0)), s(x0))
The TRS R consists of the following rules:
inc(0) → s(0)
inc(s(x)) → s(inc(x))
inc(x) → s(x)
p(s(x)) → x
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)))
inc(x0)
p(0)
p(s(x0))
We have to consider all minimal (P,Q,R)-chains.
(73) Instantiation (EQUIVALENT transformation)
By instantiating [LPAR04] the rule
IFPLUS(
false,
s(
x0),
y1) →
PLUS(
x0,
y1) we obtained the following new rules [LPAR04]:
IFPLUS(false, s(0), s(0)) → PLUS(0, s(0))
IFPLUS(false, s(0), s(y_0)) → PLUS(0, s(y_0))
IFPLUS(false, s(s(z0)), s(0)) → PLUS(s(z0), s(0))
IFPLUS(false, s(s(z0)), s(y_1)) → PLUS(s(z0), s(y_1))
(74) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IFPLUS(false, s(s(x0)), y1) → PLUS(s(p(s(x0))), y1)
PLUS(s(0), 0) → IFPLUS(false, s(0), s(0))
PLUS(s(0), s(x0)) → IFPLUS(false, s(0), s(inc(x0)))
PLUS(s(0), x0) → IFPLUS(false, s(0), s(x0))
PLUS(s(s(y0)), 0) → IFPLUS(isZero(s(y0)), s(s(y0)), s(0))
PLUS(s(s(y0)), s(x0)) → IFPLUS(isZero(s(y0)), s(s(y0)), s(inc(x0)))
PLUS(s(s(y0)), x0) → IFPLUS(isZero(s(y0)), s(s(y0)), s(x0))
IFPLUS(false, s(0), s(0)) → PLUS(0, s(0))
IFPLUS(false, s(0), s(y_0)) → PLUS(0, s(y_0))
IFPLUS(false, s(s(z0)), s(0)) → PLUS(s(z0), s(0))
IFPLUS(false, s(s(z0)), s(y_1)) → PLUS(s(z0), s(y_1))
The TRS R consists of the following rules:
inc(0) → s(0)
inc(s(x)) → s(inc(x))
inc(x) → s(x)
p(s(x)) → x
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)))
inc(x0)
p(0)
p(s(x0))
We have to consider all minimal (P,Q,R)-chains.
(75) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 5 less nodes.
(76) Obligation:
Q DP problem:
The TRS P consists of the following rules:
PLUS(s(s(y0)), 0) → IFPLUS(isZero(s(y0)), s(s(y0)), s(0))
IFPLUS(false, s(s(x0)), y1) → PLUS(s(p(s(x0))), y1)
PLUS(s(s(y0)), s(x0)) → IFPLUS(isZero(s(y0)), s(s(y0)), s(inc(x0)))
IFPLUS(false, s(s(z0)), s(0)) → PLUS(s(z0), s(0))
PLUS(s(s(y0)), x0) → IFPLUS(isZero(s(y0)), s(s(y0)), s(x0))
IFPLUS(false, s(s(z0)), s(y_1)) → PLUS(s(z0), s(y_1))
The TRS R consists of the following rules:
inc(0) → s(0)
inc(s(x)) → s(inc(x))
inc(x) → s(x)
p(s(x)) → x
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)))
inc(x0)
p(0)
p(s(x0))
We have to consider all minimal (P,Q,R)-chains.
(77) Instantiation (EQUIVALENT transformation)
By instantiating [LPAR04] the rule
IFPLUS(
false,
s(
s(
x0)),
y1) →
PLUS(
s(
p(
s(
x0))),
y1) we obtained the following new rules [LPAR04]:
IFPLUS(false, s(s(z0)), s(0)) → PLUS(s(p(s(z0))), s(0))
IFPLUS(false, s(s(z0)), s(y_1)) → PLUS(s(p(s(z0))), s(y_1))
(78) Obligation:
Q DP problem:
The TRS P consists of the following rules:
PLUS(s(s(y0)), 0) → IFPLUS(isZero(s(y0)), s(s(y0)), s(0))
PLUS(s(s(y0)), s(x0)) → IFPLUS(isZero(s(y0)), s(s(y0)), s(inc(x0)))
IFPLUS(false, s(s(z0)), s(0)) → PLUS(s(z0), s(0))
PLUS(s(s(y0)), x0) → IFPLUS(isZero(s(y0)), s(s(y0)), s(x0))
IFPLUS(false, s(s(z0)), s(y_1)) → PLUS(s(z0), s(y_1))
IFPLUS(false, s(s(z0)), s(0)) → PLUS(s(p(s(z0))), s(0))
IFPLUS(false, s(s(z0)), s(y_1)) → PLUS(s(p(s(z0))), s(y_1))
The TRS R consists of the following rules:
inc(0) → s(0)
inc(s(x)) → s(inc(x))
inc(x) → s(x)
p(s(x)) → x
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)))
inc(x0)
p(0)
p(s(x0))
We have to consider all minimal (P,Q,R)-chains.
(79) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.
(80) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IFPLUS(false, s(s(z0)), s(0)) → PLUS(s(z0), s(0))
PLUS(s(s(y0)), s(x0)) → IFPLUS(isZero(s(y0)), s(s(y0)), s(inc(x0)))
IFPLUS(false, s(s(z0)), s(y_1)) → PLUS(s(z0), s(y_1))
PLUS(s(s(y0)), x0) → IFPLUS(isZero(s(y0)), s(s(y0)), s(x0))
IFPLUS(false, s(s(z0)), s(0)) → PLUS(s(p(s(z0))), s(0))
IFPLUS(false, s(s(z0)), s(y_1)) → PLUS(s(p(s(z0))), s(y_1))
The TRS R consists of the following rules:
inc(0) → s(0)
inc(s(x)) → s(inc(x))
inc(x) → s(x)
p(s(x)) → x
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)))
inc(x0)
p(0)
p(s(x0))
We have to consider all minimal (P,Q,R)-chains.
(81) Instantiation (EQUIVALENT transformation)
By instantiating [LPAR04] the rule
PLUS(
s(
s(
y0)),
x0) →
IFPLUS(
isZero(
s(
y0)),
s(
s(
y0)),
s(
x0)) we obtained the following new rules [LPAR04]:
PLUS(s(s(x0)), s(0)) → IFPLUS(isZero(s(x0)), s(s(x0)), s(s(0)))
PLUS(s(s(x0)), s(z1)) → IFPLUS(isZero(s(x0)), s(s(x0)), s(s(z1)))
(82) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IFPLUS(false, s(s(z0)), s(0)) → PLUS(s(z0), s(0))
PLUS(s(s(y0)), s(x0)) → IFPLUS(isZero(s(y0)), s(s(y0)), s(inc(x0)))
IFPLUS(false, s(s(z0)), s(y_1)) → PLUS(s(z0), s(y_1))
IFPLUS(false, s(s(z0)), s(0)) → PLUS(s(p(s(z0))), s(0))
IFPLUS(false, s(s(z0)), s(y_1)) → PLUS(s(p(s(z0))), s(y_1))
PLUS(s(s(x0)), s(0)) → IFPLUS(isZero(s(x0)), s(s(x0)), s(s(0)))
PLUS(s(s(x0)), s(z1)) → IFPLUS(isZero(s(x0)), s(s(x0)), s(s(z1)))
The TRS R consists of the following rules:
inc(0) → s(0)
inc(s(x)) → s(inc(x))
inc(x) → s(x)
p(s(x)) → x
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)))
inc(x0)
p(0)
p(s(x0))
We have to consider all minimal (P,Q,R)-chains.
(83) Narrowing (EQUIVALENT transformation)
By narrowing [LPAR04] the rule
PLUS(
s(
s(
y0)),
s(
x0)) →
IFPLUS(
isZero(
s(
y0)),
s(
s(
y0)),
s(
inc(
x0))) at position [2,0] we obtained the following new rules [LPAR04]:
PLUS(s(s(y0)), s(0)) → IFPLUS(isZero(s(y0)), s(s(y0)), s(s(0)))
PLUS(s(s(y0)), s(s(x0))) → IFPLUS(isZero(s(y0)), s(s(y0)), s(s(inc(x0))))
PLUS(s(s(y0)), s(x0)) → IFPLUS(isZero(s(y0)), s(s(y0)), s(s(x0)))
(84) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IFPLUS(false, s(s(z0)), s(0)) → PLUS(s(z0), s(0))
IFPLUS(false, s(s(z0)), s(y_1)) → PLUS(s(z0), s(y_1))
IFPLUS(false, s(s(z0)), s(0)) → PLUS(s(p(s(z0))), s(0))
IFPLUS(false, s(s(z0)), s(y_1)) → PLUS(s(p(s(z0))), s(y_1))
PLUS(s(s(x0)), s(0)) → IFPLUS(isZero(s(x0)), s(s(x0)), s(s(0)))
PLUS(s(s(x0)), s(z1)) → IFPLUS(isZero(s(x0)), s(s(x0)), s(s(z1)))
PLUS(s(s(y0)), s(s(x0))) → IFPLUS(isZero(s(y0)), s(s(y0)), s(s(inc(x0))))
The TRS R consists of the following rules:
inc(0) → s(0)
inc(s(x)) → s(inc(x))
inc(x) → s(x)
p(s(x)) → x
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)))
inc(x0)
p(0)
p(s(x0))
We have to consider all minimal (P,Q,R)-chains.
(85) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 2 less nodes.
(86) Obligation:
Q DP problem:
The TRS P consists of the following rules:
PLUS(s(s(x0)), s(0)) → IFPLUS(isZero(s(x0)), s(s(x0)), s(s(0)))
IFPLUS(false, s(s(z0)), s(y_1)) → PLUS(s(z0), s(y_1))
PLUS(s(s(x0)), s(z1)) → IFPLUS(isZero(s(x0)), s(s(x0)), s(s(z1)))
IFPLUS(false, s(s(z0)), s(y_1)) → PLUS(s(p(s(z0))), s(y_1))
PLUS(s(s(y0)), s(s(x0))) → IFPLUS(isZero(s(y0)), s(s(y0)), s(s(inc(x0))))
The TRS R consists of the following rules:
inc(0) → s(0)
inc(s(x)) → s(inc(x))
inc(x) → s(x)
p(s(x)) → x
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)))
inc(x0)
p(0)
p(s(x0))
We have to consider all minimal (P,Q,R)-chains.
(87) Instantiation (EQUIVALENT transformation)
By instantiating [LPAR04] the rule
IFPLUS(
false,
s(
s(
z0)),
s(
y_1)) →
PLUS(
s(
z0),
s(
y_1)) we obtained the following new rules [LPAR04]:
IFPLUS(false, s(s(z0)), s(s(0))) → PLUS(s(z0), s(s(0)))
IFPLUS(false, s(s(z0)), s(s(z1))) → PLUS(s(z0), s(s(z1)))
(88) Obligation:
Q DP problem:
The TRS P consists of the following rules:
PLUS(s(s(x0)), s(0)) → IFPLUS(isZero(s(x0)), s(s(x0)), s(s(0)))
PLUS(s(s(x0)), s(z1)) → IFPLUS(isZero(s(x0)), s(s(x0)), s(s(z1)))
IFPLUS(false, s(s(z0)), s(y_1)) → PLUS(s(p(s(z0))), s(y_1))
PLUS(s(s(y0)), s(s(x0))) → IFPLUS(isZero(s(y0)), s(s(y0)), s(s(inc(x0))))
IFPLUS(false, s(s(z0)), s(s(0))) → PLUS(s(z0), s(s(0)))
IFPLUS(false, s(s(z0)), s(s(z1))) → PLUS(s(z0), s(s(z1)))
The TRS R consists of the following rules:
inc(0) → s(0)
inc(s(x)) → s(inc(x))
inc(x) → s(x)
p(s(x)) → x
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)))
inc(x0)
p(0)
p(s(x0))
We have to consider all minimal (P,Q,R)-chains.
(89) Instantiation (EQUIVALENT transformation)
By instantiating [LPAR04] the rule
IFPLUS(
false,
s(
s(
z0)),
s(
y_1)) →
PLUS(
s(
p(
s(
z0))),
s(
y_1)) we obtained the following new rules [LPAR04]:
IFPLUS(false, s(s(z0)), s(s(0))) → PLUS(s(p(s(z0))), s(s(0)))
IFPLUS(false, s(s(z0)), s(s(z1))) → PLUS(s(p(s(z0))), s(s(z1)))
(90) Obligation:
Q DP problem:
The TRS P consists of the following rules:
PLUS(s(s(x0)), s(0)) → IFPLUS(isZero(s(x0)), s(s(x0)), s(s(0)))
PLUS(s(s(x0)), s(z1)) → IFPLUS(isZero(s(x0)), s(s(x0)), s(s(z1)))
PLUS(s(s(y0)), s(s(x0))) → IFPLUS(isZero(s(y0)), s(s(y0)), s(s(inc(x0))))
IFPLUS(false, s(s(z0)), s(s(0))) → PLUS(s(z0), s(s(0)))
IFPLUS(false, s(s(z0)), s(s(z1))) → PLUS(s(z0), s(s(z1)))
IFPLUS(false, s(s(z0)), s(s(0))) → PLUS(s(p(s(z0))), s(s(0)))
IFPLUS(false, s(s(z0)), s(s(z1))) → PLUS(s(p(s(z0))), s(s(z1)))
The TRS R consists of the following rules:
inc(0) → s(0)
inc(s(x)) → s(inc(x))
inc(x) → s(x)
p(s(x)) → x
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)))
inc(x0)
p(0)
p(s(x0))
We have to consider all minimal (P,Q,R)-chains.
(91) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.
(92) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IFPLUS(false, s(s(z0)), s(s(0))) → PLUS(s(z0), s(s(0)))
PLUS(s(s(x0)), s(z1)) → IFPLUS(isZero(s(x0)), s(s(x0)), s(s(z1)))
IFPLUS(false, s(s(z0)), s(s(z1))) → PLUS(s(z0), s(s(z1)))
PLUS(s(s(y0)), s(s(x0))) → IFPLUS(isZero(s(y0)), s(s(y0)), s(s(inc(x0))))
IFPLUS(false, s(s(z0)), s(s(0))) → PLUS(s(p(s(z0))), s(s(0)))
IFPLUS(false, s(s(z0)), s(s(z1))) → PLUS(s(p(s(z0))), s(s(z1)))
The TRS R consists of the following rules:
inc(0) → s(0)
inc(s(x)) → s(inc(x))
inc(x) → s(x)
p(s(x)) → x
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)))
inc(x0)
p(0)
p(s(x0))
We have to consider all minimal (P,Q,R)-chains.
(93) Instantiation (EQUIVALENT transformation)
By instantiating [LPAR04] the rule
PLUS(
s(
s(
x0)),
s(
z1)) →
IFPLUS(
isZero(
s(
x0)),
s(
s(
x0)),
s(
s(
z1))) we obtained the following new rules [LPAR04]:
PLUS(s(s(x0)), s(s(0))) → IFPLUS(isZero(s(x0)), s(s(x0)), s(s(s(0))))
PLUS(s(s(x0)), s(s(z1))) → IFPLUS(isZero(s(x0)), s(s(x0)), s(s(s(z1))))
(94) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IFPLUS(false, s(s(z0)), s(s(0))) → PLUS(s(z0), s(s(0)))
IFPLUS(false, s(s(z0)), s(s(z1))) → PLUS(s(z0), s(s(z1)))
PLUS(s(s(y0)), s(s(x0))) → IFPLUS(isZero(s(y0)), s(s(y0)), s(s(inc(x0))))
IFPLUS(false, s(s(z0)), s(s(0))) → PLUS(s(p(s(z0))), s(s(0)))
IFPLUS(false, s(s(z0)), s(s(z1))) → PLUS(s(p(s(z0))), s(s(z1)))
PLUS(s(s(x0)), s(s(0))) → IFPLUS(isZero(s(x0)), s(s(x0)), s(s(s(0))))
PLUS(s(s(x0)), s(s(z1))) → IFPLUS(isZero(s(x0)), s(s(x0)), s(s(s(z1))))
The TRS R consists of the following rules:
inc(0) → s(0)
inc(s(x)) → s(inc(x))
inc(x) → s(x)
p(s(x)) → x
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)))
inc(x0)
p(0)
p(s(x0))
We have to consider all minimal (P,Q,R)-chains.
(95) Narrowing (EQUIVALENT transformation)
By narrowing [LPAR04] the rule
PLUS(
s(
s(
y0)),
s(
s(
x0))) →
IFPLUS(
isZero(
s(
y0)),
s(
s(
y0)),
s(
s(
inc(
x0)))) at position [2,0,0] we obtained the following new rules [LPAR04]:
PLUS(s(s(y0)), s(s(0))) → IFPLUS(isZero(s(y0)), s(s(y0)), s(s(s(0))))
PLUS(s(s(y0)), s(s(s(x0)))) → IFPLUS(isZero(s(y0)), s(s(y0)), s(s(s(inc(x0)))))
PLUS(s(s(y0)), s(s(x0))) → IFPLUS(isZero(s(y0)), s(s(y0)), s(s(s(x0))))
(96) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IFPLUS(false, s(s(z0)), s(s(0))) → PLUS(s(z0), s(s(0)))
IFPLUS(false, s(s(z0)), s(s(z1))) → PLUS(s(z0), s(s(z1)))
IFPLUS(false, s(s(z0)), s(s(0))) → PLUS(s(p(s(z0))), s(s(0)))
IFPLUS(false, s(s(z0)), s(s(z1))) → PLUS(s(p(s(z0))), s(s(z1)))
PLUS(s(s(x0)), s(s(0))) → IFPLUS(isZero(s(x0)), s(s(x0)), s(s(s(0))))
PLUS(s(s(x0)), s(s(z1))) → IFPLUS(isZero(s(x0)), s(s(x0)), s(s(s(z1))))
PLUS(s(s(y0)), s(s(s(x0)))) → IFPLUS(isZero(s(y0)), s(s(y0)), s(s(s(inc(x0)))))
The TRS R consists of the following rules:
inc(0) → s(0)
inc(s(x)) → s(inc(x))
inc(x) → s(x)
p(s(x)) → x
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)))
inc(x0)
p(0)
p(s(x0))
We have to consider all minimal (P,Q,R)-chains.
(97) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 2 less nodes.
(98) Obligation:
Q DP problem:
The TRS P consists of the following rules:
PLUS(s(s(x0)), s(s(0))) → IFPLUS(isZero(s(x0)), s(s(x0)), s(s(s(0))))
IFPLUS(false, s(s(z0)), s(s(z1))) → PLUS(s(z0), s(s(z1)))
PLUS(s(s(x0)), s(s(z1))) → IFPLUS(isZero(s(x0)), s(s(x0)), s(s(s(z1))))
IFPLUS(false, s(s(z0)), s(s(z1))) → PLUS(s(p(s(z0))), s(s(z1)))
PLUS(s(s(y0)), s(s(s(x0)))) → IFPLUS(isZero(s(y0)), s(s(y0)), s(s(s(inc(x0)))))
The TRS R consists of the following rules:
inc(0) → s(0)
inc(s(x)) → s(inc(x))
inc(x) → s(x)
p(s(x)) → x
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)))
inc(x0)
p(0)
p(s(x0))
We have to consider all minimal (P,Q,R)-chains.
(99) ForwardInstantiation (EQUIVALENT transformation)
By forward instantiating [JAR06] the rule
IFPLUS(
false,
s(
s(
z0)),
s(
s(
z1))) →
PLUS(
s(
z0),
s(
s(
z1))) we obtained the following new rules [LPAR04]:
IFPLUS(false, s(s(s(y_0))), s(s(0))) → PLUS(s(s(y_0)), s(s(0)))
IFPLUS(false, s(s(s(y_0))), s(s(x1))) → PLUS(s(s(y_0)), s(s(x1)))
IFPLUS(false, s(s(s(y_0))), s(s(s(y_1)))) → PLUS(s(s(y_0)), s(s(s(y_1))))
(100) Obligation:
Q DP problem:
The TRS P consists of the following rules:
PLUS(s(s(x0)), s(s(0))) → IFPLUS(isZero(s(x0)), s(s(x0)), s(s(s(0))))
PLUS(s(s(x0)), s(s(z1))) → IFPLUS(isZero(s(x0)), s(s(x0)), s(s(s(z1))))
IFPLUS(false, s(s(z0)), s(s(z1))) → PLUS(s(p(s(z0))), s(s(z1)))
PLUS(s(s(y0)), s(s(s(x0)))) → IFPLUS(isZero(s(y0)), s(s(y0)), s(s(s(inc(x0)))))
IFPLUS(false, s(s(s(y_0))), s(s(0))) → PLUS(s(s(y_0)), s(s(0)))
IFPLUS(false, s(s(s(y_0))), s(s(x1))) → PLUS(s(s(y_0)), s(s(x1)))
IFPLUS(false, s(s(s(y_0))), s(s(s(y_1)))) → PLUS(s(s(y_0)), s(s(s(y_1))))
The TRS R consists of the following rules:
inc(0) → s(0)
inc(s(x)) → s(inc(x))
inc(x) → s(x)
p(s(x)) → x
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)))
inc(x0)
p(0)
p(s(x0))
We have to consider all minimal (P,Q,R)-chains.
(101) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.
(102) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IFPLUS(false, s(s(z0)), s(s(z1))) → PLUS(s(p(s(z0))), s(s(z1)))
PLUS(s(s(x0)), s(s(0))) → IFPLUS(isZero(s(x0)), s(s(x0)), s(s(s(0))))
IFPLUS(false, s(s(s(y_0))), s(s(x1))) → PLUS(s(s(y_0)), s(s(x1)))
PLUS(s(s(x0)), s(s(z1))) → IFPLUS(isZero(s(x0)), s(s(x0)), s(s(s(z1))))
IFPLUS(false, s(s(s(y_0))), s(s(s(y_1)))) → PLUS(s(s(y_0)), s(s(s(y_1))))
PLUS(s(s(y0)), s(s(s(x0)))) → IFPLUS(isZero(s(y0)), s(s(y0)), s(s(s(inc(x0)))))
The TRS R consists of the following rules:
inc(0) → s(0)
inc(s(x)) → s(inc(x))
inc(x) → s(x)
p(s(x)) → x
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)))
inc(x0)
p(0)
p(s(x0))
We have to consider all minimal (P,Q,R)-chains.
(103) QDPOrderProof (EQUIVALENT transformation)
We use the reduction pair processor [LPAR04].
The following pairs can be oriented strictly and are deleted.
IFPLUS(false, s(s(s(y_0))), s(s(x1))) → PLUS(s(s(y_0)), s(s(x1)))
IFPLUS(false, s(s(s(y_0))), s(s(s(y_1)))) → PLUS(s(s(y_0)), s(s(s(y_1))))
The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO]:
POL(IFPLUS(x1, x2, x3)) = | | + | | · | x1 | + | | · | x2 | + | | · | x3 |
POL(PLUS(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
The following usable rules [FROCOS05] were oriented:
p(s(s(x))) → s(p(s(x)))
p(s(x)) → x
(104) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IFPLUS(false, s(s(z0)), s(s(z1))) → PLUS(s(p(s(z0))), s(s(z1)))
PLUS(s(s(x0)), s(s(0))) → IFPLUS(isZero(s(x0)), s(s(x0)), s(s(s(0))))
PLUS(s(s(x0)), s(s(z1))) → IFPLUS(isZero(s(x0)), s(s(x0)), s(s(s(z1))))
PLUS(s(s(y0)), s(s(s(x0)))) → IFPLUS(isZero(s(y0)), s(s(y0)), s(s(s(inc(x0)))))
The TRS R consists of the following rules:
inc(0) → s(0)
inc(s(x)) → s(inc(x))
inc(x) → s(x)
p(s(x)) → x
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)))
inc(x0)
p(0)
p(s(x0))
We have to consider all minimal (P,Q,R)-chains.
(105) QDPOrderProof (EQUIVALENT transformation)
We use the reduction pair processor [LPAR04].
The following pairs can be oriented strictly and are deleted.
IFPLUS(false, s(s(z0)), s(s(z1))) → PLUS(s(p(s(z0))), s(s(z1)))
The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO]:
POL(IFPLUS(x1, x2, x3)) = | | + | | · | x1 | + | | · | x2 | + | | · | x3 |
POL(PLUS(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
The following usable rules [FROCOS05] were oriented:
p(s(s(x))) → s(p(s(x)))
p(s(x)) → x
(106) Obligation:
Q DP problem:
The TRS P consists of the following rules:
PLUS(s(s(x0)), s(s(0))) → IFPLUS(isZero(s(x0)), s(s(x0)), s(s(s(0))))
PLUS(s(s(x0)), s(s(z1))) → IFPLUS(isZero(s(x0)), s(s(x0)), s(s(s(z1))))
PLUS(s(s(y0)), s(s(s(x0)))) → IFPLUS(isZero(s(y0)), s(s(y0)), s(s(s(inc(x0)))))
The TRS R consists of the following rules:
inc(0) → s(0)
inc(s(x)) → s(inc(x))
inc(x) → s(x)
p(s(x)) → x
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)))
inc(x0)
p(0)
p(s(x0))
We have to consider all minimal (P,Q,R)-chains.
(107) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 3 less nodes.
(108) TRUE
(109) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IFTIMES(false, i, x, y, z) → TIMESITER(inc(i), x, y, plus(z, y))
TIMESITER(i, x, y, z) → IFTIMES(ge(i, x), i, x, y, z)
The TRS R consists of the following rules:
plus(x, y) → ifPlus(isZero(x), x, inc(y))
ifPlus(true, x, y) → p(y)
ifPlus(false, x, y) → plus(p(x), y)
times(x, y) → timesIter(0, x, y, 0)
timesIter(i, x, y, z) → ifTimes(ge(i, x), i, x, y, z)
ifTimes(true, i, x, y, z) → z
ifTimes(false, i, x, y, z) → timesIter(inc(i), x, y, plus(z, y))
isZero(0) → true
isZero(s(0)) → false
isZero(s(s(x))) → isZero(s(x))
inc(0) → s(0)
inc(s(x)) → s(inc(x))
inc(x) → s(x)
p(0) → 0
p(s(x)) → x
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)
f0(0, y, x) → f1(x, y, x)
f1(x, y, z) → f2(x, y, z)
f2(x, 1, z) → f0(x, z, z)
f0(x, y, z) → d
f1(x, y, z) → c
The set Q consists of the following terms:
plus(x0, x1)
ifPlus(true, x0, x1)
ifPlus(false, x0, x1)
times(x0, x1)
timesIter(x0, x1, x2, x3)
ifTimes(true, x0, x1, x2, x3)
ifTimes(false, x0, x1, x2, x3)
isZero(0)
isZero(s(0))
isZero(s(s(x0)))
inc(x0)
p(0)
p(s(x0))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
f1(x0, x1, x2)
f2(x0, 1, x1)
f0(x0, x1, x2)
We have to consider all minimal (P,Q,R)-chains.
(110) 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.
(111) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IFTIMES(false, i, x, y, z) → TIMESITER(inc(i), x, y, plus(z, y))
TIMESITER(i, x, y, z) → IFTIMES(ge(i, x), i, 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)
inc(0) → s(0)
inc(s(x)) → s(inc(x))
inc(x) → s(x)
ifPlus(false, x, y) → plus(p(x), y)
plus(x, y) → ifPlus(isZero(x), x, inc(y))
p(0) → 0
p(s(x)) → x
p(s(s(x))) → s(p(s(x)))
isZero(0) → true
isZero(s(0)) → false
isZero(s(s(x))) → isZero(s(x))
ifPlus(true, x, y) → p(y)
The set Q consists of the following terms:
plus(x0, x1)
ifPlus(true, x0, x1)
ifPlus(false, x0, x1)
times(x0, x1)
timesIter(x0, x1, x2, x3)
ifTimes(true, x0, x1, x2, x3)
ifTimes(false, x0, x1, x2, x3)
isZero(0)
isZero(s(0))
isZero(s(s(x0)))
inc(x0)
p(0)
p(s(x0))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
f1(x0, x1, x2)
f2(x0, 1, x1)
f0(x0, x1, x2)
We have to consider all minimal (P,Q,R)-chains.
(112) 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)
timesIter(x0, x1, x2, x3)
ifTimes(true, x0, x1, x2, x3)
ifTimes(false, x0, x1, x2, x3)
f1(x0, x1, x2)
f2(x0, 1, x1)
f0(x0, x1, x2)
(113) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IFTIMES(false, i, x, y, z) → TIMESITER(inc(i), x, y, plus(z, y))
TIMESITER(i, x, y, z) → IFTIMES(ge(i, x), i, 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)
inc(0) → s(0)
inc(s(x)) → s(inc(x))
inc(x) → s(x)
ifPlus(false, x, y) → plus(p(x), y)
plus(x, y) → ifPlus(isZero(x), x, inc(y))
p(0) → 0
p(s(x)) → x
p(s(s(x))) → s(p(s(x)))
isZero(0) → true
isZero(s(0)) → false
isZero(s(s(x))) → isZero(s(x))
ifPlus(true, x, y) → p(y)
The set Q consists of the following terms:
plus(x0, x1)
ifPlus(true, x0, x1)
ifPlus(false, x0, x1)
isZero(0)
isZero(s(0))
isZero(s(s(x0)))
inc(x0)
p(0)
p(s(x0))
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
IFTIMES(
false,
i,
x,
y,
z) →
TIMESITER(
inc(
i),
x,
y,
plus(
z,
y)) the following chains were created:
- We consider the chain TIMESITER(i, x, y, z) → IFTIMES(ge(i, x), i, x, y, z), IFTIMES(false, i, x, y, z) → TIMESITER(inc(i), x, y, plus(z, y)) which results in the following constraint:
(1) (IFTIMES(ge(x4, x5), x4, x5, x6, x7)=IFTIMES(false, x8, x9, x10, x11) ⇒ IFTIMES(false, x8, x9, x10, x11)≥TIMESITER(inc(x8), x9, x10, plus(x11, x10)))
We simplified constraint (1) using rules (I), (II), (III) which results in the following new constraint:
(2) (ge(x4, x5)=false ⇒ IFTIMES(false, x4, x5, x6, x7)≥TIMESITER(inc(x4), x5, x6, plus(x7, x6)))
We simplified constraint (2) using rule (V) (with possible (I) afterwards) using induction on ge(x4, x5)=false which results in the following new constraints:
(3) (false=false ⇒ IFTIMES(false, 0, s(x25), x6, x7)≥TIMESITER(inc(0), s(x25), x6, plus(x7, x6)))
(4) (ge(x27, x26)=false∧(∀x28,x29:ge(x27, x26)=false ⇒ IFTIMES(false, x27, x26, x28, x29)≥TIMESITER(inc(x27), x26, x28, plus(x29, x28))) ⇒ IFTIMES(false, s(x27), s(x26), x6, x7)≥TIMESITER(inc(s(x27)), s(x26), x6, plus(x7, x6)))
We simplified constraint (3) using rules (I), (II) which results in the following new constraint:
(5) (IFTIMES(false, 0, s(x25), x6, x7)≥TIMESITER(inc(0), s(x25), x6, plus(x7, x6)))
We simplified constraint (4) using rule (VI) where we applied the induction hypothesis (∀x28,x29:ge(x27, x26)=false ⇒ IFTIMES(false, x27, x26, x28, x29)≥TIMESITER(inc(x27), x26, x28, plus(x29, x28))) with σ = [x28 / x6, x29 / x7] which results in the following new constraint:
(6) (IFTIMES(false, x27, x26, x6, x7)≥TIMESITER(inc(x27), x26, x6, plus(x7, x6)) ⇒ IFTIMES(false, s(x27), s(x26), x6, x7)≥TIMESITER(inc(s(x27)), s(x26), x6, plus(x7, x6)))
For Pair
TIMESITER(
i,
x,
y,
z) →
IFTIMES(
ge(
i,
x),
i,
x,
y,
z) the following chains were created:
- We consider the chain IFTIMES(false, i, x, y, z) → TIMESITER(inc(i), x, y, plus(z, y)), TIMESITER(i, x, y, z) → IFTIMES(ge(i, x), i, x, y, z) which results in the following constraint:
(7) (TIMESITER(inc(x12), x13, x14, plus(x15, x14))=TIMESITER(x16, x17, x18, x19) ⇒ TIMESITER(x16, x17, x18, x19)≥IFTIMES(ge(x16, x17), x16, x17, x18, x19))
We simplified constraint (7) using rules (I), (II), (III), (IV) which results in the following new constraint:
(8) (TIMESITER(x16, x13, x14, x19)≥IFTIMES(ge(x16, x13), x16, x13, x14, x19))
To summarize, we get the following constraints P
≥ for the following pairs.
- IFTIMES(false, i, x, y, z) → TIMESITER(inc(i), x, y, plus(z, y))
- (IFTIMES(false, 0, s(x25), x6, x7)≥TIMESITER(inc(0), s(x25), x6, plus(x7, x6)))
- (IFTIMES(false, x27, x26, x6, x7)≥TIMESITER(inc(x27), x26, x6, plus(x7, x6)) ⇒ IFTIMES(false, s(x27), s(x26), x6, x7)≥TIMESITER(inc(s(x27)), s(x26), x6, plus(x7, x6)))
- TIMESITER(i, x, y, z) → IFTIMES(ge(i, x), i, x, y, z)
- (TIMESITER(x16, x13, x14, x19)≥IFTIMES(ge(x16, x13), x16, x13, x14, x19))
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) = 0
POL(IFTIMES(x1, x2, x3, x4, x5)) = -1 - x1 - x2 + x3 + x4
POL(TIMESITER(x1, x2, x3, x4)) = -1 - x1 + x2 + x3
POL(c) = -1
POL(false) = 0
POL(ge(x1, x2)) = 0
POL(ifPlus(x1, x2, x3)) = 0
POL(inc(x1)) = 1 + x1
POL(isZero(x1)) = 0
POL(p(x1)) = 0
POL(plus(x1, x2)) = 0
POL(s(x1)) = 1 + x1
POL(true) = 1
The following pairs are in P
>:
IFTIMES(false, i, x, y, z) → TIMESITER(inc(i), x, y, plus(z, y))
The following pairs are in P
bound:
IFTIMES(false, i, x, y, z) → TIMESITER(inc(i), x, y, plus(z, y))
The following rules are usable:
s(inc(x)) → inc(s(x))
s(x) → inc(x)
ge(x, y) → ge(s(x), s(y))
s(0) → inc(0)
true → ge(x, 0)
false → ge(0, s(y))
(115) Obligation:
Q DP problem:
The TRS P consists of the following rules:
TIMESITER(i, x, y, z) → IFTIMES(ge(i, x), i, 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)
inc(0) → s(0)
inc(s(x)) → s(inc(x))
inc(x) → s(x)
ifPlus(false, x, y) → plus(p(x), y)
plus(x, y) → ifPlus(isZero(x), x, inc(y))
p(0) → 0
p(s(x)) → x
p(s(s(x))) → s(p(s(x)))
isZero(0) → true
isZero(s(0)) → false
isZero(s(s(x))) → isZero(s(x))
ifPlus(true, x, y) → p(y)
The set Q consists of the following terms:
plus(x0, x1)
ifPlus(true, x0, x1)
ifPlus(false, x0, x1)
isZero(0)
isZero(s(0))
isZero(s(s(x0)))
inc(x0)
p(0)
p(s(x0))
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