(VAR n m l b r x ys xs)
(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)
)
(COMMENT
transforms a tree into a list
)