Termination w.r.t. Q of the given QTRS could be proven:

0 QTRS
↳1 AAECC Innermost (⇔)
↳2 QTRS
↳3 DependencyPairsProof (⇔)
↳4 QDP
↳5 DependencyGraphProof (⇔)
↳6 AND
  ↳7 QDP
    ↳8 UsableRulesProof (⇔)
    ↳9 QDP
    ↳10 QReductionProof (⇔)
    ↳11 QDP
      ↳12 Instantiation (⇔)
        ↳13 QDP
      ↳14 Instantiation (⇔)
        ↳15 QDP
        ↳16 Instantiation (⇔)
        ↳17 QDP
        ↳18 Instantiation (⇔)
        ↳19 QDP
        ↳20 Instantiation (⇔)
        ↳21 QDP
        ↳22 DependencyGraphProof (⇔)
        ↳23 TRUE
  ↳24 QDP
    ↳25 UsableRulesProof (⇔)
    ↳26 QDP
    ↳27 QReductionProof (⇔)
    ↳28 QDP
    ↳29 QDPSizeChangeProof (⇔)
    ↳30 TRUE
  ↳31 QDP
    ↳32 UsableRulesProof (⇔)
    ↳33 QDP
    ↳34 QReductionProof (⇔)
    ↳35 QDP
    ↳36 QDPSizeChangeProof (⇔)
    ↳37 TRUE
  ↳38 QDP
    ↳39 UsableRulesProof (⇔)
    ↳40 QDP
    ↳41 QReductionProof (⇔)
    ↳42 QDP
    ↳43 QDPSizeChangeProof (⇔)
    ↳44 TRUE
  ↳45 QDP
    ↳46 UsableRulesProof (⇔)
    ↳47 QDP
    ↳48 QReductionProof (⇔)
    ↳49 QDP
    ↳50 QDPSizeChangeProof (⇔)
    ↳51 TRUE
  ↳52 QDP
    ↳53 UsableRulesProof (⇔)
    ↳54 QDP
    ↳55 QReductionProof (⇔)
    ↳56 QDP
    ↳57 Narrowing (⇔)
    ↳58 QDP
    ↳59 DependencyGraphProof (⇔)
    ↳60 QDP
    ↳61 UsableRulesProof (⇔)
    ↳62 QDP
    ↳63 Narrowing (⇔)
    ↳64 QDP
    ↳65 Narrowing (⇔)
    ↳66 QDP
    ↳67 DependencyGraphProof (⇔)
    ↳68 QDP
    ↳69 UsableRulesProof (⇔)
    ↳70 QDP
    ↳71 Narrowing (⇔)
    ↳72 QDP
    ↳73 Instantiation (⇔)
    ↳74 QDP
    ↳75 DependencyGraphProof (⇔)
    ↳76 QDP
    ↳77 Instantiation (⇔)
    ↳78 QDP
    ↳79 DependencyGraphProof (⇔)
    ↳80 QDP
    ↳81 Instantiation (⇔)
    ↳82 QDP
    ↳83 Narrowing (⇔)
    ↳84 QDP
    ↳85 DependencyGraphProof (⇔)
    ↳86 QDP
    ↳87 Instantiation (⇔)
    ↳88 QDP
    ↳89 Instantiation (⇔)
    ↳90 QDP
    ↳91 DependencyGraphProof (⇔)
    ↳92 QDP
    ↳93 Instantiation (⇔)
    ↳94 QDP
    ↳95 Narrowing (⇔)
    ↳96 QDP
    ↳97 DependencyGraphProof (⇔)
    ↳98 QDP
    ↳99 ForwardInstantiation (⇔)
    ↳100 QDP
    ↳101 DependencyGraphProof (⇔)
    ↳102 QDP
    ↳103 QDPOrderProof (⇔)
    ↳104 QDP
    ↳105 QDPOrderProof (⇔)
    ↳106 QDP
    ↳107 DependencyGraphProof (⇔)
    ↳108 TRUE
  ↳109 QDP
    ↳110 UsableRulesProof (⇔)
    ↳111 QDP
    ↳112 QReductionProof (⇔)
    ↳113 QDP
    ↳114 NonInfProof (⇔)
    ↳115 QDP
    ↳116 DependencyGraphProof (⇔)
    ↳117 TRUE

(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: Polynomial interpretation [POLO]:

POL(0) = 0   
POL(IFPLUS(x1, x2, x3)) = x2   
POL(PLUS(x1, x2)) = x1   
POL(false) = 0   
POL(inc(x1)) = 0   
POL(isZero(x1)) = 0   
POL(p(x1)) = x1   
POL(s(x1)) = 1 + x1   

The following usable rules [FROCOS05] were oriented:

p(s(x)) → x
p(s(s(x))) → s(p(s(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.


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 remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO]:

POL(IFPLUS(x1, x2, x3)) =
/0\
\0/
 +
/00\
\00/
·x1 +
/10\
\00/
·x2 +
/00\
\00/
·x3

POL(false) =
/1\
\1/

POL(s(x1)) =
/0\
\1/
 +
/11\
\11/
·x1

POL(PLUS(x1, x2)) =
/1\
\0/
 +
/10\
\00/
·x1 +
/00\
\00/
·x2

POL(p(x1)) =
/0\
\0/
 +
/10\
\10/
·x1

POL(0) =
/1\
\0/

POL(isZero(x1)) =
/0\
\0/
 +
/00\
\00/
·x1

POL(inc(x1)) =
/0\
\0/
 +
/00\
\00/
·x1

The following usable rules [FROCOS05] were oriented:

p(s(x)) → x
p(s(s(x))) → s(p(s(x)))

(106) 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)))

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 1 less node.

(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 Pbound 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 Pbound.
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   
POL(TIMESITER(x1, x2, x3, x4)) = -1 - x1 + x2   
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)) = 1   
POL(p(x1)) = 0   
POL(plus(x1, x2)) = 1   
POL(s(x1)) = 1 + x1   
POL(true) = 0   

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 Pbound:

IFTIMES(false, i, x, y, z) → TIMESITER(inc(i), x, y, plus(z, y))
The following rules are usable:

s(0) → inc(0)
s(inc(x)) → inc(s(x))
false → ge(0, s(y))
ge(x, y) → ge(s(x), s(y))
true → ge(x, 0)
s(x) → inc(x)

(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