(VAR b l m n r x xs ys )
(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)
        
)