(STARTTERM
    CONSTRUCTOR-BASED)
(STRATEGY
    INNERMOST)

(VAR
    @_ @l @x @xs @y @ys)
(RULES
    #abs(#0()) -> #0()
    #abs(#neg(@x)) -> #pos(@x)
    #abs(#pos(@x)) -> #pos(@x)
    #abs(#s(@x)) -> #pos(#s(@x))
    #less(@x,@y) -> #cklt(#compare(@x,@y))
    insert(@x,@l) -> insert#1(@l,@x)
    insert#1(::(@y,@ys),@x) -> insert#2(#less(@y,@x),@x,@y,@ys)
    insert#1(nil(),@x) -> ::(@x,nil())
    insert#2(#false(),@x,@y,@ys) -> ::(@x,::(@y,@ys))
    insert#2(#true(),@x,@y,@ys) -> ::(@y,insert(@x,@ys))
    insertD(@x,@l) -> insertD#1(@l,@x)
    insertD#1(::(@y,@ys),@x) -> insertD#2(#less(@y,@x),@x,@y,@ys)
    insertD#1(nil(),@x) -> ::(@x,nil())
    insertD#2(#false(),@x,@y,@ys) -> ::(@x,::(@y,@ys))
    insertD#2(#true(),@x,@y,@ys) -> ::(@y,insertD(@x,@ys))
    insertionsort(@l) -> insertionsort#1(@l)
    insertionsort#1(::(@x,@xs)) -> insert(@x,insertionsort(@xs))
    insertionsort#1(nil()) -> nil()
    insertionsortD(@l) -> insertionsortD#1(@l)
    insertionsortD#1(::(@x,@xs)) -> insertD(@x,insertionsortD(@xs))
    insertionsortD#1(nil()) -> nil()
    #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 'insertionsort.raml', c.f. http://raml.tcs.ifi.lmu.de/)