(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/)