Step
*
of Lemma
vr_test_55
(∀p:ℙ. ((¬¬p)
⇒ p))
⇒ (∀p:ℙ. (p ∨ (¬p)))
BY
{ ((D 0 THENA Auto)
THEN (D 0 THENA (Thin 1 THEN Auto))
THEN (BHyp (-2) THENA (Thin 1 THEN Auto))
THEN (D 0 THENA (Thin 1 THEN Auto))
THEN RWO "not_over_or" (-1)
THEN Thin 1
THEN Auto) }
Latex:
(\mforall{}p:\mBbbP{}. ((\mneg{}\mneg{}p) {}\mRightarrow{} p)) {}\mRightarrow{} (\mforall{}p:\mBbbP{}. (p \mvee{} (\mneg{}p)))
By
((D 0 THENA Auto)
THEN (D 0 THENA (Thin 1 THEN Auto))
THEN (BHyp (-2) THENA (Thin 1 THEN Auto))
THEN (D 0 THENA (Thin 1 THEN Auto))
THEN RWO "not\_over\_or" (-1)
THEN Thin 1
THEN Auto)
Home
Index