Step * of Lemma assert-bnot

[p:𝔹]. ((↑¬bp)  (¬↑p))
BY
(Auto THEN BoolInd THEN All Reduce THEN Auto) }


Latex:


Latex:
\mforall{}[p:\mBbbB{}].  ((\muparrow{}\mneg{}\msubb{}p)  {}\mRightarrow{}  (\mneg{}\muparrow{}p))


By


Latex:
(Auto  THEN  BoolInd  1  THEN  All  Reduce  THEN  Auto)




Home Index