YES Termination w.r.t. Q proof of AProVE_07_otto02.ari

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

0 QTRS
↳1 Overlay + Local Confluence (⇔, 0 ms)
↳2 QTRS
↳3 DependencyPairsProof (⇔, 0 ms)
↳4 QDP
↳5 DependencyGraphProof (⇔, 0 ms)
↳6 AND
    ↳7 QDP
        ↳8 UsableRulesProof (⇔, 0 ms)
        ↳9 QDP
        ↳10 QReductionProof (⇔, 0 ms)
        ↳11 QDP
        ↳12 QDPSizeChangeProof (⇔, 0 ms)
        ↳13 YES
    ↳14 QDP
        ↳15 UsableRulesProof (⇔, 0 ms)
        ↳16 QDP
        ↳17 QReductionProof (⇔, 0 ms)
        ↳18 QDP
        ↳19 QDPSizeChangeProof (⇔, 0 ms)
        ↳20 YES
    ↳21 QDP
        ↳22 UsableRulesProof (⇔, 0 ms)
        ↳23 QDP
        ↳24 QReductionProof (⇔, 0 ms)
        ↳25 QDP
        ↳26 NonInfProof (⇔, 0 ms)
        ↳27 AND
            ↳28 QDP
                ↳29 DependencyGraphProof (⇔, 0 ms)
                ↳30 TRUE
            ↳31 QDP
                ↳32 DependencyGraphProof (⇔, 0 ms)
                ↳33 TRUE
    ↳34 QDP
        ↳35 UsableRulesProof (⇔, 0 ms)
        ↳36 QDP
        ↳37 QReductionProof (⇔, 0 ms)
        ↳38 QDP
        ↳39 QDPSizeChangeProof (⇔, 0 ms)
        ↳40 YES
    ↳41 QDP
        ↳42 UsableRulesProof (⇔, 0 ms)
        ↳43 QDP
        ↳44 QReductionProof (⇔, 0 ms)
        ↳45 QDP
        ↳46 QDPSizeChangeProof (⇔, 0 ms)
        ↳47 YES

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

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

(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) 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(x8, x9, x10, x11) → IF(ge(x8, x9), x8, x9, x10, x11), IF(false, x12, x13, x14, x15) → HELPB(x12, x13, x14, x15) 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, x16, x17, x18, x19) → HELPB(x16, x17, x18, x19), HELPB(x20, x21, x22, x23) → HELPA(s(x20), x21, x22, x23) which results in the following constraint:
    (1)    (HELPB(x16, x17, x18, x19)=HELPB(x20, x21, x22, x23) ⇒ HELPB(x20, x21, x22, x23)≥HELPA(s(x20), x21, x22, x23))


    We simplified constraint (1) using rules (I), (II), (III) which results in the following new constraint:
    (2)    (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(x36, x37, x38, x39) → HELPA(s(x36), x37, x38, x39), HELPA(x40, x41, x42, x43) → IF(ge(x40, x41), x40, x41, x42, x43) which results in the following constraint:
    (1)    (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 (1) using rules (I), (II), (III) which results in the following new constraint:
    (2)    (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 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) = 1   
POL(HELPA(x1, x2, x3, x4)) = -1 - x1 + x2   
POL(HELPB(x1, x2, x3, x4)) = -1 - x1 + x2   
POL(IF(x1, x2, x3, x4, x5)) = -1 + x1 - x2 + x3   
POL(c) = -2   
POL(false) = 0   
POL(ge(x1, x2)) = 0   
POL(s(x1)) = 1 + x1   
POL(true) = 0   

The following pairs are in P>:

HELPB(c, l, ys, zs) → HELPA(s(c), l, ys, zs)
The following pairs are in Pbound:

IF(false, c, l, ys, zs) → HELPB(c, l, ys, zs)
The following rules are usable:

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

(27) Complex Obligation (AND)

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

(29) DependencyGraphProof (EQUIVALENT transformation)

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

(30) TRUE

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

(32) DependencyGraphProof (EQUIVALENT transformation)

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

(33) TRUE

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

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

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

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

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

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

(40) YES

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

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

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

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

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

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

(47) YES