[~bandali/bndl.org] / se212-f19 / se212-h02q04d-soln.grg

#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
Commit	Line	Data
ff620ce6 AB	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