(STRATEGY
    INNERMOST)

(VAR
    min x x' xs xs' y)
(DATATYPES
    A = µX.< Cons(X, X), Nil, True, False, S(X), 0 >)
(SIGNATURES
    remove :: [A x A] -> A
    minsort :: [A] -> A
    appmin :: [A x A x A] -> A
    notEmpty :: [A] -> A
    goal :: [A] -> A
    !EQ :: [A x A] -> A
    < :: [A x A] -> A
    remove[Ite][True][Ite] :: [A x A x A] -> A
    appmin[Ite][True][Ite] :: [A x A x A x A] -> A)
(RULES
    remove(x',Cons(x,xs)) ->
      remove[Ite][True][Ite](!EQ(x',x)
                            ,x'
                            ,Cons(x,xs))
    remove(x,Nil()) -> Nil()
    minsort(Cons(x,xs)) -> appmin(x
                                 ,xs
                                 ,Cons(x,xs))
    minsort(Nil()) -> Nil()
    appmin(min,Cons(x,xs),xs') ->
      appmin[Ite][True][Ite](<(x,min)
                            ,min
                            ,Cons(x,xs)
                            ,xs')
    appmin(min,Nil(),xs) -> Cons(min
                                ,minsort(remove(min,xs)))
    notEmpty(Cons(x,xs)) -> True()
    notEmpty(Nil()) -> False()
    goal(xs) -> minsort(xs)
    !EQ(S(x),S(y)) ->= !EQ(x,y)
    !EQ(0(),S(y)) ->= False()
    !EQ(S(x),0()) ->= False()
    !EQ(0(),0()) ->= True()
    <(S(x),S(y)) ->= <(x,y)
    <(0(),S(y)) ->= True()
    <(x,0()) ->= False()
    remove[Ite][True][Ite](False()
                          ,x'
                          ,Cons(x,xs)) ->= Cons(x
                                               ,remove(x',xs))
    appmin[Ite][True][Ite](True()
                          ,min
                          ,Cons(x,xs)
                          ,xs') ->= appmin(x,xs,xs')
    remove[Ite][True][Ite](True()
                          ,x'
                          ,Cons(x,xs)) ->= xs
    appmin[Ite][True][Ite](False()
                          ,min
                          ,Cons(x,xs)
                          ,xs') ->= appmin(min,xs,xs'))