add concluding blog post for my fsf internship :-)
[~bandali/bndl.org] / static / se212-h02q04d-soln.grg
CommitLineData
ff620ce6
AB
1#u abandali
2#a h02
3
4#q q04d
5
6p <=> q, p & q <=> (p | q)
7
8#check TP
9
10p <=> 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
2110) (!p | p) & (!q | p) & (!p | q) & (!q | q) by distr * 2
2211) true & (!q | p) & (!p | q) & true by lem * 2
2312) (!q | p) & (!p | q) by simp1 * 2
2413) (q => p) & (p => q) by impl * 2
2514) p <=> q by equiv