(STARTTERM CONSTRUCTOR-BASED) (STRATEGY INNERMOST) (VAR @key @key1 @keyX @l @l1 @ls @pivot @rs @valX @vals @vals1 @x @x_1 @x_2 @xs @y @y_1 @y_2 @ys @z @zs) (RULES #equal(@x,@y) -> #eq(@x,@y) #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 insert(@x,@l) -> insert#1(@x,@l,@x) insert#1(tuple#2(@valX,@keyX),@l,@x) -> insert#2(@l,@keyX,@valX,@x) insert#2(::(@l1,@ls),@keyX,@valX,@x) -> insert#3(@l1,@keyX,@ls,@valX,@x) insert#2(nil(),@keyX,@valX,@x) -> ::(tuple#2(::(@valX,nil()),@keyX),nil()) insert#3(tuple#2(@vals1,@key1),@keyX,@ls,@valX,@x) -> insert#4(#equal(@key1,@keyX),@key1,@ls,@valX,@vals1,@x) insert#4(#false(),@key1,@ls,@valX,@vals1,@x) -> ::(tuple#2(@vals1,@key1),insert(@x,@ls)) insert#4(#true(),@key1,@ls,@valX,@vals1,@x) -> ::(tuple#2(::(@valX,@vals1),@key1),@ls) quicksort(@l) -> quicksort#1(@l) quicksort#1(::(@z,@zs)) -> quicksort#2(splitqs(@z,@zs),@z) quicksort#1(nil()) -> nil() quicksort#2(tuple#2(@xs,@ys),@z) -> append(quicksort(@xs),::(@z,quicksort(@ys))) sortAll(@l) -> sortAll#1(@l) sortAll#1(::(@x,@xs)) -> sortAll#2(@x,@xs) sortAll#1(nil()) -> nil() sortAll#2(tuple#2(@vals,@key),@xs) -> ::(tuple#2(quicksort(@vals),@key),sortAll(@xs)) split(@l) -> split#1(@l) split#1(::(@x,@xs)) -> insert(@x,split(@xs)) split#1(nil()) -> nil() splitAndSort(@l) -> sortAll(split(@l)) splitqs(@pivot,@l) -> splitqs#1(@l,@pivot) splitqs#1(::(@x,@xs),@pivot) -> splitqs#2(splitqs(@pivot,@xs),@pivot,@x) splitqs#1(nil(),@pivot) -> tuple#2(nil(),nil()) splitqs#2(tuple#2(@ls,@rs),@pivot,@x) -> splitqs#3(#greater(@x,@pivot),@ls,@rs,@x) splitqs#3(#false(),@ls,@rs,@x) -> tuple#2(::(@x,@ls),@rs) splitqs#3(#true(),@ls,@rs,@x) -> tuple#2(@ls,::(@x,@rs)) #and(#false(),#false()) ->= #false() #and(#false(),#true()) ->= #false() #and(#true(),#false()) ->= #false() #and(#true(),#true()) ->= #true() #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) #eq(#0(),#0()) ->= #true() #eq(#0(),#neg(@y)) ->= #false() #eq(#0(),#pos(@y)) ->= #false() #eq(#0(),#s(@y)) ->= #false() #eq(#neg(@x),#0()) ->= #false() #eq(#neg(@x),#neg(@y)) ->= #eq(@x,@y) #eq(#neg(@x),#pos(@y)) ->= #false() #eq(#pos(@x),#0()) ->= #false() #eq(#pos(@x),#neg(@y)) ->= #false() #eq(#pos(@x),#pos(@y)) ->= #eq(@x,@y) #eq(#s(@x),#0()) ->= #false() #eq(#s(@x),#s(@y)) ->= #eq(@x,@y) #eq(::(@x_1,@x_2),::(@y_1,@y_2)) ->= #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) #eq(::(@x_1,@x_2),nil()) ->= #false() #eq(::(@x_1,@x_2),tuple#2(@y_1,@y_2)) ->= #false() #eq(nil(),::(@y_1,@y_2)) ->= #false() #eq(nil(),nil()) ->= #true() #eq(nil(),tuple#2(@y_1,@y_2)) ->= #false() #eq(tuple#2(@x_1,@x_2),::(@y_1,@y_2)) ->= #false() #eq(tuple#2(@x_1,@x_2),nil()) ->= #false() #eq(tuple#2(@x_1,@x_2),tuple#2(@y_1,@y_2)) ->= #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2))) (COMMENT This TRS was automatically generated from the resource aware ML program 'splitandsort.raml', c.f. http://raml.tcs.ifi.lmu.de/)