(STARTTERM CONSTRUCTOR-BASED) (STRATEGY INNERMOST) (VAR @l @ls @pivot @rs @x @xs @y @ys @z @zs) (RULES #abs(#0()) -> #0() #abs(#neg(@x)) -> #pos(@x) #abs(#pos(@x)) -> #pos(@x) #abs(#s(@x)) -> #pos(#s(@x)) #greater(@x,@y) -> #ckgt(#compare(@x,@y)) append(@l,@ys) -> append#1(@l,@ys) append#1(::(@x,@xs),@ys) -> ::(@x,append(@xs,@ys)) append#1(nil(),@ys) -> @ys appendD(@l,@ys) -> appendD#1(@l,@ys) appendD#1(::(@x,@xs),@ys) -> ::(@x,appendD(@xs,@ys)) appendD#1(nil(),@ys) -> @ys quicksort(@l) -> quicksort#1(@l) quicksort#1(::(@z,@zs)) -> quicksort#2(split(@z,@zs),@z) quicksort#1(nil()) -> nil() quicksort#2(tuple#2(@xs,@ys),@z) -> append(quicksort(@xs),::(@z,quicksort(@ys))) quicksortD(@l) -> quicksortD#1(@l) quicksortD#1(::(@z,@zs)) -> quicksortD#2(splitD(@z,@zs),@z) quicksortD#1(nil()) -> nil() quicksortD#2(tuple#2(@xs,@ys),@z) -> appendD(quicksortD(@xs),::(@z,quicksortD(@ys))) split(@pivot,@l) -> split#1(@l,@pivot) split#1(::(@x,@xs),@pivot) -> split#2(split(@pivot,@xs),@pivot,@x) split#1(nil(),@pivot) -> tuple#2(nil(),nil()) split#2(tuple#2(@ls,@rs),@pivot,@x) -> split#3(#greater(@x,@pivot),@ls,@rs,@x) split#3(#false(),@ls,@rs,@x) -> tuple#2(::(@x,@ls),@rs) split#3(#true(),@ls,@rs,@x) -> tuple#2(@ls,::(@x,@rs)) splitD(@pivot,@l) -> splitD#1(@l,@pivot) splitD#1(::(@x,@xs),@pivot) -> splitD#2(splitD(@pivot,@xs),@pivot,@x) splitD#1(nil(),@pivot) -> tuple#2(nil(),nil()) splitD#2(tuple#2(@ls,@rs),@pivot,@x) -> splitD#3(#greater(@x,@pivot),@ls,@rs,@x) splitD#3(#false(),@ls,@rs,@x) -> tuple#2(::(@x,@ls),@rs) splitD#3(#true(),@ls,@rs,@x) -> tuple#2(@ls,::(@x,@rs)) #ckgt(#EQ()) ->= #false() #ckgt(#GT()) ->= #true() #ckgt(#LT()) ->= #false() #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 'quicksort.raml', c.f. http://raml.tcs.ifi.lmu.de/)