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

(0) Obligation:

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

isEmpty(empty) → true
isEmpty(node(l, x, r)) → false
left(empty) → empty
left(node(l, x, r)) → l
right(empty) → empty
right(node(l, x, r)) → r
elem(node(l, x, r)) → x
append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))
listify(n, xs) → if(isEmpty(n), isEmpty(left(n)), right(n), node(left(left(n)), elem(left(n)), node(right(left(n)), elem(n), right(n))), xs, append(xs, n))
if(true, b, n, m, xs, ys) → xs
if(false, false, n, m, xs, ys) → listify(m, xs)
if(false, true, n, m, xs, ys) → listify(n, ys)
toList(n) → listify(n, nil)

Q is empty.

(1) Overlay + Local Confluence (EQUIVALENT transformation)

The TRS is overlay and locally confluent. By [NOC] we can switch to innermost.

(2) Obligation:

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

isEmpty(empty) → true
isEmpty(node(l, x, r)) → false
left(empty) → empty
left(node(l, x, r)) → l
right(empty) → empty
right(node(l, x, r)) → r
elem(node(l, x, r)) → x
append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))
listify(n, xs) → if(isEmpty(n), isEmpty(left(n)), right(n), node(left(left(n)), elem(left(n)), node(right(left(n)), elem(n), right(n))), xs, append(xs, n))
if(true, b, n, m, xs, ys) → xs
if(false, false, n, m, xs, ys) → listify(m, xs)
if(false, true, n, m, xs, ys) → listify(n, ys)
toList(n) → listify(n, nil)

The set Q consists of the following terms:

isEmpty(empty)
isEmpty(node(x0, x1, x2))
left(empty)
left(node(x0, x1, x2))
right(empty)
right(node(x0, x1, x2))
elem(node(x0, x1, x2))
append(nil, x0)
append(cons(y, x0), x1)
listify(x0, x1)
if(true, x0, x1, x2, x3, x4)
if(false, false, x0, x1, x2, x3)
if(false, true, x0, x1, x2, x3)
toList(x0)

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

APPEND(cons(y, ys), x) → APPEND(ys, x)
LISTIFY(n, xs) → IF(isEmpty(n), isEmpty(left(n)), right(n), node(left(left(n)), elem(left(n)), node(right(left(n)), elem(n), right(n))), xs, append(xs, n))
LISTIFY(n, xs) → ISEMPTY(n)
LISTIFY(n, xs) → ISEMPTY(left(n))
LISTIFY(n, xs) → LEFT(n)
LISTIFY(n, xs) → RIGHT(n)
LISTIFY(n, xs) → LEFT(left(n))
LISTIFY(n, xs) → ELEM(left(n))
LISTIFY(n, xs) → RIGHT(left(n))
LISTIFY(n, xs) → ELEM(n)
LISTIFY(n, xs) → APPEND(xs, n)
IF(false, false, n, m, xs, ys) → LISTIFY(m, xs)
IF(false, true, n, m, xs, ys) → LISTIFY(n, ys)
TOLIST(n) → LISTIFY(n, nil)

The TRS R consists of the following rules:

isEmpty(empty) → true
isEmpty(node(l, x, r)) → false
left(empty) → empty
left(node(l, x, r)) → l
right(empty) → empty
right(node(l, x, r)) → r
elem(node(l, x, r)) → x
append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))
listify(n, xs) → if(isEmpty(n), isEmpty(left(n)), right(n), node(left(left(n)), elem(left(n)), node(right(left(n)), elem(n), right(n))), xs, append(xs, n))
if(true, b, n, m, xs, ys) → xs
if(false, false, n, m, xs, ys) → listify(m, xs)
if(false, true, n, m, xs, ys) → listify(n, ys)
toList(n) → listify(n, nil)

The set Q consists of the following terms:

isEmpty(empty)
isEmpty(node(x0, x1, x2))
left(empty)
left(node(x0, x1, x2))
right(empty)
right(node(x0, x1, x2))
elem(node(x0, x1, x2))
append(nil, x0)
append(cons(y, x0), x1)
listify(x0, x1)
if(true, x0, x1, x2, x3, x4)
if(false, false, x0, x1, x2, x3)
if(false, true, x0, x1, x2, x3)
toList(x0)

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

(5) DependencyGraphProof (EQUIVALENT transformation)

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

(6) Complex Obligation (AND)

(7) Obligation:

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

APPEND(cons(y, ys), x) → APPEND(ys, x)

The TRS R consists of the following rules:

isEmpty(empty) → true
isEmpty(node(l, x, r)) → false
left(empty) → empty
left(node(l, x, r)) → l
right(empty) → empty
right(node(l, x, r)) → r
elem(node(l, x, r)) → x
append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))
listify(n, xs) → if(isEmpty(n), isEmpty(left(n)), right(n), node(left(left(n)), elem(left(n)), node(right(left(n)), elem(n), right(n))), xs, append(xs, n))
if(true, b, n, m, xs, ys) → xs
if(false, false, n, m, xs, ys) → listify(m, xs)
if(false, true, n, m, xs, ys) → listify(n, ys)
toList(n) → listify(n, nil)

The set Q consists of the following terms:

isEmpty(empty)
isEmpty(node(x0, x1, x2))
left(empty)
left(node(x0, x1, x2))
right(empty)
right(node(x0, x1, x2))
elem(node(x0, x1, x2))
append(nil, x0)
append(cons(y, x0), x1)
listify(x0, x1)
if(true, x0, x1, x2, x3, x4)
if(false, false, x0, x1, x2, x3)
if(false, true, x0, x1, x2, x3)
toList(x0)

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:

APPEND(cons(y, ys), x) → APPEND(ys, x)

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

isEmpty(empty)
isEmpty(node(x0, x1, x2))
left(empty)
left(node(x0, x1, x2))
right(empty)
right(node(x0, x1, x2))
elem(node(x0, x1, x2))
append(nil, x0)
append(cons(y, x0), x1)
listify(x0, x1)
if(true, x0, x1, x2, x3, x4)
if(false, false, x0, x1, x2, x3)
if(false, true, x0, x1, x2, x3)
toList(x0)

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

isEmpty(empty)
isEmpty(node(x0, x1, x2))
left(empty)
left(node(x0, x1, x2))
right(empty)
right(node(x0, x1, x2))
elem(node(x0, x1, x2))
append(nil, x0)
append(cons(y, x0), x1)
listify(x0, x1)
if(true, x0, x1, x2, x3, x4)
if(false, false, x0, x1, x2, x3)
if(false, true, x0, x1, x2, x3)
toList(x0)

(11) Obligation:

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

APPEND(cons(y, ys), x) → APPEND(ys, x)

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:

• APPEND(cons(y, ys), x) → APPEND(ys, x)
  The graph contains the following edges 1 > 1, 2 >= 2

(13) TRUE

(14) Obligation:

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

LISTIFY(n, xs) → IF(isEmpty(n), isEmpty(left(n)), right(n), node(left(left(n)), elem(left(n)), node(right(left(n)), elem(n), right(n))), xs, append(xs, n))
IF(false, false, n, m, xs, ys) → LISTIFY(m, xs)
IF(false, true, n, m, xs, ys) → LISTIFY(n, ys)

The TRS R consists of the following rules:

isEmpty(empty) → true
isEmpty(node(l, x, r)) → false
left(empty) → empty
left(node(l, x, r)) → l
right(empty) → empty
right(node(l, x, r)) → r
elem(node(l, x, r)) → x
append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))
listify(n, xs) → if(isEmpty(n), isEmpty(left(n)), right(n), node(left(left(n)), elem(left(n)), node(right(left(n)), elem(n), right(n))), xs, append(xs, n))
if(true, b, n, m, xs, ys) → xs
if(false, false, n, m, xs, ys) → listify(m, xs)
if(false, true, n, m, xs, ys) → listify(n, ys)
toList(n) → listify(n, nil)

The set Q consists of the following terms:

isEmpty(empty)
isEmpty(node(x0, x1, x2))
left(empty)
left(node(x0, x1, x2))
right(empty)
right(node(x0, x1, x2))
elem(node(x0, x1, x2))
append(nil, x0)
append(cons(y, x0), x1)
listify(x0, x1)
if(true, x0, x1, x2, x3, x4)
if(false, false, x0, x1, x2, x3)
if(false, true, x0, x1, x2, x3)
toList(x0)

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:

LISTIFY(n, xs) → IF(isEmpty(n), isEmpty(left(n)), right(n), node(left(left(n)), elem(left(n)), node(right(left(n)), elem(n), right(n))), xs, append(xs, n))
IF(false, false, n, m, xs, ys) → LISTIFY(m, xs)
IF(false, true, n, m, xs, ys) → LISTIFY(n, ys)

The TRS R consists of the following rules:

isEmpty(empty) → true
isEmpty(node(l, x, r)) → false
left(empty) → empty
left(node(l, x, r)) → l
right(empty) → empty
right(node(l, x, r)) → r
elem(node(l, x, r)) → x
append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))

The set Q consists of the following terms:

isEmpty(empty)
isEmpty(node(x0, x1, x2))
left(empty)
left(node(x0, x1, x2))
right(empty)
right(node(x0, x1, x2))
elem(node(x0, x1, x2))
append(nil, x0)
append(cons(y, x0), x1)
listify(x0, x1)
if(true, x0, x1, x2, x3, x4)
if(false, false, x0, x1, x2, x3)
if(false, true, x0, x1, x2, x3)
toList(x0)

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

listify(x0, x1)
if(true, x0, x1, x2, x3, x4)
if(false, false, x0, x1, x2, x3)
if(false, true, x0, x1, x2, x3)
toList(x0)

(18) Obligation:

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

LISTIFY(n, xs) → IF(isEmpty(n), isEmpty(left(n)), right(n), node(left(left(n)), elem(left(n)), node(right(left(n)), elem(n), right(n))), xs, append(xs, n))
IF(false, false, n, m, xs, ys) → LISTIFY(m, xs)
IF(false, true, n, m, xs, ys) → LISTIFY(n, ys)

The TRS R consists of the following rules:

isEmpty(empty) → true
isEmpty(node(l, x, r)) → false
left(empty) → empty
left(node(l, x, r)) → l
right(empty) → empty
right(node(l, x, r)) → r
elem(node(l, x, r)) → x
append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))

The set Q consists of the following terms:

isEmpty(empty)
isEmpty(node(x0, x1, x2))
left(empty)
left(node(x0, x1, x2))
right(empty)
right(node(x0, x1, x2))
elem(node(x0, x1, x2))
append(nil, x0)
append(cons(y, x0), x1)

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

(19) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule IF(false, false, n, m, xs, ys) → LISTIFY(m, xs) we obtained the following new rules [LPAR04]:

IF(false, false, y_3, node(y_5, y_7, node(y_9, y_10, y_11)), z1, y_12) → LISTIFY(node(y_5, y_7, node(y_9, y_10, y_11)), z1)

(20) Obligation:

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

LISTIFY(n, xs) → IF(isEmpty(n), isEmpty(left(n)), right(n), node(left(left(n)), elem(left(n)), node(right(left(n)), elem(n), right(n))), xs, append(xs, n))
IF(false, true, n, m, xs, ys) → LISTIFY(n, ys)
IF(false, false, y_3, node(y_5, y_7, node(y_9, y_10, y_11)), z1, y_12) → LISTIFY(node(y_5, y_7, node(y_9, y_10, y_11)), z1)

The TRS R consists of the following rules:

isEmpty(empty) → true
isEmpty(node(l, x, r)) → false
left(empty) → empty
left(node(l, x, r)) → l
right(empty) → empty
right(node(l, x, r)) → r
elem(node(l, x, r)) → x
append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))

The set Q consists of the following terms:

isEmpty(empty)
isEmpty(node(x0, x1, x2))
left(empty)
left(node(x0, x1, x2))
right(empty)
right(node(x0, x1, x2))
elem(node(x0, x1, x2))
append(nil, x0)
append(cons(y, x0), x1)

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

(21) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule LISTIFY(n, xs) → IF(isEmpty(n), isEmpty(left(n)), right(n), node(left(left(n)), elem(left(n)), node(right(left(n)), elem(n), right(n))), xs, append(xs, n)) at position [0] we obtained the following new rules [LPAR04]:

LISTIFY(empty, y1) → IF(true, isEmpty(left(empty)), right(empty), node(left(left(empty)), elem(left(empty)), node(right(left(empty)), elem(empty), right(empty))), y1, append(y1, empty))
LISTIFY(node(x0, x1, x2), y1) → IF(false, isEmpty(left(node(x0, x1, x2))), right(node(x0, x1, x2)), node(left(left(node(x0, x1, x2))), elem(left(node(x0, x1, x2))), node(right(left(node(x0, x1, x2))), elem(node(x0, x1, x2)), right(node(x0, x1, x2)))), y1, append(y1, node(x0, x1, x2)))

(22) Obligation:

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

IF(false, false, n, m, xs, ys) → LISTIFY(m, xs)
IF(false, true, n, m, xs, ys) → LISTIFY(n, ys)
LISTIFY(empty, y1) → IF(true, isEmpty(left(empty)), right(empty), node(left(left(empty)), elem(left(empty)), node(right(left(empty)), elem(empty), right(empty))), y1, append(y1, empty))
LISTIFY(node(x0, x1, x2), y1) → IF(false, isEmpty(left(node(x0, x1, x2))), right(node(x0, x1, x2)), node(left(left(node(x0, x1, x2))), elem(left(node(x0, x1, x2))), node(right(left(node(x0, x1, x2))), elem(node(x0, x1, x2)), right(node(x0, x1, x2)))), y1, append(y1, node(x0, x1, x2)))

The TRS R consists of the following rules:

isEmpty(empty) → true
isEmpty(node(l, x, r)) → false
left(empty) → empty
left(node(l, x, r)) → l
right(empty) → empty
right(node(l, x, r)) → r
elem(node(l, x, r)) → x
append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))

The set Q consists of the following terms:

isEmpty(empty)
isEmpty(node(x0, x1, x2))
left(empty)
left(node(x0, x1, x2))
right(empty)
right(node(x0, x1, x2))
elem(node(x0, x1, x2))
append(nil, x0)
append(cons(y, x0), x1)

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

(23) DependencyGraphProof (EQUIVALENT transformation)

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

(24) Obligation:

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

LISTIFY(node(x0, x1, x2), y1) → IF(false, isEmpty(left(node(x0, x1, x2))), right(node(x0, x1, x2)), node(left(left(node(x0, x1, x2))), elem(left(node(x0, x1, x2))), node(right(left(node(x0, x1, x2))), elem(node(x0, x1, x2)), right(node(x0, x1, x2)))), y1, append(y1, node(x0, x1, x2)))
IF(false, false, n, m, xs, ys) → LISTIFY(m, xs)
IF(false, true, n, m, xs, ys) → LISTIFY(n, ys)

The TRS R consists of the following rules:

isEmpty(empty) → true
isEmpty(node(l, x, r)) → false
left(empty) → empty
left(node(l, x, r)) → l
right(empty) → empty
right(node(l, x, r)) → r
elem(node(l, x, r)) → x
append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))

The set Q consists of the following terms:

isEmpty(empty)
isEmpty(node(x0, x1, x2))
left(empty)
left(node(x0, x1, x2))
right(empty)
right(node(x0, x1, x2))
elem(node(x0, x1, x2))
append(nil, x0)
append(cons(y, x0), x1)

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

(25) Rewriting (EQUIVALENT transformation)

By rewriting [LPAR04] the rule LISTIFY(node(x0, x1, x2), y1) → IF(false, isEmpty(left(node(x0, x1, x2))), right(node(x0, x1, x2)), node(left(left(node(x0, x1, x2))), elem(left(node(x0, x1, x2))), node(right(left(node(x0, x1, x2))), elem(node(x0, x1, x2)), right(node(x0, x1, x2)))), y1, append(y1, node(x0, x1, x2))) at position [1,0] we obtained the following new rules [LPAR04]:

LISTIFY(node(x0, x1, x2), y1) → IF(false, isEmpty(x0), right(node(x0, x1, x2)), node(left(left(node(x0, x1, x2))), elem(left(node(x0, x1, x2))), node(right(left(node(x0, x1, x2))), elem(node(x0, x1, x2)), right(node(x0, x1, x2)))), y1, append(y1, node(x0, x1, x2)))

(26) Obligation:

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

IF(false, false, n, m, xs, ys) → LISTIFY(m, xs)
IF(false, true, n, m, xs, ys) → LISTIFY(n, ys)
LISTIFY(node(x0, x1, x2), y1) → IF(false, isEmpty(x0), right(node(x0, x1, x2)), node(left(left(node(x0, x1, x2))), elem(left(node(x0, x1, x2))), node(right(left(node(x0, x1, x2))), elem(node(x0, x1, x2)), right(node(x0, x1, x2)))), y1, append(y1, node(x0, x1, x2)))

The TRS R consists of the following rules:

isEmpty(empty) → true
isEmpty(node(l, x, r)) → false
left(empty) → empty
left(node(l, x, r)) → l
right(empty) → empty
right(node(l, x, r)) → r
elem(node(l, x, r)) → x
append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))

The set Q consists of the following terms:

isEmpty(empty)
isEmpty(node(x0, x1, x2))
left(empty)
left(node(x0, x1, x2))
right(empty)
right(node(x0, x1, x2))
elem(node(x0, x1, x2))
append(nil, x0)
append(cons(y, x0), x1)

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

(27) Rewriting (EQUIVALENT transformation)

By rewriting [LPAR04] the rule LISTIFY(node(x0, x1, x2), y1) → IF(false, isEmpty(x0), right(node(x0, x1, x2)), node(left(left(node(x0, x1, x2))), elem(left(node(x0, x1, x2))), node(right(left(node(x0, x1, x2))), elem(node(x0, x1, x2)), right(node(x0, x1, x2)))), y1, append(y1, node(x0, x1, x2))) at position [2] we obtained the following new rules [LPAR04]:

LISTIFY(node(x0, x1, x2), y1) → IF(false, isEmpty(x0), x2, node(left(left(node(x0, x1, x2))), elem(left(node(x0, x1, x2))), node(right(left(node(x0, x1, x2))), elem(node(x0, x1, x2)), right(node(x0, x1, x2)))), y1, append(y1, node(x0, x1, x2)))

(28) Obligation:

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

IF(false, false, n, m, xs, ys) → LISTIFY(m, xs)
IF(false, true, n, m, xs, ys) → LISTIFY(n, ys)
LISTIFY(node(x0, x1, x2), y1) → IF(false, isEmpty(x0), x2, node(left(left(node(x0, x1, x2))), elem(left(node(x0, x1, x2))), node(right(left(node(x0, x1, x2))), elem(node(x0, x1, x2)), right(node(x0, x1, x2)))), y1, append(y1, node(x0, x1, x2)))

The TRS R consists of the following rules:

isEmpty(empty) → true
isEmpty(node(l, x, r)) → false
left(empty) → empty
left(node(l, x, r)) → l
right(empty) → empty
right(node(l, x, r)) → r
elem(node(l, x, r)) → x
append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))

The set Q consists of the following terms:

isEmpty(empty)
isEmpty(node(x0, x1, x2))
left(empty)
left(node(x0, x1, x2))
right(empty)
right(node(x0, x1, x2))
elem(node(x0, x1, x2))
append(nil, x0)
append(cons(y, x0), x1)

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

(29) Rewriting (EQUIVALENT transformation)

By rewriting [LPAR04] the rule LISTIFY(node(x0, x1, x2), y1) → IF(false, isEmpty(x0), x2, node(left(left(node(x0, x1, x2))), elem(left(node(x0, x1, x2))), node(right(left(node(x0, x1, x2))), elem(node(x0, x1, x2)), right(node(x0, x1, x2)))), y1, append(y1, node(x0, x1, x2))) at position [3,0,0] we obtained the following new rules [LPAR04]:

LISTIFY(node(x0, x1, x2), y1) → IF(false, isEmpty(x0), x2, node(left(x0), elem(left(node(x0, x1, x2))), node(right(left(node(x0, x1, x2))), elem(node(x0, x1, x2)), right(node(x0, x1, x2)))), y1, append(y1, node(x0, x1, x2)))

(30) Obligation:

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

IF(false, false, n, m, xs, ys) → LISTIFY(m, xs)
IF(false, true, n, m, xs, ys) → LISTIFY(n, ys)
LISTIFY(node(x0, x1, x2), y1) → IF(false, isEmpty(x0), x2, node(left(x0), elem(left(node(x0, x1, x2))), node(right(left(node(x0, x1, x2))), elem(node(x0, x1, x2)), right(node(x0, x1, x2)))), y1, append(y1, node(x0, x1, x2)))

The TRS R consists of the following rules:

isEmpty(empty) → true
isEmpty(node(l, x, r)) → false
left(empty) → empty
left(node(l, x, r)) → l
right(empty) → empty
right(node(l, x, r)) → r
elem(node(l, x, r)) → x
append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))

The set Q consists of the following terms:

isEmpty(empty)
isEmpty(node(x0, x1, x2))
left(empty)
left(node(x0, x1, x2))
right(empty)
right(node(x0, x1, x2))
elem(node(x0, x1, x2))
append(nil, x0)
append(cons(y, x0), x1)

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

(31) Rewriting (EQUIVALENT transformation)

By rewriting [LPAR04] the rule LISTIFY(node(x0, x1, x2), y1) → IF(false, isEmpty(x0), x2, node(left(x0), elem(left(node(x0, x1, x2))), node(right(left(node(x0, x1, x2))), elem(node(x0, x1, x2)), right(node(x0, x1, x2)))), y1, append(y1, node(x0, x1, x2))) at position [3,1,0] we obtained the following new rules [LPAR04]:

LISTIFY(node(x0, x1, x2), y1) → IF(false, isEmpty(x0), x2, node(left(x0), elem(x0), node(right(left(node(x0, x1, x2))), elem(node(x0, x1, x2)), right(node(x0, x1, x2)))), y1, append(y1, node(x0, x1, x2)))

(32) Obligation:

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

IF(false, false, n, m, xs, ys) → LISTIFY(m, xs)
IF(false, true, n, m, xs, ys) → LISTIFY(n, ys)
LISTIFY(node(x0, x1, x2), y1) → IF(false, isEmpty(x0), x2, node(left(x0), elem(x0), node(right(left(node(x0, x1, x2))), elem(node(x0, x1, x2)), right(node(x0, x1, x2)))), y1, append(y1, node(x0, x1, x2)))

The TRS R consists of the following rules:

isEmpty(empty) → true
isEmpty(node(l, x, r)) → false
left(empty) → empty
left(node(l, x, r)) → l
right(empty) → empty
right(node(l, x, r)) → r
elem(node(l, x, r)) → x
append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))

The set Q consists of the following terms:

isEmpty(empty)
isEmpty(node(x0, x1, x2))
left(empty)
left(node(x0, x1, x2))
right(empty)
right(node(x0, x1, x2))
elem(node(x0, x1, x2))
append(nil, x0)
append(cons(y, x0), x1)

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

(33) Rewriting (EQUIVALENT transformation)

By rewriting [LPAR04] the rule LISTIFY(node(x0, x1, x2), y1) → IF(false, isEmpty(x0), x2, node(left(x0), elem(x0), node(right(left(node(x0, x1, x2))), elem(node(x0, x1, x2)), right(node(x0, x1, x2)))), y1, append(y1, node(x0, x1, x2))) at position [3,2,0,0] we obtained the following new rules [LPAR04]:

LISTIFY(node(x0, x1, x2), y1) → IF(false, isEmpty(x0), x2, node(left(x0), elem(x0), node(right(x0), elem(node(x0, x1, x2)), right(node(x0, x1, x2)))), y1, append(y1, node(x0, x1, x2)))

(34) Obligation:

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

IF(false, false, n, m, xs, ys) → LISTIFY(m, xs)
IF(false, true, n, m, xs, ys) → LISTIFY(n, ys)
LISTIFY(node(x0, x1, x2), y1) → IF(false, isEmpty(x0), x2, node(left(x0), elem(x0), node(right(x0), elem(node(x0, x1, x2)), right(node(x0, x1, x2)))), y1, append(y1, node(x0, x1, x2)))

The TRS R consists of the following rules:

isEmpty(empty) → true
isEmpty(node(l, x, r)) → false
left(empty) → empty
left(node(l, x, r)) → l
right(empty) → empty
right(node(l, x, r)) → r
elem(node(l, x, r)) → x
append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))

The set Q consists of the following terms:

isEmpty(empty)
isEmpty(node(x0, x1, x2))
left(empty)
left(node(x0, x1, x2))
right(empty)
right(node(x0, x1, x2))
elem(node(x0, x1, x2))
append(nil, x0)
append(cons(y, x0), x1)

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

(35) Rewriting (EQUIVALENT transformation)

By rewriting [LPAR04] the rule LISTIFY(node(x0, x1, x2), y1) → IF(false, isEmpty(x0), x2, node(left(x0), elem(x0), node(right(x0), elem(node(x0, x1, x2)), right(node(x0, x1, x2)))), y1, append(y1, node(x0, x1, x2))) at position [3,2,1] we obtained the following new rules [LPAR04]:

LISTIFY(node(x0, x1, x2), y1) → IF(false, isEmpty(x0), x2, node(left(x0), elem(x0), node(right(x0), x1, right(node(x0, x1, x2)))), y1, append(y1, node(x0, x1, x2)))

(36) Obligation:

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

IF(false, false, n, m, xs, ys) → LISTIFY(m, xs)
IF(false, true, n, m, xs, ys) → LISTIFY(n, ys)
LISTIFY(node(x0, x1, x2), y1) → IF(false, isEmpty(x0), x2, node(left(x0), elem(x0), node(right(x0), x1, right(node(x0, x1, x2)))), y1, append(y1, node(x0, x1, x2)))

The TRS R consists of the following rules:

isEmpty(empty) → true
isEmpty(node(l, x, r)) → false
left(empty) → empty
left(node(l, x, r)) → l
right(empty) → empty
right(node(l, x, r)) → r
elem(node(l, x, r)) → x
append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))

The set Q consists of the following terms:

isEmpty(empty)
isEmpty(node(x0, x1, x2))
left(empty)
left(node(x0, x1, x2))
right(empty)
right(node(x0, x1, x2))
elem(node(x0, x1, x2))
append(nil, x0)
append(cons(y, x0), x1)

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

(37) Rewriting (EQUIVALENT transformation)

By rewriting [LPAR04] the rule LISTIFY(node(x0, x1, x2), y1) → IF(false, isEmpty(x0), x2, node(left(x0), elem(x0), node(right(x0), x1, right(node(x0, x1, x2)))), y1, append(y1, node(x0, x1, x2))) at position [3,2,2] we obtained the following new rules [LPAR04]:

LISTIFY(node(x0, x1, x2), y1) → IF(false, isEmpty(x0), x2, node(left(x0), elem(x0), node(right(x0), x1, x2)), y1, append(y1, node(x0, x1, x2)))

(38) Obligation:

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

IF(false, false, n, m, xs, ys) → LISTIFY(m, xs)
IF(false, true, n, m, xs, ys) → LISTIFY(n, ys)
LISTIFY(node(x0, x1, x2), y1) → IF(false, isEmpty(x0), x2, node(left(x0), elem(x0), node(right(x0), x1, x2)), y1, append(y1, node(x0, x1, x2)))

The TRS R consists of the following rules:

isEmpty(empty) → true
isEmpty(node(l, x, r)) → false
left(empty) → empty
left(node(l, x, r)) → l
right(empty) → empty
right(node(l, x, r)) → r
elem(node(l, x, r)) → x
append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))

The set Q consists of the following terms:

isEmpty(empty)
isEmpty(node(x0, x1, x2))
left(empty)
left(node(x0, x1, x2))
right(empty)
right(node(x0, x1, x2))
elem(node(x0, x1, x2))
append(nil, x0)
append(cons(y, x0), x1)

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

(39) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule LISTIFY(node(x0, x1, x2), y1) → IF(false, isEmpty(x0), x2, node(left(x0), elem(x0), node(right(x0), x1, x2)), y1, append(y1, node(x0, x1, x2))) at position [1] we obtained the following new rules [LPAR04]:

LISTIFY(node(empty, y1, y2), y3) → IF(false, true, y2, node(left(empty), elem(empty), node(right(empty), y1, y2)), y3, append(y3, node(empty, y1, y2)))
LISTIFY(node(node(x0, x1, x2), y1, y2), y3) → IF(false, false, y2, node(left(node(x0, x1, x2)), elem(node(x0, x1, x2)), node(right(node(x0, x1, x2)), y1, y2)), y3, append(y3, node(node(x0, x1, x2), y1, y2)))

(40) Obligation:

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

IF(false, false, n, m, xs, ys) → LISTIFY(m, xs)
IF(false, true, n, m, xs, ys) → LISTIFY(n, ys)
LISTIFY(node(empty, y1, y2), y3) → IF(false, true, y2, node(left(empty), elem(empty), node(right(empty), y1, y2)), y3, append(y3, node(empty, y1, y2)))
LISTIFY(node(node(x0, x1, x2), y1, y2), y3) → IF(false, false, y2, node(left(node(x0, x1, x2)), elem(node(x0, x1, x2)), node(right(node(x0, x1, x2)), y1, y2)), y3, append(y3, node(node(x0, x1, x2), y1, y2)))

The TRS R consists of the following rules:

isEmpty(empty) → true
isEmpty(node(l, x, r)) → false
left(empty) → empty
left(node(l, x, r)) → l
right(empty) → empty
right(node(l, x, r)) → r
elem(node(l, x, r)) → x
append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))

The set Q consists of the following terms:

isEmpty(empty)
isEmpty(node(x0, x1, x2))
left(empty)
left(node(x0, x1, x2))
right(empty)
right(node(x0, x1, x2))
elem(node(x0, x1, x2))
append(nil, x0)
append(cons(y, x0), x1)

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

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

(42) Obligation:

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

IF(false, false, n, m, xs, ys) → LISTIFY(m, xs)
IF(false, true, n, m, xs, ys) → LISTIFY(n, ys)
LISTIFY(node(empty, y1, y2), y3) → IF(false, true, y2, node(left(empty), elem(empty), node(right(empty), y1, y2)), y3, append(y3, node(empty, y1, y2)))
LISTIFY(node(node(x0, x1, x2), y1, y2), y3) → IF(false, false, y2, node(left(node(x0, x1, x2)), elem(node(x0, x1, x2)), node(right(node(x0, x1, x2)), y1, y2)), y3, append(y3, node(node(x0, x1, x2), y1, y2)))

The TRS R consists of the following rules:

left(node(l, x, r)) → l
elem(node(l, x, r)) → x
right(node(l, x, r)) → r
append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))
left(empty) → empty
right(empty) → empty

The set Q consists of the following terms:

isEmpty(empty)
isEmpty(node(x0, x1, x2))
left(empty)
left(node(x0, x1, x2))
right(empty)
right(node(x0, x1, x2))
elem(node(x0, x1, x2))
append(nil, x0)
append(cons(y, x0), x1)

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

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

isEmpty(empty)
isEmpty(node(x0, x1, x2))

(44) Obligation:

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

IF(false, false, n, m, xs, ys) → LISTIFY(m, xs)
IF(false, true, n, m, xs, ys) → LISTIFY(n, ys)
LISTIFY(node(empty, y1, y2), y3) → IF(false, true, y2, node(left(empty), elem(empty), node(right(empty), y1, y2)), y3, append(y3, node(empty, y1, y2)))
LISTIFY(node(node(x0, x1, x2), y1, y2), y3) → IF(false, false, y2, node(left(node(x0, x1, x2)), elem(node(x0, x1, x2)), node(right(node(x0, x1, x2)), y1, y2)), y3, append(y3, node(node(x0, x1, x2), y1, y2)))

The TRS R consists of the following rules:

left(node(l, x, r)) → l
elem(node(l, x, r)) → x
right(node(l, x, r)) → r
append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))
left(empty) → empty
right(empty) → empty

The set Q consists of the following terms:

left(empty)
left(node(x0, x1, x2))
right(empty)
right(node(x0, x1, x2))
elem(node(x0, x1, x2))
append(nil, x0)
append(cons(y, x0), x1)

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

(45) Rewriting (EQUIVALENT transformation)

By rewriting [LPAR04] the rule LISTIFY(node(empty, y1, y2), y3) → IF(false, true, y2, node(left(empty), elem(empty), node(right(empty), y1, y2)), y3, append(y3, node(empty, y1, y2))) at position [3,0] we obtained the following new rules [LPAR04]:

LISTIFY(node(empty, y1, y2), y3) → IF(false, true, y2, node(empty, elem(empty), node(right(empty), y1, y2)), y3, append(y3, node(empty, y1, y2)))

(46) Obligation:

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

IF(false, false, n, m, xs, ys) → LISTIFY(m, xs)
IF(false, true, n, m, xs, ys) → LISTIFY(n, ys)
LISTIFY(node(node(x0, x1, x2), y1, y2), y3) → IF(false, false, y2, node(left(node(x0, x1, x2)), elem(node(x0, x1, x2)), node(right(node(x0, x1, x2)), y1, y2)), y3, append(y3, node(node(x0, x1, x2), y1, y2)))
LISTIFY(node(empty, y1, y2), y3) → IF(false, true, y2, node(empty, elem(empty), node(right(empty), y1, y2)), y3, append(y3, node(empty, y1, y2)))

The TRS R consists of the following rules:

left(node(l, x, r)) → l
elem(node(l, x, r)) → x
right(node(l, x, r)) → r
append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))
left(empty) → empty
right(empty) → empty

The set Q consists of the following terms:

left(empty)
left(node(x0, x1, x2))
right(empty)
right(node(x0, x1, x2))
elem(node(x0, x1, x2))
append(nil, x0)
append(cons(y, x0), x1)

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

(47) UsableRulesProof (EQUIVALENT transformation)

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

(48) Obligation:

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

IF(false, false, n, m, xs, ys) → LISTIFY(m, xs)
IF(false, true, n, m, xs, ys) → LISTIFY(n, ys)
LISTIFY(node(node(x0, x1, x2), y1, y2), y3) → IF(false, false, y2, node(left(node(x0, x1, x2)), elem(node(x0, x1, x2)), node(right(node(x0, x1, x2)), y1, y2)), y3, append(y3, node(node(x0, x1, x2), y1, y2)))
LISTIFY(node(empty, y1, y2), y3) → IF(false, true, y2, node(empty, elem(empty), node(right(empty), y1, y2)), y3, append(y3, node(empty, y1, y2)))

The TRS R consists of the following rules:

right(empty) → empty
append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))
left(node(l, x, r)) → l
elem(node(l, x, r)) → x
right(node(l, x, r)) → r

The set Q consists of the following terms:

left(empty)
left(node(x0, x1, x2))
right(empty)
right(node(x0, x1, x2))
elem(node(x0, x1, x2))
append(nil, x0)
append(cons(y, x0), x1)

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

(49) Rewriting (EQUIVALENT transformation)

By rewriting [LPAR04] the rule LISTIFY(node(node(x0, x1, x2), y1, y2), y3) → IF(false, false, y2, node(left(node(x0, x1, x2)), elem(node(x0, x1, x2)), node(right(node(x0, x1, x2)), y1, y2)), y3, append(y3, node(node(x0, x1, x2), y1, y2))) at position [3,0] we obtained the following new rules [LPAR04]:

LISTIFY(node(node(x0, x1, x2), y1, y2), y3) → IF(false, false, y2, node(x0, elem(node(x0, x1, x2)), node(right(node(x0, x1, x2)), y1, y2)), y3, append(y3, node(node(x0, x1, x2), y1, y2)))

(50) Obligation:

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

IF(false, false, n, m, xs, ys) → LISTIFY(m, xs)
IF(false, true, n, m, xs, ys) → LISTIFY(n, ys)
LISTIFY(node(empty, y1, y2), y3) → IF(false, true, y2, node(empty, elem(empty), node(right(empty), y1, y2)), y3, append(y3, node(empty, y1, y2)))
LISTIFY(node(node(x0, x1, x2), y1, y2), y3) → IF(false, false, y2, node(x0, elem(node(x0, x1, x2)), node(right(node(x0, x1, x2)), y1, y2)), y3, append(y3, node(node(x0, x1, x2), y1, y2)))

The TRS R consists of the following rules:

right(empty) → empty
append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))
left(node(l, x, r)) → l
elem(node(l, x, r)) → x
right(node(l, x, r)) → r

The set Q consists of the following terms:

left(empty)
left(node(x0, x1, x2))
right(empty)
right(node(x0, x1, x2))
elem(node(x0, x1, x2))
append(nil, x0)
append(cons(y, x0), x1)

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

(51) UsableRulesProof (EQUIVALENT transformation)

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

(52) Obligation:

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

IF(false, false, n, m, xs, ys) → LISTIFY(m, xs)
IF(false, true, n, m, xs, ys) → LISTIFY(n, ys)
LISTIFY(node(empty, y1, y2), y3) → IF(false, true, y2, node(empty, elem(empty), node(right(empty), y1, y2)), y3, append(y3, node(empty, y1, y2)))
LISTIFY(node(node(x0, x1, x2), y1, y2), y3) → IF(false, false, y2, node(x0, elem(node(x0, x1, x2)), node(right(node(x0, x1, x2)), y1, y2)), y3, append(y3, node(node(x0, x1, x2), y1, y2)))

The TRS R consists of the following rules:

elem(node(l, x, r)) → x
right(node(l, x, r)) → r
append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))
right(empty) → empty

The set Q consists of the following terms:

left(empty)
left(node(x0, x1, x2))
right(empty)
right(node(x0, x1, x2))
elem(node(x0, x1, x2))
append(nil, x0)
append(cons(y, x0), x1)

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

(53) QReductionProof (EQUIVALENT transformation)

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

left(empty)
left(node(x0, x1, x2))

(54) Obligation:

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

IF(false, false, n, m, xs, ys) → LISTIFY(m, xs)
IF(false, true, n, m, xs, ys) → LISTIFY(n, ys)
LISTIFY(node(empty, y1, y2), y3) → IF(false, true, y2, node(empty, elem(empty), node(right(empty), y1, y2)), y3, append(y3, node(empty, y1, y2)))
LISTIFY(node(node(x0, x1, x2), y1, y2), y3) → IF(false, false, y2, node(x0, elem(node(x0, x1, x2)), node(right(node(x0, x1, x2)), y1, y2)), y3, append(y3, node(node(x0, x1, x2), y1, y2)))

The TRS R consists of the following rules:

elem(node(l, x, r)) → x
right(node(l, x, r)) → r
append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))
right(empty) → empty

The set Q consists of the following terms:

right(empty)
right(node(x0, x1, x2))
elem(node(x0, x1, x2))
append(nil, x0)
append(cons(y, x0), x1)

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

(55) Rewriting (EQUIVALENT transformation)

By rewriting [LPAR04] the rule LISTIFY(node(empty, y1, y2), y3) → IF(false, true, y2, node(empty, elem(empty), node(right(empty), y1, y2)), y3, append(y3, node(empty, y1, y2))) at position [3,2,0] we obtained the following new rules [LPAR04]:

LISTIFY(node(empty, y1, y2), y3) → IF(false, true, y2, node(empty, elem(empty), node(empty, y1, y2)), y3, append(y3, node(empty, y1, y2)))

(56) Obligation:

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

IF(false, false, n, m, xs, ys) → LISTIFY(m, xs)
IF(false, true, n, m, xs, ys) → LISTIFY(n, ys)
LISTIFY(node(node(x0, x1, x2), y1, y2), y3) → IF(false, false, y2, node(x0, elem(node(x0, x1, x2)), node(right(node(x0, x1, x2)), y1, y2)), y3, append(y3, node(node(x0, x1, x2), y1, y2)))
LISTIFY(node(empty, y1, y2), y3) → IF(false, true, y2, node(empty, elem(empty), node(empty, y1, y2)), y3, append(y3, node(empty, y1, y2)))

The TRS R consists of the following rules:

elem(node(l, x, r)) → x
right(node(l, x, r)) → r
append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))
right(empty) → empty

The set Q consists of the following terms:

right(empty)
right(node(x0, x1, x2))
elem(node(x0, x1, x2))
append(nil, x0)
append(cons(y, x0), x1)

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

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

(58) Obligation:

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

IF(false, false, n, m, xs, ys) → LISTIFY(m, xs)
IF(false, true, n, m, xs, ys) → LISTIFY(n, ys)
LISTIFY(node(node(x0, x1, x2), y1, y2), y3) → IF(false, false, y2, node(x0, elem(node(x0, x1, x2)), node(right(node(x0, x1, x2)), y1, y2)), y3, append(y3, node(node(x0, x1, x2), y1, y2)))
LISTIFY(node(empty, y1, y2), y3) → IF(false, true, y2, node(empty, elem(empty), node(empty, y1, y2)), y3, append(y3, node(empty, y1, y2)))

The TRS R consists of the following rules:

append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))
elem(node(l, x, r)) → x
right(node(l, x, r)) → r

The set Q consists of the following terms:

right(empty)
right(node(x0, x1, x2))
elem(node(x0, x1, x2))
append(nil, x0)
append(cons(y, x0), x1)

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

(59) Rewriting (EQUIVALENT transformation)

By rewriting [LPAR04] the rule LISTIFY(node(node(x0, x1, x2), y1, y2), y3) → IF(false, false, y2, node(x0, elem(node(x0, x1, x2)), node(right(node(x0, x1, x2)), y1, y2)), y3, append(y3, node(node(x0, x1, x2), y1, y2))) at position [3,1] we obtained the following new rules [LPAR04]:

LISTIFY(node(node(x0, x1, x2), y1, y2), y3) → IF(false, false, y2, node(x0, x1, node(right(node(x0, x1, x2)), y1, y2)), y3, append(y3, node(node(x0, x1, x2), y1, y2)))

(60) Obligation:

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

IF(false, false, n, m, xs, ys) → LISTIFY(m, xs)
IF(false, true, n, m, xs, ys) → LISTIFY(n, ys)
LISTIFY(node(empty, y1, y2), y3) → IF(false, true, y2, node(empty, elem(empty), node(empty, y1, y2)), y3, append(y3, node(empty, y1, y2)))
LISTIFY(node(node(x0, x1, x2), y1, y2), y3) → IF(false, false, y2, node(x0, x1, node(right(node(x0, x1, x2)), y1, y2)), y3, append(y3, node(node(x0, x1, x2), y1, y2)))

The TRS R consists of the following rules:

append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))
elem(node(l, x, r)) → x
right(node(l, x, r)) → r

The set Q consists of the following terms:

right(empty)
right(node(x0, x1, x2))
elem(node(x0, x1, x2))
append(nil, x0)
append(cons(y, x0), x1)

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

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

(62) Obligation:

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

IF(false, false, n, m, xs, ys) → LISTIFY(m, xs)
IF(false, true, n, m, xs, ys) → LISTIFY(n, ys)
LISTIFY(node(empty, y1, y2), y3) → IF(false, true, y2, node(empty, elem(empty), node(empty, y1, y2)), y3, append(y3, node(empty, y1, y2)))
LISTIFY(node(node(x0, x1, x2), y1, y2), y3) → IF(false, false, y2, node(x0, x1, node(right(node(x0, x1, x2)), y1, y2)), y3, append(y3, node(node(x0, x1, x2), y1, y2)))

The TRS R consists of the following rules:

right(node(l, x, r)) → r
append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))

The set Q consists of the following terms:

right(empty)
right(node(x0, x1, x2))
elem(node(x0, x1, x2))
append(nil, x0)
append(cons(y, x0), x1)

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

(63) Rewriting (EQUIVALENT transformation)

By rewriting [LPAR04] the rule LISTIFY(node(node(x0, x1, x2), y1, y2), y3) → IF(false, false, y2, node(x0, x1, node(right(node(x0, x1, x2)), y1, y2)), y3, append(y3, node(node(x0, x1, x2), y1, y2))) at position [3,2,0] we obtained the following new rules [LPAR04]:

LISTIFY(node(node(x0, x1, x2), y1, y2), y3) → IF(false, false, y2, node(x0, x1, node(x2, y1, y2)), y3, append(y3, node(node(x0, x1, x2), y1, y2)))

(64) Obligation:

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

IF(false, false, n, m, xs, ys) → LISTIFY(m, xs)
IF(false, true, n, m, xs, ys) → LISTIFY(n, ys)
LISTIFY(node(empty, y1, y2), y3) → IF(false, true, y2, node(empty, elem(empty), node(empty, y1, y2)), y3, append(y3, node(empty, y1, y2)))
LISTIFY(node(node(x0, x1, x2), y1, y2), y3) → IF(false, false, y2, node(x0, x1, node(x2, y1, y2)), y3, append(y3, node(node(x0, x1, x2), y1, y2)))

The TRS R consists of the following rules:

right(node(l, x, r)) → r
append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))

The set Q consists of the following terms:

right(empty)
right(node(x0, x1, x2))
elem(node(x0, x1, x2))
append(nil, x0)
append(cons(y, x0), x1)

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

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

(66) Obligation:

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

IF(false, false, n, m, xs, ys) → LISTIFY(m, xs)
IF(false, true, n, m, xs, ys) → LISTIFY(n, ys)
LISTIFY(node(empty, y1, y2), y3) → IF(false, true, y2, node(empty, elem(empty), node(empty, y1, y2)), y3, append(y3, node(empty, y1, y2)))
LISTIFY(node(node(x0, x1, x2), y1, y2), y3) → IF(false, false, y2, node(x0, x1, node(x2, y1, y2)), y3, append(y3, node(node(x0, x1, x2), y1, y2)))

The TRS R consists of the following rules:

append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))

The set Q consists of the following terms:

right(empty)
right(node(x0, x1, x2))
elem(node(x0, x1, x2))
append(nil, x0)
append(cons(y, x0), x1)

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

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

right(empty)
right(node(x0, x1, x2))

(68) Obligation:

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

IF(false, false, n, m, xs, ys) → LISTIFY(m, xs)
IF(false, true, n, m, xs, ys) → LISTIFY(n, ys)
LISTIFY(node(empty, y1, y2), y3) → IF(false, true, y2, node(empty, elem(empty), node(empty, y1, y2)), y3, append(y3, node(empty, y1, y2)))
LISTIFY(node(node(x0, x1, x2), y1, y2), y3) → IF(false, false, y2, node(x0, x1, node(x2, y1, y2)), y3, append(y3, node(node(x0, x1, x2), y1, y2)))

The TRS R consists of the following rules:

append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))

The set Q consists of the following terms:

elem(node(x0, x1, x2))
append(nil, x0)
append(cons(y, x0), x1)

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

(69) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule IF(false, false, n, m, xs, ys) → LISTIFY(m, xs) we obtained the following new rules [LPAR04]:

IF(false, false, z4, node(z0, z1, node(z2, z3, z4)), z5, y_0) → LISTIFY(node(z0, z1, node(z2, z3, z4)), z5)

(70) Obligation:

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

IF(false, true, n, m, xs, ys) → LISTIFY(n, ys)
LISTIFY(node(empty, y1, y2), y3) → IF(false, true, y2, node(empty, elem(empty), node(empty, y1, y2)), y3, append(y3, node(empty, y1, y2)))
LISTIFY(node(node(x0, x1, x2), y1, y2), y3) → IF(false, false, y2, node(x0, x1, node(x2, y1, y2)), y3, append(y3, node(node(x0, x1, x2), y1, y2)))
IF(false, false, z4, node(z0, z1, node(z2, z3, z4)), z5, y_0) → LISTIFY(node(z0, z1, node(z2, z3, z4)), z5)

The TRS R consists of the following rules:

append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))

The set Q consists of the following terms:

elem(node(x0, x1, x2))
append(nil, x0)
append(cons(y, x0), x1)

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

(71) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule IF(false, false, n, m, xs, ys) → LISTIFY(m, xs) we obtained the following new rules [LPAR04]:

IF(false, false, z4, node(z0, z1, node(z2, z3, z4)), z5, y_0) → LISTIFY(node(z0, z1, node(z2, z3, z4)), z5)

(72) Obligation:

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

IF(false, true, n, m, xs, ys) → LISTIFY(n, ys)
LISTIFY(node(empty, y1, y2), y3) → IF(false, true, y2, node(empty, elem(empty), node(empty, y1, y2)), y3, append(y3, node(empty, y1, y2)))
LISTIFY(node(node(x0, x1, x2), y1, y2), y3) → IF(false, false, y2, node(x0, x1, node(x2, y1, y2)), y3, append(y3, node(node(x0, x1, x2), y1, y2)))
IF(false, false, z4, node(z0, z1, node(z2, z3, z4)), z5, y_0) → LISTIFY(node(z0, z1, node(z2, z3, z4)), z5)

The TRS R consists of the following rules:

append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))

The set Q consists of the following terms:

elem(node(x0, x1, x2))
append(nil, x0)
append(cons(y, x0), x1)

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

(73) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule IF(false, true, n, m, xs, ys) → LISTIFY(n, ys) we obtained the following new rules [LPAR04]:

IF(false, true, z1, node(empty, elem(empty), node(empty, z0, z1)), z2, y_0) → LISTIFY(z1, y_0)

(74) Obligation:

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

LISTIFY(node(empty, y1, y2), y3) → IF(false, true, y2, node(empty, elem(empty), node(empty, y1, y2)), y3, append(y3, node(empty, y1, y2)))
LISTIFY(node(node(x0, x1, x2), y1, y2), y3) → IF(false, false, y2, node(x0, x1, node(x2, y1, y2)), y3, append(y3, node(node(x0, x1, x2), y1, y2)))
IF(false, false, z4, node(z0, z1, node(z2, z3, z4)), z5, y_0) → LISTIFY(node(z0, z1, node(z2, z3, z4)), z5)
IF(false, true, z1, node(empty, elem(empty), node(empty, z0, z1)), z2, y_0) → LISTIFY(z1, y_0)

The TRS R consists of the following rules:

append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))

The set Q consists of the following terms:

elem(node(x0, x1, x2))
append(nil, x0)
append(cons(y, x0), x1)

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

(75) ForwardInstantiation (EQUIVALENT transformation)

By forward instantiating [JAR06] the rule IF(false, false, z4, node(z0, z1, node(z2, z3, z4)), z5, y_0) → LISTIFY(node(z0, z1, node(z2, z3, z4)), z5) we obtained the following new rules [LPAR04]:

IF(false, false, x0, node(empty, x2, node(x3, x4, x0)), x5, x6) → LISTIFY(node(empty, x2, node(x3, x4, x0)), x5)
IF(false, false, x0, node(node(y_0, y_1, y_2), x2, node(x3, x4, x0)), x5, x6) → LISTIFY(node(node(y_0, y_1, y_2), x2, node(x3, x4, x0)), x5)

(76) Obligation:

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

LISTIFY(node(empty, y1, y2), y3) → IF(false, true, y2, node(empty, elem(empty), node(empty, y1, y2)), y3, append(y3, node(empty, y1, y2)))
LISTIFY(node(node(x0, x1, x2), y1, y2), y3) → IF(false, false, y2, node(x0, x1, node(x2, y1, y2)), y3, append(y3, node(node(x0, x1, x2), y1, y2)))
IF(false, true, z1, node(empty, elem(empty), node(empty, z0, z1)), z2, y_0) → LISTIFY(z1, y_0)
IF(false, false, x0, node(empty, x2, node(x3, x4, x0)), x5, x6) → LISTIFY(node(empty, x2, node(x3, x4, x0)), x5)
IF(false, false, x0, node(node(y_0, y_1, y_2), x2, node(x3, x4, x0)), x5, x6) → LISTIFY(node(node(y_0, y_1, y_2), x2, node(x3, x4, x0)), x5)

The TRS R consists of the following rules:

append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))

The set Q consists of the following terms:

elem(node(x0, x1, x2))
append(nil, x0)
append(cons(y, x0), x1)

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

(77) ForwardInstantiation (EQUIVALENT transformation)

By forward instantiating [JAR06] the rule LISTIFY(node(node(x0, x1, x2), y1, y2), y3) → IF(false, false, y2, node(x0, x1, node(x2, y1, y2)), y3, append(y3, node(node(x0, x1, x2), y1, y2))) we obtained the following new rules [LPAR04]:

LISTIFY(node(node(empty, x1, x2), x3, x4), x5) → IF(false, false, x4, node(empty, x1, node(x2, x3, x4)), x5, append(x5, node(node(empty, x1, x2), x3, x4)))
LISTIFY(node(node(node(y_1, y_2, y_3), x1, x2), x3, x4), x5) → IF(false, false, x4, node(node(y_1, y_2, y_3), x1, node(x2, x3, x4)), x5, append(x5, node(node(node(y_1, y_2, y_3), x1, x2), x3, x4)))

(78) Obligation:

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

LISTIFY(node(empty, y1, y2), y3) → IF(false, true, y2, node(empty, elem(empty), node(empty, y1, y2)), y3, append(y3, node(empty, y1, y2)))
IF(false, true, z1, node(empty, elem(empty), node(empty, z0, z1)), z2, y_0) → LISTIFY(z1, y_0)
IF(false, false, x0, node(empty, x2, node(x3, x4, x0)), x5, x6) → LISTIFY(node(empty, x2, node(x3, x4, x0)), x5)
IF(false, false, x0, node(node(y_0, y_1, y_2), x2, node(x3, x4, x0)), x5, x6) → LISTIFY(node(node(y_0, y_1, y_2), x2, node(x3, x4, x0)), x5)
LISTIFY(node(node(empty, x1, x2), x3, x4), x5) → IF(false, false, x4, node(empty, x1, node(x2, x3, x4)), x5, append(x5, node(node(empty, x1, x2), x3, x4)))
LISTIFY(node(node(node(y_1, y_2, y_3), x1, x2), x3, x4), x5) → IF(false, false, x4, node(node(y_1, y_2, y_3), x1, node(x2, x3, x4)), x5, append(x5, node(node(node(y_1, y_2, y_3), x1, x2), x3, x4)))

The TRS R consists of the following rules:

append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))

The set Q consists of the following terms:

elem(node(x0, x1, x2))
append(nil, x0)
append(cons(y, x0), x1)

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

(79) ForwardInstantiation (EQUIVALENT transformation)

By forward instantiating [JAR06] the rule IF(false, true, z1, node(empty, elem(empty), node(empty, z0, z1)), z2, y_0) → LISTIFY(z1, y_0) we obtained the following new rules [LPAR04]:

IF(false, true, node(empty, y_0, y_1), node(empty, elem(empty), node(empty, x1, node(empty, y_0, y_1))), x2, x3) → LISTIFY(node(empty, y_0, y_1), x3)
IF(false, true, node(node(empty, y_0, y_1), y_2, y_3), node(empty, elem(empty), node(empty, x1, node(node(empty, y_0, y_1), y_2, y_3))), x2, x3) → LISTIFY(node(node(empty, y_0, y_1), y_2, y_3), x3)
IF(false, true, node(node(node(y_0, y_1, y_2), y_3, y_4), y_5, y_6), node(empty, elem(empty), node(empty, x1, node(node(node(y_0, y_1, y_2), y_3, y_4), y_5, y_6))), x2, x3) → LISTIFY(node(node(node(y_0, y_1, y_2), y_3, y_4), y_5, y_6), x3)

(80) Obligation:

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

LISTIFY(node(empty, y1, y2), y3) → IF(false, true, y2, node(empty, elem(empty), node(empty, y1, y2)), y3, append(y3, node(empty, y1, y2)))
IF(false, false, x0, node(empty, x2, node(x3, x4, x0)), x5, x6) → LISTIFY(node(empty, x2, node(x3, x4, x0)), x5)
IF(false, false, x0, node(node(y_0, y_1, y_2), x2, node(x3, x4, x0)), x5, x6) → LISTIFY(node(node(y_0, y_1, y_2), x2, node(x3, x4, x0)), x5)
LISTIFY(node(node(empty, x1, x2), x3, x4), x5) → IF(false, false, x4, node(empty, x1, node(x2, x3, x4)), x5, append(x5, node(node(empty, x1, x2), x3, x4)))
LISTIFY(node(node(node(y_1, y_2, y_3), x1, x2), x3, x4), x5) → IF(false, false, x4, node(node(y_1, y_2, y_3), x1, node(x2, x3, x4)), x5, append(x5, node(node(node(y_1, y_2, y_3), x1, x2), x3, x4)))
IF(false, true, node(empty, y_0, y_1), node(empty, elem(empty), node(empty, x1, node(empty, y_0, y_1))), x2, x3) → LISTIFY(node(empty, y_0, y_1), x3)
IF(false, true, node(node(empty, y_0, y_1), y_2, y_3), node(empty, elem(empty), node(empty, x1, node(node(empty, y_0, y_1), y_2, y_3))), x2, x3) → LISTIFY(node(node(empty, y_0, y_1), y_2, y_3), x3)
IF(false, true, node(node(node(y_0, y_1, y_2), y_3, y_4), y_5, y_6), node(empty, elem(empty), node(empty, x1, node(node(node(y_0, y_1, y_2), y_3, y_4), y_5, y_6))), x2, x3) → LISTIFY(node(node(node(y_0, y_1, y_2), y_3, y_4), y_5, y_6), x3)

The TRS R consists of the following rules:

append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))

The set Q consists of the following terms:

elem(node(x0, x1, x2))
append(nil, x0)
append(cons(y, x0), x1)

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

(81) ForwardInstantiation (EQUIVALENT transformation)

By forward instantiating [JAR06] the rule LISTIFY(node(empty, y1, y2), y3) → IF(false, true, y2, node(empty, elem(empty), node(empty, y1, y2)), y3, append(y3, node(empty, y1, y2))) we obtained the following new rules [LPAR04]:

LISTIFY(node(empty, x0, node(empty, y_0, y_1)), x2) → IF(false, true, node(empty, y_0, y_1), node(empty, elem(empty), node(empty, x0, node(empty, y_0, y_1))), x2, append(x2, node(empty, x0, node(empty, y_0, y_1))))
LISTIFY(node(empty, x0, node(node(empty, y_0, y_1), y_2, y_3)), x2) → IF(false, true, node(node(empty, y_0, y_1), y_2, y_3), node(empty, elem(empty), node(empty, x0, node(node(empty, y_0, y_1), y_2, y_3))), x2, append(x2, node(empty, x0, node(node(empty, y_0, y_1), y_2, y_3))))
LISTIFY(node(empty, x0, node(node(node(y_0, y_1, y_2), y_3, y_4), y_5, y_6)), x2) → IF(false, true, node(node(node(y_0, y_1, y_2), y_3, y_4), y_5, y_6), node(empty, elem(empty), node(empty, x0, node(node(node(y_0, y_1, y_2), y_3, y_4), y_5, y_6))), x2, append(x2, node(empty, x0, node(node(node(y_0, y_1, y_2), y_3, y_4), y_5, y_6))))

(82) Obligation:

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

IF(false, false, x0, node(empty, x2, node(x3, x4, x0)), x5, x6) → LISTIFY(node(empty, x2, node(x3, x4, x0)), x5)
IF(false, false, x0, node(node(y_0, y_1, y_2), x2, node(x3, x4, x0)), x5, x6) → LISTIFY(node(node(y_0, y_1, y_2), x2, node(x3, x4, x0)), x5)
LISTIFY(node(node(empty, x1, x2), x3, x4), x5) → IF(false, false, x4, node(empty, x1, node(x2, x3, x4)), x5, append(x5, node(node(empty, x1, x2), x3, x4)))
LISTIFY(node(node(node(y_1, y_2, y_3), x1, x2), x3, x4), x5) → IF(false, false, x4, node(node(y_1, y_2, y_3), x1, node(x2, x3, x4)), x5, append(x5, node(node(node(y_1, y_2, y_3), x1, x2), x3, x4)))
IF(false, true, node(empty, y_0, y_1), node(empty, elem(empty), node(empty, x1, node(empty, y_0, y_1))), x2, x3) → LISTIFY(node(empty, y_0, y_1), x3)
IF(false, true, node(node(empty, y_0, y_1), y_2, y_3), node(empty, elem(empty), node(empty, x1, node(node(empty, y_0, y_1), y_2, y_3))), x2, x3) → LISTIFY(node(node(empty, y_0, y_1), y_2, y_3), x3)
IF(false, true, node(node(node(y_0, y_1, y_2), y_3, y_4), y_5, y_6), node(empty, elem(empty), node(empty, x1, node(node(node(y_0, y_1, y_2), y_3, y_4), y_5, y_6))), x2, x3) → LISTIFY(node(node(node(y_0, y_1, y_2), y_3, y_4), y_5, y_6), x3)
LISTIFY(node(empty, x0, node(empty, y_0, y_1)), x2) → IF(false, true, node(empty, y_0, y_1), node(empty, elem(empty), node(empty, x0, node(empty, y_0, y_1))), x2, append(x2, node(empty, x0, node(empty, y_0, y_1))))
LISTIFY(node(empty, x0, node(node(empty, y_0, y_1), y_2, y_3)), x2) → IF(false, true, node(node(empty, y_0, y_1), y_2, y_3), node(empty, elem(empty), node(empty, x0, node(node(empty, y_0, y_1), y_2, y_3))), x2, append(x2, node(empty, x0, node(node(empty, y_0, y_1), y_2, y_3))))
LISTIFY(node(empty, x0, node(node(node(y_0, y_1, y_2), y_3, y_4), y_5, y_6)), x2) → IF(false, true, node(node(node(y_0, y_1, y_2), y_3, y_4), y_5, y_6), node(empty, elem(empty), node(empty, x0, node(node(node(y_0, y_1, y_2), y_3, y_4), y_5, y_6))), x2, append(x2, node(empty, x0, node(node(node(y_0, y_1, y_2), y_3, y_4), y_5, y_6))))

The TRS R consists of the following rules:

append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))

The set Q consists of the following terms:

elem(node(x0, x1, x2))
append(nil, x0)
append(cons(y, x0), x1)

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

(83) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

IF(false, true, node(empty, y_0, y_1), node(empty, elem(empty), node(empty, x1, node(empty, y_0, y_1))), x2, x3) → LISTIFY(node(empty, y_0, y_1), x3)
IF(false, true, node(node(empty, y_0, y_1), y_2, y_3), node(empty, elem(empty), node(empty, x1, node(node(empty, y_0, y_1), y_2, y_3))), x2, x3) → LISTIFY(node(node(empty, y_0, y_1), y_2, y_3), x3)
IF(false, true, node(node(node(y_0, y_1, y_2), y_3, y_4), y_5, y_6), node(empty, elem(empty), node(empty, x1, node(node(node(y_0, y_1, y_2), y_3, y_4), y_5, y_6))), x2, x3) → LISTIFY(node(node(node(y_0, y_1, y_2), y_3, y_4), y_5, y_6), x3)

The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:

POL(IF(x₁, x₂, x₃, x₄, x₅, x₆)) = x₂ + x₄   
POL(LISTIFY(x₁, x₂)) = 1 + x₁   
POL(append(x₁, x₂)) = 0   
POL(cons(x₁, x₂)) = 0   
POL(elem(x₁)) = 0   
POL(empty) = 0   
POL(false) = 1   
POL(nil) = 0   
POL(node(x₁, x₂, x₃)) = 1 + x₁ + x₃   
POL(true) = 0   
POL(y) = 0   

The following usable rules [FROCOS05] were oriented: none

(84) Obligation:

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

IF(false, false, x0, node(empty, x2, node(x3, x4, x0)), x5, x6) → LISTIFY(node(empty, x2, node(x3, x4, x0)), x5)
IF(false, false, x0, node(node(y_0, y_1, y_2), x2, node(x3, x4, x0)), x5, x6) → LISTIFY(node(node(y_0, y_1, y_2), x2, node(x3, x4, x0)), x5)
LISTIFY(node(node(empty, x1, x2), x3, x4), x5) → IF(false, false, x4, node(empty, x1, node(x2, x3, x4)), x5, append(x5, node(node(empty, x1, x2), x3, x4)))
LISTIFY(node(node(node(y_1, y_2, y_3), x1, x2), x3, x4), x5) → IF(false, false, x4, node(node(y_1, y_2, y_3), x1, node(x2, x3, x4)), x5, append(x5, node(node(node(y_1, y_2, y_3), x1, x2), x3, x4)))
LISTIFY(node(empty, x0, node(empty, y_0, y_1)), x2) → IF(false, true, node(empty, y_0, y_1), node(empty, elem(empty), node(empty, x0, node(empty, y_0, y_1))), x2, append(x2, node(empty, x0, node(empty, y_0, y_1))))
LISTIFY(node(empty, x0, node(node(empty, y_0, y_1), y_2, y_3)), x2) → IF(false, true, node(node(empty, y_0, y_1), y_2, y_3), node(empty, elem(empty), node(empty, x0, node(node(empty, y_0, y_1), y_2, y_3))), x2, append(x2, node(empty, x0, node(node(empty, y_0, y_1), y_2, y_3))))
LISTIFY(node(empty, x0, node(node(node(y_0, y_1, y_2), y_3, y_4), y_5, y_6)), x2) → IF(false, true, node(node(node(y_0, y_1, y_2), y_3, y_4), y_5, y_6), node(empty, elem(empty), node(empty, x0, node(node(node(y_0, y_1, y_2), y_3, y_4), y_5, y_6))), x2, append(x2, node(empty, x0, node(node(node(y_0, y_1, y_2), y_3, y_4), y_5, y_6))))

The TRS R consists of the following rules:

append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))

The set Q consists of the following terms:

elem(node(x0, x1, x2))
append(nil, x0)
append(cons(y, x0), x1)

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

(85) DependencyGraphProof (EQUIVALENT transformation)

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

(86) Obligation:

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

LISTIFY(node(node(node(y_1, y_2, y_3), x1, x2), x3, x4), x5) → IF(false, false, x4, node(node(y_1, y_2, y_3), x1, node(x2, x3, x4)), x5, append(x5, node(node(node(y_1, y_2, y_3), x1, x2), x3, x4)))
IF(false, false, x0, node(node(y_0, y_1, y_2), x2, node(x3, x4, x0)), x5, x6) → LISTIFY(node(node(y_0, y_1, y_2), x2, node(x3, x4, x0)), x5)

The TRS R consists of the following rules:

append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))

The set Q consists of the following terms:

elem(node(x0, x1, x2))
append(nil, x0)
append(cons(y, x0), x1)

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

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

elem(node(x0, x1, x2))

(88) Obligation:

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

LISTIFY(node(node(node(y_1, y_2, y_3), x1, x2), x3, x4), x5) → IF(false, false, x4, node(node(y_1, y_2, y_3), x1, node(x2, x3, x4)), x5, append(x5, node(node(node(y_1, y_2, y_3), x1, x2), x3, x4)))
IF(false, false, x0, node(node(y_0, y_1, y_2), x2, node(x3, x4, x0)), x5, x6) → LISTIFY(node(node(y_0, y_1, y_2), x2, node(x3, x4, x0)), x5)

The TRS R consists of the following rules:

append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))

The set Q consists of the following terms:

append(nil, x0)
append(cons(y, x0), x1)

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

(89) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

LISTIFY(node(node(node(y_1, y_2, y_3), x1, x2), x3, x4), x5) → IF(false, false, x4, node(node(y_1, y_2, y_3), x1, node(x2, x3, x4)), x5, append(x5, node(node(node(y_1, y_2, y_3), x1, x2), x3, x4)))

The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:

POL(IF(x₁, x₂, x₃, x₄, x₅, x₆)) = x₄   
POL(LISTIFY(x₁, x₂)) = x₁   
POL(append(x₁, x₂)) = 0   
POL(cons(x₁, x₂)) = 0   
POL(false) = 0   
POL(nil) = 0   
POL(node(x₁, x₂, x₃)) = 1 + x₁ + x₂   
POL(y) = 0   

The following usable rules [FROCOS05] were oriented: none

(90) Obligation:

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

IF(false, false, x0, node(node(y_0, y_1, y_2), x2, node(x3, x4, x0)), x5, x6) → LISTIFY(node(node(y_0, y_1, y_2), x2, node(x3, x4, x0)), x5)

The TRS R consists of the following rules:

append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))

The set Q consists of the following terms:

append(nil, x0)
append(cons(y, x0), x1)

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

(91) DependencyGraphProof (EQUIVALENT transformation)

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

(92) TRUE