-#u abandali
-#a h02
-
-#q q04d
-
-p <=> q, p & q <=> (p | q)
-
-#check TP
-
-p <=> q <-> p & q <=> (p | q)
-
- 1) p & q <=> (p | q)
- 2) (p & q => p | q) & (p | q => p & q) by equiv
- 3) (!(p & q) | p | q) & (!(p | q) | p & q) by impl * 2
- 4) (!p | !q | p | q) & (!(p | q) | p & q) by dm
- 5) (true | !q | q) & (!(p | q) | p & q) by lem
- 6) true & (!(p | q) | p & q) by simp1
- 7) !(p | q) | p & q by simp1
- 8) !p & !q | p & q by dm
- 9) (!p & !q | p) & (!p & !q | q) by distr
-10) (!p | p) & (!q | p) & (!p | q) & (!q | q) by distr * 2
-11) true & (!q | p) & (!p | q) & true by lem * 2
-12) (!q | p) & (!p | q) by simp1 * 2
-13) (q => p) & (p => q) by impl * 2
-14) p <=> q by equiv