(STRATEGY
    INNERMOST)

(VAR
    c l x y ys zs)
(DATATYPES
    A = µX.< 0, s(X), nil, cons(X, X), true, false, xs >)
(SIGNATURES
    app :: [A x A] -> A
    plus :: [A x A] -> A
    length :: [A] -> A
    helpa :: [A x A x A x A] -> A
    ge :: [A x A] -> A
    if :: [A x A x A x A x A] -> A
    take :: [A x A x A] -> A
    helpb :: [A x A x A x A] -> A)
(RULES
    app(x,y) -> helpa(0()
                     ,plus(length(x),length(y))
                     ,x
                     ,y)
    plus(x,0()) -> x
    plus(x,s(y)) -> s(plus(x,y))
    length(nil()) -> 0()
    length(cons(x,y)) ->
      s(length(y))
    helpa(c,l,ys,zs) -> if(ge(c,l)
                          ,c
                          ,l
                          ,ys
                          ,zs)
    ge(x,0()) -> true()
    ge(0(),s(x)) -> false()
    ge(s(x),s(y)) -> ge(x,y)
    if(true(),c,l,ys,zs) -> nil()
    if(false(),c,l,ys,zs) -> helpb(c
                                  ,l
                                  ,ys
                                  ,zs)
    take(0(),cons(x,xs()),ys) -> x
    take(0(),nil(),cons(y,ys)) -> y
    take(s(c),cons(x,xs()),ys) ->
      take(c,xs(),ys)
    take(s(c),nil(),cons(y,ys)) ->
      take(c,nil(),ys)
    helpb(c,l,ys,zs) -> cons(take(c
                                 ,ys
                                 ,zs)
                            ,helpa(s(c),l,ys,zs)))