(STRATEGY
    INNERMOST)

(VAR
    l m n u v x y)
(DATATYPES
    A = µX.< 0, true, cons(X, X), s(X), false, nil >)
(SIGNATURES
    sort :: [A] -> A
    st :: [A x A] -> A
    cond1 :: [A x A x A] -> A
    cond2 :: [A x A x A] -> A
    member :: [A x A] -> A
    or :: [A x A] -> A
    equal :: [A x A] -> A
    gt :: [A x A] -> A
    max :: [A] -> A
    if :: [A x A x A] -> A)
(RULES
    sort(l) -> st(0(),l)
    st(n,l) -> cond1(member(n,l)
                    ,n
                    ,l)
    cond1(true(),n,l) -> cons(n
                             ,st(s(n),l))
    cond1(false(),n,l) -> cond2(gt(n
                                  ,max(l))
                               ,n
                               ,l)
    cond2(true(),n,l) -> nil()
    cond2(false(),n,l) -> st(s(n),l)
    member(n,nil()) -> false()
    member(n,cons(m,l)) ->
      or(equal(n,m),member(n,l))
    or(x,true()) -> true()
    or(x,false()) -> x
    equal(0(),0()) -> true()
    equal(s(x),0()) -> false()
    equal(0(),s(y)) -> false()
    equal(s(x),s(y)) -> equal(x,y)
    gt(0(),v) -> false()
    gt(s(u),0()) -> true()
    gt(s(u),s(v)) -> gt(u,v)
    max(nil()) -> 0()
    max(cons(u,l)) -> if(gt(u
                           ,max(l))
                        ,u
                        ,max(l))
    if(true(),u,v) -> u
    if(false(),u,v) -> v)