(STRATEGY
    INNERMOST)

(VAR
    k m n x)
(DATATYPES
    A = µX.< 0, true, s(X), false, cons(X, X), nil >)
(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
    sort :: [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(0(),nil())) -> 0()
    min(cons(s(n),nil())) -> s(n)
    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))
    sort(nil()) -> nil()
    sort(cons(n,x)) ->
      cons(min(cons(n,x))
          ,sort(replace(min(cons(n,x))
                       ,n
                       ,x))))