sets-s4.out

max expr size  =    4
  |- on ineqs  =    3
  |- on conds  =    3
max  #-tests   =  500
min  #-tests   =   25  (to consider p ==> q true)
max  #-vars    =    2  (for inequational and conditional laws)

_ :: Bool
_ :: Int
_ :: Set Int
emptyS :: Set Int
singleS :: Int -> Set Int
insertS :: Int -> Set Int -> Set Int
deleteS :: Int -> Set Int -> Set Int
sizeS :: Set Int -> Int
(<~) :: Int -> Set Int -> Bool
(\/) :: Set Int -> Set Int -> Set Int
(/\) :: Set Int -> Set Int -> Set Int
False :: Bool
True :: Bool
(==) :: Bool -> Bool -> Bool
(==) :: Int -> Int -> Bool
(==) :: Set Int -> Set Int -> Bool

          x <~ emptyS == False
       x <~ singleS x == True
(emptyS == singleS x) == False
             (x == y) == x <~ singleS y
       x <~ singleS y == y <~ singleS x
    sizeS (singleS x) == sizeS (singleS y)
               s \/ s == s
               s /\ s == s
          s \/ emptyS == s
     deleteS x emptyS == emptyS
          s /\ emptyS == emptyS
     insertS x emptyS == singleS x
deleteS x (singleS x) == emptyS
               s \/ t == t \/ s
               s /\ t == t /\ s
insertS x (singleS x) == singleS x
       s \/ singleS x == insertS x s
insertS x (singleS y) == insertS y (singleS x)

          sizeS emptyS <= sizeS s
                emptyS <= s
singleS (sizeS emptyS) <= singleS (sizeS s)

x <~ s ==>    insertS x s == s
x <~ s ==> s /\ singleS x == singleS x