(STARTTERM CONSTRUCTOR-BASED) (STRATEGY INNERMOST) (VAR @l @l1 @l2 @x @x_1 @x_2 @xs @y @y_1 @y_2 @ys) (RULES #equal(@x,@y) -> #eq(@x,@y) #less(@x,@y) -> #cklt(#compare(@x,@y)) and(@x,@y) -> #and(@x,@y) insert(@x,@l) -> insert#1(@l,@x) insert#1(::(@y,@ys),@x) -> insert#2(leq(@x,@y),@x,@y,@ys) insert#1(nil(),@x) -> ::(@x,nil()) insert#2(#false(),@x,@y,@ys) -> ::(@y,insert(@x,@ys)) insert#2(#true(),@x,@y,@ys) -> ::(@x,::(@y,@ys)) isortlist(@l) -> isortlist#1(@l) isortlist#1(::(@x,@xs)) -> insert(@x,isortlist(@xs)) isortlist#1(nil()) -> nil() leq(@l1,@l2) -> leq#1(@l1,@l2) leq#1(::(@x,@xs),@l2) -> leq#2(@l2,@x,@xs) leq#1(nil(),@l2) -> #true() leq#2(::(@y,@ys),@x,@xs) -> or(#less(@x,@y),and(#equal(@x,@y),leq(@xs,@ys))) leq#2(nil(),@x,@xs) -> #false() or(@x,@y) -> #or(@x,@y) #and(#false(),#false()) ->= #false() #and(#false(),#true()) ->= #false() #and(#true(),#false()) ->= #false() #and(#true(),#true()) ->= #true() #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) #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(nil(),::(@y_1,@y_2)) ->= #false() #eq(nil(),nil()) ->= #true() #or(#false(),#false()) ->= #false() #or(#false(),#true()) ->= #true() #or(#true(),#false()) ->= #true() #or(#true(),#true()) ->= #true()) (COMMENT This TRS was automatically generated from the resource aware ML program 'listsort.raml', c.f. http://raml.tcs.ifi.lmu.de/)