Step
*
1
of Lemma
un-half-squash-test
1. [P] : ℙ
2. [Q] : ℙ
3. [R] : ℙ
4. (P ∧ R)
⇒ Q
5. R
6. half-squash-stable(Q)
7. P
8. True
⊢ {Q ∧ ⇃(P) ∧ (∀n:ℕ. Q)}
BY
{ (D 0 THEN EAuto 1) }
Latex:
Latex:
1. [P] : \mBbbP{}
2. [Q] : \mBbbP{}
3. [R] : \mBbbP{}
4. (P \mwedge{} R) {}\mRightarrow{} Q
5. R
6. half-squash-stable(Q)
7. P
8. True
\mvdash{} \{Q \mwedge{} \00D9(P) \mwedge{} (\mforall{}n:\mBbbN{}. Q)\}
By
Latex:
(D 0 THEN EAuto 1)
Home
Index