Commit ff58eb53c8794a2af004284aecd5291f61af9950 - Eqthy

fix incorrect theorem Proloy Mishra 1 year, 9 months ago

1 changed file(s) with 11 addition(s) and 9 deletion(s). Raw diff Collapse all Expand all

+11

-9

eg/boolean-algebra.eqthy.md less more

170	170	theorem
171	171	not(not(A)) = A
172	172	proof
173		1 = 1
174		1 = or(A, not(A))
175		1 = or(not(A), A)
176		or(not(not(A)), 1) = or(not(not(A)), or(not(A), A)) [by congruence of X and or(not(not(A)), X)]
177		not(not(A)) = or(not(not(A)), or(not(A), A))
178		not(not(A)) = or(or(not(not(A)), not(A)), A)
179		not(not(A)) = or(or(not(A), not(not(A))), A)
180		not(not(A)) = or(1, A)
181		not(not(A)) = or(A, 1)
	173	and(or(not(not(A)), A), 1) = and(or(not(not(A)), A), 1)
	174	and(or(not(not(A)), A), 1) = and(or(A, not(not(A))), 1)
	175	and(or(not(not(A)), A), 1) = and(or(A, not(not(A))), or(A, not(A)))
	176	and(or(not(not(A)), A), 1) = or(A, and(not(not(A)), not(A)))
	177	and(or(not(not(A)), A), 1) = or(A, and(not(A), not(not(A))))
	178	and(or(not(not(A)), A), 1) = or(A, 0)
	179	and(or(not(not(A)), A), 1) = A
	180	and(or(not(not(A)), A), or(not(A), not(not(A)))) = A [by #or-comp with A=not(A)]
	181	and(or(not(not(A)), A), or(not(not(A)), not(A))) = A
	182	or(not(not(A)), and(A, not(A))) = A
	183	or(not(not(A)), 0) = A
182	184	not(not(A)) = A
183	185	qed