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

(0) Obligation:

Q restricted rewrite system:
The TRS R consists of the following rules:

times(x, y) → sum(generate(x, y))
generate(x, y) → gen(x, y, 0)
gen(x, y, z) → if(ge(z, x), x, y, z)
if(true, x, y, z) → nil
if(false, x, y, z) → cons(y, gen(x, y, s(z)))
sum(xs) → sum2(xs, 0)
sum2(xs, y) → ifsum(isNil(xs), isZero(head(xs)), xs, y)
ifsum(true, b, xs, y) → y
ifsum(false, b, xs, y) → ifsum2(b, xs, y)
ifsum2(true, xs, y) → sum2(tail(xs), y)
ifsum2(false, xs, y) → sum2(cons(p(head(xs)), tail(xs)), s(y))
isNil(nil) → true
isNil(cons(x, xs)) → false
tail(nil) → nil
tail(cons(x, xs)) → xs
head(cons(x, xs)) → x
head(nil) → error
isZero(0) → true
isZero(s(0)) → false
isZero(s(s(x))) → isZero(s(x))
p(0) → s(s(0))
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
ge(x, 0) → true
ge(0, s(y)) → false
ge(s(x), s(y)) → ge(x, y)
a → c
a → d

Q is empty.

(1) AAECC Innermost (EQUIVALENT transformation)

We have applied [NOC,AAECCNOC] to switch to innermost. The TRS R 1 is

generate(x, y) → gen(x, y, 0)
gen(x, y, z) → if(ge(z, x), x, y, z)
if(true, x, y, z) → nil
if(false, x, y, z) → cons(y, gen(x, y, s(z)))
ifsum(true, b, xs, y) → y
ifsum(false, b, xs, y) → ifsum2(b, xs, y)
ifsum2(true, xs, y) → sum2(tail(xs), y)
ifsum2(false, xs, y) → sum2(cons(p(head(xs)), tail(xs)), s(y))
isNil(nil) → true
isNil(cons(x, xs)) → false
tail(nil) → nil
tail(cons(x, xs)) → xs
head(cons(x, xs)) → x
head(nil) → error
isZero(0) → true
isZero(s(0)) → false
isZero(s(s(x))) → isZero(s(x))
p(0) → s(s(0))
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
ge(x, 0) → true
ge(0, s(y)) → false
ge(s(x), s(y)) → ge(x, y)
sum(xs) → sum2(xs, 0)
sum2(xs, y) → ifsum(isNil(xs), isZero(head(xs)), xs, y)
times(x, y) → sum(generate(x, y))

The TRS R 2 is

a → c
a → d

The signature Sigma is {c, a, d}

(2) Obligation:

Q restricted rewrite system:
The TRS R consists of the following rules:

times(x, y) → sum(generate(x, y))
generate(x, y) → gen(x, y, 0)
gen(x, y, z) → if(ge(z, x), x, y, z)
if(true, x, y, z) → nil
if(false, x, y, z) → cons(y, gen(x, y, s(z)))
sum(xs) → sum2(xs, 0)
sum2(xs, y) → ifsum(isNil(xs), isZero(head(xs)), xs, y)
ifsum(true, b, xs, y) → y
ifsum(false, b, xs, y) → ifsum2(b, xs, y)
ifsum2(true, xs, y) → sum2(tail(xs), y)
ifsum2(false, xs, y) → sum2(cons(p(head(xs)), tail(xs)), s(y))
isNil(nil) → true
isNil(cons(x, xs)) → false
tail(nil) → nil
tail(cons(x, xs)) → xs
head(cons(x, xs)) → x
head(nil) → error
isZero(0) → true
isZero(s(0)) → false
isZero(s(s(x))) → isZero(s(x))
p(0) → s(s(0))
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
ge(x, 0) → true
ge(0, s(y)) → false
ge(s(x), s(y)) → ge(x, y)
a → c
a → d

The set Q consists of the following terms:

times(x0, x1)
generate(x0, x1)
gen(x0, x1, x2)
if(true, x0, x1, x2)
if(false, x0, x1, x2)
sum(x0)
sum2(x0, x1)
ifsum(true, x0, x1, x2)
ifsum(false, x0, x1, x2)
ifsum2(true, x0, x1)
ifsum2(false, x0, x1)
isNil(nil)
isNil(cons(x0, x1))
tail(nil)
tail(cons(x0, x1))
head(cons(x0, x1))
head(nil)
isZero(0)
isZero(s(0))
isZero(s(s(x0)))
p(0)
p(s(0))
p(s(s(x0)))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
a

(3) DependencyPairsProof (EQUIVALENT transformation)

Using Dependency Pairs [AG00,LPAR04] we result in the following initial DP problem.

(4) Obligation:

Q DP problem:
The TRS P consists of the following rules:

TIMES(x, y) → SUM(generate(x, y))
TIMES(x, y) → GENERATE(x, y)
GENERATE(x, y) → GEN(x, y, 0)
GEN(x, y, z) → IF(ge(z, x), x, y, z)
GEN(x, y, z) → GE(z, x)
IF(false, x, y, z) → GEN(x, y, s(z))
SUM(xs) → SUM2(xs, 0)
SUM2(xs, y) → IFSUM(isNil(xs), isZero(head(xs)), xs, y)
SUM2(xs, y) → ISNIL(xs)
SUM2(xs, y) → ISZERO(head(xs))
SUM2(xs, y) → HEAD(xs)
IFSUM(false, b, xs, y) → IFSUM2(b, xs, y)
IFSUM2(true, xs, y) → SUM2(tail(xs), y)
IFSUM2(true, xs, y) → TAIL(xs)
IFSUM2(false, xs, y) → SUM2(cons(p(head(xs)), tail(xs)), s(y))
IFSUM2(false, xs, y) → P(head(xs))
IFSUM2(false, xs, y) → HEAD(xs)
IFSUM2(false, xs, y) → TAIL(xs)
ISZERO(s(s(x))) → ISZERO(s(x))
P(s(s(x))) → P(s(x))
GE(s(x), s(y)) → GE(x, y)

The TRS R consists of the following rules:

times(x, y) → sum(generate(x, y))
generate(x, y) → gen(x, y, 0)
gen(x, y, z) → if(ge(z, x), x, y, z)
if(true, x, y, z) → nil
if(false, x, y, z) → cons(y, gen(x, y, s(z)))
sum(xs) → sum2(xs, 0)
sum2(xs, y) → ifsum(isNil(xs), isZero(head(xs)), xs, y)
ifsum(true, b, xs, y) → y
ifsum(false, b, xs, y) → ifsum2(b, xs, y)
ifsum2(true, xs, y) → sum2(tail(xs), y)
ifsum2(false, xs, y) → sum2(cons(p(head(xs)), tail(xs)), s(y))
isNil(nil) → true
isNil(cons(x, xs)) → false
tail(nil) → nil
tail(cons(x, xs)) → xs
head(cons(x, xs)) → x
head(nil) → error
isZero(0) → true
isZero(s(0)) → false
isZero(s(s(x))) → isZero(s(x))
p(0) → s(s(0))
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
ge(x, 0) → true
ge(0, s(y)) → false
ge(s(x), s(y)) → ge(x, y)
a → c
a → d

The set Q consists of the following terms:

times(x0, x1)
generate(x0, x1)
gen(x0, x1, x2)
if(true, x0, x1, x2)
if(false, x0, x1, x2)
sum(x0)
sum2(x0, x1)
ifsum(true, x0, x1, x2)
ifsum(false, x0, x1, x2)
ifsum2(true, x0, x1)
ifsum2(false, x0, x1)
isNil(nil)
isNil(cons(x0, x1))
tail(nil)
tail(cons(x0, x1))
head(cons(x0, x1))
head(nil)
isZero(0)
isZero(s(0))
isZero(s(s(x0)))
p(0)
p(s(0))
p(s(s(x0)))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
a

We have to consider all minimal (P,Q,R)-chains.

(5) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 5 SCCs with 12 less nodes.

(6) Complex Obligation (AND)

(7) Obligation:

Q DP problem:
The TRS P consists of the following rules:

GE(s(x), s(y)) → GE(x, y)

The TRS R consists of the following rules:

times(x, y) → sum(generate(x, y))
generate(x, y) → gen(x, y, 0)
gen(x, y, z) → if(ge(z, x), x, y, z)
if(true, x, y, z) → nil
if(false, x, y, z) → cons(y, gen(x, y, s(z)))
sum(xs) → sum2(xs, 0)
sum2(xs, y) → ifsum(isNil(xs), isZero(head(xs)), xs, y)
ifsum(true, b, xs, y) → y
ifsum(false, b, xs, y) → ifsum2(b, xs, y)
ifsum2(true, xs, y) → sum2(tail(xs), y)
ifsum2(false, xs, y) → sum2(cons(p(head(xs)), tail(xs)), s(y))
isNil(nil) → true
isNil(cons(x, xs)) → false
tail(nil) → nil
tail(cons(x, xs)) → xs
head(cons(x, xs)) → x
head(nil) → error
isZero(0) → true
isZero(s(0)) → false
isZero(s(s(x))) → isZero(s(x))
p(0) → s(s(0))
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
ge(x, 0) → true
ge(0, s(y)) → false
ge(s(x), s(y)) → ge(x, y)
a → c
a → d

The set Q consists of the following terms:

times(x0, x1)
generate(x0, x1)
gen(x0, x1, x2)
if(true, x0, x1, x2)
if(false, x0, x1, x2)
sum(x0)
sum2(x0, x1)
ifsum(true, x0, x1, x2)
ifsum(false, x0, x1, x2)
ifsum2(true, x0, x1)
ifsum2(false, x0, x1)
isNil(nil)
isNil(cons(x0, x1))
tail(nil)
tail(cons(x0, x1))
head(cons(x0, x1))
head(nil)
isZero(0)
isZero(s(0))
isZero(s(s(x0)))
p(0)
p(s(0))
p(s(s(x0)))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
a

We have to consider all minimal (P,Q,R)-chains.

(8) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(9) Obligation:

Q DP problem:
The TRS P consists of the following rules:

GE(s(x), s(y)) → GE(x, y)

R is empty.
The set Q consists of the following terms:

times(x0, x1)
generate(x0, x1)
gen(x0, x1, x2)
if(true, x0, x1, x2)
if(false, x0, x1, x2)
sum(x0)
sum2(x0, x1)
ifsum(true, x0, x1, x2)
ifsum(false, x0, x1, x2)
ifsum2(true, x0, x1)
ifsum2(false, x0, x1)
isNil(nil)
isNil(cons(x0, x1))
tail(nil)
tail(cons(x0, x1))
head(cons(x0, x1))
head(nil)
isZero(0)
isZero(s(0))
isZero(s(s(x0)))
p(0)
p(s(0))
p(s(s(x0)))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
a

We have to consider all minimal (P,Q,R)-chains.

(10) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

times(x0, x1)
generate(x0, x1)
gen(x0, x1, x2)
if(true, x0, x1, x2)
if(false, x0, x1, x2)
sum(x0)
sum2(x0, x1)
ifsum(true, x0, x1, x2)
ifsum(false, x0, x1, x2)
ifsum2(true, x0, x1)
ifsum2(false, x0, x1)
isNil(nil)
isNil(cons(x0, x1))
tail(nil)
tail(cons(x0, x1))
head(cons(x0, x1))
head(nil)
isZero(0)
isZero(s(0))
isZero(s(s(x0)))
p(0)
p(s(0))
p(s(s(x0)))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
a

(11) Obligation:

Q DP problem:
The TRS P consists of the following rules:

GE(s(x), s(y)) → GE(x, y)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(12) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • GE(s(x), s(y)) → GE(x, y)
    The graph contains the following edges 1 > 1, 2 > 2

(13) TRUE

(14) Obligation:

Q DP problem:
The TRS P consists of the following rules:

P(s(s(x))) → P(s(x))

The TRS R consists of the following rules:

times(x, y) → sum(generate(x, y))
generate(x, y) → gen(x, y, 0)
gen(x, y, z) → if(ge(z, x), x, y, z)
if(true, x, y, z) → nil
if(false, x, y, z) → cons(y, gen(x, y, s(z)))
sum(xs) → sum2(xs, 0)
sum2(xs, y) → ifsum(isNil(xs), isZero(head(xs)), xs, y)
ifsum(true, b, xs, y) → y
ifsum(false, b, xs, y) → ifsum2(b, xs, y)
ifsum2(true, xs, y) → sum2(tail(xs), y)
ifsum2(false, xs, y) → sum2(cons(p(head(xs)), tail(xs)), s(y))
isNil(nil) → true
isNil(cons(x, xs)) → false
tail(nil) → nil
tail(cons(x, xs)) → xs
head(cons(x, xs)) → x
head(nil) → error
isZero(0) → true
isZero(s(0)) → false
isZero(s(s(x))) → isZero(s(x))
p(0) → s(s(0))
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
ge(x, 0) → true
ge(0, s(y)) → false
ge(s(x), s(y)) → ge(x, y)
a → c
a → d

The set Q consists of the following terms:

times(x0, x1)
generate(x0, x1)
gen(x0, x1, x2)
if(true, x0, x1, x2)
if(false, x0, x1, x2)
sum(x0)
sum2(x0, x1)
ifsum(true, x0, x1, x2)
ifsum(false, x0, x1, x2)
ifsum2(true, x0, x1)
ifsum2(false, x0, x1)
isNil(nil)
isNil(cons(x0, x1))
tail(nil)
tail(cons(x0, x1))
head(cons(x0, x1))
head(nil)
isZero(0)
isZero(s(0))
isZero(s(s(x0)))
p(0)
p(s(0))
p(s(s(x0)))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
a

We have to consider all minimal (P,Q,R)-chains.

(15) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(16) Obligation:

Q DP problem:
The TRS P consists of the following rules:

P(s(s(x))) → P(s(x))

R is empty.
The set Q consists of the following terms:

times(x0, x1)
generate(x0, x1)
gen(x0, x1, x2)
if(true, x0, x1, x2)
if(false, x0, x1, x2)
sum(x0)
sum2(x0, x1)
ifsum(true, x0, x1, x2)
ifsum(false, x0, x1, x2)
ifsum2(true, x0, x1)
ifsum2(false, x0, x1)
isNil(nil)
isNil(cons(x0, x1))
tail(nil)
tail(cons(x0, x1))
head(cons(x0, x1))
head(nil)
isZero(0)
isZero(s(0))
isZero(s(s(x0)))
p(0)
p(s(0))
p(s(s(x0)))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
a

We have to consider all minimal (P,Q,R)-chains.

(17) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

times(x0, x1)
generate(x0, x1)
gen(x0, x1, x2)
if(true, x0, x1, x2)
if(false, x0, x1, x2)
sum(x0)
sum2(x0, x1)
ifsum(true, x0, x1, x2)
ifsum(false, x0, x1, x2)
ifsum2(true, x0, x1)
ifsum2(false, x0, x1)
isNil(nil)
isNil(cons(x0, x1))
tail(nil)
tail(cons(x0, x1))
head(cons(x0, x1))
head(nil)
isZero(0)
isZero(s(0))
isZero(s(s(x0)))
p(0)
p(s(0))
p(s(s(x0)))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
a

(18) Obligation:

Q DP problem:
The TRS P consists of the following rules:

P(s(s(x))) → P(s(x))

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(19) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • P(s(s(x))) → P(s(x))
    The graph contains the following edges 1 > 1

(20) TRUE

(21) Obligation:

Q DP problem:
The TRS P consists of the following rules:

ISZERO(s(s(x))) → ISZERO(s(x))

The TRS R consists of the following rules:

times(x, y) → sum(generate(x, y))
generate(x, y) → gen(x, y, 0)
gen(x, y, z) → if(ge(z, x), x, y, z)
if(true, x, y, z) → nil
if(false, x, y, z) → cons(y, gen(x, y, s(z)))
sum(xs) → sum2(xs, 0)
sum2(xs, y) → ifsum(isNil(xs), isZero(head(xs)), xs, y)
ifsum(true, b, xs, y) → y
ifsum(false, b, xs, y) → ifsum2(b, xs, y)
ifsum2(true, xs, y) → sum2(tail(xs), y)
ifsum2(false, xs, y) → sum2(cons(p(head(xs)), tail(xs)), s(y))
isNil(nil) → true
isNil(cons(x, xs)) → false
tail(nil) → nil
tail(cons(x, xs)) → xs
head(cons(x, xs)) → x
head(nil) → error
isZero(0) → true
isZero(s(0)) → false
isZero(s(s(x))) → isZero(s(x))
p(0) → s(s(0))
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
ge(x, 0) → true
ge(0, s(y)) → false
ge(s(x), s(y)) → ge(x, y)
a → c
a → d

The set Q consists of the following terms:

times(x0, x1)
generate(x0, x1)
gen(x0, x1, x2)
if(true, x0, x1, x2)
if(false, x0, x1, x2)
sum(x0)
sum2(x0, x1)
ifsum(true, x0, x1, x2)
ifsum(false, x0, x1, x2)
ifsum2(true, x0, x1)
ifsum2(false, x0, x1)
isNil(nil)
isNil(cons(x0, x1))
tail(nil)
tail(cons(x0, x1))
head(cons(x0, x1))
head(nil)
isZero(0)
isZero(s(0))
isZero(s(s(x0)))
p(0)
p(s(0))
p(s(s(x0)))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
a

We have to consider all minimal (P,Q,R)-chains.

(22) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(23) Obligation:

Q DP problem:
The TRS P consists of the following rules:

ISZERO(s(s(x))) → ISZERO(s(x))

R is empty.
The set Q consists of the following terms:

times(x0, x1)
generate(x0, x1)
gen(x0, x1, x2)
if(true, x0, x1, x2)
if(false, x0, x1, x2)
sum(x0)
sum2(x0, x1)
ifsum(true, x0, x1, x2)
ifsum(false, x0, x1, x2)
ifsum2(true, x0, x1)
ifsum2(false, x0, x1)
isNil(nil)
isNil(cons(x0, x1))
tail(nil)
tail(cons(x0, x1))
head(cons(x0, x1))
head(nil)
isZero(0)
isZero(s(0))
isZero(s(s(x0)))
p(0)
p(s(0))
p(s(s(x0)))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
a

We have to consider all minimal (P,Q,R)-chains.

(24) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

times(x0, x1)
generate(x0, x1)
gen(x0, x1, x2)
if(true, x0, x1, x2)
if(false, x0, x1, x2)
sum(x0)
sum2(x0, x1)
ifsum(true, x0, x1, x2)
ifsum(false, x0, x1, x2)
ifsum2(true, x0, x1)
ifsum2(false, x0, x1)
isNil(nil)
isNil(cons(x0, x1))
tail(nil)
tail(cons(x0, x1))
head(cons(x0, x1))
head(nil)
isZero(0)
isZero(s(0))
isZero(s(s(x0)))
p(0)
p(s(0))
p(s(s(x0)))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
a

(25) Obligation:

Q DP problem:
The TRS P consists of the following rules:

ISZERO(s(s(x))) → ISZERO(s(x))

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(26) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • ISZERO(s(s(x))) → ISZERO(s(x))
    The graph contains the following edges 1 > 1

(27) TRUE

(28) Obligation:

Q DP problem:
The TRS P consists of the following rules:

IFSUM(false, b, xs, y) → IFSUM2(b, xs, y)
IFSUM2(true, xs, y) → SUM2(tail(xs), y)
SUM2(xs, y) → IFSUM(isNil(xs), isZero(head(xs)), xs, y)
IFSUM2(false, xs, y) → SUM2(cons(p(head(xs)), tail(xs)), s(y))

The TRS R consists of the following rules:

times(x, y) → sum(generate(x, y))
generate(x, y) → gen(x, y, 0)
gen(x, y, z) → if(ge(z, x), x, y, z)
if(true, x, y, z) → nil
if(false, x, y, z) → cons(y, gen(x, y, s(z)))
sum(xs) → sum2(xs, 0)
sum2(xs, y) → ifsum(isNil(xs), isZero(head(xs)), xs, y)
ifsum(true, b, xs, y) → y
ifsum(false, b, xs, y) → ifsum2(b, xs, y)
ifsum2(true, xs, y) → sum2(tail(xs), y)
ifsum2(false, xs, y) → sum2(cons(p(head(xs)), tail(xs)), s(y))
isNil(nil) → true
isNil(cons(x, xs)) → false
tail(nil) → nil
tail(cons(x, xs)) → xs
head(cons(x, xs)) → x
head(nil) → error
isZero(0) → true
isZero(s(0)) → false
isZero(s(s(x))) → isZero(s(x))
p(0) → s(s(0))
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
ge(x, 0) → true
ge(0, s(y)) → false
ge(s(x), s(y)) → ge(x, y)
a → c
a → d

The set Q consists of the following terms:

times(x0, x1)
generate(x0, x1)
gen(x0, x1, x2)
if(true, x0, x1, x2)
if(false, x0, x1, x2)
sum(x0)
sum2(x0, x1)
ifsum(true, x0, x1, x2)
ifsum(false, x0, x1, x2)
ifsum2(true, x0, x1)
ifsum2(false, x0, x1)
isNil(nil)
isNil(cons(x0, x1))
tail(nil)
tail(cons(x0, x1))
head(cons(x0, x1))
head(nil)
isZero(0)
isZero(s(0))
isZero(s(s(x0)))
p(0)
p(s(0))
p(s(s(x0)))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
a

We have to consider all minimal (P,Q,R)-chains.

(29) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(30) Obligation:

Q DP problem:
The TRS P consists of the following rules:

IFSUM(false, b, xs, y) → IFSUM2(b, xs, y)
IFSUM2(true, xs, y) → SUM2(tail(xs), y)
SUM2(xs, y) → IFSUM(isNil(xs), isZero(head(xs)), xs, y)
IFSUM2(false, xs, y) → SUM2(cons(p(head(xs)), tail(xs)), s(y))

The TRS R consists of the following rules:

head(cons(x, xs)) → x
head(nil) → error
p(0) → s(s(0))
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
tail(nil) → nil
tail(cons(x, xs)) → xs
isNil(nil) → true
isNil(cons(x, xs)) → false
isZero(0) → true
isZero(s(0)) → false
isZero(s(s(x))) → isZero(s(x))

The set Q consists of the following terms:

times(x0, x1)
generate(x0, x1)
gen(x0, x1, x2)
if(true, x0, x1, x2)
if(false, x0, x1, x2)
sum(x0)
sum2(x0, x1)
ifsum(true, x0, x1, x2)
ifsum(false, x0, x1, x2)
ifsum2(true, x0, x1)
ifsum2(false, x0, x1)
isNil(nil)
isNil(cons(x0, x1))
tail(nil)
tail(cons(x0, x1))
head(cons(x0, x1))
head(nil)
isZero(0)
isZero(s(0))
isZero(s(s(x0)))
p(0)
p(s(0))
p(s(s(x0)))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
a

We have to consider all minimal (P,Q,R)-chains.

(31) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

times(x0, x1)
generate(x0, x1)
gen(x0, x1, x2)
if(true, x0, x1, x2)
if(false, x0, x1, x2)
sum(x0)
sum2(x0, x1)
ifsum(true, x0, x1, x2)
ifsum(false, x0, x1, x2)
ifsum2(true, x0, x1)
ifsum2(false, x0, x1)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
a

(32) Obligation:

Q DP problem:
The TRS P consists of the following rules:

IFSUM(false, b, xs, y) → IFSUM2(b, xs, y)
IFSUM2(true, xs, y) → SUM2(tail(xs), y)
SUM2(xs, y) → IFSUM(isNil(xs), isZero(head(xs)), xs, y)
IFSUM2(false, xs, y) → SUM2(cons(p(head(xs)), tail(xs)), s(y))

The TRS R consists of the following rules:

head(cons(x, xs)) → x
head(nil) → error
p(0) → s(s(0))
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
tail(nil) → nil
tail(cons(x, xs)) → xs
isNil(nil) → true
isNil(cons(x, xs)) → false
isZero(0) → true
isZero(s(0)) → false
isZero(s(s(x))) → isZero(s(x))

The set Q consists of the following terms:

isNil(nil)
isNil(cons(x0, x1))
tail(nil)
tail(cons(x0, x1))
head(cons(x0, x1))
head(nil)
isZero(0)
isZero(s(0))
isZero(s(s(x0)))
p(0)
p(s(0))
p(s(s(x0)))

We have to consider all minimal (P,Q,R)-chains.

(33) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule SUM2(xs, y) → IFSUM(isNil(xs), isZero(head(xs)), xs, y) at position [0] we obtained the following new rules [LPAR04]:

SUM2(nil, y1) → IFSUM(true, isZero(head(nil)), nil, y1)
SUM2(cons(x0, x1), y1) → IFSUM(false, isZero(head(cons(x0, x1))), cons(x0, x1), y1)

(34) Obligation:

Q DP problem:
The TRS P consists of the following rules:

IFSUM(false, b, xs, y) → IFSUM2(b, xs, y)
IFSUM2(true, xs, y) → SUM2(tail(xs), y)
IFSUM2(false, xs, y) → SUM2(cons(p(head(xs)), tail(xs)), s(y))
SUM2(nil, y1) → IFSUM(true, isZero(head(nil)), nil, y1)
SUM2(cons(x0, x1), y1) → IFSUM(false, isZero(head(cons(x0, x1))), cons(x0, x1), y1)

The TRS R consists of the following rules:

head(cons(x, xs)) → x
head(nil) → error
p(0) → s(s(0))
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
tail(nil) → nil
tail(cons(x, xs)) → xs
isNil(nil) → true
isNil(cons(x, xs)) → false
isZero(0) → true
isZero(s(0)) → false
isZero(s(s(x))) → isZero(s(x))

The set Q consists of the following terms:

isNil(nil)
isNil(cons(x0, x1))
tail(nil)
tail(cons(x0, x1))
head(cons(x0, x1))
head(nil)
isZero(0)
isZero(s(0))
isZero(s(s(x0)))
p(0)
p(s(0))
p(s(s(x0)))

We have to consider all minimal (P,Q,R)-chains.

(35) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.

(36) Obligation:

Q DP problem:
The TRS P consists of the following rules:

IFSUM2(true, xs, y) → SUM2(tail(xs), y)
SUM2(cons(x0, x1), y1) → IFSUM(false, isZero(head(cons(x0, x1))), cons(x0, x1), y1)
IFSUM(false, b, xs, y) → IFSUM2(b, xs, y)
IFSUM2(false, xs, y) → SUM2(cons(p(head(xs)), tail(xs)), s(y))

The TRS R consists of the following rules:

head(cons(x, xs)) → x
head(nil) → error
p(0) → s(s(0))
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
tail(nil) → nil
tail(cons(x, xs)) → xs
isNil(nil) → true
isNil(cons(x, xs)) → false
isZero(0) → true
isZero(s(0)) → false
isZero(s(s(x))) → isZero(s(x))

The set Q consists of the following terms:

isNil(nil)
isNil(cons(x0, x1))
tail(nil)
tail(cons(x0, x1))
head(cons(x0, x1))
head(nil)
isZero(0)
isZero(s(0))
isZero(s(s(x0)))
p(0)
p(s(0))
p(s(s(x0)))

We have to consider all minimal (P,Q,R)-chains.

(37) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(38) Obligation:

Q DP problem:
The TRS P consists of the following rules:

IFSUM2(true, xs, y) → SUM2(tail(xs), y)
SUM2(cons(x0, x1), y1) → IFSUM(false, isZero(head(cons(x0, x1))), cons(x0, x1), y1)
IFSUM(false, b, xs, y) → IFSUM2(b, xs, y)
IFSUM2(false, xs, y) → SUM2(cons(p(head(xs)), tail(xs)), s(y))

The TRS R consists of the following rules:

head(cons(x, xs)) → x
head(nil) → error
p(0) → s(s(0))
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
tail(nil) → nil
tail(cons(x, xs)) → xs
isZero(0) → true
isZero(s(0)) → false
isZero(s(s(x))) → isZero(s(x))

The set Q consists of the following terms:

isNil(nil)
isNil(cons(x0, x1))
tail(nil)
tail(cons(x0, x1))
head(cons(x0, x1))
head(nil)
isZero(0)
isZero(s(0))
isZero(s(s(x0)))
p(0)
p(s(0))
p(s(s(x0)))

We have to consider all minimal (P,Q,R)-chains.

(39) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

isNil(nil)
isNil(cons(x0, x1))

(40) Obligation:

Q DP problem:
The TRS P consists of the following rules:

IFSUM2(true, xs, y) → SUM2(tail(xs), y)
SUM2(cons(x0, x1), y1) → IFSUM(false, isZero(head(cons(x0, x1))), cons(x0, x1), y1)
IFSUM(false, b, xs, y) → IFSUM2(b, xs, y)
IFSUM2(false, xs, y) → SUM2(cons(p(head(xs)), tail(xs)), s(y))

The TRS R consists of the following rules:

head(cons(x, xs)) → x
head(nil) → error
p(0) → s(s(0))
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
tail(nil) → nil
tail(cons(x, xs)) → xs
isZero(0) → true
isZero(s(0)) → false
isZero(s(s(x))) → isZero(s(x))

The set Q consists of the following terms:

tail(nil)
tail(cons(x0, x1))
head(cons(x0, x1))
head(nil)
isZero(0)
isZero(s(0))
isZero(s(s(x0)))
p(0)
p(s(0))
p(s(s(x0)))

We have to consider all minimal (P,Q,R)-chains.

(41) Rewriting (EQUIVALENT transformation)

By rewriting [LPAR04] the rule SUM2(cons(x0, x1), y1) → IFSUM(false, isZero(head(cons(x0, x1))), cons(x0, x1), y1) at position [1,0] we obtained the following new rules [LPAR04]:

SUM2(cons(x0, x1), y1) → IFSUM(false, isZero(x0), cons(x0, x1), y1)

(42) Obligation:

Q DP problem:
The TRS P consists of the following rules:

IFSUM2(true, xs, y) → SUM2(tail(xs), y)
IFSUM(false, b, xs, y) → IFSUM2(b, xs, y)
IFSUM2(false, xs, y) → SUM2(cons(p(head(xs)), tail(xs)), s(y))
SUM2(cons(x0, x1), y1) → IFSUM(false, isZero(x0), cons(x0, x1), y1)

The TRS R consists of the following rules:

head(cons(x, xs)) → x
head(nil) → error
p(0) → s(s(0))
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
tail(nil) → nil
tail(cons(x, xs)) → xs
isZero(0) → true
isZero(s(0)) → false
isZero(s(s(x))) → isZero(s(x))

The set Q consists of the following terms:

tail(nil)
tail(cons(x0, x1))
head(cons(x0, x1))
head(nil)
isZero(0)
isZero(s(0))
isZero(s(s(x0)))
p(0)
p(s(0))
p(s(s(x0)))

We have to consider all minimal (P,Q,R)-chains.

(43) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule IFSUM2(true, xs, y) → SUM2(tail(xs), y) at position [0] we obtained the following new rules [LPAR04]:

IFSUM2(true, nil, y1) → SUM2(nil, y1)
IFSUM2(true, cons(x0, x1), y1) → SUM2(x1, y1)

(44) Obligation:

Q DP problem:
The TRS P consists of the following rules:

IFSUM(false, b, xs, y) → IFSUM2(b, xs, y)
IFSUM2(false, xs, y) → SUM2(cons(p(head(xs)), tail(xs)), s(y))
SUM2(cons(x0, x1), y1) → IFSUM(false, isZero(x0), cons(x0, x1), y1)
IFSUM2(true, nil, y1) → SUM2(nil, y1)
IFSUM2(true, cons(x0, x1), y1) → SUM2(x1, y1)

The TRS R consists of the following rules:

head(cons(x, xs)) → x
head(nil) → error
p(0) → s(s(0))
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
tail(nil) → nil
tail(cons(x, xs)) → xs
isZero(0) → true
isZero(s(0)) → false
isZero(s(s(x))) → isZero(s(x))

The set Q consists of the following terms:

tail(nil)
tail(cons(x0, x1))
head(cons(x0, x1))
head(nil)
isZero(0)
isZero(s(0))
isZero(s(s(x0)))
p(0)
p(s(0))
p(s(s(x0)))

We have to consider all minimal (P,Q,R)-chains.

(45) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.

(46) Obligation:

Q DP problem:
The TRS P consists of the following rules:

IFSUM2(false, xs, y) → SUM2(cons(p(head(xs)), tail(xs)), s(y))
SUM2(cons(x0, x1), y1) → IFSUM(false, isZero(x0), cons(x0, x1), y1)
IFSUM(false, b, xs, y) → IFSUM2(b, xs, y)
IFSUM2(true, cons(x0, x1), y1) → SUM2(x1, y1)

The TRS R consists of the following rules:

head(cons(x, xs)) → x
head(nil) → error
p(0) → s(s(0))
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
tail(nil) → nil
tail(cons(x, xs)) → xs
isZero(0) → true
isZero(s(0)) → false
isZero(s(s(x))) → isZero(s(x))

The set Q consists of the following terms:

tail(nil)
tail(cons(x0, x1))
head(cons(x0, x1))
head(nil)
isZero(0)
isZero(s(0))
isZero(s(s(x0)))
p(0)
p(s(0))
p(s(s(x0)))

We have to consider all minimal (P,Q,R)-chains.

(47) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule IFSUM(false, b, xs, y) → IFSUM2(b, xs, y) we obtained the following new rules [LPAR04]:

IFSUM(false, y_0, cons(z0, z1), z2) → IFSUM2(y_0, cons(z0, z1), z2)

(48) Obligation:

Q DP problem:
The TRS P consists of the following rules:

IFSUM2(false, xs, y) → SUM2(cons(p(head(xs)), tail(xs)), s(y))
SUM2(cons(x0, x1), y1) → IFSUM(false, isZero(x0), cons(x0, x1), y1)
IFSUM2(true, cons(x0, x1), y1) → SUM2(x1, y1)
IFSUM(false, y_0, cons(z0, z1), z2) → IFSUM2(y_0, cons(z0, z1), z2)

The TRS R consists of the following rules:

head(cons(x, xs)) → x
head(nil) → error
p(0) → s(s(0))
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
tail(nil) → nil
tail(cons(x, xs)) → xs
isZero(0) → true
isZero(s(0)) → false
isZero(s(s(x))) → isZero(s(x))

The set Q consists of the following terms:

tail(nil)
tail(cons(x0, x1))
head(cons(x0, x1))
head(nil)
isZero(0)
isZero(s(0))
isZero(s(s(x0)))
p(0)
p(s(0))
p(s(s(x0)))

We have to consider all minimal (P,Q,R)-chains.

(49) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule IFSUM(false, b, xs, y) → IFSUM2(b, xs, y) we obtained the following new rules [LPAR04]:

IFSUM(false, y_0, cons(z0, z1), z2) → IFSUM2(y_0, cons(z0, z1), z2)

(50) Obligation:

Q DP problem:
The TRS P consists of the following rules:

IFSUM2(false, xs, y) → SUM2(cons(p(head(xs)), tail(xs)), s(y))
SUM2(cons(x0, x1), y1) → IFSUM(false, isZero(x0), cons(x0, x1), y1)
IFSUM2(true, cons(x0, x1), y1) → SUM2(x1, y1)
IFSUM(false, y_0, cons(z0, z1), z2) → IFSUM2(y_0, cons(z0, z1), z2)

The TRS R consists of the following rules:

head(cons(x, xs)) → x
head(nil) → error
p(0) → s(s(0))
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
tail(nil) → nil
tail(cons(x, xs)) → xs
isZero(0) → true
isZero(s(0)) → false
isZero(s(s(x))) → isZero(s(x))

The set Q consists of the following terms:

tail(nil)
tail(cons(x0, x1))
head(cons(x0, x1))
head(nil)
isZero(0)
isZero(s(0))
isZero(s(s(x0)))
p(0)
p(s(0))
p(s(s(x0)))

We have to consider all minimal (P,Q,R)-chains.

(51) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule IFSUM2(false, xs, y) → SUM2(cons(p(head(xs)), tail(xs)), s(y)) we obtained the following new rules [LPAR04]:

IFSUM2(false, cons(z1, z2), z3) → SUM2(cons(p(head(cons(z1, z2))), tail(cons(z1, z2))), s(z3))

(52) Obligation:

Q DP problem:
The TRS P consists of the following rules:

SUM2(cons(x0, x1), y1) → IFSUM(false, isZero(x0), cons(x0, x1), y1)
IFSUM2(true, cons(x0, x1), y1) → SUM2(x1, y1)
IFSUM(false, y_0, cons(z0, z1), z2) → IFSUM2(y_0, cons(z0, z1), z2)
IFSUM2(false, cons(z1, z2), z3) → SUM2(cons(p(head(cons(z1, z2))), tail(cons(z1, z2))), s(z3))

The TRS R consists of the following rules:

head(cons(x, xs)) → x
head(nil) → error
p(0) → s(s(0))
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
tail(nil) → nil
tail(cons(x, xs)) → xs
isZero(0) → true
isZero(s(0)) → false
isZero(s(s(x))) → isZero(s(x))

The set Q consists of the following terms:

tail(nil)
tail(cons(x0, x1))
head(cons(x0, x1))
head(nil)
isZero(0)
isZero(s(0))
isZero(s(s(x0)))
p(0)
p(s(0))
p(s(s(x0)))

We have to consider all minimal (P,Q,R)-chains.

(53) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(54) Obligation:

Q DP problem:
The TRS P consists of the following rules:

SUM2(cons(x0, x1), y1) → IFSUM(false, isZero(x0), cons(x0, x1), y1)
IFSUM2(true, cons(x0, x1), y1) → SUM2(x1, y1)
IFSUM(false, y_0, cons(z0, z1), z2) → IFSUM2(y_0, cons(z0, z1), z2)
IFSUM2(false, cons(z1, z2), z3) → SUM2(cons(p(head(cons(z1, z2))), tail(cons(z1, z2))), s(z3))

The TRS R consists of the following rules:

head(cons(x, xs)) → x
p(0) → s(s(0))
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
tail(cons(x, xs)) → xs
isZero(0) → true
isZero(s(0)) → false
isZero(s(s(x))) → isZero(s(x))

The set Q consists of the following terms:

tail(nil)
tail(cons(x0, x1))
head(cons(x0, x1))
head(nil)
isZero(0)
isZero(s(0))
isZero(s(s(x0)))
p(0)
p(s(0))
p(s(s(x0)))

We have to consider all minimal (P,Q,R)-chains.

(55) Rewriting (EQUIVALENT transformation)

By rewriting [LPAR04] the rule IFSUM2(false, cons(z1, z2), z3) → SUM2(cons(p(head(cons(z1, z2))), tail(cons(z1, z2))), s(z3)) at position [0,0,0] we obtained the following new rules [LPAR04]:

IFSUM2(false, cons(z1, z2), z3) → SUM2(cons(p(z1), tail(cons(z1, z2))), s(z3))

(56) Obligation:

Q DP problem:
The TRS P consists of the following rules:

SUM2(cons(x0, x1), y1) → IFSUM(false, isZero(x0), cons(x0, x1), y1)
IFSUM2(true, cons(x0, x1), y1) → SUM2(x1, y1)
IFSUM(false, y_0, cons(z0, z1), z2) → IFSUM2(y_0, cons(z0, z1), z2)
IFSUM2(false, cons(z1, z2), z3) → SUM2(cons(p(z1), tail(cons(z1, z2))), s(z3))

The TRS R consists of the following rules:

head(cons(x, xs)) → x
p(0) → s(s(0))
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
tail(cons(x, xs)) → xs
isZero(0) → true
isZero(s(0)) → false
isZero(s(s(x))) → isZero(s(x))

The set Q consists of the following terms:

tail(nil)
tail(cons(x0, x1))
head(cons(x0, x1))
head(nil)
isZero(0)
isZero(s(0))
isZero(s(s(x0)))
p(0)
p(s(0))
p(s(s(x0)))

We have to consider all minimal (P,Q,R)-chains.

(57) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(58) Obligation:

Q DP problem:
The TRS P consists of the following rules:

SUM2(cons(x0, x1), y1) → IFSUM(false, isZero(x0), cons(x0, x1), y1)
IFSUM2(true, cons(x0, x1), y1) → SUM2(x1, y1)
IFSUM(false, y_0, cons(z0, z1), z2) → IFSUM2(y_0, cons(z0, z1), z2)
IFSUM2(false, cons(z1, z2), z3) → SUM2(cons(p(z1), tail(cons(z1, z2))), s(z3))

The TRS R consists of the following rules:

p(0) → s(s(0))
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
tail(cons(x, xs)) → xs
isZero(0) → true
isZero(s(0)) → false
isZero(s(s(x))) → isZero(s(x))

The set Q consists of the following terms:

tail(nil)
tail(cons(x0, x1))
head(cons(x0, x1))
head(nil)
isZero(0)
isZero(s(0))
isZero(s(s(x0)))
p(0)
p(s(0))
p(s(s(x0)))

We have to consider all minimal (P,Q,R)-chains.

(59) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

head(cons(x0, x1))
head(nil)

(60) Obligation:

Q DP problem:
The TRS P consists of the following rules:

SUM2(cons(x0, x1), y1) → IFSUM(false, isZero(x0), cons(x0, x1), y1)
IFSUM2(true, cons(x0, x1), y1) → SUM2(x1, y1)
IFSUM(false, y_0, cons(z0, z1), z2) → IFSUM2(y_0, cons(z0, z1), z2)
IFSUM2(false, cons(z1, z2), z3) → SUM2(cons(p(z1), tail(cons(z1, z2))), s(z3))

The TRS R consists of the following rules:

p(0) → s(s(0))
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
tail(cons(x, xs)) → xs
isZero(0) → true
isZero(s(0)) → false
isZero(s(s(x))) → isZero(s(x))

The set Q consists of the following terms:

tail(nil)
tail(cons(x0, x1))
isZero(0)
isZero(s(0))
isZero(s(s(x0)))
p(0)
p(s(0))
p(s(s(x0)))

We have to consider all minimal (P,Q,R)-chains.

(61) Rewriting (EQUIVALENT transformation)

By rewriting [LPAR04] the rule IFSUM2(false, cons(z1, z2), z3) → SUM2(cons(p(z1), tail(cons(z1, z2))), s(z3)) at position [0,1] we obtained the following new rules [LPAR04]:

IFSUM2(false, cons(z1, z2), z3) → SUM2(cons(p(z1), z2), s(z3))

(62) Obligation:

Q DP problem:
The TRS P consists of the following rules:

SUM2(cons(x0, x1), y1) → IFSUM(false, isZero(x0), cons(x0, x1), y1)
IFSUM2(true, cons(x0, x1), y1) → SUM2(x1, y1)
IFSUM(false, y_0, cons(z0, z1), z2) → IFSUM2(y_0, cons(z0, z1), z2)
IFSUM2(false, cons(z1, z2), z3) → SUM2(cons(p(z1), z2), s(z3))

The TRS R consists of the following rules:

p(0) → s(s(0))
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
tail(cons(x, xs)) → xs
isZero(0) → true
isZero(s(0)) → false
isZero(s(s(x))) → isZero(s(x))

The set Q consists of the following terms:

tail(nil)
tail(cons(x0, x1))
isZero(0)
isZero(s(0))
isZero(s(s(x0)))
p(0)
p(s(0))
p(s(s(x0)))

We have to consider all minimal (P,Q,R)-chains.

(63) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(64) Obligation:

Q DP problem:
The TRS P consists of the following rules:

SUM2(cons(x0, x1), y1) → IFSUM(false, isZero(x0), cons(x0, x1), y1)
IFSUM2(true, cons(x0, x1), y1) → SUM2(x1, y1)
IFSUM(false, y_0, cons(z0, z1), z2) → IFSUM2(y_0, cons(z0, z1), z2)
IFSUM2(false, cons(z1, z2), z3) → SUM2(cons(p(z1), z2), s(z3))

The TRS R consists of the following rules:

p(0) → s(s(0))
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
isZero(0) → true
isZero(s(0)) → false
isZero(s(s(x))) → isZero(s(x))

The set Q consists of the following terms:

tail(nil)
tail(cons(x0, x1))
isZero(0)
isZero(s(0))
isZero(s(s(x0)))
p(0)
p(s(0))
p(s(s(x0)))

We have to consider all minimal (P,Q,R)-chains.

(65) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

tail(nil)
tail(cons(x0, x1))

(66) Obligation:

Q DP problem:
The TRS P consists of the following rules:

SUM2(cons(x0, x1), y1) → IFSUM(false, isZero(x0), cons(x0, x1), y1)
IFSUM2(true, cons(x0, x1), y1) → SUM2(x1, y1)
IFSUM(false, y_0, cons(z0, z1), z2) → IFSUM2(y_0, cons(z0, z1), z2)
IFSUM2(false, cons(z1, z2), z3) → SUM2(cons(p(z1), z2), s(z3))

The TRS R consists of the following rules:

p(0) → s(s(0))
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
isZero(0) → true
isZero(s(0)) → false
isZero(s(s(x))) → isZero(s(x))

The set Q consists of the following terms:

isZero(0)
isZero(s(0))
isZero(s(s(x0)))
p(0)
p(s(0))
p(s(s(x0)))

We have to consider all minimal (P,Q,R)-chains.

(67) ForwardInstantiation (EQUIVALENT transformation)

By forward instantiating [JAR06] the rule IFSUM2(true, cons(x0, x1), y1) → SUM2(x1, y1) we obtained the following new rules [LPAR04]:

IFSUM2(true, cons(x0, cons(y_0, y_1)), x2) → SUM2(cons(y_0, y_1), x2)

(68) Obligation:

Q DP problem:
The TRS P consists of the following rules:

SUM2(cons(x0, x1), y1) → IFSUM(false, isZero(x0), cons(x0, x1), y1)
IFSUM(false, y_0, cons(z0, z1), z2) → IFSUM2(y_0, cons(z0, z1), z2)
IFSUM2(false, cons(z1, z2), z3) → SUM2(cons(p(z1), z2), s(z3))
IFSUM2(true, cons(x0, cons(y_0, y_1)), x2) → SUM2(cons(y_0, y_1), x2)

The TRS R consists of the following rules:

p(0) → s(s(0))
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
isZero(0) → true
isZero(s(0)) → false
isZero(s(s(x))) → isZero(s(x))

The set Q consists of the following terms:

isZero(0)
isZero(s(0))
isZero(s(s(x0)))
p(0)
p(s(0))
p(s(s(x0)))

We have to consider all minimal (P,Q,R)-chains.

(69) ForwardInstantiation (EQUIVALENT transformation)

By forward instantiating [JAR06] the rule IFSUM(false, y_0, cons(z0, z1), z2) → IFSUM2(y_0, cons(z0, z1), z2) we obtained the following new rules [LPAR04]:

IFSUM(false, false, cons(x1, x2), x3) → IFSUM2(false, cons(x1, x2), x3)
IFSUM(false, true, cons(x1, cons(y_1, y_2)), x3) → IFSUM2(true, cons(x1, cons(y_1, y_2)), x3)

(70) Obligation:

Q DP problem:
The TRS P consists of the following rules:

SUM2(cons(x0, x1), y1) → IFSUM(false, isZero(x0), cons(x0, x1), y1)
IFSUM2(false, cons(z1, z2), z3) → SUM2(cons(p(z1), z2), s(z3))
IFSUM2(true, cons(x0, cons(y_0, y_1)), x2) → SUM2(cons(y_0, y_1), x2)
IFSUM(false, false, cons(x1, x2), x3) → IFSUM2(false, cons(x1, x2), x3)
IFSUM(false, true, cons(x1, cons(y_1, y_2)), x3) → IFSUM2(true, cons(x1, cons(y_1, y_2)), x3)

The TRS R consists of the following rules:

p(0) → s(s(0))
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
isZero(0) → true
isZero(s(0)) → false
isZero(s(s(x))) → isZero(s(x))

The set Q consists of the following terms:

isZero(0)
isZero(s(0))
isZero(s(s(x0)))
p(0)
p(s(0))
p(s(s(x0)))

We have to consider all minimal (P,Q,R)-chains.

(71) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule SUM2(cons(x0, x1), y1) → IFSUM(false, isZero(x0), cons(x0, x1), y1) at position [1] we obtained the following new rules [LPAR04]:

SUM2(cons(0, y1), y2) → IFSUM(false, true, cons(0, y1), y2)
SUM2(cons(s(0), y1), y2) → IFSUM(false, false, cons(s(0), y1), y2)
SUM2(cons(s(s(x0)), y1), y2) → IFSUM(false, isZero(s(x0)), cons(s(s(x0)), y1), y2)

(72) Obligation:

Q DP problem:
The TRS P consists of the following rules:

IFSUM2(false, cons(z1, z2), z3) → SUM2(cons(p(z1), z2), s(z3))
IFSUM2(true, cons(x0, cons(y_0, y_1)), x2) → SUM2(cons(y_0, y_1), x2)
IFSUM(false, false, cons(x1, x2), x3) → IFSUM2(false, cons(x1, x2), x3)
IFSUM(false, true, cons(x1, cons(y_1, y_2)), x3) → IFSUM2(true, cons(x1, cons(y_1, y_2)), x3)
SUM2(cons(0, y1), y2) → IFSUM(false, true, cons(0, y1), y2)
SUM2(cons(s(0), y1), y2) → IFSUM(false, false, cons(s(0), y1), y2)
SUM2(cons(s(s(x0)), y1), y2) → IFSUM(false, isZero(s(x0)), cons(s(s(x0)), y1), y2)

The TRS R consists of the following rules:

p(0) → s(s(0))
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
isZero(0) → true
isZero(s(0)) → false
isZero(s(s(x))) → isZero(s(x))

The set Q consists of the following terms:

isZero(0)
isZero(s(0))
isZero(s(s(x0)))
p(0)
p(s(0))
p(s(s(x0)))

We have to consider all minimal (P,Q,R)-chains.

(73) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(74) Obligation:

Q DP problem:
The TRS P consists of the following rules:

IFSUM2(false, cons(z1, z2), z3) → SUM2(cons(p(z1), z2), s(z3))
IFSUM2(true, cons(x0, cons(y_0, y_1)), x2) → SUM2(cons(y_0, y_1), x2)
IFSUM(false, false, cons(x1, x2), x3) → IFSUM2(false, cons(x1, x2), x3)
IFSUM(false, true, cons(x1, cons(y_1, y_2)), x3) → IFSUM2(true, cons(x1, cons(y_1, y_2)), x3)
SUM2(cons(0, y1), y2) → IFSUM(false, true, cons(0, y1), y2)
SUM2(cons(s(0), y1), y2) → IFSUM(false, false, cons(s(0), y1), y2)
SUM2(cons(s(s(x0)), y1), y2) → IFSUM(false, isZero(s(x0)), cons(s(s(x0)), y1), y2)

The TRS R consists of the following rules:

isZero(s(0)) → false
isZero(s(s(x))) → isZero(s(x))
p(0) → s(s(0))
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))

The set Q consists of the following terms:

isZero(0)
isZero(s(0))
isZero(s(s(x0)))
p(0)
p(s(0))
p(s(s(x0)))

We have to consider all minimal (P,Q,R)-chains.

(75) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule IFSUM2(false, cons(z1, z2), z3) → SUM2(cons(p(z1), z2), s(z3)) at position [0,0] we obtained the following new rules [LPAR04]:

IFSUM2(false, cons(0, y1), y2) → SUM2(cons(s(s(0)), y1), s(y2))
IFSUM2(false, cons(s(0), y1), y2) → SUM2(cons(0, y1), s(y2))
IFSUM2(false, cons(s(s(x0)), y1), y2) → SUM2(cons(s(p(s(x0))), y1), s(y2))

(76) Obligation:

Q DP problem:
The TRS P consists of the following rules:

IFSUM2(true, cons(x0, cons(y_0, y_1)), x2) → SUM2(cons(y_0, y_1), x2)
IFSUM(false, false, cons(x1, x2), x3) → IFSUM2(false, cons(x1, x2), x3)
IFSUM(false, true, cons(x1, cons(y_1, y_2)), x3) → IFSUM2(true, cons(x1, cons(y_1, y_2)), x3)
SUM2(cons(0, y1), y2) → IFSUM(false, true, cons(0, y1), y2)
SUM2(cons(s(0), y1), y2) → IFSUM(false, false, cons(s(0), y1), y2)
SUM2(cons(s(s(x0)), y1), y2) → IFSUM(false, isZero(s(x0)), cons(s(s(x0)), y1), y2)
IFSUM2(false, cons(0, y1), y2) → SUM2(cons(s(s(0)), y1), s(y2))
IFSUM2(false, cons(s(0), y1), y2) → SUM2(cons(0, y1), s(y2))
IFSUM2(false, cons(s(s(x0)), y1), y2) → SUM2(cons(s(p(s(x0))), y1), s(y2))

The TRS R consists of the following rules:

isZero(s(0)) → false
isZero(s(s(x))) → isZero(s(x))
p(0) → s(s(0))
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))

The set Q consists of the following terms:

isZero(0)
isZero(s(0))
isZero(s(s(x0)))
p(0)
p(s(0))
p(s(s(x0)))

We have to consider all minimal (P,Q,R)-chains.

(77) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(78) Obligation:

Q DP problem:
The TRS P consists of the following rules:

IFSUM2(true, cons(x0, cons(y_0, y_1)), x2) → SUM2(cons(y_0, y_1), x2)
IFSUM(false, false, cons(x1, x2), x3) → IFSUM2(false, cons(x1, x2), x3)
IFSUM(false, true, cons(x1, cons(y_1, y_2)), x3) → IFSUM2(true, cons(x1, cons(y_1, y_2)), x3)
SUM2(cons(0, y1), y2) → IFSUM(false, true, cons(0, y1), y2)
SUM2(cons(s(0), y1), y2) → IFSUM(false, false, cons(s(0), y1), y2)
SUM2(cons(s(s(x0)), y1), y2) → IFSUM(false, isZero(s(x0)), cons(s(s(x0)), y1), y2)
IFSUM2(false, cons(0, y1), y2) → SUM2(cons(s(s(0)), y1), s(y2))
IFSUM2(false, cons(s(0), y1), y2) → SUM2(cons(0, y1), s(y2))
IFSUM2(false, cons(s(s(x0)), y1), y2) → SUM2(cons(s(p(s(x0))), y1), s(y2))

The TRS R consists of the following rules:

p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
isZero(s(0)) → false
isZero(s(s(x))) → isZero(s(x))

The set Q consists of the following terms:

isZero(0)
isZero(s(0))
isZero(s(s(x0)))
p(0)
p(s(0))
p(s(s(x0)))

We have to consider all minimal (P,Q,R)-chains.

(79) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule IFSUM(false, false, cons(x1, x2), x3) → IFSUM2(false, cons(x1, x2), x3) we obtained the following new rules [LPAR04]:

IFSUM(false, false, cons(s(0), z0), z1) → IFSUM2(false, cons(s(0), z0), z1)
IFSUM(false, false, cons(s(s(z0)), z1), z2) → IFSUM2(false, cons(s(s(z0)), z1), z2)

(80) Obligation:

Q DP problem:
The TRS P consists of the following rules:

IFSUM2(true, cons(x0, cons(y_0, y_1)), x2) → SUM2(cons(y_0, y_1), x2)
IFSUM(false, true, cons(x1, cons(y_1, y_2)), x3) → IFSUM2(true, cons(x1, cons(y_1, y_2)), x3)
SUM2(cons(0, y1), y2) → IFSUM(false, true, cons(0, y1), y2)
SUM2(cons(s(0), y1), y2) → IFSUM(false, false, cons(s(0), y1), y2)
SUM2(cons(s(s(x0)), y1), y2) → IFSUM(false, isZero(s(x0)), cons(s(s(x0)), y1), y2)
IFSUM2(false, cons(0, y1), y2) → SUM2(cons(s(s(0)), y1), s(y2))
IFSUM2(false, cons(s(0), y1), y2) → SUM2(cons(0, y1), s(y2))
IFSUM2(false, cons(s(s(x0)), y1), y2) → SUM2(cons(s(p(s(x0))), y1), s(y2))
IFSUM(false, false, cons(s(0), z0), z1) → IFSUM2(false, cons(s(0), z0), z1)
IFSUM(false, false, cons(s(s(z0)), z1), z2) → IFSUM2(false, cons(s(s(z0)), z1), z2)

The TRS R consists of the following rules:

p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
isZero(s(0)) → false
isZero(s(s(x))) → isZero(s(x))

The set Q consists of the following terms:

isZero(0)
isZero(s(0))
isZero(s(s(x0)))
p(0)
p(s(0))
p(s(s(x0)))

We have to consider all minimal (P,Q,R)-chains.

(81) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.

(82) Obligation:

Q DP problem:
The TRS P consists of the following rules:

SUM2(cons(0, y1), y2) → IFSUM(false, true, cons(0, y1), y2)
IFSUM(false, true, cons(x1, cons(y_1, y_2)), x3) → IFSUM2(true, cons(x1, cons(y_1, y_2)), x3)
IFSUM2(true, cons(x0, cons(y_0, y_1)), x2) → SUM2(cons(y_0, y_1), x2)
SUM2(cons(s(0), y1), y2) → IFSUM(false, false, cons(s(0), y1), y2)
IFSUM(false, false, cons(s(0), z0), z1) → IFSUM2(false, cons(s(0), z0), z1)
IFSUM2(false, cons(s(0), y1), y2) → SUM2(cons(0, y1), s(y2))
SUM2(cons(s(s(x0)), y1), y2) → IFSUM(false, isZero(s(x0)), cons(s(s(x0)), y1), y2)
IFSUM(false, false, cons(s(s(z0)), z1), z2) → IFSUM2(false, cons(s(s(z0)), z1), z2)
IFSUM2(false, cons(s(s(x0)), y1), y2) → SUM2(cons(s(p(s(x0))), y1), s(y2))

The TRS R consists of the following rules:

p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
isZero(s(0)) → false
isZero(s(s(x))) → isZero(s(x))

The set Q consists of the following terms:

isZero(0)
isZero(s(0))
isZero(s(s(x0)))
p(0)
p(s(0))
p(s(s(x0)))

We have to consider all minimal (P,Q,R)-chains.

(83) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule IFSUM(false, true, cons(x1, cons(y_1, y_2)), x3) → IFSUM2(true, cons(x1, cons(y_1, y_2)), x3) we obtained the following new rules [LPAR04]:

IFSUM(false, true, cons(0, cons(x1, x2)), z1) → IFSUM2(true, cons(0, cons(x1, x2)), z1)

(84) Obligation:

Q DP problem:
The TRS P consists of the following rules:

SUM2(cons(0, y1), y2) → IFSUM(false, true, cons(0, y1), y2)
IFSUM2(true, cons(x0, cons(y_0, y_1)), x2) → SUM2(cons(y_0, y_1), x2)
SUM2(cons(s(0), y1), y2) → IFSUM(false, false, cons(s(0), y1), y2)
IFSUM(false, false, cons(s(0), z0), z1) → IFSUM2(false, cons(s(0), z0), z1)
IFSUM2(false, cons(s(0), y1), y2) → SUM2(cons(0, y1), s(y2))
SUM2(cons(s(s(x0)), y1), y2) → IFSUM(false, isZero(s(x0)), cons(s(s(x0)), y1), y2)
IFSUM(false, false, cons(s(s(z0)), z1), z2) → IFSUM2(false, cons(s(s(z0)), z1), z2)
IFSUM2(false, cons(s(s(x0)), y1), y2) → SUM2(cons(s(p(s(x0))), y1), s(y2))
IFSUM(false, true, cons(0, cons(x1, x2)), z1) → IFSUM2(true, cons(0, cons(x1, x2)), z1)

The TRS R consists of the following rules:

p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
isZero(s(0)) → false
isZero(s(s(x))) → isZero(s(x))

The set Q consists of the following terms:

isZero(0)
isZero(s(0))
isZero(s(s(x0)))
p(0)
p(s(0))
p(s(s(x0)))

We have to consider all minimal (P,Q,R)-chains.

(85) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule IFSUM2(true, cons(x0, cons(y_0, y_1)), x2) → SUM2(cons(y_0, y_1), x2) we obtained the following new rules [LPAR04]:

IFSUM2(true, cons(0, cons(z0, z1)), z2) → SUM2(cons(z0, z1), z2)

(86) Obligation:

Q DP problem:
The TRS P consists of the following rules:

SUM2(cons(0, y1), y2) → IFSUM(false, true, cons(0, y1), y2)
SUM2(cons(s(0), y1), y2) → IFSUM(false, false, cons(s(0), y1), y2)
IFSUM(false, false, cons(s(0), z0), z1) → IFSUM2(false, cons(s(0), z0), z1)
IFSUM2(false, cons(s(0), y1), y2) → SUM2(cons(0, y1), s(y2))
SUM2(cons(s(s(x0)), y1), y2) → IFSUM(false, isZero(s(x0)), cons(s(s(x0)), y1), y2)
IFSUM(false, false, cons(s(s(z0)), z1), z2) → IFSUM2(false, cons(s(s(z0)), z1), z2)
IFSUM2(false, cons(s(s(x0)), y1), y2) → SUM2(cons(s(p(s(x0))), y1), s(y2))
IFSUM(false, true, cons(0, cons(x1, x2)), z1) → IFSUM2(true, cons(0, cons(x1, x2)), z1)
IFSUM2(true, cons(0, cons(z0, z1)), z2) → SUM2(cons(z0, z1), z2)

The TRS R consists of the following rules:

p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
isZero(s(0)) → false
isZero(s(s(x))) → isZero(s(x))

The set Q consists of the following terms:

isZero(0)
isZero(s(0))
isZero(s(s(x0)))
p(0)
p(s(0))
p(s(s(x0)))

We have to consider all minimal (P,Q,R)-chains.

(87) ForwardInstantiation (EQUIVALENT transformation)

By forward instantiating [JAR06] the rule SUM2(cons(0, y1), y2) → IFSUM(false, true, cons(0, y1), y2) we obtained the following new rules [LPAR04]:

SUM2(cons(0, cons(y_0, y_1)), x1) → IFSUM(false, true, cons(0, cons(y_0, y_1)), x1)

(88) Obligation:

Q DP problem:
The TRS P consists of the following rules:

SUM2(cons(s(0), y1), y2) → IFSUM(false, false, cons(s(0), y1), y2)
IFSUM(false, false, cons(s(0), z0), z1) → IFSUM2(false, cons(s(0), z0), z1)
IFSUM2(false, cons(s(0), y1), y2) → SUM2(cons(0, y1), s(y2))
SUM2(cons(s(s(x0)), y1), y2) → IFSUM(false, isZero(s(x0)), cons(s(s(x0)), y1), y2)
IFSUM(false, false, cons(s(s(z0)), z1), z2) → IFSUM2(false, cons(s(s(z0)), z1), z2)
IFSUM2(false, cons(s(s(x0)), y1), y2) → SUM2(cons(s(p(s(x0))), y1), s(y2))
IFSUM(false, true, cons(0, cons(x1, x2)), z1) → IFSUM2(true, cons(0, cons(x1, x2)), z1)
IFSUM2(true, cons(0, cons(z0, z1)), z2) → SUM2(cons(z0, z1), z2)
SUM2(cons(0, cons(y_0, y_1)), x1) → IFSUM(false, true, cons(0, cons(y_0, y_1)), x1)

The TRS R consists of the following rules:

p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
isZero(s(0)) → false
isZero(s(s(x))) → isZero(s(x))

The set Q consists of the following terms:

isZero(0)
isZero(s(0))
isZero(s(s(x0)))
p(0)
p(s(0))
p(s(s(x0)))

We have to consider all minimal (P,Q,R)-chains.

(89) ForwardInstantiation (EQUIVALENT transformation)

By forward instantiating [JAR06] the rule IFSUM2(false, cons(s(0), y1), y2) → SUM2(cons(0, y1), s(y2)) we obtained the following new rules [LPAR04]:

IFSUM2(false, cons(s(0), cons(y_0, y_1)), x1) → SUM2(cons(0, cons(y_0, y_1)), s(x1))

(90) Obligation:

Q DP problem:
The TRS P consists of the following rules:

SUM2(cons(s(0), y1), y2) → IFSUM(false, false, cons(s(0), y1), y2)
IFSUM(false, false, cons(s(0), z0), z1) → IFSUM2(false, cons(s(0), z0), z1)
SUM2(cons(s(s(x0)), y1), y2) → IFSUM(false, isZero(s(x0)), cons(s(s(x0)), y1), y2)
IFSUM(false, false, cons(s(s(z0)), z1), z2) → IFSUM2(false, cons(s(s(z0)), z1), z2)
IFSUM2(false, cons(s(s(x0)), y1), y2) → SUM2(cons(s(p(s(x0))), y1), s(y2))
IFSUM(false, true, cons(0, cons(x1, x2)), z1) → IFSUM2(true, cons(0, cons(x1, x2)), z1)
IFSUM2(true, cons(0, cons(z0, z1)), z2) → SUM2(cons(z0, z1), z2)
SUM2(cons(0, cons(y_0, y_1)), x1) → IFSUM(false, true, cons(0, cons(y_0, y_1)), x1)
IFSUM2(false, cons(s(0), cons(y_0, y_1)), x1) → SUM2(cons(0, cons(y_0, y_1)), s(x1))

The TRS R consists of the following rules:

p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
isZero(s(0)) → false
isZero(s(s(x))) → isZero(s(x))

The set Q consists of the following terms:

isZero(0)
isZero(s(0))
isZero(s(s(x0)))
p(0)
p(s(0))
p(s(s(x0)))

We have to consider all minimal (P,Q,R)-chains.

(91) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


IFSUM2(false, cons(s(0), cons(y_0, y_1)), x1) → SUM2(cons(0, cons(y_0, y_1)), s(x1))
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:

POL(0) = 0   
POL(IFSUM(x1, x2, x3, x4)) = x3   
POL(IFSUM2(x1, x2, x3)) = x2   
POL(SUM2(x1, x2)) = x1   
POL(cons(x1, x2)) = x1 + x2   
POL(false) = 0   
POL(isZero(x1)) = 0   
POL(p(x1)) = 1 + x1   
POL(s(x1)) = 1   
POL(true) = 0   

The following usable rules [FROCOS05] were oriented: none

(92) Obligation:

Q DP problem:
The TRS P consists of the following rules:

SUM2(cons(s(0), y1), y2) → IFSUM(false, false, cons(s(0), y1), y2)
IFSUM(false, false, cons(s(0), z0), z1) → IFSUM2(false, cons(s(0), z0), z1)
SUM2(cons(s(s(x0)), y1), y2) → IFSUM(false, isZero(s(x0)), cons(s(s(x0)), y1), y2)
IFSUM(false, false, cons(s(s(z0)), z1), z2) → IFSUM2(false, cons(s(s(z0)), z1), z2)
IFSUM2(false, cons(s(s(x0)), y1), y2) → SUM2(cons(s(p(s(x0))), y1), s(y2))
IFSUM(false, true, cons(0, cons(x1, x2)), z1) → IFSUM2(true, cons(0, cons(x1, x2)), z1)
IFSUM2(true, cons(0, cons(z0, z1)), z2) → SUM2(cons(z0, z1), z2)
SUM2(cons(0, cons(y_0, y_1)), x1) → IFSUM(false, true, cons(0, cons(y_0, y_1)), x1)

The TRS R consists of the following rules:

p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
isZero(s(0)) → false
isZero(s(s(x))) → isZero(s(x))

The set Q consists of the following terms:

isZero(0)
isZero(s(0))
isZero(s(s(x0)))
p(0)
p(s(0))
p(s(s(x0)))

We have to consider all minimal (P,Q,R)-chains.

(93) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 2 SCCs with 2 less nodes.

(94) Complex Obligation (AND)

(95) Obligation:

Q DP problem:
The TRS P consists of the following rules:

SUM2(cons(s(s(x0)), y1), y2) → IFSUM(false, isZero(s(x0)), cons(s(s(x0)), y1), y2)
IFSUM(false, false, cons(s(s(z0)), z1), z2) → IFSUM2(false, cons(s(s(z0)), z1), z2)
IFSUM2(false, cons(s(s(x0)), y1), y2) → SUM2(cons(s(p(s(x0))), y1), s(y2))

The TRS R consists of the following rules:

p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
isZero(s(0)) → false
isZero(s(s(x))) → isZero(s(x))

The set Q consists of the following terms:

isZero(0)
isZero(s(0))
isZero(s(s(x0)))
p(0)
p(s(0))
p(s(s(x0)))

We have to consider all minimal (P,Q,R)-chains.

(96) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


IFSUM2(false, cons(s(s(x0)), y1), y2) → SUM2(cons(s(p(s(x0))), y1), s(y2))
The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO]:

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

POL(cons(x1, x2)) =
/0\
\0/
 +
/01\
\00/
·x1 +
/00\
\00/
·x2

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

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

POL(false) =
/1\
\0/

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

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

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

POL(0) =
/1\
\1/

The following usable rules [FROCOS05] were oriented:

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

(97) Obligation:

Q DP problem:
The TRS P consists of the following rules:

SUM2(cons(s(s(x0)), y1), y2) → IFSUM(false, isZero(s(x0)), cons(s(s(x0)), y1), y2)
IFSUM(false, false, cons(s(s(z0)), z1), z2) → IFSUM2(false, cons(s(s(z0)), z1), z2)

The TRS R consists of the following rules:

p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
isZero(s(0)) → false
isZero(s(s(x))) → isZero(s(x))

The set Q consists of the following terms:

isZero(0)
isZero(s(0))
isZero(s(s(x0)))
p(0)
p(s(0))
p(s(s(x0)))

We have to consider all minimal (P,Q,R)-chains.

(98) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 2 less nodes.

(99) TRUE

(100) Obligation:

Q DP problem:
The TRS P consists of the following rules:

SUM2(cons(0, cons(y_0, y_1)), x1) → IFSUM(false, true, cons(0, cons(y_0, y_1)), x1)
IFSUM(false, true, cons(0, cons(x1, x2)), z1) → IFSUM2(true, cons(0, cons(x1, x2)), z1)
IFSUM2(true, cons(0, cons(z0, z1)), z2) → SUM2(cons(z0, z1), z2)

The TRS R consists of the following rules:

p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
isZero(s(0)) → false
isZero(s(s(x))) → isZero(s(x))

The set Q consists of the following terms:

isZero(0)
isZero(s(0))
isZero(s(s(x0)))
p(0)
p(s(0))
p(s(s(x0)))

We have to consider all minimal (P,Q,R)-chains.

(101) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(102) Obligation:

Q DP problem:
The TRS P consists of the following rules:

SUM2(cons(0, cons(y_0, y_1)), x1) → IFSUM(false, true, cons(0, cons(y_0, y_1)), x1)
IFSUM(false, true, cons(0, cons(x1, x2)), z1) → IFSUM2(true, cons(0, cons(x1, x2)), z1)
IFSUM2(true, cons(0, cons(z0, z1)), z2) → SUM2(cons(z0, z1), z2)

R is empty.
The set Q consists of the following terms:

isZero(0)
isZero(s(0))
isZero(s(s(x0)))
p(0)
p(s(0))
p(s(s(x0)))

We have to consider all minimal (P,Q,R)-chains.

(103) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

isZero(0)
isZero(s(0))
isZero(s(s(x0)))
p(0)
p(s(0))
p(s(s(x0)))

(104) Obligation:

Q DP problem:
The TRS P consists of the following rules:

SUM2(cons(0, cons(y_0, y_1)), x1) → IFSUM(false, true, cons(0, cons(y_0, y_1)), x1)
IFSUM(false, true, cons(0, cons(x1, x2)), z1) → IFSUM2(true, cons(0, cons(x1, x2)), z1)
IFSUM2(true, cons(0, cons(z0, z1)), z2) → SUM2(cons(z0, z1), z2)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(105) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • IFSUM(false, true, cons(0, cons(x1, x2)), z1) → IFSUM2(true, cons(0, cons(x1, x2)), z1)
    The graph contains the following edges 2 >= 1, 3 >= 2, 4 >= 3

  • IFSUM2(true, cons(0, cons(z0, z1)), z2) → SUM2(cons(z0, z1), z2)
    The graph contains the following edges 2 > 1, 3 >= 2

  • SUM2(cons(0, cons(y_0, y_1)), x1) → IFSUM(false, true, cons(0, cons(y_0, y_1)), x1)
    The graph contains the following edges 1 >= 3, 2 >= 4

(106) TRUE

(107) Obligation:

Q DP problem:
The TRS P consists of the following rules:

IF(false, x, y, z) → GEN(x, y, s(z))
GEN(x, y, z) → IF(ge(z, x), x, y, z)

The TRS R consists of the following rules:

times(x, y) → sum(generate(x, y))
generate(x, y) → gen(x, y, 0)
gen(x, y, z) → if(ge(z, x), x, y, z)
if(true, x, y, z) → nil
if(false, x, y, z) → cons(y, gen(x, y, s(z)))
sum(xs) → sum2(xs, 0)
sum2(xs, y) → ifsum(isNil(xs), isZero(head(xs)), xs, y)
ifsum(true, b, xs, y) → y
ifsum(false, b, xs, y) → ifsum2(b, xs, y)
ifsum2(true, xs, y) → sum2(tail(xs), y)
ifsum2(false, xs, y) → sum2(cons(p(head(xs)), tail(xs)), s(y))
isNil(nil) → true
isNil(cons(x, xs)) → false
tail(nil) → nil
tail(cons(x, xs)) → xs
head(cons(x, xs)) → x
head(nil) → error
isZero(0) → true
isZero(s(0)) → false
isZero(s(s(x))) → isZero(s(x))
p(0) → s(s(0))
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
ge(x, 0) → true
ge(0, s(y)) → false
ge(s(x), s(y)) → ge(x, y)
a → c
a → d

The set Q consists of the following terms:

times(x0, x1)
generate(x0, x1)
gen(x0, x1, x2)
if(true, x0, x1, x2)
if(false, x0, x1, x2)
sum(x0)
sum2(x0, x1)
ifsum(true, x0, x1, x2)
ifsum(false, x0, x1, x2)
ifsum2(true, x0, x1)
ifsum2(false, x0, x1)
isNil(nil)
isNil(cons(x0, x1))
tail(nil)
tail(cons(x0, x1))
head(cons(x0, x1))
head(nil)
isZero(0)
isZero(s(0))
isZero(s(s(x0)))
p(0)
p(s(0))
p(s(s(x0)))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
a

We have to consider all minimal (P,Q,R)-chains.

(108) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(109) Obligation:

Q DP problem:
The TRS P consists of the following rules:

IF(false, x, y, z) → GEN(x, y, s(z))
GEN(x, y, z) → IF(ge(z, x), x, y, z)

The TRS R consists of the following rules:

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

The set Q consists of the following terms:

times(x0, x1)
generate(x0, x1)
gen(x0, x1, x2)
if(true, x0, x1, x2)
if(false, x0, x1, x2)
sum(x0)
sum2(x0, x1)
ifsum(true, x0, x1, x2)
ifsum(false, x0, x1, x2)
ifsum2(true, x0, x1)
ifsum2(false, x0, x1)
isNil(nil)
isNil(cons(x0, x1))
tail(nil)
tail(cons(x0, x1))
head(cons(x0, x1))
head(nil)
isZero(0)
isZero(s(0))
isZero(s(s(x0)))
p(0)
p(s(0))
p(s(s(x0)))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
a

We have to consider all minimal (P,Q,R)-chains.

(110) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

times(x0, x1)
generate(x0, x1)
gen(x0, x1, x2)
if(true, x0, x1, x2)
if(false, x0, x1, x2)
sum(x0)
sum2(x0, x1)
ifsum(true, x0, x1, x2)
ifsum(false, x0, x1, x2)
ifsum2(true, x0, x1)
ifsum2(false, x0, x1)
isNil(nil)
isNil(cons(x0, x1))
tail(nil)
tail(cons(x0, x1))
head(cons(x0, x1))
head(nil)
isZero(0)
isZero(s(0))
isZero(s(s(x0)))
p(0)
p(s(0))
p(s(s(x0)))
a

(111) Obligation:

Q DP problem:
The TRS P consists of the following rules:

IF(false, x, y, z) → GEN(x, y, s(z))
GEN(x, y, z) → IF(ge(z, x), x, y, z)

The TRS R consists of the following rules:

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

The set Q consists of the following terms:

ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))

We have to consider all minimal (P,Q,R)-chains.

(112) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule GEN(x, y, z) → IF(ge(z, x), x, y, z) we obtained the following new rules [LPAR04]:

GEN(z0, z1, s(z2)) → IF(ge(s(z2), z0), z0, z1, s(z2))

(113) Obligation:

Q DP problem:
The TRS P consists of the following rules:

IF(false, x, y, z) → GEN(x, y, s(z))
GEN(z0, z1, s(z2)) → IF(ge(s(z2), z0), z0, z1, s(z2))

The TRS R consists of the following rules:

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

The set Q consists of the following terms:

ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))

We have to consider all minimal (P,Q,R)-chains.

(114) NonInfProof (EQUIVALENT transformation)

The DP Problem is simplified using the Induction Calculus [NONINF] with the following steps:
Note that final constraints are written in bold face.


For Pair IF(false, x, y, z) → GEN(x, y, s(z)) the following chains were created:
  • We consider the chain GEN(x, y, z) → IF(ge(z, x), x, y, z), IF(false, x, y, z) → GEN(x, y, s(z)) which results in the following constraint:

    (1)    (IF(ge(x5, x3), x3, x4, x5)=IF(false, x6, x7, x8) ⇒ IF(false, x6, x7, x8)≥GEN(x6, x7, s(x8)))



    We simplified constraint (1) using rules (I), (II), (III) which results in the following new constraint:

    (2)    (ge(x5, x3)=false ⇒ IF(false, x3, x4, x5)≥GEN(x3, x4, s(x5)))



    We simplified constraint (2) using rule (V) (with possible (I) afterwards) using induction on ge(x5, x3)=false which results in the following new constraints:

    (3)    (false=false ⇒ IF(false, s(x19), x4, 0)≥GEN(s(x19), x4, s(0)))


    (4)    (ge(x21, x20)=false∧(∀x22:ge(x21, x20)=false ⇒ IF(false, x20, x22, x21)≥GEN(x20, x22, s(x21))) ⇒ IF(false, s(x20), x4, s(x21))≥GEN(s(x20), x4, s(s(x21))))



    We simplified constraint (3) using rules (I), (II) which results in the following new constraint:

    (5)    (IF(false, s(x19), x4, 0)≥GEN(s(x19), x4, s(0)))



    We simplified constraint (4) using rule (VI) where we applied the induction hypothesis (∀x22:ge(x21, x20)=false ⇒ IF(false, x20, x22, x21)≥GEN(x20, x22, s(x21))) with σ = [x22 / x4] which results in the following new constraint:

    (6)    (IF(false, x20, x4, x21)≥GEN(x20, x4, s(x21)) ⇒ IF(false, s(x20), x4, s(x21))≥GEN(s(x20), x4, s(s(x21))))







For Pair GEN(x, y, z) → IF(ge(z, x), x, y, z) the following chains were created:
  • We consider the chain IF(false, x, y, z) → GEN(x, y, s(z)), GEN(x, y, z) → IF(ge(z, x), x, y, z) which results in the following constraint:

    (7)    (GEN(x9, x10, s(x11))=GEN(x12, x13, x14) ⇒ GEN(x12, x13, x14)≥IF(ge(x14, x12), x12, x13, x14))



    We simplified constraint (7) using rules (I), (II), (III) which results in the following new constraint:

    (8)    (GEN(x9, x10, s(x11))≥IF(ge(s(x11), x9), x9, x10, s(x11)))







To summarize, we get the following constraints P≥ for the following pairs.
  • IF(false, x, y, z) → GEN(x, y, s(z))
    • (IF(false, s(x19), x4, 0)≥GEN(s(x19), x4, s(0)))
    • (IF(false, x20, x4, x21)≥GEN(x20, x4, s(x21)) ⇒ IF(false, s(x20), x4, s(x21))≥GEN(s(x20), x4, s(s(x21))))

  • GEN(x, y, z) → IF(ge(z, x), x, y, z)
    • (GEN(x9, x10, s(x11))≥IF(ge(s(x11), x9), x9, x10, s(x11)))




The constraints for P> respective 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(GEN(x1, x2, x3)) = 1 + x1 + x2 - x3   
POL(IF(x1, x2, x3, x4)) = -1 + x1 + x2 + x3 - x4   
POL(c) = -1   
POL(false) = 1   
POL(ge(x1, x2)) = 1   
POL(s(x1)) = 1 + x1   
POL(true) = 0   

The following pairs are in P>:

GEN(x, y, z) → IF(ge(z, x), x, y, z)
The following pairs are in Pbound:

IF(false, x, y, z) → GEN(x, y, s(z))
The following rules are usable:

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

(115) Complex Obligation (AND)

(116) Obligation:

Q DP problem:
The TRS P consists of the following rules:

IF(false, x, y, z) → GEN(x, y, s(z))

The TRS R consists of the following rules:

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

The set Q consists of the following terms:

ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))

We have to consider all minimal (P,Q,R)-chains.

(117) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 1 less node.

(118) TRUE

(119) Obligation:

Q DP problem:
The TRS P consists of the following rules:

GEN(x, y, z) → IF(ge(z, x), x, y, z)

The TRS R consists of the following rules:

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

The set Q consists of the following terms:

ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))

We have to consider all minimal (P,Q,R)-chains.

(120) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 1 less node.

(121) TRUE