binarytree.out

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

_ :: Bool  (holes: Bool)
_ :: Word2  (holes: Word2)
_ :: BT Word2  (holes: BT Word2)
_ :: [Word2]  (holes: [Word2])
Null :: BT Word2
insert :: Word2 -> BT Word2 -> BT Word2
delete :: Word2 -> BT Word2 -> BT Word2
isIn :: Word2 -> BT Word2 -> Bool
(<=) :: Word2 -> Word2 -> Bool
(/=) :: Word2 -> Word2 -> Bool
ordered :: [Word2] -> Bool
strictlyOrdered :: [Word2] -> Bool
toList :: BT Word2 -> [Word2]
fromList :: [Word2] -> BT Word2
isSearch :: BT Word2 -> Bool
[] :: [Word2]
True :: Bool
False :: Bool
(==) :: Bool -> Bool -> Bool
(==) :: Word2 -> Word2 -> Bool
(==) :: BT Word2 -> BT Word2 -> Bool
(==) :: [Word2] -> [Word2] -> Bool

           isIn x Null == False
   isIn x (insert x t) == True
   isIn x (delete x t) == False
  (Null == insert x t) == False
            (xs == []) == (Null == fromList xs)
     (t == insert x t) == isIn x t
              (x == y) == isIn x (insert y Null)
     (t == delete x t) == (False == isIn x t)
isIn x (insert y Null) == isIn y (insert x Null)
   (False == (x /= y)) == isIn x (insert y Null)
         delete x Null == Null
 insert x (insert x t) == insert x t
 delete x (delete x t) == delete x t
 insert x (delete x t) == insert x t
 delete x (insert x t) == delete x t
 insert x (insert y t) == insert y (insert x t)
 delete x (delete y t) == delete y (delete x t)

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

x /= y ==> delete y (insert x t) == insert x (delete y t)