(VAR b l l1 l2 m n t t1 t2 )
(RULES 
        lessElements(l, t) -> lessE(l, t, 0)
        lessE(l, t, n) -> if(le(length(l), n), le(length(toList(t)), n), l, t, n)
        if(true, b, l, t, n) -> l
        if(false, true, l, t, n) -> t
        if(false, false, l, t, n) -> lessE(l, t, s(n))
        length(nil) -> 0
        length(cons(n, l)) -> s(length(l))
        toList(leaf) -> nil
        toList(node(t1, n, t2)) -> append(toList(t1), cons(n, toList(t2)))
        append(nil, l2) -> l2
        append(cons(n, l1), l2) -> cons(n, append(l1, l2))
        le(s(n), 0) -> false
        le(0, m) -> true
        le(s(n), s(m)) -> le(n, m)
        a -> c
        a -> d
        
)