binarytree0-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
_ :: Word2
_ :: BT Word2
Null :: BT Word2
insert :: Word2 -> BT Word2 -> BT Word2
delete :: Word2 -> BT Word2 -> BT Word2
isIn :: Word2 -> BT Word2 -> Bool
(/=) :: Word2 -> Word2 -> Bool
True :: Bool
False :: Bool
(==) :: Bool -> Bool -> Bool
(==) :: Word2 -> Word2 -> Bool
(==) :: BT Word2 -> BT Word2 -> Bool

  isIn x Null == False
delete x Null == Null

         Null <= t
            t <= insert x t
   delete x t <= t
insert x Null <= insert x t

isIn x t ==> insert x t == t