(STRATEGY
    INNERMOST)

(VAR
    c l x y ys zs)
(DATATYPES
    A = µX.< 0, s(X), nil, cons(X, X), true, false >)
(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
    greater :: [A x A] -> A
    smaller :: [A x A] -> A
    helpc :: [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
                                  ,greater(ys,zs)
                                  ,smaller(ys,zs))
    greater(ys,zs) ->
      helpc(ge(length(ys),length(zs))
           ,ys
           ,zs)
    smaller(ys,zs) ->
      helpc(ge(length(ys),length(zs))
           ,zs
           ,ys)
    helpc(true(),ys,zs) -> ys
    helpc(false(),ys,zs) -> zs
    helpb(c,l,cons(y,ys),zs) ->
      cons(y,helpa(s(c),l,ys,zs)))