git.shemshak.org - ~bandali/bndl.org/blob - static/se212-h02q04d-soln.grg

   1 #u abandali
   2 #a h02
   3
   4 #q q04d
   5
   6 p <=> q, p & q <=> (p | q)
   7
   8 #check TP
   9
  10 p <=> q  <->  p & q <=> (p | q)
  11
  12  1) p & q             <=> (p | q)
  13  2) (p & q   => p | q) &  (p | q => p & q)                by equiv
  14  3) (!(p & q) | p | q) & (!(p | q) | p & q)               by impl * 2
  15  4) (!p | !q  | p | q) & (!(p | q) | p & q)               by dm
  16  5) (true | !q | q)    & (!(p | q) | p & q)               by lem
  17  6) true               & (!(p | q) | p & q)               by simp1
  18  7)                       !(p | q) | p & q                by simp1
  19  8)                       !p & !q  | p & q                by dm
  20  9)                  (!p & !q | p) & (!p & !q | q)        by distr
  21 10)            (!p | p) & (!q | p) & (!p | q) & (!q | q)  by distr * 2
  22 11)                true & (!q | p) & (!p | q) & true      by lem * 2
  23 12)                       (!q | p) & (!p | q)             by simp1 * 2
  24 13)                       (q => p) & (p => q)             by impl * 2
  25 14)                       p <=> q                         by equiv