X-Git-Url: https://git.shemshak.org/~bandali/bndl.org/blobdiff_plain/505a94190f4aba9404b7c9d95444bfa0a14925ec..a9bc018ee07125709a2814a194a7bfb3433907fe:/static/se212-h02q04d-soln.grg

diff --git a/static/se212-h02q04d-soln.grg b/static/se212-h02q04d-soln.grg
new file mode 100644
index 0000000..e395717
--- /dev/null
+++ b/static/se212-h02q04d-soln.grg
@@ -0,0 +1,25 @@
+#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