(STRATEGY
    INNERMOST)

(VAR
    b l m n r x xs ys)
(DATATYPES
    A = µX.< empty, true, node(X, X, X), false, nil, cons(X, X), y >)
(SIGNATURES
    isEmpty :: [A] -> A
    left :: [A] -> A
    right :: [A] -> A
    elem :: [A] -> A
    append :: [A x A] -> A
    listify :: [A x A] -> A
    if :: [A x A x A x A x A x A] -> A
    toList :: [A] -> A)
(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()))