tauts.out

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

_ :: Bool
_ :: Name
_ :: Prop
False :: Bool
True :: Bool
(==) :: Prop -> Prop -> Bool
eval :: Prop -> Prop
varOf :: Prop -> Name
subst :: Name -> Bool -> Prop -> Prop
taut :: Prop -> Bool
(==) :: Bool -> Bool -> Bool
(==) :: Name -> Name -> Bool

     (p == p) == True
     (p == p) == True
  (p == True) == p
     (n == n) == True
taut (eval p) == taut p
     (p == q) == (q == p)
eval (eval p) == eval p

              p ==> True
          False ==> p
    p == eval q ==> p == eval p
    subst n p q <=  q
    subst n p q <=  subst n True q
subst n False p <=  subst n q p

taut q ==> subst n (taut q) p == subst n True p