(VAR @l @l1 @l2 @x @x_1 @x_2 @xs @y @y_1 @y_2 @ys )
(STRATEGY INNERMOST)
(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
)