(STRATEGY
    INNERMOST)

(VAR
    k m n x y z)
(DATATYPES
    A = µX.< 0, true, s(X), false, cons(X, X), nil, append(X, X) >)
(SIGNATURES
    eq :: [A x A] -> A
    le :: [A x A] -> A
    min :: [A] -> A
    if_min :: [A x A] -> A
    replace :: [A x A x A] -> A
    if_replace :: [A x A x A x A] -> A
    empty :: [A] -> A
    head :: [A] -> A
    tail :: [A] -> A
    sort :: [A] -> A
    sortIter :: [A x A] -> A
    if :: [A x A x A x A] -> A)
(RULES
    eq(0(),0()) -> true()
    eq(0(),s(m)) -> false()
    eq(s(n),0()) -> false()
    eq(s(n),s(m)) -> eq(n,m)
    le(0(),m) -> true()
    le(s(n),0()) -> false()
    le(s(n),s(m)) -> le(n,m)
    min(cons(x,nil())) -> x
    min(cons(n,cons(m,x))) ->
      if_min(le(n,m)
            ,cons(n,cons(m,x)))
    if_min(true()
          ,cons(n,cons(m,x))) ->
      min(cons(n,x))
    if_min(false()
          ,cons(n,cons(m,x))) ->
      min(cons(m,x))
    replace(n,m,nil()) -> nil()
    replace(n,m,cons(k,x)) ->
      if_replace(eq(n,k)
                ,n
                ,m
                ,cons(k,x))
    if_replace(true()
              ,n
              ,m
              ,cons(k,x)) -> cons(m,x)
    if_replace(false()
              ,n
              ,m
              ,cons(k,x)) -> cons(k
                                 ,replace(n,m,x))
    empty(nil()) -> true()
    empty(cons(n,x)) -> false()
    head(cons(n,x)) -> n
    tail(nil()) -> nil()
    tail(cons(n,x)) -> x
    sort(x) -> sortIter(x,nil())
    sortIter(x,y) -> if(empty(x)
                       ,x
                       ,y
                       ,append(y,cons(min(x),nil())))
    if(true(),x,y,z) -> y
    if(false(),x,y,z) ->
      sortIter(replace(min(x)
                      ,head(x)
                      ,tail(x))
              ,z))