(VAR @key @key1 @keyX @l @l1 @ls @pivot @rs @valX @vals @vals1 @x @x_1 @x_2 @xs @y @y_1 @y_2 @ys @z @zs )
(STRATEGY INNERMOST)
(RULES 
        #equal(@x,@y) -> #eq(@x,@y)
        #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
        insert(@x,@l) -> insert#1(@x,@l,@x)
        insert#1(tuple#2(@valX,@keyX),@l,@x) -> insert#2(@l,@keyX,@valX,@x)
        insert#2(::(@l1,@ls),@keyX,@valX,@x) -> insert#3(@l1,@keyX,@ls,@valX,@x)
        insert#2(nil,@keyX,@valX,@x) -> ::(tuple#2(::(@valX,nil),@keyX),nil)
        insert#3(tuple#2(@vals1,@key1),@keyX,@ls,@valX,@x) -> insert#4(#equal(@key1,@keyX),@key1,@ls,@valX,@vals1,@x)
        insert#4(#false,@key1,@ls,@valX,@vals1,@x) -> ::(tuple#2(@vals1,@key1),insert(@x,@ls))
        insert#4(#true,@key1,@ls,@valX,@vals1,@x) -> ::(tuple#2(::(@valX,@vals1),@key1),@ls)
        quicksort(@l) -> quicksort#1(@l)
        quicksort#1(::(@z,@zs)) -> quicksort#2(splitqs(@z,@zs),@z)
        quicksort#1(nil) -> nil
        quicksort#2(tuple#2(@xs,@ys),@z) -> append(quicksort(@xs),::(@z,quicksort(@ys)))
        sortAll(@l) -> sortAll#1(@l)
        sortAll#1(::(@x,@xs)) -> sortAll#2(@x,@xs)
        sortAll#1(nil) -> nil
        sortAll#2(tuple#2(@vals,@key),@xs) -> ::(tuple#2(quicksort(@vals),@key),sortAll(@xs))
        split(@l) -> split#1(@l)
        split#1(::(@x,@xs)) -> insert(@x,split(@xs))
        split#1(nil) -> nil
        splitAndSort(@l) -> sortAll(split(@l))
        splitqs(@pivot,@l) -> splitqs#1(@l,@pivot)
        splitqs#1(::(@x,@xs),@pivot) -> splitqs#2(splitqs(@pivot,@xs),@pivot,@x)
        splitqs#1(nil,@pivot) -> tuple#2(nil,nil)
        splitqs#2(tuple#2(@ls,@rs),@pivot,@x) -> splitqs#3(#greater(@x,@pivot),@ls,@rs,@x)
        splitqs#3(#false,@ls,@rs,@x) -> tuple#2(::(@x,@ls),@rs)
        splitqs#3(#true,@ls,@rs,@x) -> tuple#2(@ls,::(@x,@rs))
        #and(#false,#false) ->= #false
        #and(#false,#true) ->= #false
        #and(#true,#false) ->= #false
        #and(#true,#true) ->= #true
        #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)
        #eq(#0,#0) ->= #true
        #eq(#0,#neg(@y)) ->= #false
        #eq(#0,#pos(@y)) ->= #false
        #eq(#0,#s(@y)) ->= #false
        #eq(#neg(@x),#0) ->= #false
        #eq(#neg(@x),#neg(@y)) ->= #eq(@x,@y)
        #eq(#neg(@x),#pos(@y)) ->= #false
        #eq(#pos(@x),#0) ->= #false
        #eq(#pos(@x),#neg(@y)) ->= #false
        #eq(#pos(@x),#pos(@y)) ->= #eq(@x,@y)
        #eq(#s(@x),#0) ->= #false
        #eq(#s(@x),#s(@y)) ->= #eq(@x,@y)
        #eq(::(@x_1,@x_2),::(@y_1,@y_2)) ->= #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2))
        #eq(::(@x_1,@x_2),nil) ->= #false
        #eq(::(@x_1,@x_2),tuple#2(@y_1,@y_2)) ->= #false
        #eq(nil,::(@y_1,@y_2)) ->= #false
        #eq(nil,nil) ->= #true
        #eq(nil,tuple#2(@y_1,@y_2)) ->= #false
        #eq(tuple#2(@x_1,@x_2),::(@y_1,@y_2)) ->= #false
        #eq(tuple#2(@x_1,@x_2),nil) ->= #false
        #eq(tuple#2(@x_1,@x_2),tuple#2(@y_1,@y_2)) ->= #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2))
)