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