(STRATEGY
    INNERMOST)

(VAR
    x x' xs y ys)
(DATATYPES
    A = µX.< Cons(X, X), Nil, True, False, S(X), 0 >)
(SIGNATURES
    quicksort :: [A] -> A
    partLt :: [A x A] -> A
    partGt :: [A x A] -> A
    app :: [A x A] -> A
    notEmpty :: [A] -> A
    part :: [A x A] -> A
    goal :: [A] -> A
    < :: [A x A] -> A
    > :: [A x A] -> A
    partLt[Ite][True][Ite] :: [A x A x A] -> A
    partGt[Ite][True][Ite] :: [A x A x A] -> A)
(RULES
    quicksort(Cons(x
                  ,Cons(x',xs))) -> part(x
                                        ,Cons(x',xs))
    quicksort(Cons(x,Nil())) ->
      Cons(x,Nil())
    quicksort(Nil()) -> Nil()
    partLt(x',Cons(x,xs)) ->
      partLt[Ite][True][Ite](<(x,x')
                            ,x'
                            ,Cons(x,xs))
    partLt(x,Nil()) -> Nil()
    partGt(x',Cons(x,xs)) ->
      partGt[Ite][True][Ite](>(x,x')
                            ,x'
                            ,Cons(x,xs))
    partGt(x,Nil()) -> Nil()
    app(Cons(x,xs),ys) -> Cons(x
                              ,app(xs,ys))
    app(Nil(),ys) -> ys
    notEmpty(Cons(x,xs)) -> True()
    notEmpty(Nil()) -> False()
    part(x,xs) ->
      app(quicksort(partLt(x,xs))
         ,Cons(x
              ,quicksort(partGt(x,xs))))
    goal(xs) -> quicksort(xs)
    <(S(x),S(y)) ->= <(x,y)
    <(0(),S(y)) ->= True()
    <(x,0()) ->= False()
    >(S(x),S(y)) ->= >(x,y)
    >(0(),y) ->= False()
    >(S(x),0()) ->= True()
    partLt[Ite][True][Ite](True()
                          ,x'
                          ,Cons(x,xs)) ->= Cons(x
                                               ,partLt(x',xs))
    partGt[Ite][True][Ite](True()
                          ,x'
                          ,Cons(x,xs)) ->= Cons(x
                                               ,partGt(x',xs))
    partLt[Ite][True][Ite](False()
                          ,x'
                          ,Cons(x,xs)) ->= partLt(x',xs)
    partGt[Ite][True][Ite](False()
                          ,x'
                          ,Cons(x,xs)) ->= partGt(x',xs))