(STRATEGY
    INNERMOST)

(VAR
    b u v y)
(DATATYPES
    A = µX.< leaf, true, cons(X, X), false >)
(SIGNATURES
    isLeaf :: [A] -> A
    left :: [A] -> A
    right :: [A] -> A
    concat :: [A x A] -> A
    less_leaves :: [A x A] -> A
    if1 :: [A x A x A x A] -> A
    if2 :: [A x A x A] -> A)
(RULES
    isLeaf(leaf()) -> true()
    isLeaf(cons(u,v)) -> false()
    left(cons(u,v)) -> u
    right(cons(u,v)) -> v
    concat(leaf(),y) -> y
    concat(cons(u,v),y) -> cons(u
                               ,concat(v,y))
    less_leaves(u,v) ->
      if1(isLeaf(u),isLeaf(v),u,v)
    if1(b,true(),u,v) -> false()
    if1(b,false(),u,v) -> if2(b,u,v)
    if2(true(),u,v) -> true()
    if2(false(),u,v) ->
      less_leaves(concat(left(u)
                        ,right(u))
                 ,concat(left(v),right(v))))