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:

lessElements(l, t) → lessE(l, t, 0)
lessE(l, t, n) → if(le(length(l), n), le(length(toList(t)), n), l, t, n)
if(true, b, l, t, n) → l
if(false, true, l, t, n) → t
if(false, false, l, t, n) → lessE(l, t, s(n))
length(nil) → 0
length(cons(n, l)) → s(length(l))
toList(leaf) → nil
toList(node(t1, n, t2)) → append(toList(t1), cons(n, toList(t2)))
append(nil, l2) → l2
append(cons(n, l1), l2) → cons(n, append(l1, l2))
le(s(n), 0) → false
le(0, m) → true
le(s(n), s(m)) → le(n, m)
a → c
a → d

Q is empty.

(1) AAECC Innermost (EQUIVALENT transformation)

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

if(true, b, l, t, n) → l
if(false, true, l, t, n) → t
if(false, false, l, t, n) → lessE(l, t, s(n))
length(nil) → 0
length(cons(n, l)) → s(length(l))
toList(leaf) → nil
toList(node(t1, n, t2)) → append(toList(t1), cons(n, toList(t2)))
append(nil, l2) → l2
append(cons(n, l1), l2) → cons(n, append(l1, l2))
le(s(n), 0) → false
le(0, m) → true
le(s(n), s(m)) → le(n, m)
lessElements(l, t) → lessE(l, t, 0)
lessE(l, t, n) → if(le(length(l), n), le(length(toList(t)), n), l, t, n)

The TRS R 2 is

a → c
a → d

The signature Sigma is {c, a, d}

(2) Obligation:

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

lessElements(l, t) → lessE(l, t, 0)
lessE(l, t, n) → if(le(length(l), n), le(length(toList(t)), n), l, t, n)
if(true, b, l, t, n) → l
if(false, true, l, t, n) → t
if(false, false, l, t, n) → lessE(l, t, s(n))
length(nil) → 0
length(cons(n, l)) → s(length(l))
toList(leaf) → nil
toList(node(t1, n, t2)) → append(toList(t1), cons(n, toList(t2)))
append(nil, l2) → l2
append(cons(n, l1), l2) → cons(n, append(l1, l2))
le(s(n), 0) → false
le(0, m) → true
le(s(n), s(m)) → le(n, m)
a → c
a → d

The set Q consists of the following terms:

lessElements(x0, x1)
lessE(x0, x1, x2)
if(true, x0, x1, x2, x3)
if(false, true, x0, x1, x2)
if(false, false, x0, x1, x2)
length(nil)
length(cons(x0, x1))
toList(leaf)
toList(node(x0, x1, x2))
append(nil, x0)
append(cons(x0, x1), x2)
le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))
a

(3) DependencyPairsProof (EQUIVALENT transformation)

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

(4) Obligation:

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

LESSELEMENTS(l, t) → LESSE(l, t, 0)
LESSE(l, t, n) → IF(le(length(l), n), le(length(toList(t)), n), l, t, n)
LESSE(l, t, n) → LE(length(l), n)
LESSE(l, t, n) → LENGTH(l)
LESSE(l, t, n) → LE(length(toList(t)), n)
LESSE(l, t, n) → LENGTH(toList(t))
LESSE(l, t, n) → TOLIST(t)
IF(false, false, l, t, n) → LESSE(l, t, s(n))
LENGTH(cons(n, l)) → LENGTH(l)
TOLIST(node(t1, n, t2)) → APPEND(toList(t1), cons(n, toList(t2)))
TOLIST(node(t1, n, t2)) → TOLIST(t1)
TOLIST(node(t1, n, t2)) → TOLIST(t2)
APPEND(cons(n, l1), l2) → APPEND(l1, l2)
LE(s(n), s(m)) → LE(n, m)

The TRS R consists of the following rules:

lessElements(l, t) → lessE(l, t, 0)
lessE(l, t, n) → if(le(length(l), n), le(length(toList(t)), n), l, t, n)
if(true, b, l, t, n) → l
if(false, true, l, t, n) → t
if(false, false, l, t, n) → lessE(l, t, s(n))
length(nil) → 0
length(cons(n, l)) → s(length(l))
toList(leaf) → nil
toList(node(t1, n, t2)) → append(toList(t1), cons(n, toList(t2)))
append(nil, l2) → l2
append(cons(n, l1), l2) → cons(n, append(l1, l2))
le(s(n), 0) → false
le(0, m) → true
le(s(n), s(m)) → le(n, m)
a → c
a → d

The set Q consists of the following terms:

lessElements(x0, x1)
lessE(x0, x1, x2)
if(true, x0, x1, x2, x3)
if(false, true, x0, x1, x2)
if(false, false, x0, x1, x2)
length(nil)
length(cons(x0, x1))
toList(leaf)
toList(node(x0, x1, x2))
append(nil, x0)
append(cons(x0, x1), x2)
le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))
a

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

(5) DependencyGraphProof (EQUIVALENT transformation)

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

(6) Complex Obligation (AND)

(7) Obligation:

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

LE(s(n), s(m)) → LE(n, m)

The TRS R consists of the following rules:

lessElements(l, t) → lessE(l, t, 0)
lessE(l, t, n) → if(le(length(l), n), le(length(toList(t)), n), l, t, n)
if(true, b, l, t, n) → l
if(false, true, l, t, n) → t
if(false, false, l, t, n) → lessE(l, t, s(n))
length(nil) → 0
length(cons(n, l)) → s(length(l))
toList(leaf) → nil
toList(node(t1, n, t2)) → append(toList(t1), cons(n, toList(t2)))
append(nil, l2) → l2
append(cons(n, l1), l2) → cons(n, append(l1, l2))
le(s(n), 0) → false
le(0, m) → true
le(s(n), s(m)) → le(n, m)
a → c
a → d

The set Q consists of the following terms:

lessElements(x0, x1)
lessE(x0, x1, x2)
if(true, x0, x1, x2, x3)
if(false, true, x0, x1, x2)
if(false, false, x0, x1, x2)
length(nil)
length(cons(x0, x1))
toList(leaf)
toList(node(x0, x1, x2))
append(nil, x0)
append(cons(x0, x1), x2)
le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))
a

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

(8) UsableRulesProof (EQUIVALENT transformation)

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

(9) Obligation:

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

LE(s(n), s(m)) → LE(n, m)

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

lessElements(x0, x1)
lessE(x0, x1, x2)
if(true, x0, x1, x2, x3)
if(false, true, x0, x1, x2)
if(false, false, x0, x1, x2)
length(nil)
length(cons(x0, x1))
toList(leaf)
toList(node(x0, x1, x2))
append(nil, x0)
append(cons(x0, x1), x2)
le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))
a

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

(10) QReductionProof (EQUIVALENT transformation)

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

lessElements(x0, x1)
lessE(x0, x1, x2)
if(true, x0, x1, x2, x3)
if(false, true, x0, x1, x2)
if(false, false, x0, x1, x2)
length(nil)
length(cons(x0, x1))
toList(leaf)
toList(node(x0, x1, x2))
append(nil, x0)
append(cons(x0, x1), x2)
le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))
a

(11) Obligation:

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

LE(s(n), s(m)) → LE(n, m)

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:

• LE(s(n), s(m)) → LE(n, m)
  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:

APPEND(cons(n, l1), l2) → APPEND(l1, l2)

The TRS R consists of the following rules:

lessElements(l, t) → lessE(l, t, 0)
lessE(l, t, n) → if(le(length(l), n), le(length(toList(t)), n), l, t, n)
if(true, b, l, t, n) → l
if(false, true, l, t, n) → t
if(false, false, l, t, n) → lessE(l, t, s(n))
length(nil) → 0
length(cons(n, l)) → s(length(l))
toList(leaf) → nil
toList(node(t1, n, t2)) → append(toList(t1), cons(n, toList(t2)))
append(nil, l2) → l2
append(cons(n, l1), l2) → cons(n, append(l1, l2))
le(s(n), 0) → false
le(0, m) → true
le(s(n), s(m)) → le(n, m)
a → c
a → d

The set Q consists of the following terms:

lessElements(x0, x1)
lessE(x0, x1, x2)
if(true, x0, x1, x2, x3)
if(false, true, x0, x1, x2)
if(false, false, x0, x1, x2)
length(nil)
length(cons(x0, x1))
toList(leaf)
toList(node(x0, x1, x2))
append(nil, x0)
append(cons(x0, x1), x2)
le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))
a

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

(15) UsableRulesProof (EQUIVALENT transformation)

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

(16) Obligation:

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

APPEND(cons(n, l1), l2) → APPEND(l1, l2)

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

lessElements(x0, x1)
lessE(x0, x1, x2)
if(true, x0, x1, x2, x3)
if(false, true, x0, x1, x2)
if(false, false, x0, x1, x2)
length(nil)
length(cons(x0, x1))
toList(leaf)
toList(node(x0, x1, x2))
append(nil, x0)
append(cons(x0, x1), x2)
le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))
a

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

(17) QReductionProof (EQUIVALENT transformation)

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

lessElements(x0, x1)
lessE(x0, x1, x2)
if(true, x0, x1, x2, x3)
if(false, true, x0, x1, x2)
if(false, false, x0, x1, x2)
length(nil)
length(cons(x0, x1))
toList(leaf)
toList(node(x0, x1, x2))
append(nil, x0)
append(cons(x0, x1), x2)
le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))
a

(18) Obligation:

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

APPEND(cons(n, l1), l2) → APPEND(l1, l2)

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:

• APPEND(cons(n, l1), l2) → APPEND(l1, l2)
  The graph contains the following edges 1 > 1, 2 >= 2

(20) TRUE

(21) Obligation:

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

TOLIST(node(t1, n, t2)) → TOLIST(t2)
TOLIST(node(t1, n, t2)) → TOLIST(t1)

The TRS R consists of the following rules:

lessElements(l, t) → lessE(l, t, 0)
lessE(l, t, n) → if(le(length(l), n), le(length(toList(t)), n), l, t, n)
if(true, b, l, t, n) → l
if(false, true, l, t, n) → t
if(false, false, l, t, n) → lessE(l, t, s(n))
length(nil) → 0
length(cons(n, l)) → s(length(l))
toList(leaf) → nil
toList(node(t1, n, t2)) → append(toList(t1), cons(n, toList(t2)))
append(nil, l2) → l2
append(cons(n, l1), l2) → cons(n, append(l1, l2))
le(s(n), 0) → false
le(0, m) → true
le(s(n), s(m)) → le(n, m)
a → c
a → d

The set Q consists of the following terms:

lessElements(x0, x1)
lessE(x0, x1, x2)
if(true, x0, x1, x2, x3)
if(false, true, x0, x1, x2)
if(false, false, x0, x1, x2)
length(nil)
length(cons(x0, x1))
toList(leaf)
toList(node(x0, x1, x2))
append(nil, x0)
append(cons(x0, x1), x2)
le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))
a

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

(22) UsableRulesProof (EQUIVALENT transformation)

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

(23) Obligation:

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

TOLIST(node(t1, n, t2)) → TOLIST(t2)
TOLIST(node(t1, n, t2)) → TOLIST(t1)

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

lessElements(x0, x1)
lessE(x0, x1, x2)
if(true, x0, x1, x2, x3)
if(false, true, x0, x1, x2)
if(false, false, x0, x1, x2)
length(nil)
length(cons(x0, x1))
toList(leaf)
toList(node(x0, x1, x2))
append(nil, x0)
append(cons(x0, x1), x2)
le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))
a

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

(24) QReductionProof (EQUIVALENT transformation)

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

lessElements(x0, x1)
lessE(x0, x1, x2)
if(true, x0, x1, x2, x3)
if(false, true, x0, x1, x2)
if(false, false, x0, x1, x2)
length(nil)
length(cons(x0, x1))
toList(leaf)
toList(node(x0, x1, x2))
append(nil, x0)
append(cons(x0, x1), x2)
le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))
a

(25) Obligation:

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

TOLIST(node(t1, n, t2)) → TOLIST(t2)
TOLIST(node(t1, n, t2)) → TOLIST(t1)

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

(26) QDPSizeChangeProof (EQUIVALENT transformation)

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

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

• TOLIST(node(t1, n, t2)) → TOLIST(t2)
  The graph contains the following edges 1 > 1

• TOLIST(node(t1, n, t2)) → TOLIST(t1)
  The graph contains the following edges 1 > 1

(27) TRUE

(28) Obligation:

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

LENGTH(cons(n, l)) → LENGTH(l)

The TRS R consists of the following rules:

lessElements(l, t) → lessE(l, t, 0)
lessE(l, t, n) → if(le(length(l), n), le(length(toList(t)), n), l, t, n)
if(true, b, l, t, n) → l
if(false, true, l, t, n) → t
if(false, false, l, t, n) → lessE(l, t, s(n))
length(nil) → 0
length(cons(n, l)) → s(length(l))
toList(leaf) → nil
toList(node(t1, n, t2)) → append(toList(t1), cons(n, toList(t2)))
append(nil, l2) → l2
append(cons(n, l1), l2) → cons(n, append(l1, l2))
le(s(n), 0) → false
le(0, m) → true
le(s(n), s(m)) → le(n, m)
a → c
a → d

The set Q consists of the following terms:

lessElements(x0, x1)
lessE(x0, x1, x2)
if(true, x0, x1, x2, x3)
if(false, true, x0, x1, x2)
if(false, false, x0, x1, x2)
length(nil)
length(cons(x0, x1))
toList(leaf)
toList(node(x0, x1, x2))
append(nil, x0)
append(cons(x0, x1), x2)
le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))
a

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

(29) UsableRulesProof (EQUIVALENT transformation)

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

(30) Obligation:

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

LENGTH(cons(n, l)) → LENGTH(l)

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

lessElements(x0, x1)
lessE(x0, x1, x2)
if(true, x0, x1, x2, x3)
if(false, true, x0, x1, x2)
if(false, false, x0, x1, x2)
length(nil)
length(cons(x0, x1))
toList(leaf)
toList(node(x0, x1, x2))
append(nil, x0)
append(cons(x0, x1), x2)
le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))
a

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

(31) QReductionProof (EQUIVALENT transformation)

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

lessElements(x0, x1)
lessE(x0, x1, x2)
if(true, x0, x1, x2, x3)
if(false, true, x0, x1, x2)
if(false, false, x0, x1, x2)
length(nil)
length(cons(x0, x1))
toList(leaf)
toList(node(x0, x1, x2))
append(nil, x0)
append(cons(x0, x1), x2)
le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))
a

(32) Obligation:

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

LENGTH(cons(n, l)) → LENGTH(l)

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

(33) 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(n, l)) → LENGTH(l)
  The graph contains the following edges 1 > 1

(34) TRUE

(35) Obligation:

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

IF(false, false, l, t, n) → LESSE(l, t, s(n))
LESSE(l, t, n) → IF(le(length(l), n), le(length(toList(t)), n), l, t, n)

The TRS R consists of the following rules:

lessElements(l, t) → lessE(l, t, 0)
lessE(l, t, n) → if(le(length(l), n), le(length(toList(t)), n), l, t, n)
if(true, b, l, t, n) → l
if(false, true, l, t, n) → t
if(false, false, l, t, n) → lessE(l, t, s(n))
length(nil) → 0
length(cons(n, l)) → s(length(l))
toList(leaf) → nil
toList(node(t1, n, t2)) → append(toList(t1), cons(n, toList(t2)))
append(nil, l2) → l2
append(cons(n, l1), l2) → cons(n, append(l1, l2))
le(s(n), 0) → false
le(0, m) → true
le(s(n), s(m)) → le(n, m)
a → c
a → d

The set Q consists of the following terms:

lessElements(x0, x1)
lessE(x0, x1, x2)
if(true, x0, x1, x2, x3)
if(false, true, x0, x1, x2)
if(false, false, x0, x1, x2)
length(nil)
length(cons(x0, x1))
toList(leaf)
toList(node(x0, x1, x2))
append(nil, x0)
append(cons(x0, x1), x2)
le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))
a

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:

IF(false, false, l, t, n) → LESSE(l, t, s(n))
LESSE(l, t, n) → IF(le(length(l), n), le(length(toList(t)), n), l, t, n)

The TRS R consists of the following rules:

length(nil) → 0
length(cons(n, l)) → s(length(l))
le(s(n), 0) → false
le(0, m) → true
le(s(n), s(m)) → le(n, m)
toList(leaf) → nil
toList(node(t1, n, t2)) → append(toList(t1), cons(n, toList(t2)))
append(nil, l2) → l2
append(cons(n, l1), l2) → cons(n, append(l1, l2))

The set Q consists of the following terms:

lessElements(x0, x1)
lessE(x0, x1, x2)
if(true, x0, x1, x2, x3)
if(false, true, x0, x1, x2)
if(false, false, x0, x1, x2)
length(nil)
length(cons(x0, x1))
toList(leaf)
toList(node(x0, x1, x2))
append(nil, x0)
append(cons(x0, x1), x2)
le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))
a

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

lessElements(x0, x1)
lessE(x0, x1, x2)
if(true, x0, x1, x2, x3)
if(false, true, x0, x1, x2)
if(false, false, x0, x1, x2)
a

(39) Obligation:

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

IF(false, false, l, t, n) → LESSE(l, t, s(n))
LESSE(l, t, n) → IF(le(length(l), n), le(length(toList(t)), n), l, t, n)

The TRS R consists of the following rules:

length(nil) → 0
length(cons(n, l)) → s(length(l))
le(s(n), 0) → false
le(0, m) → true
le(s(n), s(m)) → le(n, m)
toList(leaf) → nil
toList(node(t1, n, t2)) → append(toList(t1), cons(n, toList(t2)))
append(nil, l2) → l2
append(cons(n, l1), l2) → cons(n, append(l1, l2))

The set Q consists of the following terms:

length(nil)
length(cons(x0, x1))
toList(leaf)
toList(node(x0, x1, x2))
append(nil, x0)
append(cons(x0, x1), x2)
le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))

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

(40) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule LESSE(l, t, n) → IF(le(length(l), n), le(length(toList(t)), n), l, t, n) we obtained the following new rules [LPAR04]:

LESSE(z0, z1, s(z2)) → IF(le(length(z0), s(z2)), le(length(toList(z1)), s(z2)), z0, z1, s(z2))

(41) Obligation:

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

IF(false, false, l, t, n) → LESSE(l, t, s(n))
LESSE(z0, z1, s(z2)) → IF(le(length(z0), s(z2)), le(length(toList(z1)), s(z2)), z0, z1, s(z2))

The TRS R consists of the following rules:

length(nil) → 0
length(cons(n, l)) → s(length(l))
le(s(n), 0) → false
le(0, m) → true
le(s(n), s(m)) → le(n, m)
toList(leaf) → nil
toList(node(t1, n, t2)) → append(toList(t1), cons(n, toList(t2)))
append(nil, l2) → l2
append(cons(n, l1), l2) → cons(n, append(l1, l2))

The set Q consists of the following terms:

length(nil)
length(cons(x0, x1))
toList(leaf)
toList(node(x0, x1, x2))
append(nil, x0)
append(cons(x0, x1), x2)
le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))

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

(42) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule LESSE(l, t, n) → IF(le(length(l), n), le(length(toList(t)), n), l, t, n) at position [0] we obtained the following new rules [LPAR04]:

LESSE(nil, y1, y2) → IF(le(0, y2), le(length(toList(y1)), y2), nil, y1, y2)
LESSE(cons(x0, x1), y1, y2) → IF(le(s(length(x1)), y2), le(length(toList(y1)), y2), cons(x0, x1), y1, y2)

(43) Obligation:

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

IF(false, false, l, t, n) → LESSE(l, t, s(n))
LESSE(nil, y1, y2) → IF(le(0, y2), le(length(toList(y1)), y2), nil, y1, y2)
LESSE(cons(x0, x1), y1, y2) → IF(le(s(length(x1)), y2), le(length(toList(y1)), y2), cons(x0, x1), y1, y2)

The TRS R consists of the following rules:

length(nil) → 0
length(cons(n, l)) → s(length(l))
le(s(n), 0) → false
le(0, m) → true
le(s(n), s(m)) → le(n, m)
toList(leaf) → nil
toList(node(t1, n, t2)) → append(toList(t1), cons(n, toList(t2)))
append(nil, l2) → l2
append(cons(n, l1), l2) → cons(n, append(l1, l2))

The set Q consists of the following terms:

length(nil)
length(cons(x0, x1))
toList(leaf)
toList(node(x0, x1, x2))
append(nil, x0)
append(cons(x0, x1), x2)
le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))

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

(44) Rewriting (EQUIVALENT transformation)

By rewriting [LPAR04] the rule LESSE(nil, y1, y2) → IF(le(0, y2), le(length(toList(y1)), y2), nil, y1, y2) at position [0] we obtained the following new rules [LPAR04]:

LESSE(nil, y1, y2) → IF(true, le(length(toList(y1)), y2), nil, y1, y2)

(45) Obligation:

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

IF(false, false, l, t, n) → LESSE(l, t, s(n))
LESSE(cons(x0, x1), y1, y2) → IF(le(s(length(x1)), y2), le(length(toList(y1)), y2), cons(x0, x1), y1, y2)
LESSE(nil, y1, y2) → IF(true, le(length(toList(y1)), y2), nil, y1, y2)

The TRS R consists of the following rules:

length(nil) → 0
length(cons(n, l)) → s(length(l))
le(s(n), 0) → false
le(0, m) → true
le(s(n), s(m)) → le(n, m)
toList(leaf) → nil
toList(node(t1, n, t2)) → append(toList(t1), cons(n, toList(t2)))
append(nil, l2) → l2
append(cons(n, l1), l2) → cons(n, append(l1, l2))

The set Q consists of the following terms:

length(nil)
length(cons(x0, x1))
toList(leaf)
toList(node(x0, x1, x2))
append(nil, x0)
append(cons(x0, x1), x2)
le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))

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

(46) DependencyGraphProof (EQUIVALENT transformation)

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

(47) Obligation:

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

LESSE(cons(x0, x1), y1, y2) → IF(le(s(length(x1)), y2), le(length(toList(y1)), y2), cons(x0, x1), y1, y2)
IF(false, false, l, t, n) → LESSE(l, t, s(n))

The TRS R consists of the following rules:

length(nil) → 0
length(cons(n, l)) → s(length(l))
le(s(n), 0) → false
le(0, m) → true
le(s(n), s(m)) → le(n, m)
toList(leaf) → nil
toList(node(t1, n, t2)) → append(toList(t1), cons(n, toList(t2)))
append(nil, l2) → l2
append(cons(n, l1), l2) → cons(n, append(l1, l2))

The set Q consists of the following terms:

length(nil)
length(cons(x0, x1))
toList(leaf)
toList(node(x0, x1, x2))
append(nil, x0)
append(cons(x0, x1), x2)
le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))

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

(48) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule LESSE(cons(x0, x1), y1, y2) → IF(le(s(length(x1)), y2), le(length(toList(y1)), y2), cons(x0, x1), y1, y2) at position [1] we obtained the following new rules [LPAR04]:

LESSE(cons(y0, y1), leaf, y3) → IF(le(s(length(y1)), y3), le(length(nil), y3), cons(y0, y1), leaf, y3)
LESSE(cons(y0, y1), node(x0, x1, x2), y3) → IF(le(s(length(y1)), y3), le(length(append(toList(x0), cons(x1, toList(x2)))), y3), cons(y0, y1), node(x0, x1, x2), y3)

(49) Obligation:

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

IF(false, false, l, t, n) → LESSE(l, t, s(n))
LESSE(cons(y0, y1), leaf, y3) → IF(le(s(length(y1)), y3), le(length(nil), y3), cons(y0, y1), leaf, y3)
LESSE(cons(y0, y1), node(x0, x1, x2), y3) → IF(le(s(length(y1)), y3), le(length(append(toList(x0), cons(x1, toList(x2)))), y3), cons(y0, y1), node(x0, x1, x2), y3)

The TRS R consists of the following rules:

length(nil) → 0
length(cons(n, l)) → s(length(l))
le(s(n), 0) → false
le(0, m) → true
le(s(n), s(m)) → le(n, m)
toList(leaf) → nil
toList(node(t1, n, t2)) → append(toList(t1), cons(n, toList(t2)))
append(nil, l2) → l2
append(cons(n, l1), l2) → cons(n, append(l1, l2))

The set Q consists of the following terms:

length(nil)
length(cons(x0, x1))
toList(leaf)
toList(node(x0, x1, x2))
append(nil, x0)
append(cons(x0, x1), x2)
le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))

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

(50) Rewriting (EQUIVALENT transformation)

By rewriting [LPAR04] the rule LESSE(cons(y0, y1), leaf, y3) → IF(le(s(length(y1)), y3), le(length(nil), y3), cons(y0, y1), leaf, y3) at position [1,0] we obtained the following new rules [LPAR04]:

LESSE(cons(y0, y1), leaf, y3) → IF(le(s(length(y1)), y3), le(0, y3), cons(y0, y1), leaf, y3)

(51) Obligation:

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

IF(false, false, l, t, n) → LESSE(l, t, s(n))
LESSE(cons(y0, y1), node(x0, x1, x2), y3) → IF(le(s(length(y1)), y3), le(length(append(toList(x0), cons(x1, toList(x2)))), y3), cons(y0, y1), node(x0, x1, x2), y3)
LESSE(cons(y0, y1), leaf, y3) → IF(le(s(length(y1)), y3), le(0, y3), cons(y0, y1), leaf, y3)

The TRS R consists of the following rules:

length(nil) → 0
length(cons(n, l)) → s(length(l))
le(s(n), 0) → false
le(0, m) → true
le(s(n), s(m)) → le(n, m)
toList(leaf) → nil
toList(node(t1, n, t2)) → append(toList(t1), cons(n, toList(t2)))
append(nil, l2) → l2
append(cons(n, l1), l2) → cons(n, append(l1, l2))

The set Q consists of the following terms:

length(nil)
length(cons(x0, x1))
toList(leaf)
toList(node(x0, x1, x2))
append(nil, x0)
append(cons(x0, x1), x2)
le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))

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

(52) Rewriting (EQUIVALENT transformation)

By rewriting [LPAR04] the rule LESSE(cons(y0, y1), leaf, y3) → IF(le(s(length(y1)), y3), le(0, y3), cons(y0, y1), leaf, y3) at position [1] we obtained the following new rules [LPAR04]:

LESSE(cons(y0, y1), leaf, y3) → IF(le(s(length(y1)), y3), true, cons(y0, y1), leaf, y3)

(53) Obligation:

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

IF(false, false, l, t, n) → LESSE(l, t, s(n))
LESSE(cons(y0, y1), node(x0, x1, x2), y3) → IF(le(s(length(y1)), y3), le(length(append(toList(x0), cons(x1, toList(x2)))), y3), cons(y0, y1), node(x0, x1, x2), y3)
LESSE(cons(y0, y1), leaf, y3) → IF(le(s(length(y1)), y3), true, cons(y0, y1), leaf, y3)

The TRS R consists of the following rules:

length(nil) → 0
length(cons(n, l)) → s(length(l))
le(s(n), 0) → false
le(0, m) → true
le(s(n), s(m)) → le(n, m)
toList(leaf) → nil
toList(node(t1, n, t2)) → append(toList(t1), cons(n, toList(t2)))
append(nil, l2) → l2
append(cons(n, l1), l2) → cons(n, append(l1, l2))

The set Q consists of the following terms:

length(nil)
length(cons(x0, x1))
toList(leaf)
toList(node(x0, x1, x2))
append(nil, x0)
append(cons(x0, x1), x2)
le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))

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

(54) DependencyGraphProof (EQUIVALENT transformation)

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

(55) Obligation:

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

LESSE(cons(y0, y1), node(x0, x1, x2), y3) → IF(le(s(length(y1)), y3), le(length(append(toList(x0), cons(x1, toList(x2)))), y3), cons(y0, y1), node(x0, x1, x2), y3)
IF(false, false, l, t, n) → LESSE(l, t, s(n))

The TRS R consists of the following rules:

length(nil) → 0
length(cons(n, l)) → s(length(l))
le(s(n), 0) → false
le(0, m) → true
le(s(n), s(m)) → le(n, m)
toList(leaf) → nil
toList(node(t1, n, t2)) → append(toList(t1), cons(n, toList(t2)))
append(nil, l2) → l2
append(cons(n, l1), l2) → cons(n, append(l1, l2))

The set Q consists of the following terms:

length(nil)
length(cons(x0, x1))
toList(leaf)
toList(node(x0, x1, x2))
append(nil, x0)
append(cons(x0, x1), x2)
le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))

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

(56) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule LESSE(cons(y0, y1), node(x0, x1, x2), y3) → IF(le(s(length(y1)), y3), le(length(append(toList(x0), cons(x1, toList(x2)))), y3), cons(y0, y1), node(x0, x1, x2), y3) we obtained the following new rules [LPAR04]:

LESSE(cons(x0, x1), node(x2, x3, x4), s(z2)) → IF(le(s(length(x1)), s(z2)), le(length(append(toList(x2), cons(x3, toList(x4)))), s(z2)), cons(x0, x1), node(x2, x3, x4), s(z2))

(57) Obligation:

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

IF(false, false, l, t, n) → LESSE(l, t, s(n))
LESSE(cons(x0, x1), node(x2, x3, x4), s(z2)) → IF(le(s(length(x1)), s(z2)), le(length(append(toList(x2), cons(x3, toList(x4)))), s(z2)), cons(x0, x1), node(x2, x3, x4), s(z2))

The TRS R consists of the following rules:

length(nil) → 0
length(cons(n, l)) → s(length(l))
le(s(n), 0) → false
le(0, m) → true
le(s(n), s(m)) → le(n, m)
toList(leaf) → nil
toList(node(t1, n, t2)) → append(toList(t1), cons(n, toList(t2)))
append(nil, l2) → l2
append(cons(n, l1), l2) → cons(n, append(l1, l2))

The set Q consists of the following terms:

length(nil)
length(cons(x0, x1))
toList(leaf)
toList(node(x0, x1, x2))
append(nil, x0)
append(cons(x0, x1), x2)
le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))

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

(58) Rewriting (EQUIVALENT transformation)

By rewriting [LPAR04] the rule LESSE(cons(x0, x1), node(x2, x3, x4), s(z2)) → IF(le(s(length(x1)), s(z2)), le(length(append(toList(x2), cons(x3, toList(x4)))), s(z2)), cons(x0, x1), node(x2, x3, x4), s(z2)) at position [0] we obtained the following new rules [LPAR04]:

LESSE(cons(x0, x1), node(x2, x3, x4), s(z2)) → IF(le(length(x1), z2), le(length(append(toList(x2), cons(x3, toList(x4)))), s(z2)), cons(x0, x1), node(x2, x3, x4), s(z2))

(59) Obligation:

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

IF(false, false, l, t, n) → LESSE(l, t, s(n))
LESSE(cons(x0, x1), node(x2, x3, x4), s(z2)) → IF(le(length(x1), z2), le(length(append(toList(x2), cons(x3, toList(x4)))), s(z2)), cons(x0, x1), node(x2, x3, x4), s(z2))

The TRS R consists of the following rules:

length(nil) → 0
length(cons(n, l)) → s(length(l))
le(s(n), 0) → false
le(0, m) → true
le(s(n), s(m)) → le(n, m)
toList(leaf) → nil
toList(node(t1, n, t2)) → append(toList(t1), cons(n, toList(t2)))
append(nil, l2) → l2
append(cons(n, l1), l2) → cons(n, append(l1, l2))

The set Q consists of the following terms:

length(nil)
length(cons(x0, x1))
toList(leaf)
toList(node(x0, x1, x2))
append(nil, x0)
append(cons(x0, x1), x2)
le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))

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

(60) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule IF(false, false, l, t, n) → LESSE(l, t, s(n)) we obtained the following new rules [LPAR04]:

IF(false, false, cons(z0, z1), node(z2, z3, z4), s(z5)) → LESSE(cons(z0, z1), node(z2, z3, z4), s(s(z5)))

(61) Obligation:

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

LESSE(cons(x0, x1), node(x2, x3, x4), s(z2)) → IF(le(length(x1), z2), le(length(append(toList(x2), cons(x3, toList(x4)))), s(z2)), cons(x0, x1), node(x2, x3, x4), s(z2))
IF(false, false, cons(z0, z1), node(z2, z3, z4), s(z5)) → LESSE(cons(z0, z1), node(z2, z3, z4), s(s(z5)))

The TRS R consists of the following rules:

length(nil) → 0
length(cons(n, l)) → s(length(l))
le(s(n), 0) → false
le(0, m) → true
le(s(n), s(m)) → le(n, m)
toList(leaf) → nil
toList(node(t1, n, t2)) → append(toList(t1), cons(n, toList(t2)))
append(nil, l2) → l2
append(cons(n, l1), l2) → cons(n, append(l1, l2))

The set Q consists of the following terms:

length(nil)
length(cons(x0, x1))
toList(leaf)
toList(node(x0, x1, x2))
append(nil, x0)
append(cons(x0, x1), x2)
le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))

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

(62) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule LESSE(cons(x0, x1), node(x2, x3, x4), s(z2)) → IF(le(length(x1), z2), le(length(append(toList(x2), cons(x3, toList(x4)))), s(z2)), cons(x0, x1), node(x2, x3, x4), s(z2)) we obtained the following new rules [LPAR04]:

LESSE(cons(z0, z1), node(z2, z3, z4), s(s(z5))) → IF(le(length(z1), s(z5)), le(length(append(toList(z2), cons(z3, toList(z4)))), s(s(z5))), cons(z0, z1), node(z2, z3, z4), s(s(z5)))

(63) Obligation:

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

IF(false, false, cons(z0, z1), node(z2, z3, z4), s(z5)) → LESSE(cons(z0, z1), node(z2, z3, z4), s(s(z5)))
LESSE(cons(z0, z1), node(z2, z3, z4), s(s(z5))) → IF(le(length(z1), s(z5)), le(length(append(toList(z2), cons(z3, toList(z4)))), s(s(z5))), cons(z0, z1), node(z2, z3, z4), s(s(z5)))

The TRS R consists of the following rules:

length(nil) → 0
length(cons(n, l)) → s(length(l))
le(s(n), 0) → false
le(0, m) → true
le(s(n), s(m)) → le(n, m)
toList(leaf) → nil
toList(node(t1, n, t2)) → append(toList(t1), cons(n, toList(t2)))
append(nil, l2) → l2
append(cons(n, l1), l2) → cons(n, append(l1, l2))

The set Q consists of the following terms:

length(nil)
length(cons(x0, x1))
toList(leaf)
toList(node(x0, x1, x2))
append(nil, x0)
append(cons(x0, x1), x2)
le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))

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

(64) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule IF(false, false, cons(z0, z1), node(z2, z3, z4), s(z5)) → LESSE(cons(z0, z1), node(z2, z3, z4), s(s(z5))) we obtained the following new rules [LPAR04]:

IF(false, false, cons(z0, z1), node(z2, z3, z4), s(s(z5))) → LESSE(cons(z0, z1), node(z2, z3, z4), s(s(s(z5))))

(65) Obligation:

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

LESSE(cons(z0, z1), node(z2, z3, z4), s(s(z5))) → IF(le(length(z1), s(z5)), le(length(append(toList(z2), cons(z3, toList(z4)))), s(s(z5))), cons(z0, z1), node(z2, z3, z4), s(s(z5)))
IF(false, false, cons(z0, z1), node(z2, z3, z4), s(s(z5))) → LESSE(cons(z0, z1), node(z2, z3, z4), s(s(s(z5))))

The TRS R consists of the following rules:

length(nil) → 0
length(cons(n, l)) → s(length(l))
le(s(n), 0) → false
le(0, m) → true
le(s(n), s(m)) → le(n, m)
toList(leaf) → nil
toList(node(t1, n, t2)) → append(toList(t1), cons(n, toList(t2)))
append(nil, l2) → l2
append(cons(n, l1), l2) → cons(n, append(l1, l2))

The set Q consists of the following terms:

length(nil)
length(cons(x0, x1))
toList(leaf)
toList(node(x0, x1, x2))
append(nil, x0)
append(cons(x0, x1), x2)
le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))

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

(66) 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 LESSE(cons(z0, z1), node(z2, z3, z4), s(s(z5))) → IF(le(length(z1), s(z5)), le(length(append(toList(z2), cons(z3, toList(z4)))), s(s(z5))), cons(z0, z1), node(z2, z3, z4), s(s(z5))) the following chains were created:

• We consider the chain IF(false, false, cons(z0, z1), node(z2, z3, z4), s(s(z5))) → LESSE(cons(z0, z1), node(z2, z3, z4), s(s(s(z5)))), LESSE(cons(z0, z1), node(z2, z3, z4), s(s(z5))) → IF(le(length(z1), s(z5)), le(length(append(toList(z2), cons(z3, toList(z4)))), s(s(z5))), cons(z0, z1), node(z2, z3, z4), s(s(z5))) which results in the following constraint:
  

  (1)    (LESSE(cons(x6, x7), node(x8, x9, x10), s(s(s(x11))))=LESSE(cons(x12, x13), node(x14, x15, x16), s(s(x17))) ⇒ LESSE(cons(x12, x13), node(x14, x15, x16), s(s(x17)))≥IF(le(length(x13), s(x17)), le(length(append(toList(x14), cons(x15, toList(x16)))), s(s(x17))), cons(x12, x13), node(x14, x15, x16), s(s(x17))))

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

  (2)    (LESSE(cons(x6, x7), node(x8, x9, x10), s(s(s(x11))))≥IF(le(length(x7), s(s(x11))), le(length(append(toList(x8), cons(x9, toList(x10)))), s(s(s(x11)))), cons(x6, x7), node(x8, x9, x10), s(s(s(x11)))))

  
  
  

For Pair IF(false, false, cons(z0, z1), node(z2, z3, z4), s(s(z5))) → LESSE(cons(z0, z1), node(z2, z3, z4), s(s(s(z5)))) the following chains were created:

• We consider the chain LESSE(cons(z0, z1), node(z2, z3, z4), s(s(z5))) → IF(le(length(z1), s(z5)), le(length(append(toList(z2), cons(z3, toList(z4)))), s(s(z5))), cons(z0, z1), node(z2, z3, z4), s(s(z5))), IF(false, false, cons(z0, z1), node(z2, z3, z4), s(s(z5))) → LESSE(cons(z0, z1), node(z2, z3, z4), s(s(s(z5)))) which results in the following constraint:
  

  (3)    (IF(le(length(x19), s(x23)), le(length(append(toList(x20), cons(x21, toList(x22)))), s(s(x23))), cons(x18, x19), node(x20, x21, x22), s(s(x23)))=IF(false, false, cons(x24, x25), node(x26, x27, x28), s(s(x29))) ⇒ IF(false, false, cons(x24, x25), node(x26, x27, x28), s(s(x29)))≥LESSE(cons(x24, x25), node(x26, x27, x28), s(s(s(x29)))))

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

  (4)    (length(x19)=x36∧s(x23)=x37∧le(x36, x37)=false∧length(x40)=x38∧s(s(x23))=x39∧le(x38, x39)=false ⇒ IF(false, false, cons(x18, x19), node(x20, x21, x22), s(s(x23)))≥LESSE(cons(x18, x19), node(x20, x21, x22), s(s(s(x23)))))

  
  
  We simplified constraint (4) using rule (V) (with possible (I) afterwards) using induction on le(x36, x37)=false which results in the following new constraints:
  

  (5)    (false=false∧length(x19)=s(x43)∧s(x23)=0∧length(x40)=x38∧s(s(x23))=x39∧le(x38, x39)=false ⇒ IF(false, false, cons(x18, x19), node(x20, x21, x22), s(s(x23)))≥LESSE(cons(x18, x19), node(x20, x21, x22), s(s(s(x23)))))

  
  

  (6)    (le(x46, x45)=false∧length(x19)=s(x46)∧s(x23)=s(x45)∧length(x40)=x38∧s(s(x23))=x39∧le(x38, x39)=false∧(∀x47,x48,x49,x50,x51,x52,x53,x54,x55:le(x46, x45)=false∧length(x47)=x46∧s(x48)=x45∧length(x49)=x50∧s(s(x48))=x51∧le(x50, x51)=false ⇒ IF(false, false, cons(x52, x47), node(x53, x54, x55), s(s(x48)))≥LESSE(cons(x52, x47), node(x53, x54, x55), s(s(s(x48))))) ⇒ IF(false, false, cons(x18, x19), node(x20, x21, x22), s(s(x23)))≥LESSE(cons(x18, x19), node(x20, x21, x22), s(s(s(x23)))))

  
  
  We solved constraint (5) using rules (I), (II).We simplified constraint (6) using rules (I), (II), (III) which results in the following new constraint:
  

  (7)    (le(x46, x45)=false∧length(x19)=s(x46)∧length(x40)=x38∧s(s(x45))=x39∧le(x38, x39)=false∧(∀x47,x48,x49,x50,x51,x52,x53,x54,x55:le(x46, x45)=false∧length(x47)=x46∧s(x48)=x45∧length(x49)=x50∧s(s(x48))=x51∧le(x50, x51)=false ⇒ IF(false, false, cons(x52, x47), node(x53, x54, x55), s(s(x48)))≥LESSE(cons(x52, x47), node(x53, x54, x55), s(s(s(x48))))) ⇒ IF(false, false, cons(x18, x19), node(x20, x21, x22), s(s(x45)))≥LESSE(cons(x18, x19), node(x20, x21, x22), s(s(s(x45)))))

  
  
  We simplified constraint (7) using rule (V) (with possible (I) afterwards) using induction on le(x38, x39)=false which results in the following new constraints:
  

  (8)    (false=false∧le(x46, x45)=false∧length(x19)=s(x46)∧length(x40)=s(x56)∧s(s(x45))=0∧(∀x47,x48,x49,x50,x51,x52,x53,x54,x55:le(x46, x45)=false∧length(x47)=x46∧s(x48)=x45∧length(x49)=x50∧s(s(x48))=x51∧le(x50, x51)=false ⇒ IF(false, false, cons(x52, x47), node(x53, x54, x55), s(s(x48)))≥LESSE(cons(x52, x47), node(x53, x54, x55), s(s(s(x48))))) ⇒ IF(false, false, cons(x18, x19), node(x20, x21, x22), s(s(x45)))≥LESSE(cons(x18, x19), node(x20, x21, x22), s(s(s(x45)))))

  
  

  (9)    (le(x59, x58)=false∧le(x46, x45)=false∧length(x19)=s(x46)∧length(x40)=s(x59)∧s(s(x45))=s(x58)∧(∀x47,x48,x49,x50,x51,x52,x53,x54,x55:le(x46, x45)=false∧length(x47)=x46∧s(x48)=x45∧length(x49)=x50∧s(s(x48))=x51∧le(x50, x51)=false ⇒ IF(false, false, cons(x52, x47), node(x53, x54, x55), s(s(x48)))≥LESSE(cons(x52, x47), node(x53, x54, x55), s(s(s(x48)))))∧(∀x60,x61,x62,x63,x64,x65,x66,x67,x68,x69,x70,x71,x72,x73,x74,x75,x76:le(x59, x58)=false∧le(x60, x61)=false∧length(x62)=s(x60)∧length(x63)=x59∧s(s(x61))=x58∧(∀x64,x65,x66,x67,x68,x69,x70,x71,x72:le(x60, x61)=false∧length(x64)=x60∧s(x65)=x61∧length(x66)=x67∧s(s(x65))=x68∧le(x67, x68)=false ⇒ IF(false, false, cons(x69, x64), node(x70, x71, x72), s(s(x65)))≥LESSE(cons(x69, x64), node(x70, x71, x72), s(s(s(x65))))) ⇒ IF(false, false, cons(x73, x62), node(x74, x75, x76), s(s(x61)))≥LESSE(cons(x73, x62), node(x74, x75, x76), s(s(s(x61))))) ⇒ IF(false, false, cons(x18, x19), node(x20, x21, x22), s(s(x45)))≥LESSE(cons(x18, x19), node(x20, x21, x22), s(s(s(x45)))))

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

  (10)    (le(x59, x58)=false∧le(x46, x45)=false∧length(x19)=s(x46)∧length(x40)=s(x59)∧s(x45)=x58∧(∀x47,x48,x49,x50,x51,x52,x53,x54,x55:le(x46, x45)=false∧length(x47)=x46∧s(x48)=x45∧length(x49)=x50∧s(s(x48))=x51∧le(x50, x51)=false ⇒ IF(false, false, cons(x52, x47), node(x53, x54, x55), s(s(x48)))≥LESSE(cons(x52, x47), node(x53, x54, x55), s(s(s(x48)))))∧(∀x60,x61,x62,x63,x64,x65,x66,x67,x68,x69,x70,x71,x72,x73,x74,x75,x76:le(x59, x58)=false∧le(x60, x61)=false∧length(x62)=s(x60)∧length(x63)=x59∧s(s(x61))=x58∧(∀x64,x65,x66,x67,x68,x69,x70,x71,x72:le(x60, x61)=false∧length(x64)=x60∧s(x65)=x61∧length(x66)=x67∧s(s(x65))=x68∧le(x67, x68)=false ⇒ IF(false, false, cons(x69, x64), node(x70, x71, x72), s(s(x65)))≥LESSE(cons(x69, x64), node(x70, x71, x72), s(s(s(x65))))) ⇒ IF(false, false, cons(x73, x62), node(x74, x75, x76), s(s(x61)))≥LESSE(cons(x73, x62), node(x74, x75, x76), s(s(s(x61))))) ⇒ IF(false, false, cons(x18, x19), node(x20, x21, x22), s(s(x45)))≥LESSE(cons(x18, x19), node(x20, x21, x22), s(s(s(x45)))))

  
  
  We simplified constraint (10) using rule (V) (with possible (I) afterwards) using induction on length(x19)=s(x46) which results in the following new constraint:
  

  (11)    (s(length(x77))=s(x46)∧le(x59, x58)=false∧le(x46, x45)=false∧length(x40)=s(x59)∧s(x45)=x58∧(∀x47,x48,x49,x50,x51,x52,x53,x54,x55:le(x46, x45)=false∧length(x47)=x46∧s(x48)=x45∧length(x49)=x50∧s(s(x48))=x51∧le(x50, x51)=false ⇒ IF(false, false, cons(x52, x47), node(x53, x54, x55), s(s(x48)))≥LESSE(cons(x52, x47), node(x53, x54, x55), s(s(s(x48)))))∧(∀x60,x61,x62,x63,x64,x65,x66,x67,x68,x69,x70,x71,x72,x73,x74,x75,x76:le(x59, x58)=false∧le(x60, x61)=false∧length(x62)=s(x60)∧length(x63)=x59∧s(s(x61))=x58∧(∀x64,x65,x66,x67,x68,x69,x70,x71,x72:le(x60, x61)=false∧length(x64)=x60∧s(x65)=x61∧length(x66)=x67∧s(s(x65))=x68∧le(x67, x68)=false ⇒ IF(false, false, cons(x69, x64), node(x70, x71, x72), s(s(x65)))≥LESSE(cons(x69, x64), node(x70, x71, x72), s(s(s(x65))))) ⇒ IF(false, false, cons(x73, x62), node(x74, x75, x76), s(s(x61)))≥LESSE(cons(x73, x62), node(x74, x75, x76), s(s(s(x61)))))∧(∀x79,x80,x81,x82,x83,x84,x85,x86,x87,x88,x89,x90,x91,x92,x93,x94,x95,x96,x97,x98,x99,x100,x101,x102,x103,x104,x105,x106,x107,x108,x109,x110,x111,x112,x113:length(x77)=s(x79)∧le(x80, x81)=false∧le(x79, x82)=false∧length(x83)=s(x80)∧s(x82)=x81∧(∀x84,x85,x86,x87,x88,x89,x90,x91,x92:le(x79, x82)=false∧length(x84)=x79∧s(x85)=x82∧length(x86)=x87∧s(s(x85))=x88∧le(x87, x88)=false ⇒ IF(false, false, cons(x89, x84), node(x90, x91, x92), s(s(x85)))≥LESSE(cons(x89, x84), node(x90, x91, x92), s(s(s(x85)))))∧(∀x93,x94,x95,x96,x97,x98,x99,x100,x101,x102,x103,x104,x105,x106,x107,x108,x109:le(x80, x81)=false∧le(x93, x94)=false∧length(x95)=s(x93)∧length(x96)=x80∧s(s(x94))=x81∧(∀x97,x98,x99,x100,x101,x102,x103,x104,x105:le(x93, x94)=false∧length(x97)=x93∧s(x98)=x94∧length(x99)=x100∧s(s(x98))=x101∧le(x100, x101)=false ⇒ IF(false, false, cons(x102, x97), node(x103, x104, x105), s(s(x98)))≥LESSE(cons(x102, x97), node(x103, x104, x105), s(s(s(x98))))) ⇒ IF(false, false, cons(x106, x95), node(x107, x108, x109), s(s(x94)))≥LESSE(cons(x106, x95), node(x107, x108, x109), s(s(s(x94))))) ⇒ IF(false, false, cons(x110, x77), node(x111, x112, x113), s(s(x82)))≥LESSE(cons(x110, x77), node(x111, x112, x113), s(s(s(x82))))) ⇒ IF(false, false, cons(x18, cons(x78, x77)), node(x20, x21, x22), s(s(x45)))≥LESSE(cons(x18, cons(x78, x77)), node(x20, x21, x22), s(s(s(x45)))))

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

  (12)    (length(x77)=x46∧le(x59, x58)=false∧le(x46, x45)=false∧length(x40)=s(x59)∧s(x45)=x58∧(∀x47,x48,x49,x50,x51,x52,x53,x54,x55:le(x46, x45)=false∧length(x47)=x46∧s(x48)=x45∧length(x49)=x50∧s(s(x48))=x51∧le(x50, x51)=false ⇒ IF(false, false, cons(x52, x47), node(x53, x54, x55), s(s(x48)))≥LESSE(cons(x52, x47), node(x53, x54, x55), s(s(s(x48)))))∧(∀x60,x61,x62,x63,x64,x65,x66,x67,x68,x69,x70,x71,x72,x73,x74,x75,x76:le(x59, x58)=false∧le(x60, x61)=false∧length(x62)=s(x60)∧length(x63)=x59∧s(s(x61))=x58∧(∀x64,x65,x66,x67,x68,x69,x70,x71,x72:le(x60, x61)=false∧length(x64)=x60∧s(x65)=x61∧length(x66)=x67∧s(s(x65))=x68∧le(x67, x68)=false ⇒ IF(false, false, cons(x69, x64), node(x70, x71, x72), s(s(x65)))≥LESSE(cons(x69, x64), node(x70, x71, x72), s(s(s(x65))))) ⇒ IF(false, false, cons(x73, x62), node(x74, x75, x76), s(s(x61)))≥LESSE(cons(x73, x62), node(x74, x75, x76), s(s(s(x61)))))∧(∀x79,x80,x81,x82,x83,x84,x85,x86,x87,x88,x89,x90,x91,x92,x93,x94,x95,x96,x97,x98,x99,x100,x101,x102,x103,x104,x105,x106,x107,x108,x109,x110,x111,x112,x113:length(x77)=s(x79)∧le(x80, x81)=false∧le(x79, x82)=false∧length(x83)=s(x80)∧s(x82)=x81∧(∀x84,x85,x86,x87,x88,x89,x90,x91,x92:le(x79, x82)=false∧length(x84)=x79∧s(x85)=x82∧length(x86)=x87∧s(s(x85))=x88∧le(x87, x88)=false ⇒ IF(false, false, cons(x89, x84), node(x90, x91, x92), s(s(x85)))≥LESSE(cons(x89, x84), node(x90, x91, x92), s(s(s(x85)))))∧(∀x93,x94,x95,x96,x97,x98,x99,x100,x101,x102,x103,x104,x105,x106,x107,x108,x109:le(x80, x81)=false∧le(x93, x94)=false∧length(x95)=s(x93)∧length(x96)=x80∧s(s(x94))=x81∧(∀x97,x98,x99,x100,x101,x102,x103,x104,x105:le(x93, x94)=false∧length(x97)=x93∧s(x98)=x94∧length(x99)=x100∧s(s(x98))=x101∧le(x100, x101)=false ⇒ IF(false, false, cons(x102, x97), node(x103, x104, x105), s(s(x98)))≥LESSE(cons(x102, x97), node(x103, x104, x105), s(s(s(x98))))) ⇒ IF(false, false, cons(x106, x95), node(x107, x108, x109), s(s(x94)))≥LESSE(cons(x106, x95), node(x107, x108, x109), s(s(s(x94))))) ⇒ IF(false, false, cons(x110, x77), node(x111, x112, x113), s(s(x82)))≥LESSE(cons(x110, x77), node(x111, x112, x113), s(s(s(x82))))) ⇒ IF(false, false, cons(x18, cons(x78, x77)), node(x20, x21, x22), s(s(x45)))≥LESSE(cons(x18, cons(x78, x77)), node(x20, x21, x22), s(s(s(x45)))))

  
  
  We simplified constraint (12) using rule (V) (with possible (I) afterwards) using induction on length(x40)=s(x59) which results in the following new constraint:
  

  (13)    (s(length(x114))=s(x59)∧length(x77)=x46∧le(x59, x58)=false∧le(x46, x45)=false∧s(x45)=x58∧(∀x47,x48,x49,x50,x51,x52,x53,x54,x55:le(x46, x45)=false∧length(x47)=x46∧s(x48)=x45∧length(x49)=x50∧s(s(x48))=x51∧le(x50, x51)=false ⇒ IF(false, false, cons(x52, x47), node(x53, x54, x55), s(s(x48)))≥LESSE(cons(x52, x47), node(x53, x54, x55), s(s(s(x48)))))∧(∀x60,x61,x62,x63,x64,x65,x66,x67,x68,x69,x70,x71,x72,x73,x74,x75,x76:le(x59, x58)=false∧le(x60, x61)=false∧length(x62)=s(x60)∧length(x63)=x59∧s(s(x61))=x58∧(∀x64,x65,x66,x67,x68,x69,x70,x71,x72:le(x60, x61)=false∧length(x64)=x60∧s(x65)=x61∧length(x66)=x67∧s(s(x65))=x68∧le(x67, x68)=false ⇒ IF(false, false, cons(x69, x64), node(x70, x71, x72), s(s(x65)))≥LESSE(cons(x69, x64), node(x70, x71, x72), s(s(s(x65))))) ⇒ IF(false, false, cons(x73, x62), node(x74, x75, x76), s(s(x61)))≥LESSE(cons(x73, x62), node(x74, x75, x76), s(s(s(x61)))))∧(∀x79,x80,x81,x82,x83,x84,x85,x86,x87,x88,x89,x90,x91,x92,x93,x94,x95,x96,x97,x98,x99,x100,x101,x102,x103,x104,x105,x106,x107,x108,x109,x110,x111,x112,x113:length(x77)=s(x79)∧le(x80, x81)=false∧le(x79, x82)=false∧length(x83)=s(x80)∧s(x82)=x81∧(∀x84,x85,x86,x87,x88,x89,x90,x91,x92:le(x79, x82)=false∧length(x84)=x79∧s(x85)=x82∧length(x86)=x87∧s(s(x85))=x88∧le(x87, x88)=false ⇒ IF(false, false, cons(x89, x84), node(x90, x91, x92), s(s(x85)))≥LESSE(cons(x89, x84), node(x90, x91, x92), s(s(s(x85)))))∧(∀x93,x94,x95,x96,x97,x98,x99,x100,x101,x102,x103,x104,x105,x106,x107,x108,x109:le(x80, x81)=false∧le(x93, x94)=false∧length(x95)=s(x93)∧length(x96)=x80∧s(s(x94))=x81∧(∀x97,x98,x99,x100,x101,x102,x103,x104,x105:le(x93, x94)=false∧length(x97)=x93∧s(x98)=x94∧length(x99)=x100∧s(s(x98))=x101∧le(x100, x101)=false ⇒ IF(false, false, cons(x102, x97), node(x103, x104, x105), s(s(x98)))≥LESSE(cons(x102, x97), node(x103, x104, x105), s(s(s(x98))))) ⇒ IF(false, false, cons(x106, x95), node(x107, x108, x109), s(s(x94)))≥LESSE(cons(x106, x95), node(x107, x108, x109), s(s(s(x94))))) ⇒ IF(false, false, cons(x110, x77), node(x111, x112, x113), s(s(x82)))≥LESSE(cons(x110, x77), node(x111, x112, x113), s(s(s(x82)))))∧(∀x116,x117,x118,x119,x120,x121,x122,x123,x124,x125,x126,x127,x128,x129,x130,x131,x132,x133,x134,x135,x136,x137,x138,x139,x140,x141,x142,x143,x144,x145,x146,x147,x148,x149,x150,x151,x152,x153,x154,x155,x156,x157,x158,x159,x160,x161,x162,x163,x164,x165,x166,x167,x168,x169,x170,x171,x172,x173,x174,x175,x176,x177,x178,x179,x180,x181,x182,x183,x184,x185,x186:length(x114)=s(x116)∧length(x117)=x118∧le(x116, x119)=false∧le(x118, x120)=false∧s(x120)=x119∧(∀x121,x122,x123,x124,x125,x126,x127,x128,x129:le(x118, x120)=false∧length(x121)=x118∧s(x122)=x120∧length(x123)=x124∧s(s(x122))=x125∧le(x124, x125)=false ⇒ IF(false, false, cons(x126, x121), node(x127, x128, x129), s(s(x122)))≥LESSE(cons(x126, x121), node(x127, x128, x129), s(s(s(x122)))))∧(∀x130,x131,x132,x133,x134,x135,x136,x137,x138,x139,x140,x141,x142,x143,x144,x145,x146:le(x116, x119)=false∧le(x130, x131)=false∧length(x132)=s(x130)∧length(x133)=x116∧s(s(x131))=x119∧(∀x134,x135,x136,x137,x138,x139,x140,x141,x142:le(x130, x131)=false∧length(x134)=x130∧s(x135)=x131∧length(x136)=x137∧s(s(x135))=x138∧le(x137, x138)=false ⇒ IF(false, false, cons(x139, x134), node(x140, x141, x142), s(s(x135)))≥LESSE(cons(x139, x134), node(x140, x141, x142), s(s(s(x135))))) ⇒ IF(false, false, cons(x143, x132), node(x144, x145, x146), s(s(x131)))≥LESSE(cons(x143, x132), node(x144, x145, x146), s(s(s(x131)))))∧(∀x147,x148,x149,x150,x151,x152,x153,x154,x155,x156,x157,x158,x159,x160,x161,x162,x163,x164,x165,x166,x167,x168,x169,x170,x171,x172,x173,x174,x175,x176,x177,x178,x179,x180,x181:length(x117)=s(x147)∧le(x148, x149)=false∧le(x147, x150)=false∧length(x151)=s(x148)∧s(x150)=x149∧(∀x152,x153,x154,x155,x156,x157,x158,x159,x160:le(x147, x150)=false∧length(x152)=x147∧s(x153)=x150∧length(x154)=x155∧s(s(x153))=x156∧le(x155, x156)=false ⇒ IF(false, false, cons(x157, x152), node(x158, x159, x160), s(s(x153)))≥LESSE(cons(x157, x152), node(x158, x159, x160), s(s(s(x153)))))∧(∀x161,x162,x163,x164,x165,x166,x167,x168,x169,x170,x171,x172,x173,x174,x175,x176,x177:le(x148, x149)=false∧le(x161, x162)=false∧length(x163)=s(x161)∧length(x164)=x148∧s(s(x162))=x149∧(∀x165,x166,x167,x168,x169,x170,x171,x172,x173:le(x161, x162)=false∧length(x165)=x161∧s(x166)=x162∧length(x167)=x168∧s(s(x166))=x169∧le(x168, x169)=false ⇒ IF(false, false, cons(x170, x165), node(x171, x172, x173), s(s(x166)))≥LESSE(cons(x170, x165), node(x171, x172, x173), s(s(s(x166))))) ⇒ IF(false, false, cons(x174, x163), node(x175, x176, x177), s(s(x162)))≥LESSE(cons(x174, x163), node(x175, x176, x177), s(s(s(x162))))) ⇒ IF(false, false, cons(x178, x117), node(x179, x180, x181), s(s(x150)))≥LESSE(cons(x178, x117), node(x179, x180, x181), s(s(s(x150))))) ⇒ IF(false, false, cons(x182, cons(x183, x117)), node(x184, x185, x186), s(s(x120)))≥LESSE(cons(x182, cons(x183, x117)), node(x184, x185, x186), s(s(s(x120))))) ⇒ IF(false, false, cons(x18, cons(x78, x77)), node(x20, x21, x22), s(s(x45)))≥LESSE(cons(x18, cons(x78, x77)), node(x20, x21, x22), s(s(s(x45)))))

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

  (14)    (length(x114)=x59∧length(x77)=x46∧le(x59, x58)=false∧le(x46, x45)=false∧s(x45)=x58∧(∀x47,x48,x49,x50,x51,x52,x53,x54,x55:le(x46, x45)=false∧length(x47)=x46∧s(x48)=x45∧length(x49)=x50∧s(s(x48))=x51∧le(x50, x51)=false ⇒ IF(false, false, cons(x52, x47), node(x53, x54, x55), s(s(x48)))≥LESSE(cons(x52, x47), node(x53, x54, x55), s(s(s(x48)))))∧(∀x79,x80,x81,x82,x83,x84,x85,x86,x87,x88,x89,x90,x91,x92,x110,x111,x112,x113:length(x77)=s(x79)∧le(x80, x81)=false∧le(x79, x82)=false∧length(x83)=s(x80)∧s(x82)=x81∧(∀x84,x85,x86,x87,x88,x89,x90,x91,x92:le(x79, x82)=false∧length(x84)=x79∧s(x85)=x82∧length(x86)=x87∧s(s(x85))=x88∧le(x87, x88)=false ⇒ IF(false, false, cons(x89, x84), node(x90, x91, x92), s(s(x85)))≥LESSE(cons(x89, x84), node(x90, x91, x92), s(s(s(x85))))) ⇒ IF(false, false, cons(x110, x77), node(x111, x112, x113), s(s(x82)))≥LESSE(cons(x110, x77), node(x111, x112, x113), s(s(s(x82)))))∧(∀x116,x117,x118,x119,x120,x121,x122,x123,x124,x125,x126,x127,x128,x129,x147,x148,x149,x150,x151,x152,x153,x154,x155,x156,x157,x158,x159,x160,x178,x179,x180,x181,x182,x183,x184,x185,x186:length(x114)=s(x116)∧length(x117)=x118∧le(x116, x119)=false∧le(x118, x120)=false∧s(x120)=x119∧(∀x121,x122,x123,x124,x125,x126,x127,x128,x129:le(x118, x120)=false∧length(x121)=x118∧s(x122)=x120∧length(x123)=x124∧s(s(x122))=x125∧le(x124, x125)=false ⇒ IF(false, false, cons(x126, x121), node(x127, x128, x129), s(s(x122)))≥LESSE(cons(x126, x121), node(x127, x128, x129), s(s(s(x122)))))∧(∀x147,x148,x149,x150,x151,x152,x153,x154,x155,x156,x157,x158,x159,x160,x178,x179,x180,x181:length(x117)=s(x147)∧le(x148, x149)=false∧le(x147, x150)=false∧length(x151)=s(x148)∧s(x150)=x149∧(∀x152,x153,x154,x155,x156,x157,x158,x159,x160:le(x147, x150)=false∧length(x152)=x147∧s(x153)=x150∧length(x154)=x155∧s(s(x153))=x156∧le(x155, x156)=false ⇒ IF(false, false, cons(x157, x152), node(x158, x159, x160), s(s(x153)))≥LESSE(cons(x157, x152), node(x158, x159, x160), s(s(s(x153))))) ⇒ IF(false, false, cons(x178, x117), node(x179, x180, x181), s(s(x150)))≥LESSE(cons(x178, x117), node(x179, x180, x181), s(s(s(x150))))) ⇒ IF(false, false, cons(x182, cons(x183, x117)), node(x184, x185, x186), s(s(x120)))≥LESSE(cons(x182, cons(x183, x117)), node(x184, x185, x186), s(s(s(x120))))) ⇒ IF(false, false, cons(x18, cons(x78, x77)), node(x20, x21, x22), s(s(x45)))≥LESSE(cons(x18, cons(x78, x77)), node(x20, x21, x22), s(s(s(x45)))))

  
  
  We simplified constraint (14) using rule (V) (with possible (I) afterwards) using induction on le(x59, x58)=false which results in the following new constraints:
  

  (15)    (false=false∧length(x114)=s(x187)∧length(x77)=x46∧le(x46, x45)=false∧s(x45)=0∧(∀x47,x48,x49,x50,x51,x52,x53,x54,x55:le(x46, x45)=false∧length(x47)=x46∧s(x48)=x45∧length(x49)=x50∧s(s(x48))=x51∧le(x50, x51)=false ⇒ IF(false, false, cons(x52, x47), node(x53, x54, x55), s(s(x48)))≥LESSE(cons(x52, x47), node(x53, x54, x55), s(s(s(x48)))))∧(∀x79,x80,x81,x82,x83,x84,x85,x86,x87,x88,x89,x90,x91,x92,x110,x111,x112,x113:length(x77)=s(x79)∧le(x80, x81)=false∧le(x79, x82)=false∧length(x83)=s(x80)∧s(x82)=x81∧(∀x84,x85,x86,x87,x88,x89,x90,x91,x92:le(x79, x82)=false∧length(x84)=x79∧s(x85)=x82∧length(x86)=x87∧s(s(x85))=x88∧le(x87, x88)=false ⇒ IF(false, false, cons(x89, x84), node(x90, x91, x92), s(s(x85)))≥LESSE(cons(x89, x84), node(x90, x91, x92), s(s(s(x85))))) ⇒ IF(false, false, cons(x110, x77), node(x111, x112, x113), s(s(x82)))≥LESSE(cons(x110, x77), node(x111, x112, x113), s(s(s(x82)))))∧(∀x116,x117,x118,x119,x120,x121,x122,x123,x124,x125,x126,x127,x128,x129,x147,x148,x149,x150,x151,x152,x153,x154,x155,x156,x157,x158,x159,x160,x178,x179,x180,x181,x182,x183,x184,x185,x186:length(x114)=s(x116)∧length(x117)=x118∧le(x116, x119)=false∧le(x118, x120)=false∧s(x120)=x119∧(∀x121,x122,x123,x124,x125,x126,x127,x128,x129:le(x118, x120)=false∧length(x121)=x118∧s(x122)=x120∧length(x123)=x124∧s(s(x122))=x125∧le(x124, x125)=false ⇒ IF(false, false, cons(x126, x121), node(x127, x128, x129), s(s(x122)))≥LESSE(cons(x126, x121), node(x127, x128, x129), s(s(s(x122)))))∧(∀x147,x148,x149,x150,x151,x152,x153,x154,x155,x156,x157,x158,x159,x160,x178,x179,x180,x181:length(x117)=s(x147)∧le(x148, x149)=false∧le(x147, x150)=false∧length(x151)=s(x148)∧s(x150)=x149∧(∀x152,x153,x154,x155,x156,x157,x158,x159,x160:le(x147, x150)=false∧length(x152)=x147∧s(x153)=x150∧length(x154)=x155∧s(s(x153))=x156∧le(x155, x156)=false ⇒ IF(false, false, cons(x157, x152), node(x158, x159, x160), s(s(x153)))≥LESSE(cons(x157, x152), node(x158, x159, x160), s(s(s(x153))))) ⇒ IF(false, false, cons(x178, x117), node(x179, x180, x181), s(s(x150)))≥LESSE(cons(x178, x117), node(x179, x180, x181), s(s(s(x150))))) ⇒ IF(false, false, cons(x182, cons(x183, x117)), node(x184, x185, x186), s(s(x120)))≥LESSE(cons(x182, cons(x183, x117)), node(x184, x185, x186), s(s(s(x120))))) ⇒ IF(false, false, cons(x18, cons(x78, x77)), node(x20, x21, x22), s(s(x45)))≥LESSE(cons(x18, cons(x78, x77)), node(x20, x21, x22), s(s(s(x45)))))

  
  

  (16)    (le(x190, x189)=false∧length(x114)=s(x190)∧length(x77)=x46∧le(x46, x45)=false∧s(x45)=s(x189)∧(∀x47,x48,x49,x50,x51,x52,x53,x54,x55:le(x46, x45)=false∧length(x47)=x46∧s(x48)=x45∧length(x49)=x50∧s(s(x48))=x51∧le(x50, x51)=false ⇒ IF(false, false, cons(x52, x47), node(x53, x54, x55), s(s(x48)))≥LESSE(cons(x52, x47), node(x53, x54, x55), s(s(s(x48)))))∧(∀x79,x80,x81,x82,x83,x84,x85,x86,x87,x88,x89,x90,x91,x92,x110,x111,x112,x113:length(x77)=s(x79)∧le(x80, x81)=false∧le(x79, x82)=false∧length(x83)=s(x80)∧s(x82)=x81∧(∀x84,x85,x86,x87,x88,x89,x90,x91,x92:le(x79, x82)=false∧length(x84)=x79∧s(x85)=x82∧length(x86)=x87∧s(s(x85))=x88∧le(x87, x88)=false ⇒ IF(false, false, cons(x89, x84), node(x90, x91, x92), s(s(x85)))≥LESSE(cons(x89, x84), node(x90, x91, x92), s(s(s(x85))))) ⇒ IF(false, false, cons(x110, x77), node(x111, x112, x113), s(s(x82)))≥LESSE(cons(x110, x77), node(x111, x112, x113), s(s(s(x82)))))∧(∀x116,x117,x118,x119,x120,x121,x122,x123,x124,x125,x126,x127,x128,x129,x147,x148,x149,x150,x151,x152,x153,x154,x155,x156,x157,x158,x159,x160,x178,x179,x180,x181,x182,x183,x184,x185,x186:length(x114)=s(x116)∧length(x117)=x118∧le(x116, x119)=false∧le(x118, x120)=false∧s(x120)=x119∧(∀x121,x122,x123,x124,x125,x126,x127,x128,x129:le(x118, x120)=false∧length(x121)=x118∧s(x122)=x120∧length(x123)=x124∧s(s(x122))=x125∧le(x124, x125)=false ⇒ IF(false, false, cons(x126, x121), node(x127, x128, x129), s(s(x122)))≥LESSE(cons(x126, x121), node(x127, x128, x129), s(s(s(x122)))))∧(∀x147,x148,x149,x150,x151,x152,x153,x154,x155,x156,x157,x158,x159,x160,x178,x179,x180,x181:length(x117)=s(x147)∧le(x148, x149)=false∧le(x147, x150)=false∧length(x151)=s(x148)∧s(x150)=x149∧(∀x152,x153,x154,x155,x156,x157,x158,x159,x160:le(x147, x150)=false∧length(x152)=x147∧s(x153)=x150∧length(x154)=x155∧s(s(x153))=x156∧le(x155, x156)=false ⇒ IF(false, false, cons(x157, x152), node(x158, x159, x160), s(s(x153)))≥LESSE(cons(x157, x152), node(x158, x159, x160), s(s(s(x153))))) ⇒ IF(false, false, cons(x178, x117), node(x179, x180, x181), s(s(x150)))≥LESSE(cons(x178, x117), node(x179, x180, x181), s(s(s(x150))))) ⇒ IF(false, false, cons(x182, cons(x183, x117)), node(x184, x185, x186), s(s(x120)))≥LESSE(cons(x182, cons(x183, x117)), node(x184, x185, x186), s(s(s(x120)))))∧(∀x191,x192,x193,x194,x195,x196,x197,x198,x199,x200,x201,x202,x203,x204,x205,x206,x207,x208,x209,x210,x211,x212,x213,x214,x215,x216,x217,x218,x219,x220,x221,x222,x223,x224,x225,x226,x227,x228,x229,x230,x231,x232,x233,x234,x235,x236,x237,x238,x239,x240,x241,x242,x243,x244,x245,x246,x247,x248,x249,x250,x251,x252,x253,x254,x255,x256,x257,x258,x259,x260,x261,x262,x263:le(x190, x189)=false∧length(x191)=x190∧length(x192)=x193∧le(x193, x194)=false∧s(x194)=x189∧(∀x195,x196,x197,x198,x199,x200,x201,x202,x203:le(x193, x194)=false∧length(x195)=x193∧s(x196)=x194∧length(x197)=x198∧s(s(x196))=x199∧le(x198, x199)=false ⇒ IF(false, false, cons(x200, x195), node(x201, x202, x203), s(s(x196)))≥LESSE(cons(x200, x195), node(x201, x202, x203), s(s(s(x196)))))∧(∀x204,x205,x206,x207,x208,x209,x210,x211,x212,x213,x214,x215,x216,x217,x218,x219,x220,x221:length(x192)=s(x204)∧le(x205, x206)=false∧le(x204, x207)=false∧length(x208)=s(x205)∧s(x207)=x206∧(∀x209,x210,x211,x212,x213,x214,x215,x216,x217:le(x204, x207)=false∧length(x209)=x204∧s(x210)=x207∧length(x211)=x212∧s(s(x210))=x213∧le(x212, x213)=false ⇒ IF(false, false, cons(x214, x209), node(x215, x216, x217), s(s(x210)))≥LESSE(cons(x214, x209), node(x215, x216, x217), s(s(s(x210))))) ⇒ IF(false, false, cons(x218, x192), node(x219, x220, x221), s(s(x207)))≥LESSE(cons(x218, x192), node(x219, x220, x221), s(s(s(x207)))))∧(∀x222,x223,x224,x225,x226,x227,x228,x229,x230,x231,x232,x233,x234,x235,x236,x237,x238,x239,x240,x241,x242,x243,x244,x245,x246,x247,x248,x249,x250,x251,x252,x253,x254,x255,x256,x257,x258:length(x191)=s(x222)∧length(x223)=x224∧le(x222, x225)=false∧le(x224, x226)=false∧s(x226)=x225∧(∀x227,x228,x229,x230,x231,x232,x233,x234,x235:le(x224, x226)=false∧length(x227)=x224∧s(x228)=x226∧length(x229)=x230∧s(s(x228))=x231∧le(x230, x231)=false ⇒ IF(false, false, cons(x232, x227), node(x233, x234, x235), s(s(x228)))≥LESSE(cons(x232, x227), node(x233, x234, x235), s(s(s(x228)))))∧(∀x236,x237,x238,x239,x240,x241,x242,x243,x244,x245,x246,x247,x248,x249,x250,x251,x252,x253:length(x223)=s(x236)∧le(x237, x238)=false∧le(x236, x239)=false∧length(x240)=s(x237)∧s(x239)=x238∧(∀x241,x242,x243,x244,x245,x246,x247,x248,x249:le(x236, x239)=false∧length(x241)=x236∧s(x242)=x239∧length(x243)=x244∧s(s(x242))=x245∧le(x244, x245)=false ⇒ IF(false, false, cons(x246, x241), node(x247, x248, x249), s(s(x242)))≥LESSE(cons(x246, x241), node(x247, x248, x249), s(s(s(x242))))) ⇒ IF(false, false, cons(x250, x223), node(x251, x252, x253), s(s(x239)))≥LESSE(cons(x250, x223), node(x251, x252, x253), s(s(s(x239))))) ⇒ IF(false, false, cons(x254, cons(x255, x223)), node(x256, x257, x258), s(s(x226)))≥LESSE(cons(x254, cons(x255, x223)), node(x256, x257, x258), s(s(s(x226))))) ⇒ IF(false, false, cons(x259, cons(x260, x192)), node(x261, x262, x263), s(s(x194)))≥LESSE(cons(x259, cons(x260, x192)), node(x261, x262, x263), s(s(s(x194))))) ⇒ IF(false, false, cons(x18, cons(x78, x77)), node(x20, x21, x22), s(s(x45)))≥LESSE(cons(x18, cons(x78, x77)), node(x20, x21, x22), s(s(s(x45)))))

  
  
  We solved constraint (15) using rules (I), (II).We simplified constraint (16) using rules (I), (II), (IV) which results in the following new constraint:
  

  (17)    (le(x190, x189)=false∧length(x114)=s(x190)∧length(x77)=x46∧le(x46, x45)=false∧x45=x189∧(∀x79,x80,x81,x82,x83,x110,x111,x112,x113:length(x77)=s(x79)∧le(x80, x81)=false∧le(x79, x82)=false∧length(x83)=s(x80)∧s(x82)=x81 ⇒ IF(false, false, cons(x110, x77), node(x111, x112, x113), s(s(x82)))≥LESSE(cons(x110, x77), node(x111, x112, x113), s(s(s(x82)))))∧(∀x116,x117,x118,x119,x120,x147,x148,x149,x150,x151,x178,x179,x180,x181,x182,x183,x184,x185,x186:length(x114)=s(x116)∧length(x117)=x118∧le(x116, x119)=false∧le(x118, x120)=false∧s(x120)=x119∧(∀x147,x148,x149,x150,x151,x178,x179,x180,x181:length(x117)=s(x147)∧le(x148, x149)=false∧le(x147, x150)=false∧length(x151)=s(x148)∧s(x150)=x149 ⇒ IF(false, false, cons(x178, x117), node(x179, x180, x181), s(s(x150)))≥LESSE(cons(x178, x117), node(x179, x180, x181), s(s(s(x150))))) ⇒ IF(false, false, cons(x182, cons(x183, x117)), node(x184, x185, x186), s(s(x120)))≥LESSE(cons(x182, cons(x183, x117)), node(x184, x185, x186), s(s(s(x120)))))∧(∀x191,x192,x193,x194,x204,x205,x206,x207,x208,x218,x219,x220,x221,x222,x223,x224,x225,x226,x236,x237,x238,x239,x240,x250,x251,x252,x253,x254,x255,x256,x257,x258,x259,x260,x261,x262,x263:le(x190, x189)=false∧length(x191)=x190∧length(x192)=x193∧le(x193, x194)=false∧s(x194)=x189∧(∀x204,x205,x206,x207,x208,x218,x219,x220,x221:length(x192)=s(x204)∧le(x205, x206)=false∧le(x204, x207)=false∧length(x208)=s(x205)∧s(x207)=x206 ⇒ IF(false, false, cons(x218, x192), node(x219, x220, x221), s(s(x207)))≥LESSE(cons(x218, x192), node(x219, x220, x221), s(s(s(x207)))))∧(∀x222,x223,x224,x225,x226,x236,x237,x238,x239,x240,x250,x251,x252,x253,x254,x255,x256,x257,x258:length(x191)=s(x222)∧length(x223)=x224∧le(x222, x225)=false∧le(x224, x226)=false∧s(x226)=x225∧(∀x236,x237,x238,x239,x240,x250,x251,x252,x253:length(x223)=s(x236)∧le(x237, x238)=false∧le(x236, x239)=false∧length(x240)=s(x237)∧s(x239)=x238 ⇒ IF(false, false, cons(x250, x223), node(x251, x252, x253), s(s(x239)))≥LESSE(cons(x250, x223), node(x251, x252, x253), s(s(s(x239))))) ⇒ IF(false, false, cons(x254, cons(x255, x223)), node(x256, x257, x258), s(s(x226)))≥LESSE(cons(x254, cons(x255, x223)), node(x256, x257, x258), s(s(s(x226))))) ⇒ IF(false, false, cons(x259, cons(x260, x192)), node(x261, x262, x263), s(s(x194)))≥LESSE(cons(x259, cons(x260, x192)), node(x261, x262, x263), s(s(s(x194))))) ⇒ IF(false, false, cons(x18, cons(x78, x77)), node(x20, x21, x22), s(s(x45)))≥LESSE(cons(x18, cons(x78, x77)), node(x20, x21, x22), s(s(s(x45)))))

  
  
  We simplified constraint (17) using rule (V) (with possible (I) afterwards) using induction on le(x46, x45)=false which results in the following new constraints:
  

  (18)    (false=false∧le(x190, x189)=false∧length(x114)=s(x190)∧length(x77)=s(x264)∧0=x189∧(∀x79,x80,x81,x82,x83,x110,x111,x112,x113:length(x77)=s(x79)∧le(x80, x81)=false∧le(x79, x82)=false∧length(x83)=s(x80)∧s(x82)=x81 ⇒ IF(false, false, cons(x110, x77), node(x111, x112, x113), s(s(x82)))≥LESSE(cons(x110, x77), node(x111, x112, x113), s(s(s(x82)))))∧(∀x116,x117,x118,x119,x120,x147,x148,x149,x150,x151,x178,x179,x180,x181,x182,x183,x184,x185,x186:length(x114)=s(x116)∧length(x117)=x118∧le(x116, x119)=false∧le(x118, x120)=false∧s(x120)=x119∧(∀x147,x148,x149,x150,x151,x178,x179,x180,x181:length(x117)=s(x147)∧le(x148, x149)=false∧le(x147, x150)=false∧length(x151)=s(x148)∧s(x150)=x149 ⇒ IF(false, false, cons(x178, x117), node(x179, x180, x181), s(s(x150)))≥LESSE(cons(x178, x117), node(x179, x180, x181), s(s(s(x150))))) ⇒ IF(false, false, cons(x182, cons(x183, x117)), node(x184, x185, x186), s(s(x120)))≥LESSE(cons(x182, cons(x183, x117)), node(x184, x185, x186), s(s(s(x120)))))∧(∀x191,x192,x193,x194,x204,x205,x206,x207,x208,x218,x219,x220,x221,x222,x223,x224,x225,x226,x236,x237,x238,x239,x240,x250,x251,x252,x253,x254,x255,x256,x257,x258,x259,x260,x261,x262,x263:le(x190, x189)=false∧length(x191)=x190∧length(x192)=x193∧le(x193, x194)=false∧s(x194)=x189∧(∀x204,x205,x206,x207,x208,x218,x219,x220,x221:length(x192)=s(x204)∧le(x205, x206)=false∧le(x204, x207)=false∧length(x208)=s(x205)∧s(x207)=x206 ⇒ IF(false, false, cons(x218, x192), node(x219, x220, x221), s(s(x207)))≥LESSE(cons(x218, x192), node(x219, x220, x221), s(s(s(x207)))))∧(∀x222,x223,x224,x225,x226,x236,x237,x238,x239,x240,x250,x251,x252,x253,x254,x255,x256,x257,x258:length(x191)=s(x222)∧length(x223)=x224∧le(x222, x225)=false∧le(x224, x226)=false∧s(x226)=x225∧(∀x236,x237,x238,x239,x240,x250,x251,x252,x253:length(x223)=s(x236)∧le(x237, x238)=false∧le(x236, x239)=false∧length(x240)=s(x237)∧s(x239)=x238 ⇒ IF(false, false, cons(x250, x223), node(x251, x252, x253), s(s(x239)))≥LESSE(cons(x250, x223), node(x251, x252, x253), s(s(s(x239))))) ⇒ IF(false, false, cons(x254, cons(x255, x223)), node(x256, x257, x258), s(s(x226)))≥LESSE(cons(x254, cons(x255, x223)), node(x256, x257, x258), s(s(s(x226))))) ⇒ IF(false, false, cons(x259, cons(x260, x192)), node(x261, x262, x263), s(s(x194)))≥LESSE(cons(x259, cons(x260, x192)), node(x261, x262, x263), s(s(s(x194))))) ⇒ IF(false, false, cons(x18, cons(x78, x77)), node(x20, x21, x22), s(s(0)))≥LESSE(cons(x18, cons(x78, x77)), node(x20, x21, x22), s(s(s(0)))))

  
  

  (19)    (le(x267, x266)=false∧le(x190, x189)=false∧length(x114)=s(x190)∧length(x77)=s(x267)∧s(x266)=x189∧(∀x79,x80,x81,x82,x83,x110,x111,x112,x113:length(x77)=s(x79)∧le(x80, x81)=false∧le(x79, x82)=false∧length(x83)=s(x80)∧s(x82)=x81 ⇒ IF(false, false, cons(x110, x77), node(x111, x112, x113), s(s(x82)))≥LESSE(cons(x110, x77), node(x111, x112, x113), s(s(s(x82)))))∧(∀x116,x117,x118,x119,x120,x147,x148,x149,x150,x151,x178,x179,x180,x181,x182,x183,x184,x185,x186:length(x114)=s(x116)∧length(x117)=x118∧le(x116, x119)=false∧le(x118, x120)=false∧s(x120)=x119∧(∀x147,x148,x149,x150,x151,x178,x179,x180,x181:length(x117)=s(x147)∧le(x148, x149)=false∧le(x147, x150)=false∧length(x151)=s(x148)∧s(x150)=x149 ⇒ IF(false, false, cons(x178, x117), node(x179, x180, x181), s(s(x150)))≥LESSE(cons(x178, x117), node(x179, x180, x181), s(s(s(x150))))) ⇒ IF(false, false, cons(x182, cons(x183, x117)), node(x184, x185, x186), s(s(x120)))≥LESSE(cons(x182, cons(x183, x117)), node(x184, x185, x186), s(s(s(x120)))))∧(∀x191,x192,x193,x194,x204,x205,x206,x207,x208,x218,x219,x220,x221,x222,x223,x224,x225,x226,x236,x237,x238,x239,x240,x250,x251,x252,x253,x254,x255,x256,x257,x258,x259,x260,x261,x262,x263:le(x190, x189)=false∧length(x191)=x190∧length(x192)=x193∧le(x193, x194)=false∧s(x194)=x189∧(∀x204,x205,x206,x207,x208,x218,x219,x220,x221:length(x192)=s(x204)∧le(x205, x206)=false∧le(x204, x207)=false∧length(x208)=s(x205)∧s(x207)=x206 ⇒ IF(false, false, cons(x218, x192), node(x219, x220, x221), s(s(x207)))≥LESSE(cons(x218, x192), node(x219, x220, x221), s(s(s(x207)))))∧(∀x222,x223,x224,x225,x226,x236,x237,x238,x239,x240,x250,x251,x252,x253,x254,x255,x256,x257,x258:length(x191)=s(x222)∧length(x223)=x224∧le(x222, x225)=false∧le(x224, x226)=false∧s(x226)=x225∧(∀x236,x237,x238,x239,x240,x250,x251,x252,x253:length(x223)=s(x236)∧le(x237, x238)=false∧le(x236, x239)=false∧length(x240)=s(x237)∧s(x239)=x238 ⇒ IF(false, false, cons(x250, x223), node(x251, x252, x253), s(s(x239)))≥LESSE(cons(x250, x223), node(x251, x252, x253), s(s(s(x239))))) ⇒ IF(false, false, cons(x254, cons(x255, x223)), node(x256, x257, x258), s(s(x226)))≥LESSE(cons(x254, cons(x255, x223)), node(x256, x257, x258), s(s(s(x226))))) ⇒ IF(false, false, cons(x259, cons(x260, x192)), node(x261, x262, x263), s(s(x194)))≥LESSE(cons(x259, cons(x260, x192)), node(x261, x262, x263), s(s(s(x194)))))∧(∀x268,x269,x270,x271,x272,x273,x274,x275,x276,x277,x278,x279,x280,x281,x282,x283,x284,x285,x286,x287,x288,x289,x290,x291,x292,x293,x294,x295,x296,x297,x298,x299,x300,x301,x302,x303,x304,x305,x306,x307,x308,x309,x310,x311,x312,x313,x314,x315,x316,x317,x318,x319,x320,x321,x322,x323,x324,x325,x326,x327,x328,x329,x330,x331,x332,x333,x334,x335,x336,x337,x338,x339,x340,x341:le(x267, x266)=false∧le(x268, x269)=false∧length(x270)=s(x268)∧length(x271)=x267∧x266=x269∧(∀x272,x273,x274,x275,x276,x277,x278,x279,x280:length(x271)=s(x272)∧le(x273, x274)=false∧le(x272, x275)=false∧length(x276)=s(x273)∧s(x275)=x274 ⇒ IF(false, false, cons(x277, x271), node(x278, x279, x280), s(s(x275)))≥LESSE(cons(x277, x271), node(x278, x279, x280), s(s(s(x275)))))∧(∀x281,x282,x283,x284,x285,x286,x287,x288,x289,x290,x291,x292,x293,x294,x295,x296,x297,x298,x299:length(x270)=s(x281)∧length(x282)=x283∧le(x281, x284)=false∧le(x283, x285)=false∧s(x285)=x284∧(∀x286,x287,x288,x289,x290,x291,x292,x293,x294:length(x282)=s(x286)∧le(x287, x288)=false∧le(x286, x289)=false∧length(x290)=s(x287)∧s(x289)=x288 ⇒ IF(false, false, cons(x291, x282), node(x292, x293, x294), s(s(x289)))≥LESSE(cons(x291, x282), node(x292, x293, x294), s(s(s(x289))))) ⇒ IF(false, false, cons(x295, cons(x296, x282)), node(x297, x298, x299), s(s(x285)))≥LESSE(cons(x295, cons(x296, x282)), node(x297, x298, x299), s(s(s(x285)))))∧(∀x300,x301,x302,x303,x304,x305,x306,x307,x308,x309,x310,x311,x312,x313,x314,x315,x316,x317,x318,x319,x320,x321,x322,x323,x324,x325,x326,x327,x328,x329,x330,x331,x332,x333,x334,x335,x336:le(x268, x269)=false∧length(x300)=x268∧length(x301)=x302∧le(x302, x303)=false∧s(x303)=x269∧(∀x304,x305,x306,x307,x308,x309,x310,x311,x312:length(x301)=s(x304)∧le(x305, x306)=false∧le(x304, x307)=false∧length(x308)=s(x305)∧s(x307)=x306 ⇒ IF(false, false, cons(x309, x301), node(x310, x311, x312), s(s(x307)))≥LESSE(cons(x309, x301), node(x310, x311, x312), s(s(s(x307)))))∧(∀x313,x314,x315,x316,x317,x318,x319,x320,x321,x322,x323,x324,x325,x326,x327,x328,x329,x330,x331:length(x300)=s(x313)∧length(x314)=x315∧le(x313, x316)=false∧le(x315, x317)=false∧s(x317)=x316∧(∀x318,x319,x320,x321,x322,x323,x324,x325,x326:length(x314)=s(x318)∧le(x319, x320)=false∧le(x318, x321)=false∧length(x322)=s(x319)∧s(x321)=x320 ⇒ IF(false, false, cons(x323, x314), node(x324, x325, x326), s(s(x321)))≥LESSE(cons(x323, x314), node(x324, x325, x326), s(s(s(x321))))) ⇒ IF(false, false, cons(x327, cons(x328, x314)), node(x329, x330, x331), s(s(x317)))≥LESSE(cons(x327, cons(x328, x314)), node(x329, x330, x331), s(s(s(x317))))) ⇒ IF(false, false, cons(x332, cons(x333, x301)), node(x334, x335, x336), s(s(x303)))≥LESSE(cons(x332, cons(x333, x301)), node(x334, x335, x336), s(s(s(x303))))) ⇒ IF(false, false, cons(x337, cons(x338, x271)), node(x339, x340, x341), s(s(x266)))≥LESSE(cons(x337, cons(x338, x271)), node(x339, x340, x341), s(s(s(x266))))) ⇒ IF(false, false, cons(x18, cons(x78, x77)), node(x20, x21, x22), s(s(s(x266))))≥LESSE(cons(x18, cons(x78, x77)), node(x20, x21, x22), s(s(s(s(x266))))))

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

  (20)    (le(x190, x189)=false∧length(x114)=s(x190)∧length(x77)=s(x264)∧0=x189∧(∀x79,x80,x81,x82,x83,x110,x111,x112,x113:length(x77)=s(x79)∧le(x80, x81)=false∧le(x79, x82)=false∧length(x83)=s(x80)∧s(x82)=x81 ⇒ IF(false, false, cons(x110, x77), node(x111, x112, x113), s(s(x82)))≥LESSE(cons(x110, x77), node(x111, x112, x113), s(s(s(x82)))))∧(∀x191,x192,x193,x194,x204,x205,x206,x207,x208,x218,x219,x220,x221,x259,x260,x261,x262,x263:le(x190, x189)=false∧length(x191)=x190∧length(x192)=x193∧le(x193, x194)=false∧s(x194)=x189∧(∀x204,x205,x206,x207,x208,x218,x219,x220,x221:length(x192)=s(x204)∧le(x205, x206)=false∧le(x204, x207)=false∧length(x208)=s(x205)∧s(x207)=x206 ⇒ IF(false, false, cons(x218, x192), node(x219, x220, x221), s(s(x207)))≥LESSE(cons(x218, x192), node(x219, x220, x221), s(s(s(x207))))) ⇒ IF(false, false, cons(x259, cons(x260, x192)), node(x261, x262, x263), s(s(x194)))≥LESSE(cons(x259, cons(x260, x192)), node(x261, x262, x263), s(s(s(x194))))) ⇒ IF(false, false, cons(x18, cons(x78, x77)), node(x20, x21, x22), s(s(0)))≥LESSE(cons(x18, cons(x78, x77)), node(x20, x21, x22), s(s(s(0)))))

  
  
  We simplified constraint (19) using rule (VI) where we applied the induction hypothesis (∀x79,x80,x81,x82,x83,x110,x111,x112,x113:length(x77)=s(x79)∧le(x80, x81)=false∧le(x79, x82)=false∧length(x83)=s(x80)∧s(x82)=x81 ⇒ IF(false, false, cons(x110, x77), node(x111, x112, x113), s(s(x82)))≥LESSE(cons(x110, x77), node(x111, x112, x113), s(s(s(x82))))) with σ = [x79 / x267, x80 / x190, x81 / x189, x82 / x266, x83 / x114, x110 / x18, x111 / x20, x112 / x21, x113 / x22] which results in the following new constraint:
  

  (21)    (IF(false, false, cons(x18, x77), node(x20, x21, x22), s(s(x266)))≥LESSE(cons(x18, x77), node(x20, x21, x22), s(s(s(x266))))∧(∀x116,x117,x118,x119,x120,x147,x148,x149,x150,x151,x178,x179,x180,x181,x182,x183,x184,x185,x186:length(x114)=s(x116)∧length(x117)=x118∧le(x116, x119)=false∧le(x118, x120)=false∧s(x120)=x119∧(∀x147,x148,x149,x150,x151,x178,x179,x180,x181:length(x117)=s(x147)∧le(x148, x149)=false∧le(x147, x150)=false∧length(x151)=s(x148)∧s(x150)=x149 ⇒ IF(false, false, cons(x178, x117), node(x179, x180, x181), s(s(x150)))≥LESSE(cons(x178, x117), node(x179, x180, x181), s(s(s(x150))))) ⇒ IF(false, false, cons(x182, cons(x183, x117)), node(x184, x185, x186), s(s(x120)))≥LESSE(cons(x182, cons(x183, x117)), node(x184, x185, x186), s(s(s(x120)))))∧(∀x191,x192,x193,x194,x204,x205,x206,x207,x208,x218,x219,x220,x221,x222,x223,x224,x225,x226,x236,x237,x238,x239,x240,x250,x251,x252,x253,x254,x255,x256,x257,x258,x259,x260,x261,x262,x263:le(x190, x189)=false∧length(x191)=x190∧length(x192)=x193∧le(x193, x194)=false∧s(x194)=x189∧(∀x204,x205,x206,x207,x208,x218,x219,x220,x221:length(x192)=s(x204)∧le(x205, x206)=false∧le(x204, x207)=false∧length(x208)=s(x205)∧s(x207)=x206 ⇒ IF(false, false, cons(x218, x192), node(x219, x220, x221), s(s(x207)))≥LESSE(cons(x218, x192), node(x219, x220, x221), s(s(s(x207)))))∧(∀x222,x223,x224,x225,x226,x236,x237,x238,x239,x240,x250,x251,x252,x253,x254,x255,x256,x257,x258:length(x191)=s(x222)∧length(x223)=x224∧le(x222, x225)=false∧le(x224, x226)=false∧s(x226)=x225∧(∀x236,x237,x238,x239,x240,x250,x251,x252,x253:length(x223)=s(x236)∧le(x237, x238)=false∧le(x236, x239)=false∧length(x240)=s(x237)∧s(x239)=x238 ⇒ IF(false, false, cons(x250, x223), node(x251, x252, x253), s(s(x239)))≥LESSE(cons(x250, x223), node(x251, x252, x253), s(s(s(x239))))) ⇒ IF(false, false, cons(x254, cons(x255, x223)), node(x256, x257, x258), s(s(x226)))≥LESSE(cons(x254, cons(x255, x223)), node(x256, x257, x258), s(s(s(x226))))) ⇒ IF(false, false, cons(x259, cons(x260, x192)), node(x261, x262, x263), s(s(x194)))≥LESSE(cons(x259, cons(x260, x192)), node(x261, x262, x263), s(s(s(x194)))))∧(∀x268,x269,x270,x271,x272,x273,x274,x275,x276,x277,x278,x279,x280,x281,x282,x283,x284,x285,x286,x287,x288,x289,x290,x291,x292,x293,x294,x295,x296,x297,x298,x299,x300,x301,x302,x303,x304,x305,x306,x307,x308,x309,x310,x311,x312,x313,x314,x315,x316,x317,x318,x319,x320,x321,x322,x323,x324,x325,x326,x327,x328,x329,x330,x331,x332,x333,x334,x335,x336,x337,x338,x339,x340,x341:le(x267, x266)=false∧le(x268, x269)=false∧length(x270)=s(x268)∧length(x271)=x267∧x266=x269∧(∀x272,x273,x274,x275,x276,x277,x278,x279,x280:length(x271)=s(x272)∧le(x273, x274)=false∧le(x272, x275)=false∧length(x276)=s(x273)∧s(x275)=x274 ⇒ IF(false, false, cons(x277, x271), node(x278, x279, x280), s(s(x275)))≥LESSE(cons(x277, x271), node(x278, x279, x280), s(s(s(x275)))))∧(∀x281,x282,x283,x284,x285,x286,x287,x288,x289,x290,x291,x292,x293,x294,x295,x296,x297,x298,x299:length(x270)=s(x281)∧length(x282)=x283∧le(x281, x284)=false∧le(x283, x285)=false∧s(x285)=x284∧(∀x286,x287,x288,x289,x290,x291,x292,x293,x294:length(x282)=s(x286)∧le(x287, x288)=false∧le(x286, x289)=false∧length(x290)=s(x287)∧s(x289)=x288 ⇒ IF(false, false, cons(x291, x282), node(x292, x293, x294), s(s(x289)))≥LESSE(cons(x291, x282), node(x292, x293, x294), s(s(s(x289))))) ⇒ IF(false, false, cons(x295, cons(x296, x282)), node(x297, x298, x299), s(s(x285)))≥LESSE(cons(x295, cons(x296, x282)), node(x297, x298, x299), s(s(s(x285)))))∧(∀x300,x301,x302,x303,x304,x305,x306,x307,x308,x309,x310,x311,x312,x313,x314,x315,x316,x317,x318,x319,x320,x321,x322,x323,x324,x325,x326,x327,x328,x329,x330,x331,x332,x333,x334,x335,x336:le(x268, x269)=false∧length(x300)=x268∧length(x301)=x302∧le(x302, x303)=false∧s(x303)=x269∧(∀x304,x305,x306,x307,x308,x309,x310,x311,x312:length(x301)=s(x304)∧le(x305, x306)=false∧le(x304, x307)=false∧length(x308)=s(x305)∧s(x307)=x306 ⇒ IF(false, false, cons(x309, x301), node(x310, x311, x312), s(s(x307)))≥LESSE(cons(x309, x301), node(x310, x311, x312), s(s(s(x307)))))∧(∀x313,x314,x315,x316,x317,x318,x319,x320,x321,x322,x323,x324,x325,x326,x327,x328,x329,x330,x331:length(x300)=s(x313)∧length(x314)=x315∧le(x313, x316)=false∧le(x315, x317)=false∧s(x317)=x316∧(∀x318,x319,x320,x321,x322,x323,x324,x325,x326:length(x314)=s(x318)∧le(x319, x320)=false∧le(x318, x321)=false∧length(x322)=s(x319)∧s(x321)=x320 ⇒ IF(false, false, cons(x323, x314), node(x324, x325, x326), s(s(x321)))≥LESSE(cons(x323, x314), node(x324, x325, x326), s(s(s(x321))))) ⇒ IF(false, false, cons(x327, cons(x328, x314)), node(x329, x330, x331), s(s(x317)))≥LESSE(cons(x327, cons(x328, x314)), node(x329, x330, x331), s(s(s(x317))))) ⇒ IF(false, false, cons(x332, cons(x333, x301)), node(x334, x335, x336), s(s(x303)))≥LESSE(cons(x332, cons(x333, x301)), node(x334, x335, x336), s(s(s(x303))))) ⇒ IF(false, false, cons(x337, cons(x338, x271)), node(x339, x340, x341), s(s(x266)))≥LESSE(cons(x337, cons(x338, x271)), node(x339, x340, x341), s(s(s(x266))))) ⇒ IF(false, false, cons(x18, cons(x78, x77)), node(x20, x21, x22), s(s(s(x266))))≥LESSE(cons(x18, cons(x78, x77)), node(x20, x21, x22), s(s(s(s(x266))))))

  
  
  We simplified constraint (20) using rule (V) (with possible (I) afterwards) using induction on length(x114)=s(x190) which results in the following new constraint:
  

  (22)    (s(length(x342))=s(x190)∧le(x190, x189)=false∧length(x77)=s(x264)∧0=x189∧(∀x79,x80,x81,x82,x83,x110,x111,x112,x113:length(x77)=s(x79)∧le(x80, x81)=false∧le(x79, x82)=false∧length(x83)=s(x80)∧s(x82)=x81 ⇒ IF(false, false, cons(x110, x77), node(x111, x112, x113), s(s(x82)))≥LESSE(cons(x110, x77), node(x111, x112, x113), s(s(s(x82)))))∧(∀x191,x192,x193,x194,x204,x205,x206,x207,x208,x218,x219,x220,x221,x259,x260,x261,x262,x263:le(x190, x189)=false∧length(x191)=x190∧length(x192)=x193∧le(x193, x194)=false∧s(x194)=x189∧(∀x204,x205,x206,x207,x208,x218,x219,x220,x221:length(x192)=s(x204)∧le(x205, x206)=false∧le(x204, x207)=false∧length(x208)=s(x205)∧s(x207)=x206 ⇒ IF(false, false, cons(x218, x192), node(x219, x220, x221), s(s(x207)))≥LESSE(cons(x218, x192), node(x219, x220, x221), s(s(s(x207))))) ⇒ IF(false, false, cons(x259, cons(x260, x192)), node(x261, x262, x263), s(s(x194)))≥LESSE(cons(x259, cons(x260, x192)), node(x261, x262, x263), s(s(s(x194)))))∧(∀x344,x345,x346,x347,x348,x349,x350,x351,x352,x353,x354,x355,x356,x357,x358,x359,x360,x361,x362,x363,x364,x365,x366,x367,x368,x369,x370,x371,x372,x373,x374,x375,x376,x377,x378,x379:length(x342)=s(x344)∧le(x344, x345)=false∧length(x346)=s(x347)∧0=x345∧(∀x348,x349,x350,x351,x352,x353,x354,x355,x356:length(x346)=s(x348)∧le(x349, x350)=false∧le(x348, x351)=false∧length(x352)=s(x349)∧s(x351)=x350 ⇒ IF(false, false, cons(x353, x346), node(x354, x355, x356), s(s(x351)))≥LESSE(cons(x353, x346), node(x354, x355, x356), s(s(s(x351)))))∧(∀x357,x358,x359,x360,x361,x362,x363,x364,x365,x366,x367,x368,x369,x370,x371,x372,x373,x374:le(x344, x345)=false∧length(x357)=x344∧length(x358)=x359∧le(x359, x360)=false∧s(x360)=x345∧(∀x361,x362,x363,x364,x365,x366,x367,x368,x369:length(x358)=s(x361)∧le(x362, x363)=false∧le(x361, x364)=false∧length(x365)=s(x362)∧s(x364)=x363 ⇒ IF(false, false, cons(x366, x358), node(x367, x368, x369), s(s(x364)))≥LESSE(cons(x366, x358), node(x367, x368, x369), s(s(s(x364))))) ⇒ IF(false, false, cons(x370, cons(x371, x358)), node(x372, x373, x374), s(s(x360)))≥LESSE(cons(x370, cons(x371, x358)), node(x372, x373, x374), s(s(s(x360))))) ⇒ IF(false, false, cons(x375, cons(x376, x346)), node(x377, x378, x379), s(s(0)))≥LESSE(cons(x375, cons(x376, x346)), node(x377, x378, x379), s(s(s(0))))) ⇒ IF(false, false, cons(x18, cons(x78, x77)), node(x20, x21, x22), s(s(0)))≥LESSE(cons(x18, cons(x78, x77)), node(x20, x21, x22), s(s(s(0)))))

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

  (23)    (length(x342)=x190∧le(x190, x189)=false∧length(x77)=s(x264)∧0=x189∧(∀x191,x192,x193,x194,x259,x260,x261,x262,x263:le(x190, x189)=false∧length(x191)=x190∧length(x192)=x193∧le(x193, x194)=false∧s(x194)=x189 ⇒ IF(false, false, cons(x259, cons(x260, x192)), node(x261, x262, x263), s(s(x194)))≥LESSE(cons(x259, cons(x260, x192)), node(x261, x262, x263), s(s(s(x194)))))∧(∀x344,x345,x346,x347,x357,x358,x359,x360,x370,x371,x372,x373,x374,x375,x376,x377,x378,x379:length(x342)=s(x344)∧le(x344, x345)=false∧length(x346)=s(x347)∧0=x345∧(∀x357,x358,x359,x360,x370,x371,x372,x373,x374:le(x344, x345)=false∧length(x357)=x344∧length(x358)=x359∧le(x359, x360)=false∧s(x360)=x345 ⇒ IF(false, false, cons(x370, cons(x371, x358)), node(x372, x373, x374), s(s(x360)))≥LESSE(cons(x370, cons(x371, x358)), node(x372, x373, x374), s(s(s(x360))))) ⇒ IF(false, false, cons(x375, cons(x376, x346)), node(x377, x378, x379), s(s(0)))≥LESSE(cons(x375, cons(x376, x346)), node(x377, x378, x379), s(s(s(0))))) ⇒ IF(false, false, cons(x18, cons(x78, x77)), node(x20, x21, x22), s(s(0)))≥LESSE(cons(x18, cons(x78, x77)), node(x20, x21, x22), s(s(s(0)))))

  
  
  We simplified constraint (23) using rule (V) (with possible (I) afterwards) using induction on length(x77)=s(x264) which results in the following new constraint:
  

  (24)    (s(length(x380))=s(x264)∧length(x342)=x190∧le(x190, x189)=false∧0=x189∧(∀x191,x192,x193,x194,x259,x260,x261,x262,x263:le(x190, x189)=false∧length(x191)=x190∧length(x192)=x193∧le(x193, x194)=false∧s(x194)=x189 ⇒ IF(false, false, cons(x259, cons(x260, x192)), node(x261, x262, x263), s(s(x194)))≥LESSE(cons(x259, cons(x260, x192)), node(x261, x262, x263), s(s(s(x194)))))∧(∀x344,x345,x346,x347,x357,x358,x359,x360,x370,x371,x372,x373,x374,x375,x376,x377,x378,x379:length(x342)=s(x344)∧le(x344, x345)=false∧length(x346)=s(x347)∧0=x345∧(∀x357,x358,x359,x360,x370,x371,x372,x373,x374:le(x344, x345)=false∧length(x357)=x344∧length(x358)=x359∧le(x359, x360)=false∧s(x360)=x345 ⇒ IF(false, false, cons(x370, cons(x371, x358)), node(x372, x373, x374), s(s(x360)))≥LESSE(cons(x370, cons(x371, x358)), node(x372, x373, x374), s(s(s(x360))))) ⇒ IF(false, false, cons(x375, cons(x376, x346)), node(x377, x378, x379), s(s(0)))≥LESSE(cons(x375, cons(x376, x346)), node(x377, x378, x379), s(s(s(0)))))∧(∀x382,x383,x384,x385,x386,x387,x388,x389,x390,x391,x392,x393,x394,x395,x396,x397,x398,x399,x400,x401,x402,x403,x404,x405,x406,x407,x408,x409,x410,x411,x412,x413,x414,x415,x416,x417:length(x380)=s(x382)∧length(x383)=x384∧le(x384, x385)=false∧0=x385∧(∀x386,x387,x388,x389,x390,x391,x392,x393,x394:le(x384, x385)=false∧length(x386)=x384∧length(x387)=x388∧le(x388, x389)=false∧s(x389)=x385 ⇒ IF(false, false, cons(x390, cons(x391, x387)), node(x392, x393, x394), s(s(x389)))≥LESSE(cons(x390, cons(x391, x387)), node(x392, x393, x394), s(s(s(x389)))))∧(∀x395,x396,x397,x398,x399,x400,x401,x402,x403,x404,x405,x406,x407,x408,x409,x410,x411,x412:length(x383)=s(x395)∧le(x395, x396)=false∧length(x397)=s(x398)∧0=x396∧(∀x399,x400,x401,x402,x403,x404,x405,x406,x407:le(x395, x396)=false∧length(x399)=x395∧length(x400)=x401∧le(x401, x402)=false∧s(x402)=x396 ⇒ IF(false, false, cons(x403, cons(x404, x400)), node(x405, x406, x407), s(s(x402)))≥LESSE(cons(x403, cons(x404, x400)), node(x405, x406, x407), s(s(s(x402))))) ⇒ IF(false, false, cons(x408, cons(x409, x397)), node(x410, x411, x412), s(s(0)))≥LESSE(cons(x408, cons(x409, x397)), node(x410, x411, x412), s(s(s(0))))) ⇒ IF(false, false, cons(x413, cons(x414, x380)), node(x415, x416, x417), s(s(0)))≥LESSE(cons(x413, cons(x414, x380)), node(x415, x416, x417), s(s(s(0))))) ⇒ IF(false, false, cons(x18, cons(x78, cons(x381, x380))), node(x20, x21, x22), s(s(0)))≥LESSE(cons(x18, cons(x78, cons(x381, x380))), node(x20, x21, x22), s(s(s(0)))))

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

  (25)    (IF(false, false, cons(x18, cons(x78, cons(x381, x380))), node(x20, x21, x22), s(s(0)))≥LESSE(cons(x18, cons(x78, cons(x381, x380))), node(x20, x21, x22), s(s(s(0)))))

  
  
  We simplified constraint (21) using rule (IV) which results in the following new constraint:
  

  (26)    (IF(false, false, cons(x18, x77), node(x20, x21, x22), s(s(x266)))≥LESSE(cons(x18, x77), node(x20, x21, x22), s(s(s(x266)))) ⇒ IF(false, false, cons(x18, cons(x78, x77)), node(x20, x21, x22), s(s(s(x266))))≥LESSE(cons(x18, cons(x78, x77)), node(x20, x21, x22), s(s(s(s(x266))))))

  
  
  

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

• LESSE(cons(z0, z1), node(z2, z3, z4), s(s(z5))) → IF(le(length(z1), s(z5)), le(length(append(toList(z2), cons(z3, toList(z4)))), s(s(z5))), cons(z0, z1), node(z2, z3, z4), s(s(z5)))
  
  • (LESSE(cons(x6, x7), node(x8, x9, x10), s(s(s(x11))))≥IF(le(length(x7), s(s(x11))), le(length(append(toList(x8), cons(x9, toList(x10)))), s(s(s(x11)))), cons(x6, x7), node(x8, x9, x10), s(s(s(x11)))))
    
  
  
• IF(false, false, cons(z0, z1), node(z2, z3, z4), s(s(z5))) → LESSE(cons(z0, z1), node(z2, z3, z4), s(s(s(z5))))
  
  • (IF(false, false, cons(x18, cons(x78, cons(x381, x380))), node(x20, x21, x22), s(s(0)))≥LESSE(cons(x18, cons(x78, cons(x381, x380))), node(x20, x21, x22), s(s(s(0)))))
    
  • (IF(false, false, cons(x18, x77), node(x20, x21, x22), s(s(x266)))≥LESSE(cons(x18, x77), node(x20, x21, x22), s(s(s(x266)))) ⇒ IF(false, false, cons(x18, cons(x78, x77)), node(x20, x21, x22), s(s(s(x266))))≥LESSE(cons(x18, cons(x78, x77)), node(x20, x21, x22), s(s(s(s(x266))))))
    
  
  

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(IF(x₁, x₂, x₃, x₄, x₅)) = 1 - x₁ - x₂ + x₃ - x₄ - x₅   
POL(LESSE(x₁, x₂, x₃)) = -1 + x₁ + x₂ - x₃   
POL(append(x₁, x₂)) = 0   
POL(c) = -2   
POL(cons(x₁, x₂)) = 1 + x₂   
POL(false) = 0   
POL(le(x₁, x₂)) = 0   
POL(leaf) = 0   
POL(length(x₁)) = 0   
POL(nil) = 0   
POL(node(x₁, x₂, x₃)) = 1   
POL(s(x₁)) = 1 + x₁   
POL(toList(x₁)) = 0   
POL(true) = 1   

The following pairs are in P_>:

IF(false, false, cons(z0, z1), node(z2, z3, z4), s(s(z5))) → LESSE(cons(z0, z1), node(z2, z3, z4), s(s(s(z5))))

The following pairs are in P_bound:

IF(false, false, cons(z0, z1), node(z2, z3, z4), s(s(z5))) → LESSE(cons(z0, z1), node(z2, z3, z4), s(s(s(z5))))

The following rules are usable:

le(n, m) → le(s(n), s(m))
true → le(0, m)
false → le(s(n), 0)

(67) Obligation:

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

LESSE(cons(z0, z1), node(z2, z3, z4), s(s(z5))) → IF(le(length(z1), s(z5)), le(length(append(toList(z2), cons(z3, toList(z4)))), s(s(z5))), cons(z0, z1), node(z2, z3, z4), s(s(z5)))

The TRS R consists of the following rules:

length(nil) → 0
length(cons(n, l)) → s(length(l))
le(s(n), 0) → false
le(0, m) → true
le(s(n), s(m)) → le(n, m)
toList(leaf) → nil
toList(node(t1, n, t2)) → append(toList(t1), cons(n, toList(t2)))
append(nil, l2) → l2
append(cons(n, l1), l2) → cons(n, append(l1, l2))

The set Q consists of the following terms:

length(nil)
length(cons(x0, x1))
toList(leaf)
toList(node(x0, x1, x2))
append(nil, x0)
append(cons(x0, x1), x2)
le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))

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

(68) DependencyGraphProof (EQUIVALENT transformation)

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

(69) TRUE