add note about my Jami talk at LibrePlanet 2021
[~bandali/bndl.org] / 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