(STRATEGY
    INNERMOST)

(VAR
    @l @l1 @l2 @ls @x @xs)
(DATATYPES
    A = µX.< ::(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(::(@x,@xs),@l2) ->
      ::(@x,append(@xs,@l2))
    append#1(nil(),@l2) -> @l2
    appendAll(@l) -> appendAll#1(@l)
    appendAll#1(::(@l1,@ls)) ->
      append(@l1,appendAll(@ls))
    appendAll#1(nil()) -> nil()
    appendAll2(@l) ->
      appendAll2#1(@l)
    appendAll2#1(::(@l1,@ls)) ->
      append(appendAll(@l1)
            ,appendAll2(@ls))
    appendAll2#1(nil()) -> nil()
    appendAll3(@l) ->
      appendAll3#1(@l)
    appendAll3#1(::(@l1,@ls)) ->
      append(appendAll2(@l1)
            ,appendAll3(@ls))
    appendAll3#1(nil()) -> nil())