(VAR l l1 l2 ls x xs)

(DATATYPES

   a = µX. < cons(X,X), nil >
)

(SIGNATURES
   append       :: a x a -> a
   append#1     :: a x a -> a
   appendAll    :: a     -> a
   appendAll#1  :: a     -> a
   appendAll2   :: a     -> a
   appendAll2#1 :: a     -> a
   appendAll3   :: a     -> a
   appendAll3#1 :: a     -> a
 )


(RULES
    append(l1,l2) -> append#1(l1,l2)
    append#1(nil,l2) -> l2
    append#1(cons(x,xs),l2) -> cons(x,append(xs,l2))

    appendAll(l) -> appendAll#1(l)
    appendAll#1(nil) -> nil
    appendAll#1(cons(l1,ls)) -> append(l1,appendAll(ls))

    appendAll2(l) -> appendAll2#1(l)
    appendAll2#1(nil) -> nil
    appendAll2#1(cons(l1,ls)) -> append(appendAll(l1),appendAll2(ls))

    appendAll3(l) -> appendAll3#1(l)
    appendAll3#1(nil) -> nil
    appendAll3#1(cons(l1,ls)) -> append(appendAll2(l1),appendAll3(ls))
    )


(COMMENT


)