(STRATEGY
    INNERMOST)

(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)
(DATATYPES
    A = µX.< ::(X, X), nil, tuple#2(X, X), #false, #true, #EQ, #GT, #LT, #0, #neg(X), #pos(X), #s(X) >)
(SIGNATURES
    #equal :: [A x A] -> A
    #greater :: [A x A] -> A
    append :: [A x A] -> A
    append#1 :: [A x A] -> A
    insert :: [A x A] -> A
    insert#1 :: [A x A x A] -> A
    insert#2 :: [A x A x A x A] -> A
    insert#3 :: [A x A x A x A x A] -> A
    insert#4 :: [A x A x A x A x A x A] -> A
    quicksort :: [A] -> A
    quicksort#1 :: [A] -> A
    quicksort#2 :: [A x A] -> A
    sortAll :: [A] -> A
    sortAll#1 :: [A] -> A
    sortAll#2 :: [A x A] -> A
    split :: [A] -> A
    split#1 :: [A] -> A
    splitAndSort :: [A] -> A
    splitqs :: [A x A] -> A
    splitqs#1 :: [A x A] -> A
    splitqs#2 :: [A x A x A] -> A
    splitqs#3 :: [A x A x A x A] -> A
    #and :: [A x A] -> A
    #ckgt :: [A] -> A
    #compare :: [A x A] -> A
    #eq :: [A x A] -> A)
(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)))