(VAR @l @ls @pivot @rs @x @xs @y @ys @z @zs )
(STRATEGY INNERMOST)
(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)
)