(VAR @_ @l @x @xs @y @ys )
(STRATEGY INNERMOST)
(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
        testInsertionsort(@x) -> insertionsort(testList(#unit))
        testInsertionsortD(@x) -> insertionsortD(testList(#unit))
        testList(@_) -> ::(#abs(#0),::(#abs(#pos(#s(#s(#s(#s(#0)))))),::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))),::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#s(#0))))))))))),::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#0))))))))),::(#abs(#pos(#s(#0))),::(#abs(#pos(#s(#s(#0)))),::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#0)))))))))),::(#abs(#pos(#s(#s(#s(#s(#s(#s(#0)))))))),::(#abs(#pos(#s(#s(#s(#0))))),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)
)