Step
*
of Lemma
or-to-and-by-cases
∀[X:ℙ]. (Dec(X)
⇒ (∀[P,Q:ℙ]. ((P
⇒ X)
⇒ (Q
⇒ (¬X))
⇒ {P ∨ Q
⇐⇒ (X
⇒ P) ∧ ((¬X)
⇒ Q)})))
BY
{ (Unfolds ``decidable guard`` 0 THEN Auto THEN SplitOrHyps THEN Auto) }
Latex:
Latex:
\mforall{}[X:\mBbbP{}]. (Dec(X) {}\mRightarrow{} (\mforall{}[P,Q:\mBbbP{}]. ((P {}\mRightarrow{} X) {}\mRightarrow{} (Q {}\mRightarrow{} (\mneg{}X)) {}\mRightarrow{} \{P \mvee{} Q \mLeftarrow{}{}\mRightarrow{} (X {}\mRightarrow{} P) \mwedge{} ((\mneg{}X) {}\mRightarrow{} Q)\})))
By
Latex:
(Unfolds ``decidable guard`` 0 THEN Auto THEN SplitOrHyps THEN Auto)
Home
Index