Termination w.r.t. Q proof of Secret_07_TRS

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

0 QTRS

↳1 AAECC Innermost (⇔, 0 ms)

↳2 QTRS

↳3 DependencyPairsProof (⇔, 0 ms)

↳4 QDP

↳5 DependencyGraphProof (⇔, 0 ms)

↳6 AND

    ↳7 QDP

        ↳8 UsableRulesProof (⇔, 0 ms)

        ↳9 QDP

        ↳10 QReductionProof (⇔, 0 ms)

        ↳11 QDP

        ↳12 QDPSizeChangeProof (⇔, 0 ms)

        ↳13 YES

    ↳14 QDP

        ↳15 UsableRulesProof (⇔, 0 ms)

        ↳16 QDP

        ↳17 QReductionProof (⇔, 0 ms)

        ↳18 QDP

        ↳19 QDPSizeChangeProof (⇔, 0 ms)

        ↳20 YES

    ↳21 QDP

        ↳22 UsableRulesProof (⇔, 0 ms)

        ↳23 QDP

        ↳24 QReductionProof (⇔, 0 ms)

        ↳25 QDP

        ↳26 QDPSizeChangeProof (⇔, 0 ms)

        ↳27 YES

    ↳28 QDP

        ↳29 UsableRulesProof (⇔, 0 ms)

        ↳30 QDP

        ↳31 QReductionProof (⇔, 0 ms)

        ↳32 QDP

        ↳33 QDPSizeChangeProof (⇔, 0 ms)

        ↳34 YES

    ↳35 QDP

        ↳36 UsableRulesProof (⇔, 0 ms)

        ↳37 QDP

        ↳38 QReductionProof (⇔, 0 ms)

        ↳39 QDP

        ↳40 TransformationProof (⇔, 0 ms)

        ↳41 QDP

        ↳42 TransformationProof (⇔, 0 ms)

        ↳43 QDP

        ↳44 DependencyGraphProof (⇔, 0 ms)

        ↳45 QDP

        ↳46 TransformationProof (⇔, 0 ms)

        ↳47 QDP

        ↳48 TransformationProof (⇔, 0 ms)

        ↳49 QDP

        ↳50 TransformationProof (⇔, 0 ms)

        ↳51 QDP

        ↳52 DependencyGraphProof (⇔, 0 ms)

        ↳53 QDP

        ↳54 TransformationProof (⇔, 0 ms)

        ↳55 QDP

        ↳56 TransformationProof (⇔, 0 ms)

        ↳57 QDP

        ↳58 TransformationProof (⇔, 0 ms)

        ↳59 QDP

        ↳60 TransformationProof (⇔, 0 ms)

        ↳61 QDP

        ↳62 TransformationProof (⇔, 0 ms)

        ↳63 QDP

        ↳64 NonInfProof (⇔, 68 ms)

        ↳65 AND

            ↳66 QDP

                ↳67 DependencyGraphProof (⇔, 0 ms)

                ↳68 TRUE

            ↳69 QDP

                ↳70 DependencyGraphProof (⇔, 0 ms)

                ↳71 TRUE

(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 {a, c, 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) YES

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

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

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

(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) TransformationProof (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(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) → LESSE(cons(x0, x1), y1, y2) → IF(le(s(length(x1)), y2), le(length(toList(y1)), y2), cons(x0, x1), y1, y2)

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

(42) TransformationProof (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) → LESSE(nil, y1, y2) → IF(true, le(length(toList(y1)), y2), nil, 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(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.

(44) DependencyGraphProof (EQUIVALENT transformation)

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

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

(46) TransformationProof (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), 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) → 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)

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

(48) TransformationProof (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) → LESSE(cons(y0, y1), leaf, y3) → IF(le(s(length(y1)), y3), le(0, y3), cons(y0, y1), leaf, 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), 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.

(50) TransformationProof (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) → LESSE(cons(y0, y1), leaf, y3) → IF(le(s(length(y1)), y3), true, 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), 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.

(52) DependencyGraphProof (EQUIVALENT transformation)

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

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

(54) TransformationProof (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)) → 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))

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

(56) TransformationProof (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)) → 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))

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

(58) TransformationProof (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))) → IF(false, false, cons(z0, z1), node(z2, z3, z4), s(z5)) → LESSE(cons(z0, z1), node(z2, z3, z4), s(s(z5)))

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

(60) TransformationProof (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))) → 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)))

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

(62) TransformationProof (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)))) → 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))))

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

(64) 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 LESSE(cons(x6, x7), node(x8, x9, x10), s(s(x11))) → IF(le(length(x7), s(x11)), le(length(append(toList(x8), cons(x9, toList(x10)))), s(s(x11))), cons(x6, x7), node(x8, x9, x10), s(s(x11))), IF(false, false, cons(x12, x13), node(x14, x15, x16), s(s(x17))) → LESSE(cons(x12, x13), node(x14, x15, x16), s(s(s(x17)))) which results in the following constraint:

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

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

(2) (length(x7)=x36∧s(x11)=x37∧le(x36, x37)=false∧length(x40)=x38∧s(s(x11))=x39∧le(x38, x39)=false ⇒ LESSE(cons(x6, x7), node(x8, x9, x10), s(s(x11)))≥IF(le(length(x7), s(x11)), le(length(append(toList(x8), cons(x9, toList(x10)))), s(s(x11))), cons(x6, x7), node(x8, x9, x10), s(s(x11))))

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

(3) (false=false∧length(x7)=s(x43)∧s(x11)=0∧length(x40)=x38∧s(s(x11))=x39∧le(x38, x39)=false ⇒ LESSE(cons(x6, x7), node(x8, x9, x10), s(s(x11)))≥IF(le(length(x7), s(x11)), le(length(append(toList(x8), cons(x9, toList(x10)))), s(s(x11))), cons(x6, x7), node(x8, x9, x10), s(s(x11))))

(4) (le(x46, x45)=false∧length(x7)=s(x46)∧s(x11)=s(x45)∧length(x40)=x38∧s(s(x11))=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 ⇒ LESSE(cons(x52, x47), node(x53, x54, x55), s(s(x48)))≥IF(le(length(x47), s(x48)), le(length(append(toList(x53), cons(x54, toList(x55)))), s(s(x48))), cons(x52, x47), node(x53, x54, x55), s(s(x48)))) ⇒ LESSE(cons(x6, x7), node(x8, x9, x10), s(s(x11)))≥IF(le(length(x7), s(x11)), le(length(append(toList(x8), cons(x9, toList(x10)))), s(s(x11))), cons(x6, x7), node(x8, x9, x10), s(s(x11))))

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

(5) (le(x46, x45)=false∧length(x7)=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 ⇒ LESSE(cons(x52, x47), node(x53, x54, x55), s(s(x48)))≥IF(le(length(x47), s(x48)), le(length(append(toList(x53), cons(x54, toList(x55)))), s(s(x48))), cons(x52, x47), node(x53, x54, x55), s(s(x48)))) ⇒ LESSE(cons(x6, x7), node(x8, x9, x10), s(s(x45)))≥IF(le(length(x7), s(x45)), le(length(append(toList(x8), cons(x9, toList(x10)))), s(s(x45))), cons(x6, x7), node(x8, x9, x10), s(s(x45))))

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

(6) (false=false∧le(x46, x45)=false∧length(x7)=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 ⇒ LESSE(cons(x52, x47), node(x53, x54, x55), s(s(x48)))≥IF(le(length(x47), s(x48)), le(length(append(toList(x53), cons(x54, toList(x55)))), s(s(x48))), cons(x52, x47), node(x53, x54, x55), s(s(x48)))) ⇒ LESSE(cons(x6, x7), node(x8, x9, x10), s(s(x45)))≥IF(le(length(x7), s(x45)), le(length(append(toList(x8), cons(x9, toList(x10)))), s(s(x45))), cons(x6, x7), node(x8, x9, x10), s(s(x45))))

(7) (le(x59, x58)=false∧le(x46, x45)=false∧length(x7)=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 ⇒ LESSE(cons(x52, x47), node(x53, x54, x55), s(s(x48)))≥IF(le(length(x47), s(x48)), le(length(append(toList(x53), cons(x54, toList(x55)))), s(s(x48))), cons(x52, x47), node(x53, x54, x55), 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 ⇒ LESSE(cons(x69, x64), node(x70, x71, x72), s(s(x65)))≥IF(le(length(x64), s(x65)), le(length(append(toList(x70), cons(x71, toList(x72)))), s(s(x65))), cons(x69, x64), node(x70, x71, x72), s(s(x65)))) ⇒ LESSE(cons(x73, x62), node(x74, x75, x76), s(s(x61)))≥IF(le(length(x62), s(x61)), le(length(append(toList(x74), cons(x75, toList(x76)))), s(s(x61))), cons(x73, x62), node(x74, x75, x76), s(s(x61)))) ⇒ LESSE(cons(x6, x7), node(x8, x9, x10), s(s(x45)))≥IF(le(length(x7), s(x45)), le(length(append(toList(x8), cons(x9, toList(x10)))), s(s(x45))), cons(x6, x7), node(x8, x9, x10), s(s(x45))))

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

(8) (le(x59, x58)=false∧le(x46, x45)=false∧length(x7)=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 ⇒ LESSE(cons(x52, x47), node(x53, x54, x55), s(s(x48)))≥IF(le(length(x47), s(x48)), le(length(append(toList(x53), cons(x54, toList(x55)))), s(s(x48))), cons(x52, x47), node(x53, x54, x55), 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 ⇒ LESSE(cons(x69, x64), node(x70, x71, x72), s(s(x65)))≥IF(le(length(x64), s(x65)), le(length(append(toList(x70), cons(x71, toList(x72)))), s(s(x65))), cons(x69, x64), node(x70, x71, x72), s(s(x65)))) ⇒ LESSE(cons(x73, x62), node(x74, x75, x76), s(s(x61)))≥IF(le(length(x62), s(x61)), le(length(append(toList(x74), cons(x75, toList(x76)))), s(s(x61))), cons(x73, x62), node(x74, x75, x76), s(s(x61)))) ⇒ LESSE(cons(x6, x7), node(x8, x9, x10), s(s(x45)))≥IF(le(length(x7), s(x45)), le(length(append(toList(x8), cons(x9, toList(x10)))), s(s(x45))), cons(x6, x7), node(x8, x9, x10), s(s(x45))))

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

(9) (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 ⇒ LESSE(cons(x52, x47), node(x53, x54, x55), s(s(x48)))≥IF(le(length(x47), s(x48)), le(length(append(toList(x53), cons(x54, toList(x55)))), s(s(x48))), cons(x52, x47), node(x53, x54, x55), 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 ⇒ LESSE(cons(x69, x64), node(x70, x71, x72), s(s(x65)))≥IF(le(length(x64), s(x65)), le(length(append(toList(x70), cons(x71, toList(x72)))), s(s(x65))), cons(x69, x64), node(x70, x71, x72), s(s(x65)))) ⇒ LESSE(cons(x73, x62), node(x74, x75, x76), s(s(x61)))≥IF(le(length(x62), s(x61)), le(length(append(toList(x74), cons(x75, toList(x76)))), s(s(x61))), cons(x73, x62), node(x74, x75, x76), 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 ⇒ LESSE(cons(x89, x84), node(x90, x91, x92), s(s(x85)))≥IF(le(length(x84), s(x85)), le(length(append(toList(x90), cons(x91, toList(x92)))), s(s(x85))), cons(x89, x84), node(x90, x91, x92), 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 ⇒ LESSE(cons(x102, x97), node(x103, x104, x105), s(s(x98)))≥IF(le(length(x97), s(x98)), le(length(append(toList(x103), cons(x104, toList(x105)))), s(s(x98))), cons(x102, x97), node(x103, x104, x105), s(s(x98)))) ⇒ LESSE(cons(x106, x95), node(x107, x108, x109), s(s(x94)))≥IF(le(length(x95), s(x94)), le(length(append(toList(x107), cons(x108, toList(x109)))), s(s(x94))), cons(x106, x95), node(x107, x108, x109), s(s(x94)))) ⇒ LESSE(cons(x110, x77), node(x111, x112, x113), s(s(x82)))≥IF(le(length(x77), s(x82)), le(length(append(toList(x111), cons(x112, toList(x113)))), s(s(x82))), cons(x110, x77), node(x111, x112, x113), s(s(x82)))) ⇒ LESSE(cons(x6, cons(x78, x77)), node(x8, x9, x10), s(s(x45)))≥IF(le(length(cons(x78, x77)), s(x45)), le(length(append(toList(x8), cons(x9, toList(x10)))), s(s(x45))), cons(x6, cons(x78, x77)), node(x8, x9, x10), s(s(x45))))

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

(10) (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 ⇒ LESSE(cons(x52, x47), node(x53, x54, x55), s(s(x48)))≥IF(le(length(x47), s(x48)), le(length(append(toList(x53), cons(x54, toList(x55)))), s(s(x48))), cons(x52, x47), node(x53, x54, x55), 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 ⇒ LESSE(cons(x69, x64), node(x70, x71, x72), s(s(x65)))≥IF(le(length(x64), s(x65)), le(length(append(toList(x70), cons(x71, toList(x72)))), s(s(x65))), cons(x69, x64), node(x70, x71, x72), s(s(x65)))) ⇒ LESSE(cons(x73, x62), node(x74, x75, x76), s(s(x61)))≥IF(le(length(x62), s(x61)), le(length(append(toList(x74), cons(x75, toList(x76)))), s(s(x61))), cons(x73, x62), node(x74, x75, x76), 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 ⇒ LESSE(cons(x89, x84), node(x90, x91, x92), s(s(x85)))≥IF(le(length(x84), s(x85)), le(length(append(toList(x90), cons(x91, toList(x92)))), s(s(x85))), cons(x89, x84), node(x90, x91, x92), 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 ⇒ LESSE(cons(x102, x97), node(x103, x104, x105), s(s(x98)))≥IF(le(length(x97), s(x98)), le(length(append(toList(x103), cons(x104, toList(x105)))), s(s(x98))), cons(x102, x97), node(x103, x104, x105), s(s(x98)))) ⇒ LESSE(cons(x106, x95), node(x107, x108, x109), s(s(x94)))≥IF(le(length(x95), s(x94)), le(length(append(toList(x107), cons(x108, toList(x109)))), s(s(x94))), cons(x106, x95), node(x107, x108, x109), s(s(x94)))) ⇒ LESSE(cons(x110, x77), node(x111, x112, x113), s(s(x82)))≥IF(le(length(x77), s(x82)), le(length(append(toList(x111), cons(x112, toList(x113)))), s(s(x82))), cons(x110, x77), node(x111, x112, x113), s(s(x82)))) ⇒ LESSE(cons(x6, cons(x78, x77)), node(x8, x9, x10), s(s(x45)))≥IF(le(length(cons(x78, x77)), s(x45)), le(length(append(toList(x8), cons(x9, toList(x10)))), s(s(x45))), cons(x6, cons(x78, x77)), node(x8, x9, x10), s(s(x45))))

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

(11) (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 ⇒ LESSE(cons(x52, x47), node(x53, x54, x55), s(s(x48)))≥IF(le(length(x47), s(x48)), le(length(append(toList(x53), cons(x54, toList(x55)))), s(s(x48))), cons(x52, x47), node(x53, x54, x55), 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 ⇒ LESSE(cons(x69, x64), node(x70, x71, x72), s(s(x65)))≥IF(le(length(x64), s(x65)), le(length(append(toList(x70), cons(x71, toList(x72)))), s(s(x65))), cons(x69, x64), node(x70, x71, x72), s(s(x65)))) ⇒ LESSE(cons(x73, x62), node(x74, x75, x76), s(s(x61)))≥IF(le(length(x62), s(x61)), le(length(append(toList(x74), cons(x75, toList(x76)))), s(s(x61))), cons(x73, x62), node(x74, x75, x76), 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 ⇒ LESSE(cons(x89, x84), node(x90, x91, x92), s(s(x85)))≥IF(le(length(x84), s(x85)), le(length(append(toList(x90), cons(x91, toList(x92)))), s(s(x85))), cons(x89, x84), node(x90, x91, x92), 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 ⇒ LESSE(cons(x102, x97), node(x103, x104, x105), s(s(x98)))≥IF(le(length(x97), s(x98)), le(length(append(toList(x103), cons(x104, toList(x105)))), s(s(x98))), cons(x102, x97), node(x103, x104, x105), s(s(x98)))) ⇒ LESSE(cons(x106, x95), node(x107, x108, x109), s(s(x94)))≥IF(le(length(x95), s(x94)), le(length(append(toList(x107), cons(x108, toList(x109)))), s(s(x94))), cons(x106, x95), node(x107, x108, x109), s(s(x94)))) ⇒ LESSE(cons(x110, x77), node(x111, x112, x113), s(s(x82)))≥IF(le(length(x77), s(x82)), le(length(append(toList(x111), cons(x112, toList(x113)))), s(s(x82))), cons(x110, x77), node(x111, x112, x113), 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 ⇒ LESSE(cons(x126, x121), node(x127, x128, x129), s(s(x122)))≥IF(le(length(x121), s(x122)), le(length(append(toList(x127), cons(x128, toList(x129)))), s(s(x122))), cons(x126, x121), node(x127, x128, x129), 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 ⇒ LESSE(cons(x139, x134), node(x140, x141, x142), s(s(x135)))≥IF(le(length(x134), s(x135)), le(length(append(toList(x140), cons(x141, toList(x142)))), s(s(x135))), cons(x139, x134), node(x140, x141, x142), s(s(x135)))) ⇒ LESSE(cons(x143, x132), node(x144, x145, x146), s(s(x131)))≥IF(le(length(x132), s(x131)), le(length(append(toList(x144), cons(x145, toList(x146)))), s(s(x131))), cons(x143, x132), node(x144, x145, x146), 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 ⇒ LESSE(cons(x157, x152), node(x158, x159, x160), s(s(x153)))≥IF(le(length(x152), s(x153)), le(length(append(toList(x158), cons(x159, toList(x160)))), s(s(x153))), cons(x157, x152), node(x158, x159, x160), 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 ⇒ LESSE(cons(x170, x165), node(x171, x172, x173), s(s(x166)))≥IF(le(length(x165), s(x166)), le(length(append(toList(x171), cons(x172, toList(x173)))), s(s(x166))), cons(x170, x165), node(x171, x172, x173), s(s(x166)))) ⇒ LESSE(cons(x174, x163), node(x175, x176, x177), s(s(x162)))≥IF(le(length(x163), s(x162)), le(length(append(toList(x175), cons(x176, toList(x177)))), s(s(x162))), cons(x174, x163), node(x175, x176, x177), s(s(x162)))) ⇒ LESSE(cons(x178, x117), node(x179, x180, x181), s(s(x150)))≥IF(le(length(x117), s(x150)), le(length(append(toList(x179), cons(x180, toList(x181)))), s(s(x150))), cons(x178, x117), node(x179, x180, x181), s(s(x150)))) ⇒ LESSE(cons(x182, cons(x183, x117)), node(x184, x185, x186), s(s(x120)))≥IF(le(length(cons(x183, x117)), s(x120)), le(length(append(toList(x184), cons(x185, toList(x186)))), s(s(x120))), cons(x182, cons(x183, x117)), node(x184, x185, x186), s(s(x120)))) ⇒ LESSE(cons(x6, cons(x78, x77)), node(x8, x9, x10), s(s(x45)))≥IF(le(length(cons(x78, x77)), s(x45)), le(length(append(toList(x8), cons(x9, toList(x10)))), s(s(x45))), cons(x6, cons(x78, x77)), node(x8, x9, x10), s(s(x45))))

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

(12) (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 ⇒ LESSE(cons(x52, x47), node(x53, x54, x55), s(s(x48)))≥IF(le(length(x47), s(x48)), le(length(append(toList(x53), cons(x54, toList(x55)))), s(s(x48))), cons(x52, x47), node(x53, x54, x55), s(s(x48)))) ⇒ LESSE(cons(x6, cons(x78, x77)), node(x8, x9, x10), s(s(x45)))≥IF(le(length(cons(x78, x77)), s(x45)), le(length(append(toList(x8), cons(x9, toList(x10)))), s(s(x45))), cons(x6, cons(x78, x77)), node(x8, x9, x10), s(s(x45))))

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

(13) (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 ⇒ LESSE(cons(x52, x47), node(x53, x54, x55), s(s(x48)))≥IF(le(length(x47), s(x48)), le(length(append(toList(x53), cons(x54, toList(x55)))), s(s(x48))), cons(x52, x47), node(x53, x54, x55), s(s(x48)))) ⇒ LESSE(cons(x6, cons(x78, x77)), node(x8, x9, x10), s(s(x45)))≥IF(le(length(cons(x78, x77)), s(x45)), le(length(append(toList(x8), cons(x9, toList(x10)))), s(s(x45))), cons(x6, cons(x78, x77)), node(x8, x9, x10), s(s(x45))))

(14) (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 ⇒ LESSE(cons(x52, x47), node(x53, x54, x55), s(s(x48)))≥IF(le(length(x47), s(x48)), le(length(append(toList(x53), cons(x54, toList(x55)))), s(s(x48))), cons(x52, x47), node(x53, x54, x55), s(s(x48))))∧(∀x191,x192,x193,x194,x195,x196,x197,x198,x199,x200,x201,x202,x203,x204,x205,x206,x207,x208: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 ⇒ LESSE(cons(x200, x195), node(x201, x202, x203), s(s(x196)))≥IF(le(length(x195), s(x196)), le(length(append(toList(x201), cons(x202, toList(x203)))), s(s(x196))), cons(x200, x195), node(x201, x202, x203), s(s(x196)))) ⇒ LESSE(cons(x204, cons(x205, x192)), node(x206, x207, x208), s(s(x194)))≥IF(le(length(cons(x205, x192)), s(x194)), le(length(append(toList(x206), cons(x207, toList(x208)))), s(s(x194))), cons(x204, cons(x205, x192)), node(x206, x207, x208), s(s(x194)))) ⇒ LESSE(cons(x6, cons(x78, x77)), node(x8, x9, x10), s(s(x45)))≥IF(le(length(cons(x78, x77)), s(x45)), le(length(append(toList(x8), cons(x9, toList(x10)))), s(s(x45))), cons(x6, cons(x78, x77)), node(x8, x9, x10), s(s(x45))))

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

(15) (le(x190, x189)=false∧length(x114)=s(x190)∧length(x77)=x46∧le(x46, x45)=false∧x45=x189 ⇒ LESSE(cons(x6, cons(x78, x77)), node(x8, x9, x10), s(s(x45)))≥IF(le(length(cons(x78, x77)), s(x45)), le(length(append(toList(x8), cons(x9, toList(x10)))), s(s(x45))), cons(x6, cons(x78, x77)), node(x8, x9, x10), s(s(x45))))

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

(16) (false=false∧le(x190, x189)=false∧length(x114)=s(x190)∧length(x77)=s(x209)∧0=x189 ⇒ LESSE(cons(x6, cons(x78, x77)), node(x8, x9, x10), s(s(0)))≥IF(le(length(cons(x78, x77)), s(0)), le(length(append(toList(x8), cons(x9, toList(x10)))), s(s(0))), cons(x6, cons(x78, x77)), node(x8, x9, x10), s(s(0))))

(17) (le(x212, x211)=false∧le(x190, x189)=false∧length(x114)=s(x190)∧length(x77)=s(x212)∧s(x211)=x189∧(∀x213,x214,x215,x216,x217,x218,x219,x220,x221:le(x212, x211)=false∧le(x213, x214)=false∧length(x215)=s(x213)∧length(x216)=x212∧x211=x214 ⇒ LESSE(cons(x217, cons(x218, x216)), node(x219, x220, x221), s(s(x211)))≥IF(le(length(cons(x218, x216)), s(x211)), le(length(append(toList(x219), cons(x220, toList(x221)))), s(s(x211))), cons(x217, cons(x218, x216)), node(x219, x220, x221), s(s(x211)))) ⇒ LESSE(cons(x6, cons(x78, x77)), node(x8, x9, x10), s(s(s(x211))))≥IF(le(length(cons(x78, x77)), s(s(x211))), le(length(append(toList(x8), cons(x9, toList(x10)))), s(s(s(x211)))), cons(x6, cons(x78, x77)), node(x8, x9, x10), s(s(s(x211)))))

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

(18) (le(x190, x189)=false∧length(x114)=s(x190)∧length(x77)=s(x209)∧0=x189 ⇒ LESSE(cons(x6, cons(x78, x77)), node(x8, x9, x10), s(s(0)))≥IF(le(length(cons(x78, x77)), s(0)), le(length(append(toList(x8), cons(x9, toList(x10)))), s(s(0))), cons(x6, cons(x78, x77)), node(x8, x9, x10), s(s(0))))

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

(19) (s(length(x302))=s(x190)∧le(x212, x211)=false∧le(x190, x189)=false∧length(x77)=s(x212)∧s(x211)=x189∧(∀x213,x214,x215,x216,x217,x218,x219,x220,x221:le(x212, x211)=false∧le(x213, x214)=false∧length(x215)=s(x213)∧length(x216)=x212∧x211=x214 ⇒ LESSE(cons(x217, cons(x218, x216)), node(x219, x220, x221), s(s(x211)))≥IF(le(length(cons(x218, x216)), s(x211)), le(length(append(toList(x219), cons(x220, toList(x221)))), s(s(x211))), cons(x217, cons(x218, x216)), node(x219, x220, x221), s(s(x211))))∧(∀x304,x305,x306,x307,x308,x309,x310,x311,x312,x313,x314,x315,x316,x317,x318,x319,x320,x321,x322:length(x302)=s(x304)∧le(x305, x306)=false∧le(x304, x307)=false∧length(x308)=s(x305)∧s(x306)=x307∧(∀x309,x310,x311,x312,x313,x314,x315,x316,x317:le(x305, x306)=false∧le(x309, x310)=false∧length(x311)=s(x309)∧length(x312)=x305∧x306=x310 ⇒ LESSE(cons(x313, cons(x314, x312)), node(x315, x316, x317), s(s(x306)))≥IF(le(length(cons(x314, x312)), s(x306)), le(length(append(toList(x315), cons(x316, toList(x317)))), s(s(x306))), cons(x313, cons(x314, x312)), node(x315, x316, x317), s(s(x306)))) ⇒ LESSE(cons(x318, cons(x319, x308)), node(x320, x321, x322), s(s(s(x306))))≥IF(le(length(cons(x319, x308)), s(s(x306))), le(length(append(toList(x320), cons(x321, toList(x322)))), s(s(s(x306)))), cons(x318, cons(x319, x308)), node(x320, x321, x322), s(s(s(x306))))) ⇒ LESSE(cons(x6, cons(x78, x77)), node(x8, x9, x10), s(s(s(x211))))≥IF(le(length(cons(x78, x77)), s(s(x211))), le(length(append(toList(x8), cons(x9, toList(x10)))), s(s(s(x211)))), cons(x6, cons(x78, x77)), node(x8, x9, x10), s(s(s(x211)))))

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

(20) (s(length(x222))=s(x190)∧le(x190, x189)=false∧length(x77)=s(x209)∧0=x189∧(∀x224,x225,x226,x227,x228,x229,x230,x231,x232:length(x222)=s(x224)∧le(x224, x225)=false∧length(x226)=s(x227)∧0=x225 ⇒ LESSE(cons(x228, cons(x229, x226)), node(x230, x231, x232), s(s(0)))≥IF(le(length(cons(x229, x226)), s(0)), le(length(append(toList(x230), cons(x231, toList(x232)))), s(s(0))), cons(x228, cons(x229, x226)), node(x230, x231, x232), s(s(0)))) ⇒ LESSE(cons(x6, cons(x78, x77)), node(x8, x9, x10), s(s(0)))≥IF(le(length(cons(x78, x77)), s(0)), le(length(append(toList(x8), cons(x9, toList(x10)))), s(s(0))), cons(x6, cons(x78, x77)), node(x8, x9, x10), s(s(0))))

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

(21) (length(x222)=x190∧le(x190, x189)=false∧length(x77)=s(x209)∧0=x189∧(∀x224,x225,x226,x227,x228,x229,x230,x231,x232:length(x222)=s(x224)∧le(x224, x225)=false∧length(x226)=s(x227)∧0=x225 ⇒ LESSE(cons(x228, cons(x229, x226)), node(x230, x231, x232), s(s(0)))≥IF(le(length(cons(x229, x226)), s(0)), le(length(append(toList(x230), cons(x231, toList(x232)))), s(s(0))), cons(x228, cons(x229, x226)), node(x230, x231, x232), s(s(0)))) ⇒ LESSE(cons(x6, cons(x78, x77)), node(x8, x9, x10), s(s(0)))≥IF(le(length(cons(x78, x77)), s(0)), le(length(append(toList(x8), cons(x9, toList(x10)))), s(s(0))), cons(x6, cons(x78, x77)), node(x8, x9, x10), s(s(0))))

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

(22) (s(length(x233))=s(x209)∧length(x222)=x190∧le(x190, x189)=false∧0=x189∧(∀x224,x225,x226,x227,x228,x229,x230,x231,x232:length(x222)=s(x224)∧le(x224, x225)=false∧length(x226)=s(x227)∧0=x225 ⇒ LESSE(cons(x228, cons(x229, x226)), node(x230, x231, x232), s(s(0)))≥IF(le(length(cons(x229, x226)), s(0)), le(length(append(toList(x230), cons(x231, toList(x232)))), s(s(0))), cons(x228, cons(x229, x226)), node(x230, x231, x232), s(s(0))))∧(∀x235,x236,x237,x238,x239,x240,x241,x242,x243,x244,x245,x246,x247,x248,x249,x250,x251,x252:length(x233)=s(x235)∧length(x236)=x237∧le(x237, x238)=false∧0=x238∧(∀x239,x240,x241,x242,x243,x244,x245,x246,x247:length(x236)=s(x239)∧le(x239, x240)=false∧length(x241)=s(x242)∧0=x240 ⇒ LESSE(cons(x243, cons(x244, x241)), node(x245, x246, x247), s(s(0)))≥IF(le(length(cons(x244, x241)), s(0)), le(length(append(toList(x245), cons(x246, toList(x247)))), s(s(0))), cons(x243, cons(x244, x241)), node(x245, x246, x247), s(s(0)))) ⇒ LESSE(cons(x248, cons(x249, x233)), node(x250, x251, x252), s(s(0)))≥IF(le(length(cons(x249, x233)), s(0)), le(length(append(toList(x250), cons(x251, toList(x252)))), s(s(0))), cons(x248, cons(x249, x233)), node(x250, x251, x252), s(s(0)))) ⇒ LESSE(cons(x6, cons(x78, cons(x234, x233))), node(x8, x9, x10), s(s(0)))≥IF(le(length(cons(x78, cons(x234, x233))), s(0)), le(length(append(toList(x8), cons(x9, toList(x10)))), s(s(0))), cons(x6, cons(x78, cons(x234, x233))), node(x8, x9, x10), s(s(0))))

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

(23) (length(x222)=x190∧le(x190, x189)=false∧0=x189∧(∀x224,x225,x226,x227,x228,x229,x230,x231,x232:length(x222)=s(x224)∧le(x224, x225)=false∧length(x226)=s(x227)∧0=x225 ⇒ LESSE(cons(x228, cons(x229, x226)), node(x230, x231, x232), s(s(0)))≥IF(le(length(cons(x229, x226)), s(0)), le(length(append(toList(x230), cons(x231, toList(x232)))), s(s(0))), cons(x228, cons(x229, x226)), node(x230, x231, x232), s(s(0))))∧(∀x235,x236,x237,x238,x239,x240,x241,x242,x243,x244,x245,x246,x247,x248,x249,x250,x251,x252:length(x233)=s(x235)∧length(x236)=x237∧le(x237, x238)=false∧0=x238∧(∀x239,x240,x241,x242,x243,x244,x245,x246,x247:length(x236)=s(x239)∧le(x239, x240)=false∧length(x241)=s(x242)∧0=x240 ⇒ LESSE(cons(x243, cons(x244, x241)), node(x245, x246, x247), s(s(0)))≥IF(le(length(cons(x244, x241)), s(0)), le(length(append(toList(x245), cons(x246, toList(x247)))), s(s(0))), cons(x243, cons(x244, x241)), node(x245, x246, x247), s(s(0)))) ⇒ LESSE(cons(x248, cons(x249, x233)), node(x250, x251, x252), s(s(0)))≥IF(le(length(cons(x249, x233)), s(0)), le(length(append(toList(x250), cons(x251, toList(x252)))), s(s(0))), cons(x248, cons(x249, x233)), node(x250, x251, x252), s(s(0)))) ⇒ LESSE(cons(x6, cons(x78, cons(x234, x233))), node(x8, x9, x10), s(s(0)))≥IF(le(length(cons(x78, cons(x234, x233))), s(0)), le(length(append(toList(x8), cons(x9, toList(x10)))), s(s(0))), cons(x6, cons(x78, cons(x234, x233))), node(x8, x9, x10), s(s(0))))

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

(24) (false=false∧length(x222)=s(x253)∧0=0∧(∀x224,x225,x226,x227,x228,x229,x230,x231,x232:length(x222)=s(x224)∧le(x224, x225)=false∧length(x226)=s(x227)∧0=x225 ⇒ LESSE(cons(x228, cons(x229, x226)), node(x230, x231, x232), s(s(0)))≥IF(le(length(cons(x229, x226)), s(0)), le(length(append(toList(x230), cons(x231, toList(x232)))), s(s(0))), cons(x228, cons(x229, x226)), node(x230, x231, x232), s(s(0))))∧(∀x235,x236,x237,x238,x239,x240,x241,x242,x243,x244,x245,x246,x247,x248,x249,x250,x251,x252:length(x233)=s(x235)∧length(x236)=x237∧le(x237, x238)=false∧0=x238∧(∀x239,x240,x241,x242,x243,x244,x245,x246,x247:length(x236)=s(x239)∧le(x239, x240)=false∧length(x241)=s(x242)∧0=x240 ⇒ LESSE(cons(x243, cons(x244, x241)), node(x245, x246, x247), s(s(0)))≥IF(le(length(cons(x244, x241)), s(0)), le(length(append(toList(x245), cons(x246, toList(x247)))), s(s(0))), cons(x243, cons(x244, x241)), node(x245, x246, x247), s(s(0)))) ⇒ LESSE(cons(x248, cons(x249, x233)), node(x250, x251, x252), s(s(0)))≥IF(le(length(cons(x249, x233)), s(0)), le(length(append(toList(x250), cons(x251, toList(x252)))), s(s(0))), cons(x248, cons(x249, x233)), node(x250, x251, x252), s(s(0)))) ⇒ LESSE(cons(x6, cons(x78, cons(x234, x233))), node(x8, x9, x10), s(s(0)))≥IF(le(length(cons(x78, cons(x234, x233))), s(0)), le(length(append(toList(x8), cons(x9, toList(x10)))), s(s(0))), cons(x6, cons(x78, cons(x234, x233))), node(x8, x9, x10), s(s(0))))

(25) (le(x256, x255)=false∧length(x222)=s(x256)∧0=s(x255)∧(∀x224,x225,x226,x227,x228,x229,x230,x231,x232:length(x222)=s(x224)∧le(x224, x225)=false∧length(x226)=s(x227)∧0=x225 ⇒ LESSE(cons(x228, cons(x229, x226)), node(x230, x231, x232), s(s(0)))≥IF(le(length(cons(x229, x226)), s(0)), le(length(append(toList(x230), cons(x231, toList(x232)))), s(s(0))), cons(x228, cons(x229, x226)), node(x230, x231, x232), s(s(0))))∧(∀x235,x236,x237,x238,x239,x240,x241,x242,x243,x244,x245,x246,x247,x248,x249,x250,x251,x252:length(x233)=s(x235)∧length(x236)=x237∧le(x237, x238)=false∧0=x238∧(∀x239,x240,x241,x242,x243,x244,x245,x246,x247:length(x236)=s(x239)∧le(x239, x240)=false∧length(x241)=s(x242)∧0=x240 ⇒ LESSE(cons(x243, cons(x244, x241)), node(x245, x246, x247), s(s(0)))≥IF(le(length(cons(x244, x241)), s(0)), le(length(append(toList(x245), cons(x246, toList(x247)))), s(s(0))), cons(x243, cons(x244, x241)), node(x245, x246, x247), s(s(0)))) ⇒ LESSE(cons(x248, cons(x249, x233)), node(x250, x251, x252), s(s(0)))≥IF(le(length(cons(x249, x233)), s(0)), le(length(append(toList(x250), cons(x251, toList(x252)))), s(s(0))), cons(x248, cons(x249, x233)), node(x250, x251, x252), s(s(0))))∧(∀x257,x258,x259,x260,x261,x262,x263,x264,x265,x266,x267,x268,x269,x270,x271,x272,x273,x274,x275,x276,x277,x278,x279,x280,x281,x282,x283,x284,x285,x286,x287,x288,x289,x290,x291:le(x256, x255)=false∧length(x257)=x256∧0=x255∧(∀x258,x259,x260,x261,x262,x263,x264,x265,x266:length(x257)=s(x258)∧le(x258, x259)=false∧length(x260)=s(x261)∧0=x259 ⇒ LESSE(cons(x262, cons(x263, x260)), node(x264, x265, x266), s(s(0)))≥IF(le(length(cons(x263, x260)), s(0)), le(length(append(toList(x264), cons(x265, toList(x266)))), s(s(0))), cons(x262, cons(x263, x260)), node(x264, x265, x266), s(s(0))))∧(∀x268,x269,x270,x271,x272,x273,x274,x275,x276,x277,x278,x279,x280,x281,x282,x283,x284,x285:length(x267)=s(x268)∧length(x269)=x270∧le(x270, x271)=false∧0=x271∧(∀x272,x273,x274,x275,x276,x277,x278,x279,x280:length(x269)=s(x272)∧le(x272, x273)=false∧length(x274)=s(x275)∧0=x273 ⇒ LESSE(cons(x276, cons(x277, x274)), node(x278, x279, x280), s(s(0)))≥IF(le(length(cons(x277, x274)), s(0)), le(length(append(toList(x278), cons(x279, toList(x280)))), s(s(0))), cons(x276, cons(x277, x274)), node(x278, x279, x280), s(s(0)))) ⇒ LESSE(cons(x281, cons(x282, x267)), node(x283, x284, x285), s(s(0)))≥IF(le(length(cons(x282, x267)), s(0)), le(length(append(toList(x283), cons(x284, toList(x285)))), s(s(0))), cons(x281, cons(x282, x267)), node(x283, x284, x285), s(s(0)))) ⇒ LESSE(cons(x286, cons(x287, cons(x288, x267))), node(x289, x290, x291), s(s(0)))≥IF(le(length(cons(x287, cons(x288, x267))), s(0)), le(length(append(toList(x289), cons(x290, toList(x291)))), s(s(0))), cons(x286, cons(x287, cons(x288, x267))), node(x289, x290, x291), s(s(0)))) ⇒ LESSE(cons(x6, cons(x78, cons(x234, x233))), node(x8, x9, x10), s(s(0)))≥IF(le(length(cons(x78, cons(x234, x233))), s(0)), le(length(append(toList(x8), cons(x9, toList(x10)))), s(s(0))), cons(x6, cons(x78, cons(x234, x233))), node(x8, x9, x10), s(s(0))))

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

(26) (length(x222)=s(x253) ⇒ LESSE(cons(x6, cons(x78, cons(x234, x233))), node(x8, x9, x10), s(s(0)))≥IF(le(length(cons(x78, cons(x234, x233))), s(0)), le(length(append(toList(x8), cons(x9, toList(x10)))), s(s(0))), cons(x6, cons(x78, cons(x234, x233))), node(x8, x9, x10), s(s(0))))

We solved constraint (25) using rules (I), (II).We simplified constraint (26) using rule (V) (with possible (I) afterwards) using induction on length(x222)=s(x253) which results in the following new constraint:

(27) (s(length(x292))=s(x253)∧(∀x294,x295,x296,x297,x298,x299,x300,x301:length(x292)=s(x294) ⇒ LESSE(cons(x295, cons(x296, cons(x297, x298))), node(x299, x300, x301), s(s(0)))≥IF(le(length(cons(x296, cons(x297, x298))), s(0)), le(length(append(toList(x299), cons(x300, toList(x301)))), s(s(0))), cons(x295, cons(x296, cons(x297, x298))), node(x299, x300, x301), s(s(0)))) ⇒ LESSE(cons(x6, cons(x78, cons(x234, x233))), node(x8, x9, x10), s(s(0)))≥IF(le(length(cons(x78, cons(x234, x233))), s(0)), le(length(append(toList(x8), cons(x9, toList(x10)))), s(s(0))), cons(x6, cons(x78, cons(x234, x233))), node(x8, x9, x10), s(s(0))))

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

(28) (LESSE(cons(x6, cons(x78, cons(x234, x233))), node(x8, x9, x10), s(s(0)))≥IF(le(length(cons(x78, cons(x234, x233))), s(0)), le(length(append(toList(x8), cons(x9, toList(x10)))), s(s(0))), cons(x6, cons(x78, cons(x234, x233))), node(x8, x9, x10), s(s(0))))

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

(29) (length(x302)=x190∧le(x212, x211)=false∧le(x190, x189)=false∧length(x77)=s(x212)∧s(x211)=x189∧(∀x213,x214,x215,x216,x217,x218,x219,x220,x221:le(x212, x211)=false∧le(x213, x214)=false∧length(x215)=s(x213)∧length(x216)=x212∧x211=x214 ⇒ LESSE(cons(x217, cons(x218, x216)), node(x219, x220, x221), s(s(x211)))≥IF(le(length(cons(x218, x216)), s(x211)), le(length(append(toList(x219), cons(x220, toList(x221)))), s(s(x211))), cons(x217, cons(x218, x216)), node(x219, x220, x221), s(s(x211))))∧(∀x304,x305,x306,x307,x308,x309,x310,x311,x312,x313,x314,x315,x316,x317,x318,x319,x320,x321,x322:length(x302)=s(x304)∧le(x305, x306)=false∧le(x304, x307)=false∧length(x308)=s(x305)∧s(x306)=x307∧(∀x309,x310,x311,x312,x313,x314,x315,x316,x317:le(x305, x306)=false∧le(x309, x310)=false∧length(x311)=s(x309)∧length(x312)=x305∧x306=x310 ⇒ LESSE(cons(x313, cons(x314, x312)), node(x315, x316, x317), s(s(x306)))≥IF(le(length(cons(x314, x312)), s(x306)), le(length(append(toList(x315), cons(x316, toList(x317)))), s(s(x306))), cons(x313, cons(x314, x312)), node(x315, x316, x317), s(s(x306)))) ⇒ LESSE(cons(x318, cons(x319, x308)), node(x320, x321, x322), s(s(s(x306))))≥IF(le(length(cons(x319, x308)), s(s(x306))), le(length(append(toList(x320), cons(x321, toList(x322)))), s(s(s(x306)))), cons(x318, cons(x319, x308)), node(x320, x321, x322), s(s(s(x306))))) ⇒ LESSE(cons(x6, cons(x78, x77)), node(x8, x9, x10), s(s(s(x211))))≥IF(le(length(cons(x78, x77)), s(s(x211))), le(length(append(toList(x8), cons(x9, toList(x10)))), s(s(s(x211)))), cons(x6, cons(x78, x77)), node(x8, x9, x10), s(s(s(x211)))))

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

(30) (s(length(x323))=s(x212)∧length(x302)=x190∧le(x212, x211)=false∧le(x190, x189)=false∧s(x211)=x189∧(∀x213,x214,x215,x216,x217,x218,x219,x220,x221:le(x212, x211)=false∧le(x213, x214)=false∧length(x215)=s(x213)∧length(x216)=x212∧x211=x214 ⇒ LESSE(cons(x217, cons(x218, x216)), node(x219, x220, x221), s(s(x211)))≥IF(le(length(cons(x218, x216)), s(x211)), le(length(append(toList(x219), cons(x220, toList(x221)))), s(s(x211))), cons(x217, cons(x218, x216)), node(x219, x220, x221), s(s(x211))))∧(∀x304,x305,x306,x307,x308,x309,x310,x311,x312,x313,x314,x315,x316,x317,x318,x319,x320,x321,x322:length(x302)=s(x304)∧le(x305, x306)=false∧le(x304, x307)=false∧length(x308)=s(x305)∧s(x306)=x307∧(∀x309,x310,x311,x312,x313,x314,x315,x316,x317:le(x305, x306)=false∧le(x309, x310)=false∧length(x311)=s(x309)∧length(x312)=x305∧x306=x310 ⇒ LESSE(cons(x313, cons(x314, x312)), node(x315, x316, x317), s(s(x306)))≥IF(le(length(cons(x314, x312)), s(x306)), le(length(append(toList(x315), cons(x316, toList(x317)))), s(s(x306))), cons(x313, cons(x314, x312)), node(x315, x316, x317), s(s(x306)))) ⇒ LESSE(cons(x318, cons(x319, x308)), node(x320, x321, x322), s(s(s(x306))))≥IF(le(length(cons(x319, x308)), s(s(x306))), le(length(append(toList(x320), cons(x321, toList(x322)))), s(s(s(x306)))), cons(x318, cons(x319, x308)), node(x320, x321, x322), s(s(s(x306)))))∧(∀x325,x326,x327,x328,x329,x330,x331,x332,x333,x334,x335,x336,x337,x338,x339,x340,x341,x342,x343,x344,x345,x346,x347,x348,x349,x350,x351,x352,x353,x354,x355,x356,x357,x358,x359,x360,x361,x362:length(x323)=s(x325)∧length(x326)=x327∧le(x325, x328)=false∧le(x327, x329)=false∧s(x328)=x329∧(∀x330,x331,x332,x333,x334,x335,x336,x337,x338:le(x325, x328)=false∧le(x330, x331)=false∧length(x332)=s(x330)∧length(x333)=x325∧x328=x331 ⇒ LESSE(cons(x334, cons(x335, x333)), node(x336, x337, x338), s(s(x328)))≥IF(le(length(cons(x335, x333)), s(x328)), le(length(append(toList(x336), cons(x337, toList(x338)))), s(s(x328))), cons(x334, cons(x335, x333)), node(x336, x337, x338), s(s(x328))))∧(∀x339,x340,x341,x342,x343,x344,x345,x346,x347,x348,x349,x350,x351,x352,x353,x354,x355,x356,x357:length(x326)=s(x339)∧le(x340, x341)=false∧le(x339, x342)=false∧length(x343)=s(x340)∧s(x341)=x342∧(∀x344,x345,x346,x347,x348,x349,x350,x351,x352:le(x340, x341)=false∧le(x344, x345)=false∧length(x346)=s(x344)∧length(x347)=x340∧x341=x345 ⇒ LESSE(cons(x348, cons(x349, x347)), node(x350, x351, x352), s(s(x341)))≥IF(le(length(cons(x349, x347)), s(x341)), le(length(append(toList(x350), cons(x351, toList(x352)))), s(s(x341))), cons(x348, cons(x349, x347)), node(x350, x351, x352), s(s(x341)))) ⇒ LESSE(cons(x353, cons(x354, x343)), node(x355, x356, x357), s(s(s(x341))))≥IF(le(length(cons(x354, x343)), s(s(x341))), le(length(append(toList(x355), cons(x356, toList(x357)))), s(s(s(x341)))), cons(x353, cons(x354, x343)), node(x355, x356, x357), s(s(s(x341))))) ⇒ LESSE(cons(x358, cons(x359, x323)), node(x360, x361, x362), s(s(s(x328))))≥IF(le(length(cons(x359, x323)), s(s(x328))), le(length(append(toList(x360), cons(x361, toList(x362)))), s(s(s(x328)))), cons(x358, cons(x359, x323)), node(x360, x361, x362), s(s(s(x328))))) ⇒ LESSE(cons(x6, cons(x78, cons(x324, x323))), node(x8, x9, x10), s(s(s(x211))))≥IF(le(length(cons(x78, cons(x324, x323))), s(s(x211))), le(length(append(toList(x8), cons(x9, toList(x10)))), s(s(s(x211)))), cons(x6, cons(x78, cons(x324, x323))), node(x8, x9, x10), s(s(s(x211)))))

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

(31) (length(x323)=x212∧length(x302)=x190∧le(x212, x211)=false∧le(x190, x189)=false∧s(x211)=x189 ⇒ LESSE(cons(x6, cons(x78, cons(x324, x323))), node(x8, x9, x10), s(s(s(x211))))≥IF(le(length(cons(x78, cons(x324, x323))), s(s(x211))), le(length(append(toList(x8), cons(x9, toList(x10)))), s(s(s(x211)))), cons(x6, cons(x78, cons(x324, x323))), node(x8, x9, x10), s(s(s(x211)))))

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

(32) (false=false∧length(x323)=s(x363)∧length(x302)=x190∧le(x190, x189)=false∧s(0)=x189 ⇒ LESSE(cons(x6, cons(x78, cons(x324, x323))), node(x8, x9, x10), s(s(s(0))))≥IF(le(length(cons(x78, cons(x324, x323))), s(s(0))), le(length(append(toList(x8), cons(x9, toList(x10)))), s(s(s(0)))), cons(x6, cons(x78, cons(x324, x323))), node(x8, x9, x10), s(s(s(0)))))

(33) (le(x366, x365)=false∧length(x323)=s(x366)∧length(x302)=x190∧le(x190, x189)=false∧s(s(x365))=x189∧(∀x367,x368,x369,x370,x371,x372,x373,x374,x375,x376:le(x366, x365)=false∧length(x367)=x366∧length(x368)=x369∧le(x369, x370)=false∧s(x365)=x370 ⇒ LESSE(cons(x371, cons(x372, cons(x373, x367))), node(x374, x375, x376), s(s(s(x365))))≥IF(le(length(cons(x372, cons(x373, x367))), s(s(x365))), le(length(append(toList(x374), cons(x375, toList(x376)))), s(s(s(x365)))), cons(x371, cons(x372, cons(x373, x367))), node(x374, x375, x376), s(s(s(x365))))) ⇒ LESSE(cons(x6, cons(x78, cons(x324, x323))), node(x8, x9, x10), s(s(s(s(x365)))))≥IF(le(length(cons(x78, cons(x324, x323))), s(s(s(x365)))), le(length(append(toList(x8), cons(x9, toList(x10)))), s(s(s(s(x365))))), cons(x6, cons(x78, cons(x324, x323))), node(x8, x9, x10), s(s(s(s(x365))))))

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

(34) (length(x323)=s(x363)∧length(x302)=x190∧le(x190, x189)=false∧s(0)=x189 ⇒ LESSE(cons(x6, cons(x78, cons(x324, x323))), node(x8, x9, x10), s(s(s(0))))≥IF(le(length(cons(x78, cons(x324, x323))), s(s(0))), le(length(append(toList(x8), cons(x9, toList(x10)))), s(s(s(0)))), cons(x6, cons(x78, cons(x324, x323))), node(x8, x9, x10), s(s(s(0)))))

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

(35) (false=false∧le(x366, x365)=false∧length(x323)=s(x366)∧length(x302)=s(x475)∧s(s(x365))=0∧(∀x367,x368,x369,x370,x371,x372,x373,x374,x375,x376:le(x366, x365)=false∧length(x367)=x366∧length(x368)=x369∧le(x369, x370)=false∧s(x365)=x370 ⇒ LESSE(cons(x371, cons(x372, cons(x373, x367))), node(x374, x375, x376), s(s(s(x365))))≥IF(le(length(cons(x372, cons(x373, x367))), s(s(x365))), le(length(append(toList(x374), cons(x375, toList(x376)))), s(s(s(x365)))), cons(x371, cons(x372, cons(x373, x367))), node(x374, x375, x376), s(s(s(x365))))) ⇒ LESSE(cons(x6, cons(x78, cons(x324, x323))), node(x8, x9, x10), s(s(s(s(x365)))))≥IF(le(length(cons(x78, cons(x324, x323))), s(s(s(x365)))), le(length(append(toList(x8), cons(x9, toList(x10)))), s(s(s(s(x365))))), cons(x6, cons(x78, cons(x324, x323))), node(x8, x9, x10), s(s(s(s(x365))))))

(36) (le(x478, x477)=false∧le(x366, x365)=false∧length(x323)=s(x366)∧length(x302)=s(x478)∧s(s(x365))=s(x477)∧(∀x367,x368,x369,x370,x371,x372,x373,x374,x375,x376:le(x366, x365)=false∧length(x367)=x366∧length(x368)=x369∧le(x369, x370)=false∧s(x365)=x370 ⇒ LESSE(cons(x371, cons(x372, cons(x373, x367))), node(x374, x375, x376), s(s(s(x365))))≥IF(le(length(cons(x372, cons(x373, x367))), s(s(x365))), le(length(append(toList(x374), cons(x375, toList(x376)))), s(s(s(x365)))), cons(x371, cons(x372, cons(x373, x367))), node(x374, x375, x376), s(s(s(x365)))))∧(∀x479,x480,x481,x482,x483,x484,x485,x486,x487,x488,x489,x490,x491,x492,x493,x494,x495,x496,x497,x498:le(x478, x477)=false∧le(x479, x480)=false∧length(x481)=s(x479)∧length(x482)=x478∧s(s(x480))=x477∧(∀x483,x484,x485,x486,x487,x488,x489,x490,x491,x492:le(x479, x480)=false∧length(x483)=x479∧length(x484)=x485∧le(x485, x486)=false∧s(x480)=x486 ⇒ LESSE(cons(x487, cons(x488, cons(x489, x483))), node(x490, x491, x492), s(s(s(x480))))≥IF(le(length(cons(x488, cons(x489, x483))), s(s(x480))), le(length(append(toList(x490), cons(x491, toList(x492)))), s(s(s(x480)))), cons(x487, cons(x488, cons(x489, x483))), node(x490, x491, x492), s(s(s(x480))))) ⇒ LESSE(cons(x493, cons(x494, cons(x495, x481))), node(x496, x497, x498), s(s(s(s(x480)))))≥IF(le(length(cons(x494, cons(x495, x481))), s(s(s(x480)))), le(length(append(toList(x496), cons(x497, toList(x498)))), s(s(s(s(x480))))), cons(x493, cons(x494, cons(x495, x481))), node(x496, x497, x498), s(s(s(s(x480)))))) ⇒ LESSE(cons(x6, cons(x78, cons(x324, x323))), node(x8, x9, x10), s(s(s(s(x365)))))≥IF(le(length(cons(x78, cons(x324, x323))), s(s(s(x365)))), le(length(append(toList(x8), cons(x9, toList(x10)))), s(s(s(s(x365))))), cons(x6, cons(x78, cons(x324, x323))), node(x8, x9, x10), s(s(s(s(x365))))))

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

(37) (false=false∧length(x323)=s(x363)∧length(x302)=s(x377)∧s(0)=0 ⇒ LESSE(cons(x6, cons(x78, cons(x324, x323))), node(x8, x9, x10), s(s(s(0))))≥IF(le(length(cons(x78, cons(x324, x323))), s(s(0))), le(length(append(toList(x8), cons(x9, toList(x10)))), s(s(s(0)))), cons(x6, cons(x78, cons(x324, x323))), node(x8, x9, x10), s(s(s(0)))))

(38) (le(x380, x379)=false∧length(x323)=s(x363)∧length(x302)=s(x380)∧s(0)=s(x379)∧(∀x381,x382,x383,x384,x385,x386,x387,x388,x389:le(x380, x379)=false∧length(x381)=s(x382)∧length(x383)=x380∧s(0)=x379 ⇒ LESSE(cons(x384, cons(x385, cons(x386, x381))), node(x387, x388, x389), s(s(s(0))))≥IF(le(length(cons(x385, cons(x386, x381))), s(s(0))), le(length(append(toList(x387), cons(x388, toList(x389)))), s(s(s(0)))), cons(x384, cons(x385, cons(x386, x381))), node(x387, x388, x389), s(s(s(0))))) ⇒ LESSE(cons(x6, cons(x78, cons(x324, x323))), node(x8, x9, x10), s(s(s(0))))≥IF(le(length(cons(x78, cons(x324, x323))), s(s(0))), le(length(append(toList(x8), cons(x9, toList(x10)))), s(s(s(0)))), cons(x6, cons(x78, cons(x324, x323))), node(x8, x9, x10), s(s(s(0)))))

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

(39) (le(x380, x379)=false∧length(x323)=s(x363)∧length(x302)=s(x380)∧0=x379∧(∀x381,x382,x383,x384,x385,x386,x387,x388,x389:le(x380, x379)=false∧length(x381)=s(x382)∧length(x383)=x380∧s(0)=x379 ⇒ LESSE(cons(x384, cons(x385, cons(x386, x381))), node(x387, x388, x389), s(s(s(0))))≥IF(le(length(cons(x385, cons(x386, x381))), s(s(0))), le(length(append(toList(x387), cons(x388, toList(x389)))), s(s(s(0)))), cons(x384, cons(x385, cons(x386, x381))), node(x387, x388, x389), s(s(s(0))))) ⇒ LESSE(cons(x6, cons(x78, cons(x324, x323))), node(x8, x9, x10), s(s(s(0))))≥IF(le(length(cons(x78, cons(x324, x323))), s(s(0))), le(length(append(toList(x8), cons(x9, toList(x10)))), s(s(s(0)))), cons(x6, cons(x78, cons(x324, x323))), node(x8, x9, x10), s(s(s(0)))))

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

(40) (s(length(x390))=s(x363)∧le(x380, x379)=false∧length(x302)=s(x380)∧0=x379∧(∀x381,x382,x383,x384,x385,x386,x387,x388,x389:le(x380, x379)=false∧length(x381)=s(x382)∧length(x383)=x380∧s(0)=x379 ⇒ LESSE(cons(x384, cons(x385, cons(x386, x381))), node(x387, x388, x389), s(s(s(0))))≥IF(le(length(cons(x385, cons(x386, x381))), s(s(0))), le(length(append(toList(x387), cons(x388, toList(x389)))), s(s(s(0)))), cons(x384, cons(x385, cons(x386, x381))), node(x387, x388, x389), s(s(s(0)))))∧(∀x392,x393,x394,x395,x396,x397,x398,x399,x400,x401,x402,x403,x404,x405,x406,x407,x408,x409,x410:length(x390)=s(x392)∧le(x393, x394)=false∧length(x395)=s(x393)∧0=x394∧(∀x396,x397,x398,x399,x400,x401,x402,x403,x404:le(x393, x394)=false∧length(x396)=s(x397)∧length(x398)=x393∧s(0)=x394 ⇒ LESSE(cons(x399, cons(x400, cons(x401, x396))), node(x402, x403, x404), s(s(s(0))))≥IF(le(length(cons(x400, cons(x401, x396))), s(s(0))), le(length(append(toList(x402), cons(x403, toList(x404)))), s(s(s(0)))), cons(x399, cons(x400, cons(x401, x396))), node(x402, x403, x404), s(s(s(0))))) ⇒ LESSE(cons(x405, cons(x406, cons(x407, x390))), node(x408, x409, x410), s(s(s(0))))≥IF(le(length(cons(x406, cons(x407, x390))), s(s(0))), le(length(append(toList(x408), cons(x409, toList(x410)))), s(s(s(0)))), cons(x405, cons(x406, cons(x407, x390))), node(x408, x409, x410), s(s(s(0))))) ⇒ LESSE(cons(x6, cons(x78, cons(x324, cons(x391, x390)))), node(x8, x9, x10), s(s(s(0))))≥IF(le(length(cons(x78, cons(x324, cons(x391, x390)))), s(s(0))), le(length(append(toList(x8), cons(x9, toList(x10)))), s(s(s(0)))), cons(x6, cons(x78, cons(x324, cons(x391, x390)))), node(x8, x9, x10), s(s(s(0)))))

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

(41) (le(x380, x379)=false∧length(x302)=s(x380)∧0=x379∧(∀x381,x382,x383,x384,x385,x386,x387,x388,x389:le(x380, x379)=false∧length(x381)=s(x382)∧length(x383)=x380∧s(0)=x379 ⇒ LESSE(cons(x384, cons(x385, cons(x386, x381))), node(x387, x388, x389), s(s(s(0))))≥IF(le(length(cons(x385, cons(x386, x381))), s(s(0))), le(length(append(toList(x387), cons(x388, toList(x389)))), s(s(s(0)))), cons(x384, cons(x385, cons(x386, x381))), node(x387, x388, x389), s(s(s(0)))))∧(∀x392,x393,x394,x395,x396,x397,x398,x399,x400,x401,x402,x403,x404,x405,x406,x407,x408,x409,x410:length(x390)=s(x392)∧le(x393, x394)=false∧length(x395)=s(x393)∧0=x394∧(∀x396,x397,x398,x399,x400,x401,x402,x403,x404:le(x393, x394)=false∧length(x396)=s(x397)∧length(x398)=x393∧s(0)=x394 ⇒ LESSE(cons(x399, cons(x400, cons(x401, x396))), node(x402, x403, x404), s(s(s(0))))≥IF(le(length(cons(x400, cons(x401, x396))), s(s(0))), le(length(append(toList(x402), cons(x403, toList(x404)))), s(s(s(0)))), cons(x399, cons(x400, cons(x401, x396))), node(x402, x403, x404), s(s(s(0))))) ⇒ LESSE(cons(x405, cons(x406, cons(x407, x390))), node(x408, x409, x410), s(s(s(0))))≥IF(le(length(cons(x406, cons(x407, x390))), s(s(0))), le(length(append(toList(x408), cons(x409, toList(x410)))), s(s(s(0)))), cons(x405, cons(x406, cons(x407, x390))), node(x408, x409, x410), s(s(s(0))))) ⇒ LESSE(cons(x6, cons(x78, cons(x324, cons(x391, x390)))), node(x8, x9, x10), s(s(s(0))))≥IF(le(length(cons(x78, cons(x324, cons(x391, x390)))), s(s(0))), le(length(append(toList(x8), cons(x9, toList(x10)))), s(s(s(0)))), cons(x6, cons(x78, cons(x324, cons(x391, x390)))), node(x8, x9, x10), s(s(s(0)))))

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

(42) (s(length(x411))=s(x380)∧le(x380, x379)=false∧0=x379∧(∀x381,x382,x383,x384,x385,x386,x387,x388,x389:le(x380, x379)=false∧length(x381)=s(x382)∧length(x383)=x380∧s(0)=x379 ⇒ LESSE(cons(x384, cons(x385, cons(x386, x381))), node(x387, x388, x389), s(s(s(0))))≥IF(le(length(cons(x385, cons(x386, x381))), s(s(0))), le(length(append(toList(x387), cons(x388, toList(x389)))), s(s(s(0)))), cons(x384, cons(x385, cons(x386, x381))), node(x387, x388, x389), s(s(s(0)))))∧(∀x392,x393,x394,x395,x396,x397,x398,x399,x400,x401,x402,x403,x404,x405,x406,x407,x408,x409,x410:length(x390)=s(x392)∧le(x393, x394)=false∧length(x395)=s(x393)∧0=x394∧(∀x396,x397,x398,x399,x400,x401,x402,x403,x404:le(x393, x394)=false∧length(x396)=s(x397)∧length(x398)=x393∧s(0)=x394 ⇒ LESSE(cons(x399, cons(x400, cons(x401, x396))), node(x402, x403, x404), s(s(s(0))))≥IF(le(length(cons(x400, cons(x401, x396))), s(s(0))), le(length(append(toList(x402), cons(x403, toList(x404)))), s(s(s(0)))), cons(x399, cons(x400, cons(x401, x396))), node(x402, x403, x404), s(s(s(0))))) ⇒ LESSE(cons(x405, cons(x406, cons(x407, x390))), node(x408, x409, x410), s(s(s(0))))≥IF(le(length(cons(x406, cons(x407, x390))), s(s(0))), le(length(append(toList(x408), cons(x409, toList(x410)))), s(s(s(0)))), cons(x405, cons(x406, cons(x407, x390))), node(x408, x409, x410), s(s(s(0)))))∧(∀x413,x414,x415,x416,x417,x418,x419,x420,x421,x422,x423,x424,x425,x426,x427,x428,x429,x430,x431,x432,x433,x434,x435,x436,x437,x438,x439,x440,x441,x442,x443,x444,x445,x446,x447,x448,x449,x450:length(x411)=s(x413)∧le(x413, x414)=false∧0=x414∧(∀x415,x416,x417,x418,x419,x420,x421,x422,x423:le(x413, x414)=false∧length(x415)=s(x416)∧length(x417)=x413∧s(0)=x414 ⇒ LESSE(cons(x418, cons(x419, cons(x420, x415))), node(x421, x422, x423), s(s(s(0))))≥IF(le(length(cons(x419, cons(x420, x415))), s(s(0))), le(length(append(toList(x421), cons(x422, toList(x423)))), s(s(s(0)))), cons(x418, cons(x419, cons(x420, x415))), node(x421, x422, x423), s(s(s(0)))))∧(∀x425,x426,x427,x428,x429,x430,x431,x432,x433,x434,x435,x436,x437,x438,x439,x440,x441,x442,x443:length(x424)=s(x425)∧le(x426, x427)=false∧length(x428)=s(x426)∧0=x427∧(∀x429,x430,x431,x432,x433,x434,x435,x436,x437:le(x426, x427)=false∧length(x429)=s(x430)∧length(x431)=x426∧s(0)=x427 ⇒ LESSE(cons(x432, cons(x433, cons(x434, x429))), node(x435, x436, x437), s(s(s(0))))≥IF(le(length(cons(x433, cons(x434, x429))), s(s(0))), le(length(append(toList(x435), cons(x436, toList(x437)))), s(s(s(0)))), cons(x432, cons(x433, cons(x434, x429))), node(x435, x436, x437), s(s(s(0))))) ⇒ LESSE(cons(x438, cons(x439, cons(x440, x424))), node(x441, x442, x443), s(s(s(0))))≥IF(le(length(cons(x439, cons(x440, x424))), s(s(0))), le(length(append(toList(x441), cons(x442, toList(x443)))), s(s(s(0)))), cons(x438, cons(x439, cons(x440, x424))), node(x441, x442, x443), s(s(s(0))))) ⇒ LESSE(cons(x444, cons(x445, cons(x446, cons(x447, x424)))), node(x448, x449, x450), s(s(s(0))))≥IF(le(length(cons(x445, cons(x446, cons(x447, x424)))), s(s(0))), le(length(append(toList(x448), cons(x449, toList(x450)))), s(s(s(0)))), cons(x444, cons(x445, cons(x446, cons(x447, x424)))), node(x448, x449, x450), s(s(s(0))))) ⇒ LESSE(cons(x6, cons(x78, cons(x324, cons(x391, x390)))), node(x8, x9, x10), s(s(s(0))))≥IF(le(length(cons(x78, cons(x324, cons(x391, x390)))), s(s(0))), le(length(append(toList(x8), cons(x9, toList(x10)))), s(s(s(0)))), cons(x6, cons(x78, cons(x324, cons(x391, x390)))), node(x8, x9, x10), s(s(s(0)))))

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

(43) (length(x411)=x380∧le(x380, x379)=false∧0=x379 ⇒ LESSE(cons(x6, cons(x78, cons(x324, cons(x391, x390)))), node(x8, x9, x10), s(s(s(0))))≥IF(le(length(cons(x78, cons(x324, cons(x391, x390)))), s(s(0))), le(length(append(toList(x8), cons(x9, toList(x10)))), s(s(s(0)))), cons(x6, cons(x78, cons(x324, cons(x391, x390)))), node(x8, x9, x10), s(s(s(0)))))

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

(44) (false=false∧length(x411)=s(x451)∧0=0 ⇒ LESSE(cons(x6, cons(x78, cons(x324, cons(x391, x390)))), node(x8, x9, x10), s(s(s(0))))≥IF(le(length(cons(x78, cons(x324, cons(x391, x390)))), s(s(0))), le(length(append(toList(x8), cons(x9, toList(x10)))), s(s(s(0)))), cons(x6, cons(x78, cons(x324, cons(x391, x390)))), node(x8, x9, x10), s(s(s(0)))))

(45) (le(x454, x453)=false∧length(x411)=s(x454)∧0=s(x453)∧(∀x455,x456,x457,x458,x459,x460,x461,x462,x463:le(x454, x453)=false∧length(x455)=x454∧0=x453 ⇒ LESSE(cons(x456, cons(x457, cons(x458, cons(x459, x460)))), node(x461, x462, x463), s(s(s(0))))≥IF(le(length(cons(x457, cons(x458, cons(x459, x460)))), s(s(0))), le(length(append(toList(x461), cons(x462, toList(x463)))), s(s(s(0)))), cons(x456, cons(x457, cons(x458, cons(x459, x460)))), node(x461, x462, x463), s(s(s(0))))) ⇒ LESSE(cons(x6, cons(x78, cons(x324, cons(x391, x390)))), node(x8, x9, x10), s(s(s(0))))≥IF(le(length(cons(x78, cons(x324, cons(x391, x390)))), s(s(0))), le(length(append(toList(x8), cons(x9, toList(x10)))), s(s(s(0)))), cons(x6, cons(x78, cons(x324, cons(x391, x390)))), node(x8, x9, x10), s(s(s(0)))))

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

(46) (length(x411)=s(x451) ⇒ LESSE(cons(x6, cons(x78, cons(x324, cons(x391, x390)))), node(x8, x9, x10), s(s(s(0))))≥IF(le(length(cons(x78, cons(x324, cons(x391, x390)))), s(s(0))), le(length(append(toList(x8), cons(x9, toList(x10)))), s(s(s(0)))), cons(x6, cons(x78, cons(x324, cons(x391, x390)))), node(x8, x9, x10), s(s(s(0)))))

We solved constraint (45) using rules (I), (II).We simplified constraint (46) using rule (V) (with possible (I) afterwards) using induction on length(x411)=s(x451) which results in the following new constraint:

(47) (s(length(x464))=s(x451)∧(∀x466,x467,x468,x469,x470,x471,x472,x473,x474:length(x464)=s(x466) ⇒ LESSE(cons(x467, cons(x468, cons(x469, cons(x470, x471)))), node(x472, x473, x474), s(s(s(0))))≥IF(le(length(cons(x468, cons(x469, cons(x470, x471)))), s(s(0))), le(length(append(toList(x472), cons(x473, toList(x474)))), s(s(s(0)))), cons(x467, cons(x468, cons(x469, cons(x470, x471)))), node(x472, x473, x474), s(s(s(0))))) ⇒ LESSE(cons(x6, cons(x78, cons(x324, cons(x391, x390)))), node(x8, x9, x10), s(s(s(0))))≥IF(le(length(cons(x78, cons(x324, cons(x391, x390)))), s(s(0))), le(length(append(toList(x8), cons(x9, toList(x10)))), s(s(s(0)))), cons(x6, cons(x78, cons(x324, cons(x391, x390)))), node(x8, x9, x10), s(s(s(0)))))

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

(48) (LESSE(cons(x6, cons(x78, cons(x324, cons(x391, x390)))), node(x8, x9, x10), s(s(s(0))))≥IF(le(length(cons(x78, cons(x324, cons(x391, x390)))), s(s(0))), le(length(append(toList(x8), cons(x9, toList(x10)))), s(s(s(0)))), cons(x6, cons(x78, cons(x324, cons(x391, x390)))), node(x8, x9, x10), s(s(s(0)))))

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

(49) (le(x478, x477)=false∧le(x366, x365)=false∧length(x323)=s(x366)∧length(x302)=s(x478)∧s(x365)=x477∧(∀x367,x368,x369,x370,x371,x372,x373,x374,x375,x376:le(x366, x365)=false∧length(x367)=x366∧length(x368)=x369∧le(x369, x370)=false∧s(x365)=x370 ⇒ LESSE(cons(x371, cons(x372, cons(x373, x367))), node(x374, x375, x376), s(s(s(x365))))≥IF(le(length(cons(x372, cons(x373, x367))), s(s(x365))), le(length(append(toList(x374), cons(x375, toList(x376)))), s(s(s(x365)))), cons(x371, cons(x372, cons(x373, x367))), node(x374, x375, x376), s(s(s(x365)))))∧(∀x479,x480,x481,x482,x483,x484,x485,x486,x487,x488,x489,x490,x491,x492,x493,x494,x495,x496,x497,x498:le(x478, x477)=false∧le(x479, x480)=false∧length(x481)=s(x479)∧length(x482)=x478∧s(s(x480))=x477∧(∀x483,x484,x485,x486,x487,x488,x489,x490,x491,x492:le(x479, x480)=false∧length(x483)=x479∧length(x484)=x485∧le(x485, x486)=false∧s(x480)=x486 ⇒ LESSE(cons(x487, cons(x488, cons(x489, x483))), node(x490, x491, x492), s(s(s(x480))))≥IF(le(length(cons(x488, cons(x489, x483))), s(s(x480))), le(length(append(toList(x490), cons(x491, toList(x492)))), s(s(s(x480)))), cons(x487, cons(x488, cons(x489, x483))), node(x490, x491, x492), s(s(s(x480))))) ⇒ LESSE(cons(x493, cons(x494, cons(x495, x481))), node(x496, x497, x498), s(s(s(s(x480)))))≥IF(le(length(cons(x494, cons(x495, x481))), s(s(s(x480)))), le(length(append(toList(x496), cons(x497, toList(x498)))), s(s(s(s(x480))))), cons(x493, cons(x494, cons(x495, x481))), node(x496, x497, x498), s(s(s(s(x480)))))) ⇒ LESSE(cons(x6, cons(x78, cons(x324, x323))), node(x8, x9, x10), s(s(s(s(x365)))))≥IF(le(length(cons(x78, cons(x324, x323))), s(s(s(x365)))), le(length(append(toList(x8), cons(x9, toList(x10)))), s(s(s(s(x365))))), cons(x6, cons(x78, cons(x324, x323))), node(x8, x9, x10), s(s(s(s(x365))))))

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

(50) (s(length(x499))=s(x366)∧le(x478, x477)=false∧le(x366, x365)=false∧length(x302)=s(x478)∧s(x365)=x477∧(∀x367,x368,x369,x370,x371,x372,x373,x374,x375,x376:le(x366, x365)=false∧length(x367)=x366∧length(x368)=x369∧le(x369, x370)=false∧s(x365)=x370 ⇒ LESSE(cons(x371, cons(x372, cons(x373, x367))), node(x374, x375, x376), s(s(s(x365))))≥IF(le(length(cons(x372, cons(x373, x367))), s(s(x365))), le(length(append(toList(x374), cons(x375, toList(x376)))), s(s(s(x365)))), cons(x371, cons(x372, cons(x373, x367))), node(x374, x375, x376), s(s(s(x365)))))∧(∀x479,x480,x481,x482,x483,x484,x485,x486,x487,x488,x489,x490,x491,x492,x493,x494,x495,x496,x497,x498:le(x478, x477)=false∧le(x479, x480)=false∧length(x481)=s(x479)∧length(x482)=x478∧s(s(x480))=x477∧(∀x483,x484,x485,x486,x487,x488,x489,x490,x491,x492:le(x479, x480)=false∧length(x483)=x479∧length(x484)=x485∧le(x485, x486)=false∧s(x480)=x486 ⇒ LESSE(cons(x487, cons(x488, cons(x489, x483))), node(x490, x491, x492), s(s(s(x480))))≥IF(le(length(cons(x488, cons(x489, x483))), s(s(x480))), le(length(append(toList(x490), cons(x491, toList(x492)))), s(s(s(x480)))), cons(x487, cons(x488, cons(x489, x483))), node(x490, x491, x492), s(s(s(x480))))) ⇒ LESSE(cons(x493, cons(x494, cons(x495, x481))), node(x496, x497, x498), s(s(s(s(x480)))))≥IF(le(length(cons(x494, cons(x495, x481))), s(s(s(x480)))), le(length(append(toList(x496), cons(x497, toList(x498)))), s(s(s(s(x480))))), cons(x493, cons(x494, cons(x495, x481))), node(x496, x497, x498), s(s(s(s(x480))))))∧(∀x501,x502,x503,x504,x505,x506,x507,x508,x509,x510,x511,x512,x513,x514,x515,x516,x517,x518,x519,x520,x521,x522,x523,x524,x525,x526,x527,x528,x529,x530,x531,x532,x533,x534,x535,x536,x537,x538,x539,x540,x541:length(x499)=s(x501)∧le(x502, x503)=false∧le(x501, x504)=false∧length(x505)=s(x502)∧s(x504)=x503∧(∀x506,x507,x508,x509,x510,x511,x512,x513,x514,x515:le(x501, x504)=false∧length(x506)=x501∧length(x507)=x508∧le(x508, x509)=false∧s(x504)=x509 ⇒ LESSE(cons(x510, cons(x511, cons(x512, x506))), node(x513, x514, x515), s(s(s(x504))))≥IF(le(length(cons(x511, cons(x512, x506))), s(s(x504))), le(length(append(toList(x513), cons(x514, toList(x515)))), s(s(s(x504)))), cons(x510, cons(x511, cons(x512, x506))), node(x513, x514, x515), s(s(s(x504)))))∧(∀x516,x517,x518,x519,x520,x521,x522,x523,x524,x525,x526,x527,x528,x529,x530,x531,x532,x533,x534,x535:le(x502, x503)=false∧le(x516, x517)=false∧length(x518)=s(x516)∧length(x519)=x502∧s(s(x517))=x503∧(∀x520,x521,x522,x523,x524,x525,x526,x527,x528,x529:le(x516, x517)=false∧length(x520)=x516∧length(x521)=x522∧le(x522, x523)=false∧s(x517)=x523 ⇒ LESSE(cons(x524, cons(x525, cons(x526, x520))), node(x527, x528, x529), s(s(s(x517))))≥IF(le(length(cons(x525, cons(x526, x520))), s(s(x517))), le(length(append(toList(x527), cons(x528, toList(x529)))), s(s(s(x517)))), cons(x524, cons(x525, cons(x526, x520))), node(x527, x528, x529), s(s(s(x517))))) ⇒ LESSE(cons(x530, cons(x531, cons(x532, x518))), node(x533, x534, x535), s(s(s(s(x517)))))≥IF(le(length(cons(x531, cons(x532, x518))), s(s(s(x517)))), le(length(append(toList(x533), cons(x534, toList(x535)))), s(s(s(s(x517))))), cons(x530, cons(x531, cons(x532, x518))), node(x533, x534, x535), s(s(s(s(x517)))))) ⇒ LESSE(cons(x536, cons(x537, cons(x538, x499))), node(x539, x540, x541), s(s(s(s(x504)))))≥IF(le(length(cons(x537, cons(x538, x499))), s(s(s(x504)))), le(length(append(toList(x539), cons(x540, toList(x541)))), s(s(s(s(x504))))), cons(x536, cons(x537, cons(x538, x499))), node(x539, x540, x541), s(s(s(s(x504)))))) ⇒ LESSE(cons(x6, cons(x78, cons(x324, cons(x500, x499)))), node(x8, x9, x10), s(s(s(s(x365)))))≥IF(le(length(cons(x78, cons(x324, cons(x500, x499)))), s(s(s(x365)))), le(length(append(toList(x8), cons(x9, toList(x10)))), s(s(s(s(x365))))), cons(x6, cons(x78, cons(x324, cons(x500, x499)))), node(x8, x9, x10), s(s(s(s(x365))))))

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

(51) (length(x499)=x366∧le(x478, x477)=false∧le(x366, x365)=false∧length(x302)=s(x478)∧s(x365)=x477∧(∀x367,x368,x369,x370,x371,x372,x373,x374,x375,x376:le(x366, x365)=false∧length(x367)=x366∧length(x368)=x369∧le(x369, x370)=false∧s(x365)=x370 ⇒ LESSE(cons(x371, cons(x372, cons(x373, x367))), node(x374, x375, x376), s(s(s(x365))))≥IF(le(length(cons(x372, cons(x373, x367))), s(s(x365))), le(length(append(toList(x374), cons(x375, toList(x376)))), s(s(s(x365)))), cons(x371, cons(x372, cons(x373, x367))), node(x374, x375, x376), s(s(s(x365)))))∧(∀x479,x480,x481,x482,x483,x484,x485,x486,x487,x488,x489,x490,x491,x492,x493,x494,x495,x496,x497,x498:le(x478, x477)=false∧le(x479, x480)=false∧length(x481)=s(x479)∧length(x482)=x478∧s(s(x480))=x477∧(∀x483,x484,x485,x486,x487,x488,x489,x490,x491,x492:le(x479, x480)=false∧length(x483)=x479∧length(x484)=x485∧le(x485, x486)=false∧s(x480)=x486 ⇒ LESSE(cons(x487, cons(x488, cons(x489, x483))), node(x490, x491, x492), s(s(s(x480))))≥IF(le(length(cons(x488, cons(x489, x483))), s(s(x480))), le(length(append(toList(x490), cons(x491, toList(x492)))), s(s(s(x480)))), cons(x487, cons(x488, cons(x489, x483))), node(x490, x491, x492), s(s(s(x480))))) ⇒ LESSE(cons(x493, cons(x494, cons(x495, x481))), node(x496, x497, x498), s(s(s(s(x480)))))≥IF(le(length(cons(x494, cons(x495, x481))), s(s(s(x480)))), le(length(append(toList(x496), cons(x497, toList(x498)))), s(s(s(s(x480))))), cons(x493, cons(x494, cons(x495, x481))), node(x496, x497, x498), s(s(s(s(x480))))))∧(∀x501,x502,x503,x504,x505,x506,x507,x508,x509,x510,x511,x512,x513,x514,x515,x516,x517,x518,x519,x520,x521,x522,x523,x524,x525,x526,x527,x528,x529,x530,x531,x532,x533,x534,x535,x536,x537,x538,x539,x540,x541:length(x499)=s(x501)∧le(x502, x503)=false∧le(x501, x504)=false∧length(x505)=s(x502)∧s(x504)=x503∧(∀x506,x507,x508,x509,x510,x511,x512,x513,x514,x515:le(x501, x504)=false∧length(x506)=x501∧length(x507)=x508∧le(x508, x509)=false∧s(x504)=x509 ⇒ LESSE(cons(x510, cons(x511, cons(x512, x506))), node(x513, x514, x515), s(s(s(x504))))≥IF(le(length(cons(x511, cons(x512, x506))), s(s(x504))), le(length(append(toList(x513), cons(x514, toList(x515)))), s(s(s(x504)))), cons(x510, cons(x511, cons(x512, x506))), node(x513, x514, x515), s(s(s(x504)))))∧(∀x516,x517,x518,x519,x520,x521,x522,x523,x524,x525,x526,x527,x528,x529,x530,x531,x532,x533,x534,x535:le(x502, x503)=false∧le(x516, x517)=false∧length(x518)=s(x516)∧length(x519)=x502∧s(s(x517))=x503∧(∀x520,x521,x522,x523,x524,x525,x526,x527,x528,x529:le(x516, x517)=false∧length(x520)=x516∧length(x521)=x522∧le(x522, x523)=false∧s(x517)=x523 ⇒ LESSE(cons(x524, cons(x525, cons(x526, x520))), node(x527, x528, x529), s(s(s(x517))))≥IF(le(length(cons(x525, cons(x526, x520))), s(s(x517))), le(length(append(toList(x527), cons(x528, toList(x529)))), s(s(s(x517)))), cons(x524, cons(x525, cons(x526, x520))), node(x527, x528, x529), s(s(s(x517))))) ⇒ LESSE(cons(x530, cons(x531, cons(x532, x518))), node(x533, x534, x535), s(s(s(s(x517)))))≥IF(le(length(cons(x531, cons(x532, x518))), s(s(s(x517)))), le(length(append(toList(x533), cons(x534, toList(x535)))), s(s(s(s(x517))))), cons(x530, cons(x531, cons(x532, x518))), node(x533, x534, x535), s(s(s(s(x517)))))) ⇒ LESSE(cons(x536, cons(x537, cons(x538, x499))), node(x539, x540, x541), s(s(s(s(x504)))))≥IF(le(length(cons(x537, cons(x538, x499))), s(s(s(x504)))), le(length(append(toList(x539), cons(x540, toList(x541)))), s(s(s(s(x504))))), cons(x536, cons(x537, cons(x538, x499))), node(x539, x540, x541), s(s(s(s(x504)))))) ⇒ LESSE(cons(x6, cons(x78, cons(x324, cons(x500, x499)))), node(x8, x9, x10), s(s(s(s(x365)))))≥IF(le(length(cons(x78, cons(x324, cons(x500, x499)))), s(s(s(x365)))), le(length(append(toList(x8), cons(x9, toList(x10)))), s(s(s(s(x365))))), cons(x6, cons(x78, cons(x324, cons(x500, x499)))), node(x8, x9, x10), s(s(s(s(x365))))))

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

(52) (s(length(x542))=s(x478)∧length(x499)=x366∧le(x478, x477)=false∧le(x366, x365)=false∧s(x365)=x477∧(∀x367,x368,x369,x370,x371,x372,x373,x374,x375,x376:le(x366, x365)=false∧length(x367)=x366∧length(x368)=x369∧le(x369, x370)=false∧s(x365)=x370 ⇒ LESSE(cons(x371, cons(x372, cons(x373, x367))), node(x374, x375, x376), s(s(s(x365))))≥IF(le(length(cons(x372, cons(x373, x367))), s(s(x365))), le(length(append(toList(x374), cons(x375, toList(x376)))), s(s(s(x365)))), cons(x371, cons(x372, cons(x373, x367))), node(x374, x375, x376), s(s(s(x365)))))∧(∀x479,x480,x481,x482,x483,x484,x485,x486,x487,x488,x489,x490,x491,x492,x493,x494,x495,x496,x497,x498:le(x478, x477)=false∧le(x479, x480)=false∧length(x481)=s(x479)∧length(x482)=x478∧s(s(x480))=x477∧(∀x483,x484,x485,x486,x487,x488,x489,x490,x491,x492:le(x479, x480)=false∧length(x483)=x479∧length(x484)=x485∧le(x485, x486)=false∧s(x480)=x486 ⇒ LESSE(cons(x487, cons(x488, cons(x489, x483))), node(x490, x491, x492), s(s(s(x480))))≥IF(le(length(cons(x488, cons(x489, x483))), s(s(x480))), le(length(append(toList(x490), cons(x491, toList(x492)))), s(s(s(x480)))), cons(x487, cons(x488, cons(x489, x483))), node(x490, x491, x492), s(s(s(x480))))) ⇒ LESSE(cons(x493, cons(x494, cons(x495, x481))), node(x496, x497, x498), s(s(s(s(x480)))))≥IF(le(length(cons(x494, cons(x495, x481))), s(s(s(x480)))), le(length(append(toList(x496), cons(x497, toList(x498)))), s(s(s(s(x480))))), cons(x493, cons(x494, cons(x495, x481))), node(x496, x497, x498), s(s(s(s(x480))))))∧(∀x501,x502,x503,x504,x505,x506,x507,x508,x509,x510,x511,x512,x513,x514,x515,x516,x517,x518,x519,x520,x521,x522,x523,x524,x525,x526,x527,x528,x529,x530,x531,x532,x533,x534,x535,x536,x537,x538,x539,x540,x541:length(x499)=s(x501)∧le(x502, x503)=false∧le(x501, x504)=false∧length(x505)=s(x502)∧s(x504)=x503∧(∀x506,x507,x508,x509,x510,x511,x512,x513,x514,x515:le(x501, x504)=false∧length(x506)=x501∧length(x507)=x508∧le(x508, x509)=false∧s(x504)=x509 ⇒ LESSE(cons(x510, cons(x511, cons(x512, x506))), node(x513, x514, x515), s(s(s(x504))))≥IF(le(length(cons(x511, cons(x512, x506))), s(s(x504))), le(length(append(toList(x513), cons(x514, toList(x515)))), s(s(s(x504)))), cons(x510, cons(x511, cons(x512, x506))), node(x513, x514, x515), s(s(s(x504)))))∧(∀x516,x517,x518,x519,x520,x521,x522,x523,x524,x525,x526,x527,x528,x529,x530,x531,x532,x533,x534,x535:le(x502, x503)=false∧le(x516, x517)=false∧length(x518)=s(x516)∧length(x519)=x502∧s(s(x517))=x503∧(∀x520,x521,x522,x523,x524,x525,x526,x527,x528,x529:le(x516, x517)=false∧length(x520)=x516∧length(x521)=x522∧le(x522, x523)=false∧s(x517)=x523 ⇒ LESSE(cons(x524, cons(x525, cons(x526, x520))), node(x527, x528, x529), s(s(s(x517))))≥IF(le(length(cons(x525, cons(x526, x520))), s(s(x517))), le(length(append(toList(x527), cons(x528, toList(x529)))), s(s(s(x517)))), cons(x524, cons(x525, cons(x526, x520))), node(x527, x528, x529), s(s(s(x517))))) ⇒ LESSE(cons(x530, cons(x531, cons(x532, x518))), node(x533, x534, x535), s(s(s(s(x517)))))≥IF(le(length(cons(x531, cons(x532, x518))), s(s(s(x517)))), le(length(append(toList(x533), cons(x534, toList(x535)))), s(s(s(s(x517))))), cons(x530, cons(x531, cons(x532, x518))), node(x533, x534, x535), s(s(s(s(x517)))))) ⇒ LESSE(cons(x536, cons(x537, cons(x538, x499))), node(x539, x540, x541), s(s(s(s(x504)))))≥IF(le(length(cons(x537, cons(x538, x499))), s(s(s(x504)))), le(length(append(toList(x539), cons(x540, toList(x541)))), s(s(s(s(x504))))), cons(x536, cons(x537, cons(x538, x499))), node(x539, x540, x541), s(s(s(s(x504))))))∧(∀x544,x545,x546,x547,x548,x549,x550,x551,x552,x553,x554,x555,x556,x557,x558,x559,x560,x561,x562,x563,x564,x565,x566,x567,x568,x569,x570,x571,x572,x573,x574,x575,x576,x577,x578,x579,x580,x581,x582,x583,x584,x585,x586,x587,x588,x589,x590,x591,x592,x593,x594,x595,x596,x597,x598,x599,x600,x601,x602,x603,x604,x605,x606,x607,x608,x609,x610,x611,x612,x613,x614,x615,x616,x617,x618,x619,x620,x621,x622,x623,x624,x625,x626:length(x542)=s(x544)∧length(x545)=x546∧le(x544, x547)=false∧le(x546, x548)=false∧s(x548)=x547∧(∀x549,x550,x551,x552,x553,x554,x555,x556,x557,x558:le(x546, x548)=false∧length(x549)=x546∧length(x550)=x551∧le(x551, x552)=false∧s(x548)=x552 ⇒ LESSE(cons(x553, cons(x554, cons(x555, x549))), node(x556, x557, x558), s(s(s(x548))))≥IF(le(length(cons(x554, cons(x555, x549))), s(s(x548))), le(length(append(toList(x556), cons(x557, toList(x558)))), s(s(s(x548)))), cons(x553, cons(x554, cons(x555, x549))), node(x556, x557, x558), s(s(s(x548)))))∧(∀x559,x560,x561,x562,x563,x564,x565,x566,x567,x568,x569,x570,x571,x572,x573,x574,x575,x576,x577,x578:le(x544, x547)=false∧le(x559, x560)=false∧length(x561)=s(x559)∧length(x562)=x544∧s(s(x560))=x547∧(∀x563,x564,x565,x566,x567,x568,x569,x570,x571,x572:le(x559, x560)=false∧length(x563)=x559∧length(x564)=x565∧le(x565, x566)=false∧s(x560)=x566 ⇒ LESSE(cons(x567, cons(x568, cons(x569, x563))), node(x570, x571, x572), s(s(s(x560))))≥IF(le(length(cons(x568, cons(x569, x563))), s(s(x560))), le(length(append(toList(x570), cons(x571, toList(x572)))), s(s(s(x560)))), cons(x567, cons(x568, cons(x569, x563))), node(x570, x571, x572), s(s(s(x560))))) ⇒ LESSE(cons(x573, cons(x574, cons(x575, x561))), node(x576, x577, x578), s(s(s(s(x560)))))≥IF(le(length(cons(x574, cons(x575, x561))), s(s(s(x560)))), le(length(append(toList(x576), cons(x577, toList(x578)))), s(s(s(s(x560))))), cons(x573, cons(x574, cons(x575, x561))), node(x576, x577, x578), s(s(s(s(x560))))))∧(∀x579,x580,x581,x582,x583,x584,x585,x586,x587,x588,x589,x590,x591,x592,x593,x594,x595,x596,x597,x598,x599,x600,x601,x602,x603,x604,x605,x606,x607,x608,x609,x610,x611,x612,x613,x614,x615,x616,x617,x618,x619:length(x545)=s(x579)∧le(x580, x581)=false∧le(x579, x582)=false∧length(x583)=s(x580)∧s(x582)=x581∧(∀x584,x585,x586,x587,x588,x589,x590,x591,x592,x593:le(x579, x582)=false∧length(x584)=x579∧length(x585)=x586∧le(x586, x587)=false∧s(x582)=x587 ⇒ LESSE(cons(x588, cons(x589, cons(x590, x584))), node(x591, x592, x593), s(s(s(x582))))≥IF(le(length(cons(x589, cons(x590, x584))), s(s(x582))), le(length(append(toList(x591), cons(x592, toList(x593)))), s(s(s(x582)))), cons(x588, cons(x589, cons(x590, x584))), node(x591, x592, x593), s(s(s(x582)))))∧(∀x594,x595,x596,x597,x598,x599,x600,x601,x602,x603,x604,x605,x606,x607,x608,x609,x610,x611,x612,x613:le(x580, x581)=false∧le(x594, x595)=false∧length(x596)=s(x594)∧length(x597)=x580∧s(s(x595))=x581∧(∀x598,x599,x600,x601,x602,x603,x604,x605,x606,x607:le(x594, x595)=false∧length(x598)=x594∧length(x599)=x600∧le(x600, x601)=false∧s(x595)=x601 ⇒ LESSE(cons(x602, cons(x603, cons(x604, x598))), node(x605, x606, x607), s(s(s(x595))))≥IF(le(length(cons(x603, cons(x604, x598))), s(s(x595))), le(length(append(toList(x605), cons(x606, toList(x607)))), s(s(s(x595)))), cons(x602, cons(x603, cons(x604, x598))), node(x605, x606, x607), s(s(s(x595))))) ⇒ LESSE(cons(x608, cons(x609, cons(x610, x596))), node(x611, x612, x613), s(s(s(s(x595)))))≥IF(le(length(cons(x609, cons(x610, x596))), s(s(s(x595)))), le(length(append(toList(x611), cons(x612, toList(x613)))), s(s(s(s(x595))))), cons(x608, cons(x609, cons(x610, x596))), node(x611, x612, x613), s(s(s(s(x595)))))) ⇒ LESSE(cons(x614, cons(x615, cons(x616, x545))), node(x617, x618, x619), s(s(s(s(x582)))))≥IF(le(length(cons(x615, cons(x616, x545))), s(s(s(x582)))), le(length(append(toList(x617), cons(x618, toList(x619)))), s(s(s(s(x582))))), cons(x614, cons(x615, cons(x616, x545))), node(x617, x618, x619), s(s(s(s(x582)))))) ⇒ LESSE(cons(x620, cons(x621, cons(x622, cons(x623, x545)))), node(x624, x625, x626), s(s(s(s(x548)))))≥IF(le(length(cons(x621, cons(x622, cons(x623, x545)))), s(s(s(x548)))), le(length(append(toList(x624), cons(x625, toList(x626)))), s(s(s(s(x548))))), cons(x620, cons(x621, cons(x622, cons(x623, x545)))), node(x624, x625, x626), s(s(s(s(x548)))))) ⇒ LESSE(cons(x6, cons(x78, cons(x324, cons(x500, x499)))), node(x8, x9, x10), s(s(s(s(x365)))))≥IF(le(length(cons(x78, cons(x324, cons(x500, x499)))), s(s(s(x365)))), le(length(append(toList(x8), cons(x9, toList(x10)))), s(s(s(s(x365))))), cons(x6, cons(x78, cons(x324, cons(x500, x499)))), node(x8, x9, x10), s(s(s(s(x365))))))

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

(53) (length(x542)=x478∧length(x499)=x366∧le(x478, x477)=false∧le(x366, x365)=false∧s(x365)=x477∧(∀x367,x368,x369,x370,x371,x372,x373,x374,x375,x376:le(x366, x365)=false∧length(x367)=x366∧length(x368)=x369∧le(x369, x370)=false∧s(x365)=x370 ⇒ LESSE(cons(x371, cons(x372, cons(x373, x367))), node(x374, x375, x376), s(s(s(x365))))≥IF(le(length(cons(x372, cons(x373, x367))), s(s(x365))), le(length(append(toList(x374), cons(x375, toList(x376)))), s(s(s(x365)))), cons(x371, cons(x372, cons(x373, x367))), node(x374, x375, x376), s(s(s(x365)))))∧(∀x479,x480,x481,x482,x483,x484,x485,x486,x487,x488,x489,x490,x491,x492,x493,x494,x495,x496,x497,x498:le(x478, x477)=false∧le(x479, x480)=false∧length(x481)=s(x479)∧length(x482)=x478∧s(s(x480))=x477∧(∀x483,x484,x485,x486,x487,x488,x489,x490,x491,x492:le(x479, x480)=false∧length(x483)=x479∧length(x484)=x485∧le(x485, x486)=false∧s(x480)=x486 ⇒ LESSE(cons(x487, cons(x488, cons(x489, x483))), node(x490, x491, x492), s(s(s(x480))))≥IF(le(length(cons(x488, cons(x489, x483))), s(s(x480))), le(length(append(toList(x490), cons(x491, toList(x492)))), s(s(s(x480)))), cons(x487, cons(x488, cons(x489, x483))), node(x490, x491, x492), s(s(s(x480))))) ⇒ LESSE(cons(x493, cons(x494, cons(x495, x481))), node(x496, x497, x498), s(s(s(s(x480)))))≥IF(le(length(cons(x494, cons(x495, x481))), s(s(s(x480)))), le(length(append(toList(x496), cons(x497, toList(x498)))), s(s(s(s(x480))))), cons(x493, cons(x494, cons(x495, x481))), node(x496, x497, x498), s(s(s(s(x480))))))∧(∀x501,x502,x503,x504,x505,x506,x507,x508,x509,x510,x511,x512,x513,x514,x515,x516,x517,x518,x519,x520,x521,x522,x523,x524,x525,x526,x527,x528,x529,x530,x531,x532,x533,x534,x535,x536,x537,x538,x539,x540,x541:length(x499)=s(x501)∧le(x502, x503)=false∧le(x501, x504)=false∧length(x505)=s(x502)∧s(x504)=x503∧(∀x506,x507,x508,x509,x510,x511,x512,x513,x514,x515:le(x501, x504)=false∧length(x506)=x501∧length(x507)=x508∧le(x508, x509)=false∧s(x504)=x509 ⇒ LESSE(cons(x510, cons(x511, cons(x512, x506))), node(x513, x514, x515), s(s(s(x504))))≥IF(le(length(cons(x511, cons(x512, x506))), s(s(x504))), le(length(append(toList(x513), cons(x514, toList(x515)))), s(s(s(x504)))), cons(x510, cons(x511, cons(x512, x506))), node(x513, x514, x515), s(s(s(x504)))))∧(∀x516,x517,x518,x519,x520,x521,x522,x523,x524,x525,x526,x527,x528,x529,x530,x531,x532,x533,x534,x535:le(x502, x503)=false∧le(x516, x517)=false∧length(x518)=s(x516)∧length(x519)=x502∧s(s(x517))=x503∧(∀x520,x521,x522,x523,x524,x525,x526,x527,x528,x529:le(x516, x517)=false∧length(x520)=x516∧length(x521)=x522∧le(x522, x523)=false∧s(x517)=x523 ⇒ LESSE(cons(x524, cons(x525, cons(x526, x520))), node(x527, x528, x529), s(s(s(x517))))≥IF(le(length(cons(x525, cons(x526, x520))), s(s(x517))), le(length(append(toList(x527), cons(x528, toList(x529)))), s(s(s(x517)))), cons(x524, cons(x525, cons(x526, x520))), node(x527, x528, x529), s(s(s(x517))))) ⇒ LESSE(cons(x530, cons(x531, cons(x532, x518))), node(x533, x534, x535), s(s(s(s(x517)))))≥IF(le(length(cons(x531, cons(x532, x518))), s(s(s(x517)))), le(length(append(toList(x533), cons(x534, toList(x535)))), s(s(s(s(x517))))), cons(x530, cons(x531, cons(x532, x518))), node(x533, x534, x535), s(s(s(s(x517)))))) ⇒ LESSE(cons(x536, cons(x537, cons(x538, x499))), node(x539, x540, x541), s(s(s(s(x504)))))≥IF(le(length(cons(x537, cons(x538, x499))), s(s(s(x504)))), le(length(append(toList(x539), cons(x540, toList(x541)))), s(s(s(s(x504))))), cons(x536, cons(x537, cons(x538, x499))), node(x539, x540, x541), s(s(s(s(x504))))))∧(∀x544,x545,x546,x547,x548,x549,x550,x551,x552,x553,x554,x555,x556,x557,x558,x559,x560,x561,x562,x563,x564,x565,x566,x567,x568,x569,x570,x571,x572,x573,x574,x575,x576,x577,x578,x579,x580,x581,x582,x583,x584,x585,x586,x587,x588,x589,x590,x591,x592,x593,x594,x595,x596,x597,x598,x599,x600,x601,x602,x603,x604,x605,x606,x607,x608,x609,x610,x611,x612,x613,x614,x615,x616,x617,x618,x619,x620,x621,x622,x623,x624,x625,x626:length(x542)=s(x544)∧length(x545)=x546∧le(x544, x547)=false∧le(x546, x548)=false∧s(x548)=x547∧(∀x549,x550,x551,x552,x553,x554,x555,x556,x557,x558:le(x546, x548)=false∧length(x549)=x546∧length(x550)=x551∧le(x551, x552)=false∧s(x548)=x552 ⇒ LESSE(cons(x553, cons(x554, cons(x555, x549))), node(x556, x557, x558), s(s(s(x548))))≥IF(le(length(cons(x554, cons(x555, x549))), s(s(x548))), le(length(append(toList(x556), cons(x557, toList(x558)))), s(s(s(x548)))), cons(x553, cons(x554, cons(x555, x549))), node(x556, x557, x558), s(s(s(x548)))))∧(∀x559,x560,x561,x562,x563,x564,x565,x566,x567,x568,x569,x570,x571,x572,x573,x574,x575,x576,x577,x578:le(x544, x547)=false∧le(x559, x560)=false∧length(x561)=s(x559)∧length(x562)=x544∧s(s(x560))=x547∧(∀x563,x564,x565,x566,x567,x568,x569,x570,x571,x572:le(x559, x560)=false∧length(x563)=x559∧length(x564)=x565∧le(x565, x566)=false∧s(x560)=x566 ⇒ LESSE(cons(x567, cons(x568, cons(x569, x563))), node(x570, x571, x572), s(s(s(x560))))≥IF(le(length(cons(x568, cons(x569, x563))), s(s(x560))), le(length(append(toList(x570), cons(x571, toList(x572)))), s(s(s(x560)))), cons(x567, cons(x568, cons(x569, x563))), node(x570, x571, x572), s(s(s(x560))))) ⇒ LESSE(cons(x573, cons(x574, cons(x575, x561))), node(x576, x577, x578), s(s(s(s(x560)))))≥IF(le(length(cons(x574, cons(x575, x561))), s(s(s(x560)))), le(length(append(toList(x576), cons(x577, toList(x578)))), s(s(s(s(x560))))), cons(x573, cons(x574, cons(x575, x561))), node(x576, x577, x578), s(s(s(s(x560))))))∧(∀x579,x580,x581,x582,x583,x584,x585,x586,x587,x588,x589,x590,x591,x592,x593,x594,x595,x596,x597,x598,x599,x600,x601,x602,x603,x604,x605,x606,x607,x608,x609,x610,x611,x612,x613,x614,x615,x616,x617,x618,x619:length(x545)=s(x579)∧le(x580, x581)=false∧le(x579, x582)=false∧length(x583)=s(x580)∧s(x582)=x581∧(∀x584,x585,x586,x587,x588,x589,x590,x591,x592,x593:le(x579, x582)=false∧length(x584)=x579∧length(x585)=x586∧le(x586, x587)=false∧s(x582)=x587 ⇒ LESSE(cons(x588, cons(x589, cons(x590, x584))), node(x591, x592, x593), s(s(s(x582))))≥IF(le(length(cons(x589, cons(x590, x584))), s(s(x582))), le(length(append(toList(x591), cons(x592, toList(x593)))), s(s(s(x582)))), cons(x588, cons(x589, cons(x590, x584))), node(x591, x592, x593), s(s(s(x582)))))∧(∀x594,x595,x596,x597,x598,x599,x600,x601,x602,x603,x604,x605,x606,x607,x608,x609,x610,x611,x612,x613:le(x580, x581)=false∧le(x594, x595)=false∧length(x596)=s(x594)∧length(x597)=x580∧s(s(x595))=x581∧(∀x598,x599,x600,x601,x602,x603,x604,x605,x606,x607:le(x594, x595)=false∧length(x598)=x594∧length(x599)=x600∧le(x600, x601)=false∧s(x595)=x601 ⇒ LESSE(cons(x602, cons(x603, cons(x604, x598))), node(x605, x606, x607), s(s(s(x595))))≥IF(le(length(cons(x603, cons(x604, x598))), s(s(x595))), le(length(append(toList(x605), cons(x606, toList(x607)))), s(s(s(x595)))), cons(x602, cons(x603, cons(x604, x598))), node(x605, x606, x607), s(s(s(x595))))) ⇒ LESSE(cons(x608, cons(x609, cons(x610, x596))), node(x611, x612, x613), s(s(s(s(x595)))))≥IF(le(length(cons(x609, cons(x610, x596))), s(s(s(x595)))), le(length(append(toList(x611), cons(x612, toList(x613)))), s(s(s(s(x595))))), cons(x608, cons(x609, cons(x610, x596))), node(x611, x612, x613), s(s(s(s(x595)))))) ⇒ LESSE(cons(x614, cons(x615, cons(x616, x545))), node(x617, x618, x619), s(s(s(s(x582)))))≥IF(le(length(cons(x615, cons(x616, x545))), s(s(s(x582)))), le(length(append(toList(x617), cons(x618, toList(x619)))), s(s(s(s(x582))))), cons(x614, cons(x615, cons(x616, x545))), node(x617, x618, x619), s(s(s(s(x582)))))) ⇒ LESSE(cons(x620, cons(x621, cons(x622, cons(x623, x545)))), node(x624, x625, x626), s(s(s(s(x548)))))≥IF(le(length(cons(x621, cons(x622, cons(x623, x545)))), s(s(s(x548)))), le(length(append(toList(x624), cons(x625, toList(x626)))), s(s(s(s(x548))))), cons(x620, cons(x621, cons(x622, cons(x623, x545)))), node(x624, x625, x626), s(s(s(s(x548)))))) ⇒ LESSE(cons(x6, cons(x78, cons(x324, cons(x500, x499)))), node(x8, x9, x10), s(s(s(s(x365)))))≥IF(le(length(cons(x78, cons(x324, cons(x500, x499)))), s(s(s(x365)))), le(length(append(toList(x8), cons(x9, toList(x10)))), s(s(s(s(x365))))), cons(x6, cons(x78, cons(x324, cons(x500, x499)))), node(x8, x9, x10), s(s(s(s(x365))))))

We simplified constraint (53) using rule (VI) where we applied the induction hypothesis (∀x367,x368,x369,x370,x371,x372,x373,x374,x375,x376:le(x366, x365)=false∧length(x367)=x366∧length(x368)=x369∧le(x369, x370)=false∧s(x365)=x370 ⇒ LESSE(cons(x371, cons(x372, cons(x373, x367))), node(x374, x375, x376), s(s(s(x365))))≥IF(le(length(cons(x372, cons(x373, x367))), s(s(x365))), le(length(append(toList(x374), cons(x375, toList(x376)))), s(s(s(x365)))), cons(x371, cons(x372, cons(x373, x367))), node(x374, x375, x376), s(s(s(x365))))) with σ = [x367 / x499, x368 / x542, x369 / x478, x370 / x477, x371 / x6, x372 / x78, x373 / x324, x374 / x8, x375 / x9, x376 / x10] which results in the following new constraint:

(54) (LESSE(cons(x6, cons(x78, cons(x324, x499))), node(x8, x9, x10), s(s(s(x365))))≥IF(le(length(cons(x78, cons(x324, x499))), s(s(x365))), le(length(append(toList(x8), cons(x9, toList(x10)))), s(s(s(x365)))), cons(x6, cons(x78, cons(x324, x499))), node(x8, x9, x10), s(s(s(x365))))∧(∀x479,x480,x481,x482,x483,x484,x485,x486,x487,x488,x489,x490,x491,x492,x493,x494,x495,x496,x497,x498:le(x478, x477)=false∧le(x479, x480)=false∧length(x481)=s(x479)∧length(x482)=x478∧s(s(x480))=x477∧(∀x483,x484,x485,x486,x487,x488,x489,x490,x491,x492:le(x479, x480)=false∧length(x483)=x479∧length(x484)=x485∧le(x485, x486)=false∧s(x480)=x486 ⇒ LESSE(cons(x487, cons(x488, cons(x489, x483))), node(x490, x491, x492), s(s(s(x480))))≥IF(le(length(cons(x488, cons(x489, x483))), s(s(x480))), le(length(append(toList(x490), cons(x491, toList(x492)))), s(s(s(x480)))), cons(x487, cons(x488, cons(x489, x483))), node(x490, x491, x492), s(s(s(x480))))) ⇒ LESSE(cons(x493, cons(x494, cons(x495, x481))), node(x496, x497, x498), s(s(s(s(x480)))))≥IF(le(length(cons(x494, cons(x495, x481))), s(s(s(x480)))), le(length(append(toList(x496), cons(x497, toList(x498)))), s(s(s(s(x480))))), cons(x493, cons(x494, cons(x495, x481))), node(x496, x497, x498), s(s(s(s(x480))))))∧(∀x501,x502,x503,x504,x505,x506,x507,x508,x509,x510,x511,x512,x513,x514,x515,x516,x517,x518,x519,x520,x521,x522,x523,x524,x525,x526,x527,x528,x529,x530,x531,x532,x533,x534,x535,x536,x537,x538,x539,x540,x541:length(x499)=s(x501)∧le(x502, x503)=false∧le(x501, x504)=false∧length(x505)=s(x502)∧s(x504)=x503∧(∀x506,x507,x508,x509,x510,x511,x512,x513,x514,x515:le(x501, x504)=false∧length(x506)=x501∧length(x507)=x508∧le(x508, x509)=false∧s(x504)=x509 ⇒ LESSE(cons(x510, cons(x511, cons(x512, x506))), node(x513, x514, x515), s(s(s(x504))))≥IF(le(length(cons(x511, cons(x512, x506))), s(s(x504))), le(length(append(toList(x513), cons(x514, toList(x515)))), s(s(s(x504)))), cons(x510, cons(x511, cons(x512, x506))), node(x513, x514, x515), s(s(s(x504)))))∧(∀x516,x517,x518,x519,x520,x521,x522,x523,x524,x525,x526,x527,x528,x529,x530,x531,x532,x533,x534,x535:le(x502, x503)=false∧le(x516, x517)=false∧length(x518)=s(x516)∧length(x519)=x502∧s(s(x517))=x503∧(∀x520,x521,x522,x523,x524,x525,x526,x527,x528,x529:le(x516, x517)=false∧length(x520)=x516∧length(x521)=x522∧le(x522, x523)=false∧s(x517)=x523 ⇒ LESSE(cons(x524, cons(x525, cons(x526, x520))), node(x527, x528, x529), s(s(s(x517))))≥IF(le(length(cons(x525, cons(x526, x520))), s(s(x517))), le(length(append(toList(x527), cons(x528, toList(x529)))), s(s(s(x517)))), cons(x524, cons(x525, cons(x526, x520))), node(x527, x528, x529), s(s(s(x517))))) ⇒ LESSE(cons(x530, cons(x531, cons(x532, x518))), node(x533, x534, x535), s(s(s(s(x517)))))≥IF(le(length(cons(x531, cons(x532, x518))), s(s(s(x517)))), le(length(append(toList(x533), cons(x534, toList(x535)))), s(s(s(s(x517))))), cons(x530, cons(x531, cons(x532, x518))), node(x533, x534, x535), s(s(s(s(x517)))))) ⇒ LESSE(cons(x536, cons(x537, cons(x538, x499))), node(x539, x540, x541), s(s(s(s(x504)))))≥IF(le(length(cons(x537, cons(x538, x499))), s(s(s(x504)))), le(length(append(toList(x539), cons(x540, toList(x541)))), s(s(s(s(x504))))), cons(x536, cons(x537, cons(x538, x499))), node(x539, x540, x541), s(s(s(s(x504))))))∧(∀x544,x545,x546,x547,x548,x549,x550,x551,x552,x553,x554,x555,x556,x557,x558,x559,x560,x561,x562,x563,x564,x565,x566,x567,x568,x569,x570,x571,x572,x573,x574,x575,x576,x577,x578,x579,x580,x581,x582,x583,x584,x585,x586,x587,x588,x589,x590,x591,x592,x593,x594,x595,x596,x597,x598,x599,x600,x601,x602,x603,x604,x605,x606,x607,x608,x609,x610,x611,x612,x613,x614,x615,x616,x617,x618,x619,x620,x621,x622,x623,x624,x625,x626:length(x542)=s(x544)∧length(x545)=x546∧le(x544, x547)=false∧le(x546, x548)=false∧s(x548)=x547∧(∀x549,x550,x551,x552,x553,x554,x555,x556,x557,x558:le(x546, x548)=false∧length(x549)=x546∧length(x550)=x551∧le(x551, x552)=false∧s(x548)=x552 ⇒ LESSE(cons(x553, cons(x554, cons(x555, x549))), node(x556, x557, x558), s(s(s(x548))))≥IF(le(length(cons(x554, cons(x555, x549))), s(s(x548))), le(length(append(toList(x556), cons(x557, toList(x558)))), s(s(s(x548)))), cons(x553, cons(x554, cons(x555, x549))), node(x556, x557, x558), s(s(s(x548)))))∧(∀x559,x560,x561,x562,x563,x564,x565,x566,x567,x568,x569,x570,x571,x572,x573,x574,x575,x576,x577,x578:le(x544, x547)=false∧le(x559, x560)=false∧length(x561)=s(x559)∧length(x562)=x544∧s(s(x560))=x547∧(∀x563,x564,x565,x566,x567,x568,x569,x570,x571,x572:le(x559, x560)=false∧length(x563)=x559∧length(x564)=x565∧le(x565, x566)=false∧s(x560)=x566 ⇒ LESSE(cons(x567, cons(x568, cons(x569, x563))), node(x570, x571, x572), s(s(s(x560))))≥IF(le(length(cons(x568, cons(x569, x563))), s(s(x560))), le(length(append(toList(x570), cons(x571, toList(x572)))), s(s(s(x560)))), cons(x567, cons(x568, cons(x569, x563))), node(x570, x571, x572), s(s(s(x560))))) ⇒ LESSE(cons(x573, cons(x574, cons(x575, x561))), node(x576, x577, x578), s(s(s(s(x560)))))≥IF(le(length(cons(x574, cons(x575, x561))), s(s(s(x560)))), le(length(append(toList(x576), cons(x577, toList(x578)))), s(s(s(s(x560))))), cons(x573, cons(x574, cons(x575, x561))), node(x576, x577, x578), s(s(s(s(x560))))))∧(∀x579,x580,x581,x582,x583,x584,x585,x586,x587,x588,x589,x590,x591,x592,x593,x594,x595,x596,x597,x598,x599,x600,x601,x602,x603,x604,x605,x606,x607,x608,x609,x610,x611,x612,x613,x614,x615,x616,x617,x618,x619:length(x545)=s(x579)∧le(x580, x581)=false∧le(x579, x582)=false∧length(x583)=s(x580)∧s(x582)=x581∧(∀x584,x585,x586,x587,x588,x589,x590,x591,x592,x593:le(x579, x582)=false∧length(x584)=x579∧length(x585)=x586∧le(x586, x587)=false∧s(x582)=x587 ⇒ LESSE(cons(x588, cons(x589, cons(x590, x584))), node(x591, x592, x593), s(s(s(x582))))≥IF(le(length(cons(x589, cons(x590, x584))), s(s(x582))), le(length(append(toList(x591), cons(x592, toList(x593)))), s(s(s(x582)))), cons(x588, cons(x589, cons(x590, x584))), node(x591, x592, x593), s(s(s(x582)))))∧(∀x594,x595,x596,x597,x598,x599,x600,x601,x602,x603,x604,x605,x606,x607,x608,x609,x610,x611,x612,x613:le(x580, x581)=false∧le(x594, x595)=false∧length(x596)=s(x594)∧length(x597)=x580∧s(s(x595))=x581∧(∀x598,x599,x600,x601,x602,x603,x604,x605,x606,x607:le(x594, x595)=false∧length(x598)=x594∧length(x599)=x600∧le(x600, x601)=false∧s(x595)=x601 ⇒ LESSE(cons(x602, cons(x603, cons(x604, x598))), node(x605, x606, x607), s(s(s(x595))))≥IF(le(length(cons(x603, cons(x604, x598))), s(s(x595))), le(length(append(toList(x605), cons(x606, toList(x607)))), s(s(s(x595)))), cons(x602, cons(x603, cons(x604, x598))), node(x605, x606, x607), s(s(s(x595))))) ⇒ LESSE(cons(x608, cons(x609, cons(x610, x596))), node(x611, x612, x613), s(s(s(s(x595)))))≥IF(le(length(cons(x609, cons(x610, x596))), s(s(s(x595)))), le(length(append(toList(x611), cons(x612, toList(x613)))), s(s(s(s(x595))))), cons(x608, cons(x609, cons(x610, x596))), node(x611, x612, x613), s(s(s(s(x595)))))) ⇒ LESSE(cons(x614, cons(x615, cons(x616, x545))), node(x617, x618, x619), s(s(s(s(x582)))))≥IF(le(length(cons(x615, cons(x616, x545))), s(s(s(x582)))), le(length(append(toList(x617), cons(x618, toList(x619)))), s(s(s(s(x582))))), cons(x614, cons(x615, cons(x616, x545))), node(x617, x618, x619), s(s(s(s(x582)))))) ⇒ LESSE(cons(x620, cons(x621, cons(x622, cons(x623, x545)))), node(x624, x625, x626), s(s(s(s(x548)))))≥IF(le(length(cons(x621, cons(x622, cons(x623, x545)))), s(s(s(x548)))), le(length(append(toList(x624), cons(x625, toList(x626)))), s(s(s(s(x548))))), cons(x620, cons(x621, cons(x622, cons(x623, x545)))), node(x624, x625, x626), s(s(s(s(x548)))))) ⇒ LESSE(cons(x6, cons(x78, cons(x324, cons(x500, x499)))), node(x8, x9, x10), s(s(s(s(x365)))))≥IF(le(length(cons(x78, cons(x324, cons(x500, x499)))), s(s(s(x365)))), le(length(append(toList(x8), cons(x9, toList(x10)))), s(s(s(s(x365))))), cons(x6, cons(x78, cons(x324, cons(x500, x499)))), node(x8, x9, x10), s(s(s(s(x365))))))

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

(55) (LESSE(cons(x6, cons(x78, cons(x324, x499))), node(x8, x9, x10), s(s(s(x365))))≥IF(le(length(cons(x78, cons(x324, x499))), s(s(x365))), le(length(append(toList(x8), cons(x9, toList(x10)))), s(s(s(x365)))), cons(x6, cons(x78, cons(x324, x499))), node(x8, x9, x10), s(s(s(x365)))) ⇒ LESSE(cons(x6, cons(x78, cons(x324, cons(x500, x499)))), node(x8, x9, x10), s(s(s(s(x365)))))≥IF(le(length(cons(x78, cons(x324, cons(x500, x499)))), s(s(s(x365)))), le(length(append(toList(x8), cons(x9, toList(x10)))), s(s(s(s(x365))))), cons(x6, cons(x78, cons(x324, cons(x500, x499)))), node(x8, x9, x10), s(s(s(s(x365))))))

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 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)))), LESSE(cons(x24, x25), node(x26, x27, x28), s(s(x29))) → IF(le(length(x25), s(x29)), le(length(append(toList(x26), cons(x27, toList(x28)))), s(s(x29))), cons(x24, x25), node(x26, x27, x28), s(s(x29))) which results in the following constraint:

(1) (LESSE(cons(x18, x19), node(x20, x21, x22), s(s(s(x23))))=LESSE(cons(x24, x25), node(x26, x27, x28), s(s(x29))) ⇒ 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 (1) using rules (I), (II), (IV) which results in the following new constraint:

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

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, cons(x78, cons(x234, x233))), node(x8, x9, x10), s(s(0)))≥IF(le(length(cons(x78, cons(x234, x233))), s(0)), le(length(append(toList(x8), cons(x9, toList(x10)))), s(s(0))), cons(x6, cons(x78, cons(x234, x233))), node(x8, x9, x10), s(s(0))))
- (LESSE(cons(x6, cons(x78, cons(x324, cons(x391, x390)))), node(x8, x9, x10), s(s(s(0))))≥IF(le(length(cons(x78, cons(x324, cons(x391, x390)))), s(s(0))), le(length(append(toList(x8), cons(x9, toList(x10)))), s(s(s(0)))), cons(x6, cons(x78, cons(x324, cons(x391, x390)))), node(x8, x9, x10), s(s(s(0)))))
- (LESSE(cons(x6, cons(x78, cons(x324, x499))), node(x8, x9, x10), s(s(s(x365))))≥IF(le(length(cons(x78, cons(x324, x499))), s(s(x365))), le(length(append(toList(x8), cons(x9, toList(x10)))), s(s(s(x365)))), cons(x6, cons(x78, cons(x324, x499))), node(x8, x9, x10), s(s(s(x365)))) ⇒ LESSE(cons(x6, cons(x78, cons(x324, cons(x500, x499)))), node(x8, x9, x10), s(s(s(s(x365)))))≥IF(le(length(cons(x78, cons(x324, cons(x500, x499)))), s(s(s(x365)))), le(length(append(toList(x8), cons(x9, toList(x10)))), s(s(s(s(x365))))), cons(x6, cons(x78, cons(x324, cons(x500, x499)))), node(x8, x9, x10), s(s(s(s(x365))))))
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, x19), node(x20, x21, x22), s(s(x23)))≥LESSE(cons(x18, x19), node(x20, x21, x22), s(s(s(x23)))))

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

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:

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

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

(65) Complex Obligation (AND)

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

(67) DependencyGraphProof (EQUIVALENT transformation)

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

(68) TRUE

(69) Obligation:

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

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.

(70) DependencyGraphProof (EQUIVALENT transformation)

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

(0) Obligation:

(1) AAECC Innermost (EQUIVALENT transformation)

(2) Obligation:

(3) DependencyPairsProof (EQUIVALENT transformation)

(4) Obligation:

(5) DependencyGraphProof (EQUIVALENT transformation)

(6) Complex Obligation (AND)

(7) Obligation:

(8) UsableRulesProof (EQUIVALENT transformation)

(9) Obligation:

(10) QReductionProof (EQUIVALENT transformation)

(11) Obligation:

(12) QDPSizeChangeProof (EQUIVALENT transformation)

(13) YES

(14) Obligation:

(15) UsableRulesProof (EQUIVALENT transformation)

(16) Obligation:

(17) QReductionProof (EQUIVALENT transformation)

(18) Obligation:

(19) QDPSizeChangeProof (EQUIVALENT transformation)

(20) YES

(21) Obligation:

(22) UsableRulesProof (EQUIVALENT transformation)

(23) Obligation:

(24) QReductionProof (EQUIVALENT transformation)

(25) Obligation:

(26) QDPSizeChangeProof (EQUIVALENT transformation)

(27) YES

(28) Obligation:

(29) UsableRulesProof (EQUIVALENT transformation)

(30) Obligation:

(31) QReductionProof (EQUIVALENT transformation)

(32) Obligation:

(33) QDPSizeChangeProof (EQUIVALENT transformation)

(34) YES

(35) Obligation:

(36) UsableRulesProof (EQUIVALENT transformation)

(37) Obligation:

(38) QReductionProof (EQUIVALENT transformation)

(39) Obligation:

(40) TransformationProof (EQUIVALENT transformation)

(41) Obligation:

(42) TransformationProof (EQUIVALENT transformation)

(43) Obligation:

(44) DependencyGraphProof (EQUIVALENT transformation)

(45) Obligation:

(46) TransformationProof (EQUIVALENT transformation)

(47) Obligation:

(48) TransformationProof (EQUIVALENT transformation)

(49) Obligation:

(50) TransformationProof (EQUIVALENT transformation)

(51) Obligation:

(52) DependencyGraphProof (EQUIVALENT transformation)

(53) Obligation:

(54) TransformationProof (EQUIVALENT transformation)

(55) Obligation:

(56) TransformationProof (EQUIVALENT transformation)

(57) Obligation:

(58) TransformationProof (EQUIVALENT transformation)

(59) Obligation:

(60) TransformationProof (EQUIVALENT transformation)

(61) Obligation:

(62) TransformationProof (EQUIVALENT transformation)

(63) Obligation:

(64) NonInfProof (EQUIVALENT transformation)

(65) Complex Obligation (AND)

(66) Obligation:

(67) DependencyGraphProof (EQUIVALENT transformation)

(68) TRUE

(69) Obligation:

(70) DependencyGraphProof (EQUIVALENT transformation)

(71) TRUE