binarytree.out2

== Signature ==
  Null :: BT Int
insert :: Int -> BT Int -> BT Int
delete :: Int -> BT Int -> BT Int
  isIn :: Int -> BT Int -> Bool
 (==>) :: Bool -> Bool -> Bool
  True :: Bool
 False :: Bool

== Laws ==
  1. x ==> x = True
  2. x ==> True = True
  3. False ==> x = True
  4. True ==> x = x
  5. delete x Null = Null
  6. isIn x Null = False
  7. x ==> (x ==> y) = x ==> y
  8. x ==> (y ==> x) = True
  9. (x ==> y) ==> x = x
 10. delete x (delete x t1) = delete x t1
 11. delete x (insert x t1) = delete x (delete x t1)
 12. insert x (delete x t1) = insert x t1
 13. isIn x (delete x t1) = False
 14. isIn x (insert x t1) = True
 15. (x ==> False) ==> False = x
 16. x ==> (y ==> z) = y ==> (x ==> z)
 17. (x ==> y) ==> y = (y ==> x) ==> x
 18. delete y (delete x t1) = delete x (delete y t1)
 19. insert y (insert x t1) = insert x (insert y t1)
 20. isIn x (insert y Null) = isIn y (insert x Null)
 21. isIn x (insert y (delete x t1)) = isIn x (insert y Null)
 22. isIn x (insert y Null) ==> False =
       isIn x (delete y (insert x t1))
 23. isIn x (delete y (insert z Null)) =
       isIn z (delete y (insert x Null))
 24. (((x ==> y) ==> z) ==> y) ==> x2 =
       (x ==> y) ==> ((z ==> y) ==> x2)
 25. isIn x t1 ==> isIn x (insert y t1) = True
 26. isIn x t1 ==> isIn y (insert x t1) = isIn x t1 ==> isIn y t1
 27. isIn x (delete y t1) ==> isIn x t2 =
       isIn x t1 ==> isIn x (insert y t2)
 28. isIn x (delete y t1) ==> isIn y t1 = isIn x t1 ==> isIn y t1
 29. isIn x (delete y (insert z (delete x t1))) =
       isIn x (delete y (insert z Null))
 30. isIn x (insert y (insert z (delete x t1))) =
       isIn x (insert y (insert z Null))
 31. isIn x (delete y (insert z Null)) ==> False =
       isIn x (insert y (delete z (insert x t1)))
 32. isIn x (insert y (insert z Null)) ==> False =
       isIn x (delete y (delete z (insert x t1)))
 33. (((x ==> x2) ==> z) ==> y) ==> x2 =
       (x ==> y) ==> ((z ==> y) ==> x2)
 34. isIn x t1 ==> isIn y (delete z t2) =
       isIn x t1 ==> isIn y (delete x t2)