X-Git-Url: https://git.shemshak.org/~bandali/bndl.org/blobdiff_plain/ff620ce6ac85cf10600b3da9a640f6ebc3568444..56af22d033482f66966fb7b8edc2bb18f2fec477:/se212-f19/se212-h02q04d-soln.grg?ds=sidebyside;pf=~bandali diff --git a/se212-f19/se212-h02q04d-soln.grg b/se212-f19/se212-h02q04d-soln.grg deleted file mode 100644 index e395717..0000000 --- a/se212-f19/se212-h02q04d-soln.grg +++ /dev/null @@ -1,25 +0,0 @@ -#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