YES
0 QTRS
↳1 Overlay + Local Confluence (⇔, 0 ms)
↳2 QTRS
↳3 DependencyPairsProof (⇔, 0 ms)
↳4 QDP
↳5 DependencyGraphProof (⇔, 0 ms)
↳6 AND
↳7 QDP
↳8 UsableRulesProof (⇔, 0 ms)
↳9 QDP
↳10 QReductionProof (⇔, 0 ms)
↳11 QDP
↳12 QDPSizeChangeProof (⇔, 0 ms)
↳13 YES
↳14 QDP
↳15 UsableRulesProof (⇔, 0 ms)
↳16 QDP
↳17 QReductionProof (⇔, 0 ms)
↳18 QDP
↳19 TransformationProof (⇔, 0 ms)
↳20 QDP
↳21 DependencyGraphProof (⇔, 0 ms)
↳22 QDP
↳23 TransformationProof (⇔, 0 ms)
↳24 QDP
↳25 TransformationProof (⇔, 0 ms)
↳26 QDP
↳27 TransformationProof (⇔, 0 ms)
↳28 QDP
↳29 TransformationProof (⇔, 0 ms)
↳30 QDP
↳31 TransformationProof (⇔, 0 ms)
↳32 QDP
↳33 TransformationProof (⇔, 0 ms)
↳34 QDP
↳35 TransformationProof (⇔, 0 ms)
↳36 QDP
↳37 TransformationProof (⇔, 0 ms)
↳38 QDP
↳39 UsableRulesProof (⇔, 0 ms)
↳40 QDP
↳41 QReductionProof (⇔, 0 ms)
↳42 QDP
↳43 TransformationProof (⇔, 0 ms)
↳44 QDP
↳45 UsableRulesProof (⇔, 0 ms)
↳46 QDP
↳47 TransformationProof (⇔, 1 ms)
↳48 QDP
↳49 UsableRulesProof (⇔, 0 ms)
↳50 QDP
↳51 QReductionProof (⇔, 0 ms)
↳52 QDP
↳53 TransformationProof (⇔, 0 ms)
↳54 QDP
↳55 UsableRulesProof (⇔, 0 ms)
↳56 QDP
↳57 TransformationProof (⇔, 0 ms)
↳58 QDP
↳59 UsableRulesProof (⇔, 0 ms)
↳60 QDP
↳61 TransformationProof (⇔, 0 ms)
↳62 QDP
↳63 UsableRulesProof (⇔, 0 ms)
↳64 QDP
↳65 QReductionProof (⇔, 0 ms)
↳66 QDP
↳67 TransformationProof (⇔, 0 ms)
↳68 QDP
↳69 TransformationProof (⇔, 0 ms)
↳70 QDP
↳71 TransformationProof (⇔, 0 ms)
↳72 QDP
↳73 TransformationProof (⇔, 0 ms)
↳74 QDP
↳75 TransformationProof (⇔, 0 ms)
↳76 QDP
↳77 TransformationProof (⇔, 0 ms)
↳78 QDP
↳79 QDPQMonotonicMRRProof (⇔, 90 ms)
↳80 QDP
↳81 DependencyGraphProof (⇔, 0 ms)
↳82 TRUE
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)
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)
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)
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)
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)
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)
APPEND(cons(y, ys), x) → APPEND(ys, x)
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)
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)
APPEND(cons(y, ys), x) → APPEND(ys, x)
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)
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)
APPEND(cons(y, ys), x) → APPEND(ys, x)
From the DPs we obtained the following set of size-change graphs:
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)
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)
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)
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)
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))
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)
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)
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)
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))
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(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(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))) → 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)
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)))
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))
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(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)
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))
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(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))) → 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)))
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)))
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))
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(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))) → 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)))
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)))
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))
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(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))) → 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)))
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)))
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))
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(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))) → 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)))
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)))
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))
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(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))) → 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)))
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)))
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))
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(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))) → 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)))
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)))
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))
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(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))) → 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)))
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)))
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))
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(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(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))) → 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)))
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)))
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))
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)
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)))
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
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)
isEmpty(empty)
isEmpty(node(x0, x1, x2))
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)))
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
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(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(empty, y1, y2), y3) → IF(false, true, y2, node(empty, elem(empty), node(right(empty), y1, y2)), y3, append(y3, node(empty, y1, y2)))
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)))
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
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)
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)))
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
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(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(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)))
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)))
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
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)
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)))
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
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)
left(empty)
left(node(x0, x1, x2))
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)))
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
right(empty)
right(node(x0, x1, x2))
elem(node(x0, x1, x2))
append(nil, x0)
append(cons(y, x0), x1)
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(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, 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)))
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
right(empty)
right(node(x0, x1, x2))
elem(node(x0, x1, x2))
append(nil, x0)
append(cons(y, x0), x1)
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)))
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
right(empty)
right(node(x0, x1, x2))
elem(node(x0, x1, x2))
append(nil, x0)
append(cons(y, x0), x1)
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))) → 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)))
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)))
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
right(empty)
right(node(x0, x1, x2))
elem(node(x0, x1, x2))
append(nil, x0)
append(cons(y, x0), x1)
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)))
right(node(l, x, r)) → r
append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))
right(empty)
right(node(x0, x1, x2))
elem(node(x0, x1, x2))
append(nil, x0)
append(cons(y, x0), x1)
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))) → 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, 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)))
right(node(l, x, r)) → r
append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))
right(empty)
right(node(x0, x1, x2))
elem(node(x0, x1, x2))
append(nil, x0)
append(cons(y, x0), x1)
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)))
append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))
right(empty)
right(node(x0, x1, x2))
elem(node(x0, x1, x2))
append(nil, x0)
append(cons(y, x0), x1)
right(empty)
right(node(x0, x1, x2))
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)))
append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))
elem(node(x0, x1, x2))
append(nil, x0)
append(cons(y, x0), x1)
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, false, z4, node(z0, z1, node(z2, z3, z4)), z5, y_0) → LISTIFY(node(z0, z1, node(z2, z3, z4)), z5)
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)
append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))
elem(node(x0, x1, x2))
append(nil, x0)
append(cons(y, x0), x1)
IF(false, true, z1, node(empty, elem(empty), node(empty, z0, z1)), z2, y_0) → LISTIFY(z1, y_0) → IF(false, true, z1, node(empty, elem(empty), node(empty, z0, z1)), z2, y_0) → LISTIFY(z1, y_0)
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)
append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))
elem(node(x0, x1, x2))
append(nil, x0)
append(cons(y, x0), x1)
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(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) → 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(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)
append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))
elem(node(x0, x1, x2))
append(nil, x0)
append(cons(y, x0), x1)
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(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(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, 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)))
append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))
elem(node(x0, x1, x2))
append(nil, x0)
append(cons(y, x0), x1)
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(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(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) → 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, 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)
append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))
elem(node(x0, x1, x2))
append(nil, x0)
append(cons(y, x0), x1)
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(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(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)))) → 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))))
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))))
append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))
elem(node(x0, x1, x2))
append(nil, x0)
append(cons(y, x0), x1)
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)
POL(IF(x1, x2, x3, x4, x5, x6)) = 2·x2 + 2·x4 + x6
POL(LISTIFY(x1, x2)) = 2 + 2·x1
POL(append(x1, x2)) = 0
POL(cons(x1, x2)) = 0
POL(elem(x1)) = 1 + x1
POL(empty) = 0
POL(false) = 1
POL(nil) = 0
POL(node(x1, x2, x3)) = 1 + 2·x1 + x3
POL(true) = 0
POL(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(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))))
append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))
elem(node(x0, x1, x2))
append(nil, x0)
append(cons(y, x0), x1)