(VAR
    l l1 l2 x x'1 x'2 xs y y'1 y'2 ys)

(DATATYPES
   a = µX. < dd(X,X), nil, #0, #neg(X), #pos(X), #s(X) >
   b = < #false, #true >
   c = < #EQ, #GT, #LT >
 )

(SIGNATURES
   #equal :: a x a -> b
   #eq :: a x a -> b
   #less :: a x a -> b
   #compare :: a x a -> c
   #cklt :: c -> b
   and :: b x b -> b
   #and :: b x b -> b
   insert :: a x a -> a
   insert#1 :: a x a -> a
   leq :: a x a -> b
   insert#2 :: b x a x a x a -> a
   isortlist :: a -> a
   isortlist#1 :: a -> a
   leq#1 :: a x a -> b
   leq#2 :: a x a x a -> b
   or :: b x b -> b
   #or :: b x b -> b
 )

(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(dd(y,ys),x) -> insert#2(leq(x,y),x,y,ys)
    insert#1(nil,x) -> dd(x,nil)
    insert#2(#false,x,y,ys) -> dd(y,insert(x,ys))
    insert#2(#true,x,y,ys) -> dd(x,dd(y,ys))
    isortlist(l) -> isortlist#1(l)
    isortlist#1(dd(x,xs)) -> insert(x,isortlist(xs))
    isortlist#1(nil) -> nil
    leq(l1,l2) -> leq#1(l1,l2)
    leq#1(dd(x,xs),l2) -> leq#2(l2,x,xs)
    leq#1(nil,l2) -> #true
    leq#2(dd(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(dd(x'1,x'2),dd(y'1,y'2)) -> #and(#eq(x'1,y'1),#eq(x'2,y'2))
    #eq(dd(x'1,x'2),nil) -> #false
    #eq(nil,dd(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)