(STARTTERM
    CONSTRUCTOR-BASED)
(STRATEGY
    INNERMOST)

(VAR
    @l @l1 @l2 @x @x1 @x2 @xs @xs' @y @ys)
(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))
(COMMENT
    This TRS was automatically generated from the resource aware ML program 'mergesort.raml', c.f. http://raml.tcs.ifi.lmu.de/)