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

(0) Obligation:

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

app(x, y) → helpa(0, plus(length(x), length(y)), x, y)
plus(x, 0) → x
plus(x, s(y)) → s(plus(x, y))
length(nil) → 0
length(cons(x, y)) → s(length(y))
helpa(c, l, ys, zs) → if(ge(c, l), c, l, ys, zs)
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
if(true, c, l, ys, zs) → nil
if(false, c, l, ys, zs) → helpb(c, l, ys, zs)
take(0, cons(x, xs), ys) → x
take(0, nil, cons(y, ys)) → y
take(s(c), cons(x, xs), ys) → take(c, xs, ys)
take(s(c), nil, cons(y, ys)) → take(c, nil, ys)
helpb(c, l, ys, zs) → cons(take(c, ys, zs), helpa(s(c), l, ys, zs))

Q is empty.

(1) Overlay + Local Confluence (EQUIVALENT transformation)

The TRS is overlay and locally confluent. By [NOC] we can switch to innermost.

(2) Obligation:

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

app(x, y) → helpa(0, plus(length(x), length(y)), x, y)
plus(x, 0) → x
plus(x, s(y)) → s(plus(x, y))
length(nil) → 0
length(cons(x, y)) → s(length(y))
helpa(c, l, ys, zs) → if(ge(c, l), c, l, ys, zs)
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
if(true, c, l, ys, zs) → nil
if(false, c, l, ys, zs) → helpb(c, l, ys, zs)
take(0, cons(x, xs), ys) → x
take(0, nil, cons(y, ys)) → y
take(s(c), cons(x, xs), ys) → take(c, xs, ys)
take(s(c), nil, cons(y, ys)) → take(c, nil, ys)
helpb(c, l, ys, zs) → cons(take(c, ys, zs), helpa(s(c), l, ys, zs))

The set Q consists of the following terms:

app(x0, x1)
plus(x0, 0)
plus(x0, s(x1))
length(nil)
length(cons(x0, x1))
helpa(x0, x1, x2, x3)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
if(true, x0, x1, x2, x3)
if(false, x0, x1, x2, x3)
take(0, cons(x0, xs), x1)
take(0, nil, cons(x0, x1))
take(s(x0), cons(x1, xs), x2)
take(s(x0), nil, cons(x1, x2))
helpb(x0, x1, x2, x3)

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

APP(x, y) → HELPA(0, plus(length(x), length(y)), x, y)
APP(x, y) → PLUS(length(x), length(y))
APP(x, y) → LENGTH(x)
APP(x, y) → LENGTH(y)
PLUS(x, s(y)) → PLUS(x, y)
LENGTH(cons(x, y)) → LENGTH(y)
HELPA(c, l, ys, zs) → IF(ge(c, l), c, l, ys, zs)
HELPA(c, l, ys, zs) → GE(c, l)
GE(s(x), s(y)) → GE(x, y)
IF(false, c, l, ys, zs) → HELPB(c, l, ys, zs)
TAKE(s(c), cons(x, xs), ys) → TAKE(c, xs, ys)
TAKE(s(c), nil, cons(y, ys)) → TAKE(c, nil, ys)
HELPB(c, l, ys, zs) → TAKE(c, ys, zs)
HELPB(c, l, ys, zs) → HELPA(s(c), l, ys, zs)

The TRS R consists of the following rules:

app(x, y) → helpa(0, plus(length(x), length(y)), x, y)
plus(x, 0) → x
plus(x, s(y)) → s(plus(x, y))
length(nil) → 0
length(cons(x, y)) → s(length(y))
helpa(c, l, ys, zs) → if(ge(c, l), c, l, ys, zs)
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
if(true, c, l, ys, zs) → nil
if(false, c, l, ys, zs) → helpb(c, l, ys, zs)
take(0, cons(x, xs), ys) → x
take(0, nil, cons(y, ys)) → y
take(s(c), cons(x, xs), ys) → take(c, xs, ys)
take(s(c), nil, cons(y, ys)) → take(c, nil, ys)
helpb(c, l, ys, zs) → cons(take(c, ys, zs), helpa(s(c), l, ys, zs))

The set Q consists of the following terms:

app(x0, x1)
plus(x0, 0)
plus(x0, s(x1))
length(nil)
length(cons(x0, x1))
helpa(x0, x1, x2, x3)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
if(true, x0, x1, x2, x3)
if(false, x0, x1, x2, x3)
take(0, cons(x0, xs), x1)
take(0, nil, cons(x0, x1))
take(s(x0), cons(x1, xs), x2)
take(s(x0), nil, cons(x1, x2))
helpb(x0, x1, x2, x3)

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 7 less nodes.

(6) Complex Obligation (AND)

(7) Obligation:

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

TAKE(s(c), nil, cons(y, ys)) → TAKE(c, nil, ys)

The TRS R consists of the following rules:

app(x, y) → helpa(0, plus(length(x), length(y)), x, y)
plus(x, 0) → x
plus(x, s(y)) → s(plus(x, y))
length(nil) → 0
length(cons(x, y)) → s(length(y))
helpa(c, l, ys, zs) → if(ge(c, l), c, l, ys, zs)
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
if(true, c, l, ys, zs) → nil
if(false, c, l, ys, zs) → helpb(c, l, ys, zs)
take(0, cons(x, xs), ys) → x
take(0, nil, cons(y, ys)) → y
take(s(c), cons(x, xs), ys) → take(c, xs, ys)
take(s(c), nil, cons(y, ys)) → take(c, nil, ys)
helpb(c, l, ys, zs) → cons(take(c, ys, zs), helpa(s(c), l, ys, zs))

The set Q consists of the following terms:

app(x0, x1)
plus(x0, 0)
plus(x0, s(x1))
length(nil)
length(cons(x0, x1))
helpa(x0, x1, x2, x3)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
if(true, x0, x1, x2, x3)
if(false, x0, x1, x2, x3)
take(0, cons(x0, xs), x1)
take(0, nil, cons(x0, x1))
take(s(x0), cons(x1, xs), x2)
take(s(x0), nil, cons(x1, x2))
helpb(x0, x1, x2, x3)

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:

TAKE(s(c), nil, cons(y, ys)) → TAKE(c, nil, ys)

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

app(x0, x1)
plus(x0, 0)
plus(x0, s(x1))
length(nil)
length(cons(x0, x1))
helpa(x0, x1, x2, x3)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
if(true, x0, x1, x2, x3)
if(false, x0, x1, x2, x3)
take(0, cons(x0, xs), x1)
take(0, nil, cons(x0, x1))
take(s(x0), cons(x1, xs), x2)
take(s(x0), nil, cons(x1, x2))
helpb(x0, x1, x2, x3)

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].

app(x0, x1)
plus(x0, 0)
plus(x0, s(x1))
length(nil)
length(cons(x0, x1))
helpa(x0, x1, x2, x3)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
if(true, x0, x1, x2, x3)
if(false, x0, x1, x2, x3)
take(0, cons(x0, xs), x1)
take(0, nil, cons(x0, x1))
take(s(x0), cons(x1, xs), x2)
take(s(x0), nil, cons(x1, x2))
helpb(x0, x1, x2, x3)

(11) Obligation:

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

TAKE(s(c), nil, cons(y, ys)) → TAKE(c, nil, ys)

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:

• TAKE(s(c), nil, cons(y, ys)) → TAKE(c, nil, ys)
  The graph contains the following edges 1 > 1, 2 >= 2, 3 > 3

(13) TRUE

(14) 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:

app(x, y) → helpa(0, plus(length(x), length(y)), x, y)
plus(x, 0) → x
plus(x, s(y)) → s(plus(x, y))
length(nil) → 0
length(cons(x, y)) → s(length(y))
helpa(c, l, ys, zs) → if(ge(c, l), c, l, ys, zs)
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
if(true, c, l, ys, zs) → nil
if(false, c, l, ys, zs) → helpb(c, l, ys, zs)
take(0, cons(x, xs), ys) → x
take(0, nil, cons(y, ys)) → y
take(s(c), cons(x, xs), ys) → take(c, xs, ys)
take(s(c), nil, cons(y, ys)) → take(c, nil, ys)
helpb(c, l, ys, zs) → cons(take(c, ys, zs), helpa(s(c), l, ys, zs))

The set Q consists of the following terms:

app(x0, x1)
plus(x0, 0)
plus(x0, s(x1))
length(nil)
length(cons(x0, x1))
helpa(x0, x1, x2, x3)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
if(true, x0, x1, x2, x3)
if(false, x0, x1, x2, x3)
take(0, cons(x0, xs), x1)
take(0, nil, cons(x0, x1))
take(s(x0), cons(x1, xs), x2)
take(s(x0), nil, cons(x1, x2))
helpb(x0, x1, x2, x3)

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:

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

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

app(x0, x1)
plus(x0, 0)
plus(x0, s(x1))
length(nil)
length(cons(x0, x1))
helpa(x0, x1, x2, x3)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
if(true, x0, x1, x2, x3)
if(false, x0, x1, x2, x3)
take(0, cons(x0, xs), x1)
take(0, nil, cons(x0, x1))
take(s(x0), cons(x1, xs), x2)
take(s(x0), nil, cons(x1, x2))
helpb(x0, x1, x2, x3)

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].

app(x0, x1)
plus(x0, 0)
plus(x0, s(x1))
length(nil)
length(cons(x0, x1))
helpa(x0, x1, x2, x3)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
if(true, x0, x1, x2, x3)
if(false, x0, x1, x2, x3)
take(0, cons(x0, xs), x1)
take(0, nil, cons(x0, x1))
take(s(x0), cons(x1, xs), x2)
take(s(x0), nil, cons(x1, x2))
helpb(x0, x1, x2, x3)

(18) 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.

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

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

(20) TRUE

(21) Obligation:

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

IF(false, c, l, ys, zs) → HELPB(c, l, ys, zs)
HELPB(c, l, ys, zs) → HELPA(s(c), l, ys, zs)
HELPA(c, l, ys, zs) → IF(ge(c, l), c, l, ys, zs)

The TRS R consists of the following rules:

app(x, y) → helpa(0, plus(length(x), length(y)), x, y)
plus(x, 0) → x
plus(x, s(y)) → s(plus(x, y))
length(nil) → 0
length(cons(x, y)) → s(length(y))
helpa(c, l, ys, zs) → if(ge(c, l), c, l, ys, zs)
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
if(true, c, l, ys, zs) → nil
if(false, c, l, ys, zs) → helpb(c, l, ys, zs)
take(0, cons(x, xs), ys) → x
take(0, nil, cons(y, ys)) → y
take(s(c), cons(x, xs), ys) → take(c, xs, ys)
take(s(c), nil, cons(y, ys)) → take(c, nil, ys)
helpb(c, l, ys, zs) → cons(take(c, ys, zs), helpa(s(c), l, ys, zs))

The set Q consists of the following terms:

app(x0, x1)
plus(x0, 0)
plus(x0, s(x1))
length(nil)
length(cons(x0, x1))
helpa(x0, x1, x2, x3)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
if(true, x0, x1, x2, x3)
if(false, x0, x1, x2, x3)
take(0, cons(x0, xs), x1)
take(0, nil, cons(x0, x1))
take(s(x0), cons(x1, xs), x2)
take(s(x0), nil, cons(x1, x2))
helpb(x0, x1, x2, x3)

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:

IF(false, c, l, ys, zs) → HELPB(c, l, ys, zs)
HELPB(c, l, ys, zs) → HELPA(s(c), l, ys, zs)
HELPA(c, l, ys, zs) → IF(ge(c, l), c, l, ys, zs)

The TRS R consists of the following rules:

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

The set Q consists of the following terms:

app(x0, x1)
plus(x0, 0)
plus(x0, s(x1))
length(nil)
length(cons(x0, x1))
helpa(x0, x1, x2, x3)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
if(true, x0, x1, x2, x3)
if(false, x0, x1, x2, x3)
take(0, cons(x0, xs), x1)
take(0, nil, cons(x0, x1))
take(s(x0), cons(x1, xs), x2)
take(s(x0), nil, cons(x1, x2))
helpb(x0, x1, x2, x3)

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].

app(x0, x1)
plus(x0, 0)
plus(x0, s(x1))
length(nil)
length(cons(x0, x1))
helpa(x0, x1, x2, x3)
if(true, x0, x1, x2, x3)
if(false, x0, x1, x2, x3)
take(0, cons(x0, xs), x1)
take(0, nil, cons(x0, x1))
take(s(x0), cons(x1, xs), x2)
take(s(x0), nil, cons(x1, x2))
helpb(x0, x1, x2, x3)

(25) Obligation:

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

IF(false, c, l, ys, zs) → HELPB(c, l, ys, zs)
HELPB(c, l, ys, zs) → HELPA(s(c), l, ys, zs)
HELPA(c, l, ys, zs) → IF(ge(c, l), c, l, ys, zs)

The TRS R consists of the following rules:

ge(x, 0) → true
ge(0, s(x)) → 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.

(26) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule HELPA(c, l, ys, zs) → IF(ge(c, l), c, l, ys, zs) we obtained the following new rules [LPAR04]:

HELPA(s(z0), z1, z2, z3) → IF(ge(s(z0), z1), s(z0), z1, z2, z3)

(27) Obligation:

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

IF(false, c, l, ys, zs) → HELPB(c, l, ys, zs)
HELPB(c, l, ys, zs) → HELPA(s(c), l, ys, zs)
HELPA(s(z0), z1, z2, z3) → IF(ge(s(z0), z1), s(z0), z1, z2, z3)

The TRS R consists of the following rules:

ge(x, 0) → true
ge(0, s(x)) → 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.

(28) 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, c, l, ys, zs) → HELPB(c, l, ys, zs) the following chains were created:

• We consider the chain HELPA(c, l, ys, zs) → IF(ge(c, l), c, l, ys, zs), IF(false, c, l, ys, zs) → HELPB(c, l, ys, zs) which results in the following constraint:
  

  (1)    (IF(ge(x8, x9), x8, x9, x10, x11)=IF(false, x12, x13, x14, x15) ⇒ IF(false, x12, x13, x14, x15)≥HELPB(x12, x13, x14, x15))

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

  (2)    (ge(x8, x9)=false ⇒ IF(false, x8, x9, x10, x11)≥HELPB(x8, x9, x10, x11))

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

  (3)    (false=false ⇒ IF(false, 0, s(x49), x10, x11)≥HELPB(0, s(x49), x10, x11))

  
  

  (4)    (ge(x51, x50)=false∧(∀x52,x53:ge(x51, x50)=false ⇒ IF(false, x51, x50, x52, x53)≥HELPB(x51, x50, x52, x53)) ⇒ IF(false, s(x51), s(x50), x10, x11)≥HELPB(s(x51), s(x50), x10, x11))

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

  (5)    (IF(false, 0, s(x49), x10, x11)≥HELPB(0, s(x49), x10, x11))

  
  
  We simplified constraint (4) using rule (VI) where we applied the induction hypothesis (∀x52,x53:ge(x51, x50)=false ⇒ IF(false, x51, x50, x52, x53)≥HELPB(x51, x50, x52, x53)) with σ = [x52 / x10, x53 / x11] which results in the following new constraint:
  

  (6)    (IF(false, x51, x50, x10, x11)≥HELPB(x51, x50, x10, x11) ⇒ IF(false, s(x51), s(x50), x10, x11)≥HELPB(s(x51), s(x50), x10, x11))

  
  
  

For Pair HELPB(c, l, ys, zs) → HELPA(s(c), l, ys, zs) the following chains were created:

• We consider the chain IF(false, c, l, ys, zs) → HELPB(c, l, ys, zs), HELPB(c, l, ys, zs) → HELPA(s(c), l, ys, zs) which results in the following constraint:
  

  (7)    (HELPB(x16, x17, x18, x19)=HELPB(x20, x21, x22, x23) ⇒ HELPB(x20, x21, x22, x23)≥HELPA(s(x20), x21, x22, x23))

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

  (8)    (HELPB(x16, x17, x18, x19)≥HELPA(s(x16), x17, x18, x19))

  
  
  

For Pair HELPA(c, l, ys, zs) → IF(ge(c, l), c, l, ys, zs) the following chains were created:

• We consider the chain HELPB(c, l, ys, zs) → HELPA(s(c), l, ys, zs), HELPA(c, l, ys, zs) → IF(ge(c, l), c, l, ys, zs) which results in the following constraint:
  

  (9)    (HELPA(s(x36), x37, x38, x39)=HELPA(x40, x41, x42, x43) ⇒ HELPA(x40, x41, x42, x43)≥IF(ge(x40, x41), x40, x41, x42, x43))

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

  (10)    (HELPA(s(x36), x37, x38, x39)≥IF(ge(s(x36), x37), s(x36), x37, x38, x39))

  
  
  

To summarize, we get the following constraints P_≥ for the following pairs.

• IF(false, c, l, ys, zs) → HELPB(c, l, ys, zs)
  
  • (IF(false, 0, s(x49), x10, x11)≥HELPB(0, s(x49), x10, x11))
    
  • (IF(false, x51, x50, x10, x11)≥HELPB(x51, x50, x10, x11) ⇒ IF(false, s(x51), s(x50), x10, x11)≥HELPB(s(x51), s(x50), x10, x11))
    
  
  
• HELPB(c, l, ys, zs) → HELPA(s(c), l, ys, zs)
  
  • (HELPB(x16, x17, x18, x19)≥HELPA(s(x16), x17, x18, x19))
    
  
  
• HELPA(c, l, ys, zs) → IF(ge(c, l), c, l, ys, zs)
  
  • (HELPA(s(x36), x37, x38, x39)≥IF(ge(s(x36), x37), s(x36), x37, x38, x39))
    
  
  

The constraints for P_> respective P_bound are constructed from P_≥ where we just replace every occurence of "t ≥ s" in P_≥ by "t > s" respective "t ≥ c". Here c stands for the fresh constant used for P_bound.
Using the following integer polynomial ordering the resulting constraints can be solved
Polynomial interpretation [NONINF]:

POL(0) = 0   
POL(HELPA(x₁, x₂, x₃, x₄)) = 1 - x₁ + x₂   
POL(HELPB(x₁, x₂, x₃, x₄)) = 1 - x₁ + x₂   
POL(IF(x₁, x₂, x₃, x₄, x₅)) = 1 - x₁ - x₂ + x₃   
POL(c) = -1   
POL(false) = 0   
POL(ge(x₁, x₂)) = 0   
POL(s(x₁)) = 1 + x₁   
POL(true) = 1   

The following pairs are in P_>:

HELPB(c, l, ys, zs) → HELPA(s(c), l, ys, zs)

The following pairs are in P_bound:

IF(false, c, l, ys, zs) → HELPB(c, l, ys, zs)

The following rules are usable:

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

(29) Complex Obligation (AND)

(30) Obligation:

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

IF(false, c, l, ys, zs) → HELPB(c, l, ys, zs)
HELPA(c, l, ys, zs) → IF(ge(c, l), c, l, ys, zs)

The TRS R consists of the following rules:

ge(x, 0) → true
ge(0, s(x)) → 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.

(31) DependencyGraphProof (EQUIVALENT transformation)

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

(32) TRUE

(33) Obligation:

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

HELPB(c, l, ys, zs) → HELPA(s(c), l, ys, zs)
HELPA(c, l, ys, zs) → IF(ge(c, l), c, l, ys, zs)

The TRS R consists of the following rules:

ge(x, 0) → true
ge(0, s(x)) → 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.

(34) DependencyGraphProof (EQUIVALENT transformation)

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

(35) TRUE

(36) Obligation:

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

LENGTH(cons(x, y)) → LENGTH(y)

The TRS R consists of the following rules:

app(x, y) → helpa(0, plus(length(x), length(y)), x, y)
plus(x, 0) → x
plus(x, s(y)) → s(plus(x, y))
length(nil) → 0
length(cons(x, y)) → s(length(y))
helpa(c, l, ys, zs) → if(ge(c, l), c, l, ys, zs)
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
if(true, c, l, ys, zs) → nil
if(false, c, l, ys, zs) → helpb(c, l, ys, zs)
take(0, cons(x, xs), ys) → x
take(0, nil, cons(y, ys)) → y
take(s(c), cons(x, xs), ys) → take(c, xs, ys)
take(s(c), nil, cons(y, ys)) → take(c, nil, ys)
helpb(c, l, ys, zs) → cons(take(c, ys, zs), helpa(s(c), l, ys, zs))

The set Q consists of the following terms:

app(x0, x1)
plus(x0, 0)
plus(x0, s(x1))
length(nil)
length(cons(x0, x1))
helpa(x0, x1, x2, x3)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
if(true, x0, x1, x2, x3)
if(false, x0, x1, x2, x3)
take(0, cons(x0, xs), x1)
take(0, nil, cons(x0, x1))
take(s(x0), cons(x1, xs), x2)
take(s(x0), nil, cons(x1, x2))
helpb(x0, x1, x2, x3)

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:

LENGTH(cons(x, y)) → LENGTH(y)

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

app(x0, x1)
plus(x0, 0)
plus(x0, s(x1))
length(nil)
length(cons(x0, x1))
helpa(x0, x1, x2, x3)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
if(true, x0, x1, x2, x3)
if(false, x0, x1, x2, x3)
take(0, cons(x0, xs), x1)
take(0, nil, cons(x0, x1))
take(s(x0), cons(x1, xs), x2)
take(s(x0), nil, cons(x1, x2))
helpb(x0, x1, x2, x3)

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].

app(x0, x1)
plus(x0, 0)
plus(x0, s(x1))
length(nil)
length(cons(x0, x1))
helpa(x0, x1, x2, x3)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
if(true, x0, x1, x2, x3)
if(false, x0, x1, x2, x3)
take(0, cons(x0, xs), x1)
take(0, nil, cons(x0, x1))
take(s(x0), cons(x1, xs), x2)
take(s(x0), nil, cons(x1, x2))
helpb(x0, x1, x2, x3)

(40) Obligation:

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

LENGTH(cons(x, y)) → LENGTH(y)

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

(41) 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:

• LENGTH(cons(x, y)) → LENGTH(y)
  The graph contains the following edges 1 > 1

(42) TRUE

(43) Obligation:

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

PLUS(x, s(y)) → PLUS(x, y)

The TRS R consists of the following rules:

app(x, y) → helpa(0, plus(length(x), length(y)), x, y)
plus(x, 0) → x
plus(x, s(y)) → s(plus(x, y))
length(nil) → 0
length(cons(x, y)) → s(length(y))
helpa(c, l, ys, zs) → if(ge(c, l), c, l, ys, zs)
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
if(true, c, l, ys, zs) → nil
if(false, c, l, ys, zs) → helpb(c, l, ys, zs)
take(0, cons(x, xs), ys) → x
take(0, nil, cons(y, ys)) → y
take(s(c), cons(x, xs), ys) → take(c, xs, ys)
take(s(c), nil, cons(y, ys)) → take(c, nil, ys)
helpb(c, l, ys, zs) → cons(take(c, ys, zs), helpa(s(c), l, ys, zs))

The set Q consists of the following terms:

app(x0, x1)
plus(x0, 0)
plus(x0, s(x1))
length(nil)
length(cons(x0, x1))
helpa(x0, x1, x2, x3)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
if(true, x0, x1, x2, x3)
if(false, x0, x1, x2, x3)
take(0, cons(x0, xs), x1)
take(0, nil, cons(x0, x1))
take(s(x0), cons(x1, xs), x2)
take(s(x0), nil, cons(x1, x2))
helpb(x0, x1, x2, x3)

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

(44) 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.

(45) Obligation:

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

PLUS(x, s(y)) → PLUS(x, y)

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

app(x0, x1)
plus(x0, 0)
plus(x0, s(x1))
length(nil)
length(cons(x0, x1))
helpa(x0, x1, x2, x3)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
if(true, x0, x1, x2, x3)
if(false, x0, x1, x2, x3)
take(0, cons(x0, xs), x1)
take(0, nil, cons(x0, x1))
take(s(x0), cons(x1, xs), x2)
take(s(x0), nil, cons(x1, x2))
helpb(x0, x1, x2, x3)

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

(46) 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].

app(x0, x1)
plus(x0, 0)
plus(x0, s(x1))
length(nil)
length(cons(x0, x1))
helpa(x0, x1, x2, x3)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
if(true, x0, x1, x2, x3)
if(false, x0, x1, x2, x3)
take(0, cons(x0, xs), x1)
take(0, nil, cons(x0, x1))
take(s(x0), cons(x1, xs), x2)
take(s(x0), nil, cons(x1, x2))
helpb(x0, x1, x2, x3)

(47) Obligation:

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

PLUS(x, s(y)) → PLUS(x, y)

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

(48) 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:

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

(49) TRUE