(STRATEGY
    INNERMOST)

(VAR
    @l @ls @pivot @rs @x @xs @y @ys
    @z @zs)
(DATATYPES
    A = µX.< #0, #neg(X), #pos(X), #s(X), ::(X, X), nil, tuple#2(X, X), #false, #true, #unit, #EQ, #GT, #LT >)
(SIGNATURES
    #abs :: [A] -> A
    #greater :: [A x A] -> A
    append :: [A x A] -> A
    append#1 :: [A x A] -> A
    appendD :: [A x A] -> A
    appendD#1 :: [A x A] -> A
    quicksort :: [A] -> A
    quicksort#1 :: [A] -> A
    quicksort#2 :: [A x A] -> A
    quicksortD :: [A] -> A
    quicksortD#1 :: [A] -> A
    quicksortD#2 :: [A x A] -> A
    split :: [A x A] -> A
    split#1 :: [A x A] -> A
    split#2 :: [A x A x A] -> A
    split#3 :: [A x A x A x A] -> A
    splitD :: [A x A] -> A
    splitD#1 :: [A x A] -> A
    splitD#2 :: [A x A x A] -> A
    splitD#3 :: [A x A x A x A] -> A
    testList :: [A] -> A
    testQuicksort :: [A] -> A
    testQuicksort2 :: [A] -> A
    #ckgt :: [A] -> A
    #compare :: [A x A] -> A)
(RULES
    #abs(#0()) -> #0()
    #abs(#neg(@x)) -> #pos(@x)
    #abs(#pos(@x)) -> #pos(@x)
    #abs(#s(@x)) -> #pos(#s(@x))
    #greater(@x,@y) ->
      #ckgt(#compare(@x,@y))
    append(@l,@ys) -> append#1(@l
                              ,@ys)
    append#1(::(@x,@xs),@ys) ->
      ::(@x,append(@xs,@ys))
    append#1(nil(),@ys) -> @ys
    appendD(@l,@ys) -> appendD#1(@l
                                ,@ys)
    appendD#1(::(@x,@xs),@ys) ->
      ::(@x,appendD(@xs,@ys))
    appendD#1(nil(),@ys) -> @ys
    quicksort(@l) -> quicksort#1(@l)
    quicksort#1(::(@z,@zs)) ->
      quicksort#2(split(@z,@zs),@z)
    quicksort#1(nil()) -> nil()
    quicksort#2(tuple#2(@xs,@ys)
               ,@z) -> append(quicksort(@xs)
                             ,::(@z,quicksort(@ys)))
    quicksortD(@l) ->
      quicksortD#1(@l)
    quicksortD#1(::(@z,@zs)) ->
      quicksortD#2(splitD(@z,@zs),@z)
    quicksortD#1(nil()) -> nil()
    quicksortD#2(tuple#2(@xs,@ys)
                ,@z) -> appendD(quicksortD(@xs)
                               ,::(@z,quicksortD(@ys)))
    split(@pivot,@l) -> split#1(@l
                               ,@pivot)
    split#1(::(@x,@xs),@pivot) ->
      split#2(split(@pivot,@xs)
             ,@pivot
             ,@x)
    split#1(nil(),@pivot) ->
      tuple#2(nil(),nil())
    split#2(tuple#2(@ls,@rs)
           ,@pivot
           ,@x) -> split#3(#greater(@x
                                   ,@pivot)
                          ,@ls
                          ,@rs
                          ,@x)
    split#3(#false(),@ls,@rs,@x) ->
      tuple#2(::(@x,@ls),@rs)
    split#3(#true(),@ls,@rs,@x) ->
      tuple#2(@ls,::(@x,@rs))
    splitD(@pivot,@l) -> splitD#1(@l
                                 ,@pivot)
    splitD#1(::(@x,@xs),@pivot) ->
      splitD#2(splitD(@pivot,@xs)
              ,@pivot
              ,@x)
    splitD#1(nil(),@pivot) ->
      tuple#2(nil(),nil())
    splitD#2(tuple#2(@ls,@rs)
            ,@pivot
            ,@x) -> splitD#3(#greater(@x
                                     ,@pivot)
                            ,@ls
                            ,@rs
                            ,@x)
    splitD#3(#false(),@ls,@rs,@x) ->
      tuple#2(::(@x,@ls),@rs)
    splitD#3(#true(),@ls,@rs,@x) ->
      tuple#2(@ls,::(@x,@rs))
    testList(@x) -> ::(#abs(#0())
                      ,::(#abs(#pos(#s(#s(#s(#s(#0()))))))
                         ,::(#abs(#pos(#s(#s(#s(#s(#s(#0())))))))
                            ,::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#s(#0())))))))))))
                               ,::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#0())))))))))
                                  ,::(#abs(#pos(#s(#0())))
                                     ,::(#abs(#pos(#s(#s(#0()))))
                                        ,::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#0()))))))))))
                                           ,::(#abs(#pos(#s(#s(#s(#s(#s(#s(#0()))))))))
                                              ,::(#abs(#pos(#s(#s(#s(#0())))))
                                                 ,nil()))))))))))
    testQuicksort(@x) ->
      quicksort(testList(#unit()))
    testQuicksort2(@x) ->
      quicksort(testList(#unit()))
    #ckgt(#EQ()) ->= #false()
    #ckgt(#GT()) ->= #true()
    #ckgt(#LT()) ->= #false()
    #compare(#0(),#0()) ->= #EQ()
    #compare(#0(),#neg(@y)) ->=
      #GT()
    #compare(#0(),#pos(@y)) ->=
      #LT()
    #compare(#0(),#s(@y)) ->= #LT()
    #compare(#neg(@x),#0()) ->=
      #LT()
    #compare(#neg(@x),#neg(@y)) ->=
      #compare(@y,@x)
    #compare(#neg(@x),#pos(@y)) ->=
      #LT()
    #compare(#pos(@x),#0()) ->=
      #GT()
    #compare(#pos(@x),#neg(@y)) ->=
      #GT()
    #compare(#pos(@x),#pos(@y)) ->=
      #compare(@x,@y)
    #compare(#s(@x),#0()) ->= #GT()
    #compare(#s(@x),#s(@y)) ->=
      #compare(@x,@y))