consensus Show Code edit
## Consensus Theorem
##
# This theorem and its dual (with {{{\/}}} and {{{/\}}}
# interchanged) are commonly used in computer logic design to eliminate
# redundant terms from Boolean expressions. Specifically, we prove that the
# term #(/\ ps ch)# on the left-hand side is redundant.
##
thm (consensus () () (<-> (\/ (\/ (/\ ph ps) (/\ (-. ph) ch)) (/\ ps ch)) (\/ (/\ ph ps) (/\ (-. ph) ch))) (\/ (/\ ph ps) (/\ (-. ph) ch)) id ph ps ch dedlema biimpd ch adantrd ph ch ps dedlemb biimpd ps adantld pm2.61i ps ph ancom ch (-. ph) ancom orbi12i sylib jaoi (\/ (/\ ph ps) (/\ (-. ph) ch)) (/\ ps ch) orc impbii)
(<-> (\/ (\/ (/\ ph ps) (/\ (-. ph) ch)) (/\ ps ch)) (\/ (/\ ph ps) (/\ (-. ph) ch)))
edit