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, 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) TRUE

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

(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) 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, z3, z4) → IF(ge(s(z0), z1), s(z0), z1, z3, z4)

(27) 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(s(z0), z1, z3, z4) → IF(ge(s(z0), z1), s(z0), z1, z3, z4)

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

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

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.

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

(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))
greater(x0, x1)
smaller(x0, x1)
helpc(true, x0, x1)
helpc(false, x0, x1)

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

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

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

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

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

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

(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))
smaller(x0, x1)
helpc(true, x0, x1)
helpc(false, x0, x1)

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

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

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

(40) 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, z3, z4) → IF(ge(s(z0), z1), s(z0), z1, z3, z4)

(41) 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))
HELPA(s(z0), z1, z3, z4) → IF(ge(s(z0), z1), s(z0), z1, z3, z4)

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.

(42) 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, c, l, ys, zs) → HELPB(c, l, helpc(ge(length(ys), length(zs)), ys, zs), helpc(ge(length(ys), length(zs)), zs, ys)), HELPB(c, l, cons(y, ys), zs) → HELPA(s(c), l, ys, zs) 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(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) which results in the following constraint:
  

  (14)    (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 (14) using rules (I), (II), (III) which results in the following new constraint:
  

  (15)    (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(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)) which results in the following constraint:
  

  (16)    (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 (16) using rules (I), (II), (III) which results in the following new constraint:
  

  (17)    (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 (17) using rule (V) (with possible (I) afterwards) using induction on ge(x40, x41)=false which results in the following new constraints:
  

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

  
  

  (19)    (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 (18) using rules (I), (II) which results in the following new constraint:
  

  (20)    (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 (19) 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:
  

  (21)    (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 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) = -2   
POL(cons(x₁, x₂)) = 1 + x₂   
POL(false) = 0   
POL(ge(x₁, x₂)) = 0   
POL(helpc(x₁, x₂, x₃)) = 0   
POL(length(x₁)) = 0   
POL(nil) = 0   
POL(s(x₁)) = 1 + x₁   
POL(true) = 0   

The following pairs are in P_>:

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

The following pairs are in P_bound:

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 rules are usable:

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

(43) Complex Obligation (AND)

(44) Obligation:

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

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.

(45) DependencyGraphProof (EQUIVALENT transformation)

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

(46) TRUE

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

(48) DependencyGraphProof (EQUIVALENT transformation)

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

(49) TRUE

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

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

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

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

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

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

(56) TRUE