(STRATEGY
    INNERMOST)

(VAR
    K L M N X Y)
(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
    ifmin :: [A x A] -> A
    replace :: [A x A x A] -> A
    ifrepl :: [A x A x A x A] -> A
    selsort :: [A] -> A
    ifselsort :: [A x A] -> A)
(RULES
    eq(0(),0()) -> true()
    eq(0(),s(Y)) -> false()
    eq(s(X),0()) -> false()
    eq(s(X),s(Y)) -> eq(X,Y)
    le(0(),Y) -> true()
    le(s(X),0()) -> false()
    le(s(X),s(Y)) -> le(X,Y)
    min(cons(0(),nil())) -> 0()
    min(cons(s(N),nil())) -> s(N)
    min(cons(N,cons(M,L))) ->
      ifmin(le(N,M),cons(N,cons(M,L)))
    ifmin(true()
         ,cons(N,cons(M,L))) ->
      min(cons(N,L))
    ifmin(false()
         ,cons(N,cons(M,L))) ->
      min(cons(M,L))
    replace(N,M,nil()) -> nil()
    replace(N,M,cons(K,L)) ->
      ifrepl(eq(N,K),N,M,cons(K,L))
    ifrepl(true(),N,M,cons(K,L)) ->
      cons(M,L)
    ifrepl(false(),N,M,cons(K,L)) ->
      cons(K,replace(N,M,L))
    selsort(nil()) -> nil()
    selsort(cons(N,L)) ->
      ifselsort(eq(N,min(cons(N,L)))
               ,cons(N,L))
    ifselsort(true(),cons(N,L)) ->
      cons(N,selsort(L))
    ifselsort(false(),cons(N,L)) ->
      cons(min(cons(N,L))
          ,selsort(replace(min(cons(N,L))
                          ,N
                          ,L))))