(STRATEGY
    INNERMOST)

(VAR
    @l @l1 @l2 @x @x1 @x2 @xs @xs'
    @y @ys)
(DATATYPES
    A = µX.< ::(X, X), nil, #false, #true, tuple#2(X, X), #EQ, #GT, #LT, #0, #neg(X), #pos(X), #s(X) >)
(SIGNATURES
    #less :: [A x A] -> A
    merge :: [A x A] -> A
    merge#1 :: [A x A] -> A
    merge#2 :: [A x A x A] -> A
    merge#3 :: [A x A x A x A x A] -> A
    mergesort :: [A] -> A
    mergesort#1 :: [A] -> A
    mergesort#2 :: [A x A] -> A
    mergesort#3 :: [A] -> A
    msplit :: [A] -> A
    msplit#1 :: [A] -> A
    msplit#2 :: [A x A] -> A
    msplit#3 :: [A x A x A] -> A
    #cklt :: [A] -> A
    #compare :: [A x A] -> A)
(RULES
    #less(@x,@y) ->
      #cklt(#compare(@x,@y))
    merge(@l1,@l2) -> merge#1(@l1
                             ,@l2)
    merge#1(::(@x,@xs),@l2) ->
      merge#2(@l2,@x,@xs)
    merge#1(nil(),@l2) -> @l2
    merge#2(::(@y,@ys),@x,@xs) ->
      merge#3(#less(@x,@y)
             ,@x
             ,@xs
             ,@y
             ,@ys)
    merge#2(nil(),@x,@xs) -> ::(@x
                               ,@xs)
    merge#3(#false()
           ,@x
           ,@xs
           ,@y
           ,@ys) -> ::(@y
                      ,merge(::(@x,@xs),@ys))
    merge#3(#true()
           ,@x
           ,@xs
           ,@y
           ,@ys) -> ::(@x
                      ,merge(@xs,::(@y,@ys)))
    mergesort(@l) -> mergesort#1(@l)
    mergesort#1(::(@x1,@xs)) ->
      mergesort#2(@xs,@x1)
    mergesort#1(nil()) -> nil()
    mergesort#2(::(@x2,@xs'),@x1) ->
      mergesort#3(msplit(::(@x1
                           ,::(@x2,@xs'))))
    mergesort#2(nil(),@x1) -> ::(@x1
                                ,nil())
    mergesort#3(tuple#2(@l1,@l2)) ->
      merge(mergesort(@l1)
           ,mergesort(@l2))
    msplit(@l) -> msplit#1(@l)
    msplit#1(::(@x1,@xs)) ->
      msplit#2(@xs,@x1)
    msplit#1(nil()) -> tuple#2(nil()
                              ,nil())
    msplit#2(::(@x2,@xs'),@x1) ->
      msplit#3(msplit(@xs'),@x1,@x2)
    msplit#2(nil(),@x1) ->
      tuple#2(::(@x1,nil()),nil())
    msplit#3(tuple#2(@l1,@l2)
            ,@x1
            ,@x2) -> tuple#2(::(@x1,@l1)
                            ,::(@x2,@l2))
    #cklt(#EQ()) ->= #false()
    #cklt(#GT()) ->= #false()
    #cklt(#LT()) ->= #true()
    #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))