YES Termination w.r.t. Q proof of AProVE_07_otto06.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 TransformationProof (⇔, 0 ms)
        ↳27 QDP
        ↳28 UsableRulesProof (⇔, 0 ms)
        ↳29 QDP
        ↳30 QReductionProof (⇔, 0 ms)
        ↳31 QDP
        ↳32 TransformationProof (⇔, 0 ms)
        ↳33 QDP
        ↳34 UsableRulesProof (⇔, 0 ms)
        ↳35 QDP
        ↳36 QReductionProof (⇔, 0 ms)
        ↳37 QDP
        ↳38 NonInfProof (⇔, 0 ms)
        ↳39 AND
            ↳40 QDP
                ↳41 DependencyGraphProof (⇔, 0 ms)
                ↳42 TRUE
            ↳43 QDP
                ↳44 DependencyGraphProof (⇔, 0 ms)
                ↳45 TRUE
    ↳46 QDP
        ↳47 UsableRulesProof (⇔, 0 ms)
        ↳48 QDP
        ↳49 QReductionProof (⇔, 0 ms)
        ↳50 QDP
        ↳51 QDPSizeChangeProof (⇔, 0 ms)
        ↳52 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, greater(ys, zs), smaller(ys, zs))
greater(ys, zs) → helpc(ge(length(ys), length(zs)), ys, zs)
smaller(ys, zs) → helpc(ge(length(ys), length(zs)), zs, ys)
helpc(true, ys, zs) → ys
helpc(false, ys, zs) → zs
helpb(c, l, cons(y, ys), zs) → cons(y, 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, greater(ys, zs), smaller(ys, zs))
greater(ys, zs) → helpc(ge(length(ys), length(zs)), ys, zs)
smaller(ys, zs) → helpc(ge(length(ys), length(zs)), zs, ys)
helpc(true, ys, zs) → ys
helpc(false, ys, zs) → zs
helpb(c, l, cons(y, ys), zs) → cons(y, 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)
greater(x0, x1)
smaller(x0, x1)
helpc(true, x0, x1)
helpc(false, x0, x1)
helpb(x0, x1, cons(x2, x3), x4)

(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, greater(ys, zs), smaller(ys, zs))
IF(false, c, l, ys, zs) → GREATER(ys, zs)
IF(false, c, l, ys, zs) → SMALLER(ys, zs)
GREATER(ys, zs) → HELPC(ge(length(ys), length(zs)), ys, zs)
GREATER(ys, zs) → GE(length(ys), length(zs))
GREATER(ys, zs) → LENGTH(ys)
GREATER(ys, zs) → LENGTH(zs)
SMALLER(ys, zs) → HELPC(ge(length(ys), length(zs)), zs, ys)
SMALLER(ys, zs) → GE(length(ys), length(zs))
SMALLER(ys, zs) → LENGTH(ys)
SMALLER(ys, zs) → LENGTH(zs)
HELPB(c, l, cons(y, 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, greater(ys, zs), smaller(ys, zs))
greater(ys, zs) → helpc(ge(length(ys), length(zs)), ys, zs)
smaller(ys, zs) → helpc(ge(length(ys), length(zs)), zs, ys)
helpc(true, ys, zs) → ys
helpc(false, ys, zs) → zs
helpb(c, l, cons(y, ys), zs) → cons(y, 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)
greater(x0, x1)
smaller(x0, x1)
helpc(true, x0, x1)
helpc(false, x0, x1)
helpb(x0, x1, cons(x2, x3), x4)

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

(5) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 4 SCCs with 15 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:

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, greater(ys, zs), smaller(ys, zs))
greater(ys, zs) → helpc(ge(length(ys), length(zs)), ys, zs)
smaller(ys, zs) → helpc(ge(length(ys), length(zs)), zs, ys)
helpc(true, ys, zs) → ys
helpc(false, ys, zs) → zs
helpb(c, l, cons(y, ys), zs) → cons(y, 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)
greater(x0, x1)
smaller(x0, x1)
helpc(true, x0, x1)
helpc(false, x0, x1)
helpb(x0, x1, cons(x2, x3), x4)

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:

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)
greater(x0, x1)
smaller(x0, x1)
helpc(true, x0, x1)
helpc(false, x0, x1)
helpb(x0, x1, cons(x2, x3), x4)

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)
greater(x0, x1)
smaller(x0, x1)
helpc(true, x0, x1)
helpc(false, x0, x1)
helpb(x0, x1, cons(x2, x3), x4)

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

(14) 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, greater(ys, zs), smaller(ys, zs))
greater(ys, zs) → helpc(ge(length(ys), length(zs)), ys, zs)
smaller(ys, zs) → helpc(ge(length(ys), length(zs)), zs, ys)
helpc(true, ys, zs) → ys
helpc(false, ys, zs) → zs
helpb(c, l, cons(y, ys), zs) → cons(y, 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)
greater(x0, x1)
smaller(x0, x1)
helpc(true, x0, x1)
helpc(false, x0, x1)
helpb(x0, x1, cons(x2, x3), x4)

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:

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)
greater(x0, x1)
smaller(x0, x1)
helpc(true, x0, x1)
helpc(false, x0, x1)
helpb(x0, x1, cons(x2, x3), x4)

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)
greater(x0, x1)
smaller(x0, x1)
helpc(true, x0, x1)
helpc(false, x0, x1)
helpb(x0, x1, cons(x2, x3), x4)

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

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

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

(20) YES

(21) Obligation:

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

IF(false, c, l, ys, zs) → HELPB(c, l, greater(ys, zs), smaller(ys, zs))
HELPB(c, l, cons(y, 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, greater(ys, zs), smaller(ys, zs))
greater(ys, zs) → helpc(ge(length(ys), length(zs)), ys, zs)
smaller(ys, zs) → helpc(ge(length(ys), length(zs)), zs, ys)
helpc(true, ys, zs) → ys
helpc(false, ys, zs) → zs
helpb(c, l, cons(y, ys), zs) → cons(y, 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)
greater(x0, x1)
smaller(x0, x1)
helpc(true, x0, x1)
helpc(false, x0, x1)
helpb(x0, x1, cons(x2, x3), x4)

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, greater(ys, zs), smaller(ys, zs))
HELPB(c, l, cons(y, 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)
greater(ys, zs) → helpc(ge(length(ys), length(zs)), ys, zs)
smaller(ys, zs) → helpc(ge(length(ys), length(zs)), zs, ys)
length(nil) → 0
length(cons(x, y)) → s(length(y))
helpc(true, ys, zs) → ys
helpc(false, ys, zs) → 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)
greater(x0, x1)
smaller(x0, x1)
helpc(true, x0, x1)
helpc(false, x0, x1)
helpb(x0, x1, cons(x2, x3), x4)

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))
helpa(x0, x1, x2, x3)
if(true, x0, x1, x2, x3)
if(false, x0, x1, x2, x3)
helpb(x0, x1, cons(x2, x3), x4)

(25) Obligation:

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

IF(false, c, l, ys, zs) → HELPB(c, l, greater(ys, zs), smaller(ys, zs))
HELPB(c, l, cons(y, 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)
greater(ys, zs) → helpc(ge(length(ys), length(zs)), ys, zs)
smaller(ys, zs) → helpc(ge(length(ys), length(zs)), zs, ys)
length(nil) → 0
length(cons(x, y)) → s(length(y))
helpc(true, ys, zs) → ys
helpc(false, ys, zs) → zs

The set Q consists of the following terms:

length(nil)
length(cons(x0, x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
greater(x0, x1)
smaller(x0, x1)
helpc(true, x0, x1)
helpc(false, x0, x1)

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

(26) TransformationProof (EQUIVALENT transformation)

By rewriting [LPAR04] the rule IF(false, c, l, ys, zs) → HELPB(c, l, greater(ys, zs), smaller(ys, zs)) at position [2] we obtained the following new rules [LPAR04]:

IF(false, c, l, ys, zs) → HELPB(c, l, helpc(ge(length(ys), length(zs)), ys, zs), smaller(ys, zs)) → IF(false, c, l, ys, zs) → HELPB(c, l, helpc(ge(length(ys), length(zs)), ys, zs), smaller(ys, zs))

(27) Obligation:

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

HELPB(c, l, cons(y, ys), zs) → HELPA(s(c), l, ys, zs)
HELPA(c, l, ys, zs) → IF(ge(c, l), c, l, ys, zs)
IF(false, c, l, ys, zs) → HELPB(c, l, helpc(ge(length(ys), length(zs)), ys, zs), smaller(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)
greater(ys, zs) → helpc(ge(length(ys), length(zs)), ys, zs)
smaller(ys, zs) → helpc(ge(length(ys), length(zs)), zs, ys)
length(nil) → 0
length(cons(x, y)) → s(length(y))
helpc(true, ys, zs) → ys
helpc(false, ys, zs) → zs

The set Q consists of the following terms:

length(nil)
length(cons(x0, x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
greater(x0, x1)
smaller(x0, x1)
helpc(true, x0, x1)
helpc(false, x0, x1)

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

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

(29) Obligation:

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

HELPB(c, l, cons(y, ys), zs) → HELPA(s(c), l, ys, zs)
HELPA(c, l, ys, zs) → IF(ge(c, l), c, l, ys, zs)
IF(false, c, l, ys, zs) → HELPB(c, l, helpc(ge(length(ys), length(zs)), ys, zs), smaller(ys, zs))

The TRS R consists of the following rules:

length(nil) → 0
length(cons(x, y)) → s(length(y))
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
helpc(true, ys, zs) → ys
helpc(false, ys, zs) → zs
smaller(ys, zs) → helpc(ge(length(ys), length(zs)), zs, ys)

The set Q consists of the following terms:

length(nil)
length(cons(x0, x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
greater(x0, x1)
smaller(x0, x1)
helpc(true, x0, x1)
helpc(false, x0, x1)

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

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

greater(x0, x1)

(31) Obligation:

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

HELPB(c, l, cons(y, ys), zs) → HELPA(s(c), l, ys, zs)
HELPA(c, l, ys, zs) → IF(ge(c, l), c, l, ys, zs)
IF(false, c, l, ys, zs) → HELPB(c, l, helpc(ge(length(ys), length(zs)), ys, zs), smaller(ys, zs))

The TRS R consists of the following rules:

length(nil) → 0
length(cons(x, y)) → s(length(y))
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
helpc(true, ys, zs) → ys
helpc(false, ys, zs) → zs
smaller(ys, zs) → helpc(ge(length(ys), length(zs)), zs, ys)

The set Q consists of the following terms:

length(nil)
length(cons(x0, x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
smaller(x0, x1)
helpc(true, x0, x1)
helpc(false, x0, x1)

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

(32) TransformationProof (EQUIVALENT transformation)

By rewriting [LPAR04] the rule IF(false, c, l, ys, zs) → HELPB(c, l, helpc(ge(length(ys), length(zs)), ys, zs), smaller(ys, zs)) at position [3] we obtained the following new rules [LPAR04]:

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

(33) Obligation:

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

HELPB(c, l, cons(y, ys), zs) → HELPA(s(c), l, ys, zs)
HELPA(c, l, ys, zs) → IF(ge(c, l), c, l, ys, zs)
IF(false, c, l, ys, zs) → HELPB(c, l, helpc(ge(length(ys), length(zs)), ys, zs), helpc(ge(length(ys), length(zs)), zs, ys))

The TRS R consists of the following rules:

length(nil) → 0
length(cons(x, y)) → s(length(y))
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
helpc(true, ys, zs) → ys
helpc(false, ys, zs) → zs
smaller(ys, zs) → helpc(ge(length(ys), length(zs)), zs, ys)

The set Q consists of the following terms:

length(nil)
length(cons(x0, x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
smaller(x0, x1)
helpc(true, x0, x1)
helpc(false, x0, x1)

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

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

(35) Obligation:

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

HELPB(c, l, cons(y, ys), zs) → HELPA(s(c), l, ys, zs)
HELPA(c, l, ys, zs) → IF(ge(c, l), c, l, ys, zs)
IF(false, c, l, ys, zs) → HELPB(c, l, helpc(ge(length(ys), length(zs)), ys, zs), helpc(ge(length(ys), length(zs)), zs, ys))

The TRS R consists of the following rules:

length(nil) → 0
length(cons(x, y)) → s(length(y))
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
helpc(true, ys, zs) → ys
helpc(false, ys, zs) → zs

The set Q consists of the following terms:

length(nil)
length(cons(x0, x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
smaller(x0, x1)
helpc(true, x0, x1)
helpc(false, x0, x1)

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

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

smaller(x0, x1)

(37) Obligation:

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

HELPB(c, l, cons(y, ys), zs) → HELPA(s(c), l, ys, zs)
HELPA(c, l, ys, zs) → IF(ge(c, l), c, l, ys, zs)
IF(false, c, l, ys, zs) → HELPB(c, l, helpc(ge(length(ys), length(zs)), ys, zs), helpc(ge(length(ys), length(zs)), zs, ys))

The TRS R consists of the following rules:

length(nil) → 0
length(cons(x, y)) → s(length(y))
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
helpc(true, ys, zs) → ys
helpc(false, ys, zs) → zs

The set Q consists of the following terms:

length(nil)
length(cons(x0, x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
helpc(true, x0, x1)
helpc(false, x0, x1)

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

(38) 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 HELPB(c, l, cons(y, ys), zs) → HELPA(s(c), l, ys, zs) the following chains were created:
  • We consider the chain IF(false, x9, x10, x11, x12) → HELPB(x9, x10, helpc(ge(length(x11), length(x12)), x11, x12), helpc(ge(length(x11), length(x12)), x12, x11)), HELPB(x13, x14, cons(x15, x16), x17) → HELPA(s(x13), x14, x16, x17) which results in the following constraint:
    (1)    (HELPB(x9, x10, helpc(ge(length(x11), length(x12)), x11, x12), helpc(ge(length(x11), length(x12)), x12, x11))=HELPB(x13, x14, cons(x15, x16), x17) ⇒ HELPB(x13, x14, cons(x15, x16), x17)≥HELPA(s(x13), x14, x16, x17))


    We simplified constraint (1) using rules (I), (II), (III), (IV), (VII) which results in the following new constraint:
    (2)    (ge(x53, x54)=x52∧helpc(x52, x11, x12)=cons(x15, x16)∧ge(x56, x57)=x55∧helpc(x55, x12, x11)=x17 ⇒ HELPB(x9, x10, cons(x15, x16), x17)≥HELPA(s(x9), x10, x16, x17))


    We simplified constraint (2) using rule (V) (with possible (I) afterwards) using induction on helpc(x52, x11, x12)=cons(x15, x16) which results in the following new constraints:
    (3)    (x59=cons(x15, x16)∧ge(x53, x54)=true∧ge(x56, x57)=x55∧helpc(x55, x58, x59)=x17 ⇒ HELPB(x9, x10, cons(x15, x16), x17)≥HELPA(s(x9), x10, x16, x17))

    (4)    (x60=cons(x15, x16)∧ge(x53, x54)=false∧ge(x56, x57)=x55∧helpc(x55, x60, x61)=x17 ⇒ HELPB(x9, x10, cons(x15, x16), x17)≥HELPA(s(x9), x10, x16, x17))


    We simplified constraint (3) using rules (III), (VII) which results in the following new constraint:
    (5)    (ge(x53, x54)=true∧ge(x56, x57)=x55∧cons(x15, x16)=x62∧helpc(x55, x58, x62)=x17 ⇒ HELPB(x9, x10, cons(x15, x16), x17)≥HELPA(s(x9), x10, x16, x17))


    We simplified constraint (4) using rules (III), (VII) which results in the following new constraint:
    (6)    (ge(x53, x54)=false∧ge(x56, x57)=x55∧cons(x15, x16)=x77∧helpc(x55, x77, x61)=x17 ⇒ HELPB(x9, x10, cons(x15, x16), x17)≥HELPA(s(x9), x10, x16, x17))


    We simplified constraint (5) using rule (V) (with possible (I) afterwards) using induction on ge(x53, x54)=true which results in the following new constraints:
    (7)    (true=true∧ge(x56, x57)=x55∧cons(x15, x16)=x62∧helpc(x55, x58, x62)=x17 ⇒ HELPB(x9, x10, cons(x15, x16), x17)≥HELPA(s(x9), x10, x16, x17))

    (8)    (ge(x66, x65)=true∧ge(x56, x57)=x55∧cons(x15, x16)=x62∧helpc(x55, x58, x62)=x17∧(∀x67,x68,x69,x70,x71,x72,x73,x74,x75,x76:ge(x66, x65)=true∧ge(x67, x68)=x69∧cons(x70, x71)=x72∧helpc(x69, x73, x72)=x74 ⇒ HELPB(x75, x76, cons(x70, x71), x74)≥HELPA(s(x75), x76, x71, x74)) ⇒ HELPB(x9, x10, cons(x15, x16), x17)≥HELPA(s(x9), x10, x16, x17))


    We simplified constraint (7) using rules (I), (II), (III), (IV) which results in the following new constraint:
    (9)    (HELPB(x9, x10, cons(x15, x16), x17)≥HELPA(s(x9), x10, x16, x17))


    We simplified constraint (8) using rule (VI) where we applied the induction hypothesis (∀x67,x68,x69,x70,x71,x72,x73,x74,x75,x76:ge(x66, x65)=true∧ge(x67, x68)=x69∧cons(x70, x71)=x72∧helpc(x69, x73, x72)=x74 ⇒ HELPB(x75, x76, cons(x70, x71), x74)≥HELPA(s(x75), x76, x71, x74)) with σ = [x67 / x56, x68 / x57, x69 / x55, x70 / x15, x71 / x16, x72 / x62, x73 / x58, x74 / x17, x75 / x9, x76 / x10] which results in the following new constraint:
    (10)    (HELPB(x9, x10, cons(x15, x16), x17)≥HELPA(s(x9), x10, x16, x17) ⇒ HELPB(x9, x10, cons(x15, x16), x17)≥HELPA(s(x9), x10, x16, x17))


    We simplified constraint (6) using rule (V) (with possible (I) afterwards) using induction on ge(x53, x54)=false which results in the following new constraints:
    (11)    (false=false∧ge(x56, x57)=x55∧cons(x15, x16)=x77∧helpc(x55, x77, x61)=x17 ⇒ HELPB(x9, x10, cons(x15, x16), x17)≥HELPA(s(x9), x10, x16, x17))

    (12)    (ge(x81, x80)=false∧ge(x56, x57)=x55∧cons(x15, x16)=x77∧helpc(x55, x77, x61)=x17∧(∀x82,x83,x84,x85,x86,x87,x88,x89,x90,x91:ge(x81, x80)=false∧ge(x82, x83)=x84∧cons(x85, x86)=x87∧helpc(x84, x87, x88)=x89 ⇒ HELPB(x90, x91, cons(x85, x86), x89)≥HELPA(s(x90), x91, x86, x89)) ⇒ HELPB(x9, x10, cons(x15, x16), x17)≥HELPA(s(x9), x10, x16, x17))


    We solved constraint (11) using rules (I), (II), (III), (IV).We simplified constraint (12) using rule (VI) where we applied the induction hypothesis (∀x82,x83,x84,x85,x86,x87,x88,x89,x90,x91:ge(x81, x80)=false∧ge(x82, x83)=x84∧cons(x85, x86)=x87∧helpc(x84, x87, x88)=x89 ⇒ HELPB(x90, x91, cons(x85, x86), x89)≥HELPA(s(x90), x91, x86, x89)) with σ = [x82 / x56, x83 / x57, x84 / x55, x85 / x15, x86 / x16, x87 / x77, x88 / x61, x89 / x17, x90 / x9, x91 / x10] which results in the following new constraint:
    (13)    (HELPB(x9, x10, cons(x15, x16), x17)≥HELPA(s(x9), x10, x16, x17) ⇒ HELPB(x9, x10, cons(x15, x16), x17)≥HELPA(s(x9), x10, x16, x17))






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(x18, x19, cons(x20, x21), x22) → HELPA(s(x18), x19, x21, x22), HELPA(x23, x24, x25, x26) → IF(ge(x23, x24), x23, x24, x25, x26) which results in the following constraint:
    (1)    (HELPA(s(x18), x19, x21, x22)=HELPA(x23, x24, x25, x26) ⇒ HELPA(x23, x24, x25, x26)≥IF(ge(x23, x24), x23, x24, x25, x26))


    We simplified constraint (1) using rules (I), (II), (III) which results in the following new constraint:
    (2)    (HELPA(s(x18), x19, x21, x22)≥IF(ge(s(x18), x19), s(x18), x19, x21, x22))






For Pair IF(false, c, l, ys, zs) → HELPB(c, l, helpc(ge(length(ys), length(zs)), ys, zs), helpc(ge(length(ys), length(zs)), zs, ys)) the following chains were created:
  • We consider the chain HELPA(x40, x41, x42, x43) → IF(ge(x40, x41), x40, x41, x42, x43), IF(false, x44, x45, x46, x47) → HELPB(x44, x45, helpc(ge(length(x46), length(x47)), x46, x47), helpc(ge(length(x46), length(x47)), x47, x46)) which results in the following constraint:
    (1)    (IF(ge(x40, x41), x40, x41, x42, x43)=IF(false, x44, x45, x46, x47) ⇒ IF(false, x44, x45, x46, x47)≥HELPB(x44, x45, helpc(ge(length(x46), length(x47)), x46, x47), helpc(ge(length(x46), length(x47)), x47, x46)))


    We simplified constraint (1) using rules (I), (II), (III) which results in the following new constraint:
    (2)    (ge(x40, x41)=false ⇒ IF(false, x40, x41, x42, x43)≥HELPB(x40, x41, helpc(ge(length(x42), length(x43)), x42, x43), helpc(ge(length(x42), length(x43)), x43, x42)))


    We simplified constraint (2) using rule (V) (with possible (I) afterwards) using induction on ge(x40, x41)=false which results in the following new constraints:
    (3)    (false=false ⇒ IF(false, 0, s(x93), x42, x43)≥HELPB(0, s(x93), helpc(ge(length(x42), length(x43)), x42, x43), helpc(ge(length(x42), length(x43)), x43, x42)))

    (4)    (ge(x95, x94)=false∧(∀x96,x97:ge(x95, x94)=false ⇒ IF(false, x95, x94, x96, x97)≥HELPB(x95, x94, helpc(ge(length(x96), length(x97)), x96, x97), helpc(ge(length(x96), length(x97)), x97, x96))) ⇒ IF(false, s(x95), s(x94), x42, x43)≥HELPB(s(x95), s(x94), helpc(ge(length(x42), length(x43)), x42, x43), helpc(ge(length(x42), length(x43)), x43, x42)))


    We simplified constraint (3) using rules (I), (II) which results in the following new constraint:
    (5)    (IF(false, 0, s(x93), x42, x43)≥HELPB(0, s(x93), helpc(ge(length(x42), length(x43)), x42, x43), helpc(ge(length(x42), length(x43)), x43, x42)))


    We simplified constraint (4) using rule (VI) where we applied the induction hypothesis (∀x96,x97:ge(x95, x94)=false ⇒ IF(false, x95, x94, x96, x97)≥HELPB(x95, x94, helpc(ge(length(x96), length(x97)), x96, x97), helpc(ge(length(x96), length(x97)), x97, x96))) with σ = [x96 / x42, x97 / x43] which results in the following new constraint:
    (6)    (IF(false, x95, x94, x42, x43)≥HELPB(x95, x94, helpc(ge(length(x42), length(x43)), x42, x43), helpc(ge(length(x42), length(x43)), x43, x42)) ⇒ IF(false, s(x95), s(x94), x42, x43)≥HELPB(s(x95), s(x94), helpc(ge(length(x42), length(x43)), x42, x43), helpc(ge(length(x42), length(x43)), x43, x42)))






To summarize, we get the following constraints P≥ for the following pairs.
  • HELPB(c, l, cons(y, ys), zs) → HELPA(s(c), l, ys, zs)
    • (HELPB(x9, x10, cons(x15, x16), x17)≥HELPA(s(x9), x10, x16, x17) ⇒ HELPB(x9, x10, cons(x15, x16), x17)≥HELPA(s(x9), x10, x16, x17))
    • (HELPB(x9, x10, cons(x15, x16), x17)≥HELPA(s(x9), x10, x16, x17) ⇒ HELPB(x9, x10, cons(x15, x16), x17)≥HELPA(s(x9), x10, x16, x17))
    • (HELPB(x9, x10, cons(x15, x16), x17)≥HELPA(s(x9), x10, x16, x17))

  • HELPA(c, l, ys, zs) → IF(ge(c, l), c, l, ys, zs)
    • (HELPA(s(x18), x19, x21, x22)≥IF(ge(s(x18), x19), s(x18), x19, x21, x22))

  • IF(false, c, l, ys, zs) → HELPB(c, l, helpc(ge(length(ys), length(zs)), ys, zs), helpc(ge(length(ys), length(zs)), zs, ys))
    • (IF(false, 0, s(x93), x42, x43)≥HELPB(0, s(x93), helpc(ge(length(x42), length(x43)), x42, x43), helpc(ge(length(x42), length(x43)), x43, x42)))
    • (IF(false, x95, x94, x42, x43)≥HELPB(x95, x94, helpc(ge(length(x42), length(x43)), x42, x43), helpc(ge(length(x42), length(x43)), x43, x42)) ⇒ IF(false, s(x95), s(x94), x42, x43)≥HELPB(s(x95), s(x94), helpc(ge(length(x42), length(x43)), x42, x43), helpc(ge(length(x42), length(x43)), x43, x42)))




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(HELPA(x1, x2, x3, x4)) = 1 - x1 + x2   
POL(HELPB(x1, x2, x3, x4)) = -x1 + x2   
POL(IF(x1, x2, x3, x4, x5)) = -x2 + x3   
POL(c) = -1   
POL(cons(x1, x2)) = 0   
POL(false) = 1   
POL(ge(x1, x2)) = x2   
POL(helpc(x1, x2, x3)) = 1 + x1 + x2 + x3   
POL(length(x1)) = 1   
POL(nil) = 0   
POL(s(x1)) = 1 + x1   
POL(true) = 0   

The following pairs are in P>:

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

IF(false, c, l, ys, zs) → HELPB(c, l, helpc(ge(length(ys), length(zs)), ys, zs), helpc(ge(length(ys), length(zs)), zs, ys))
There are no usable rules

(39) Complex Obligation (AND)

(40) Obligation:

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

HELPB(c, l, cons(y, ys), zs) → HELPA(s(c), l, ys, zs)
IF(false, c, l, ys, zs) → HELPB(c, l, helpc(ge(length(ys), length(zs)), ys, zs), helpc(ge(length(ys), length(zs)), zs, ys))

The TRS R consists of the following rules:

length(nil) → 0
length(cons(x, y)) → s(length(y))
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
helpc(true, ys, zs) → ys
helpc(false, ys, zs) → zs

The set Q consists of the following terms:

length(nil)
length(cons(x0, x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
helpc(true, x0, x1)
helpc(false, x0, x1)

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

(41) DependencyGraphProof (EQUIVALENT transformation)

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

(42) TRUE

(43) Obligation:

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

HELPB(c, l, cons(y, 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:

length(nil) → 0
length(cons(x, y)) → s(length(y))
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
helpc(true, ys, zs) → ys
helpc(false, ys, zs) → zs

The set Q consists of the following terms:

length(nil)
length(cons(x0, x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
helpc(true, x0, x1)
helpc(false, x0, x1)

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

(44) DependencyGraphProof (EQUIVALENT transformation)

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

(45) TRUE

(46) 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, greater(ys, zs), smaller(ys, zs))
greater(ys, zs) → helpc(ge(length(ys), length(zs)), ys, zs)
smaller(ys, zs) → helpc(ge(length(ys), length(zs)), zs, ys)
helpc(true, ys, zs) → ys
helpc(false, ys, zs) → zs
helpb(c, l, cons(y, ys), zs) → cons(y, 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)
greater(x0, x1)
smaller(x0, x1)
helpc(true, x0, x1)
helpc(false, x0, x1)
helpb(x0, x1, cons(x2, x3), x4)

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

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

(48) 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)
greater(x0, x1)
smaller(x0, x1)
helpc(true, x0, x1)
helpc(false, x0, x1)
helpb(x0, x1, cons(x2, x3), x4)

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

(49) 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)
greater(x0, x1)
smaller(x0, x1)
helpc(true, x0, x1)
helpc(false, x0, x1)
helpb(x0, x1, cons(x2, x3), x4)

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

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

(52) YES