---

Step * of Lemma un-half-squash-test

∀[P,Q,R:ℙ].  (((P ∧ R) ⇒ Q) ⇒ ⇃(R) ⇒ half-squash-stable(Q) ⇒ ⇃(P) ⇒ True ⇒ {Q ∧ ⇃(P) ∧ (∀n:ℕ. Q)})
BY
{ (Auto THEN UnHalfSquash THEN Auto) }

1
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)}

---

Latex:

---

Latex:
\mforall{}[P,Q,R:\mBbbP{}].
    (((P  \mwedge{}  R)  {}\mRightarrow{}  Q)  {}\mRightarrow{}  \00D9(R)  {}\mRightarrow{}  half-squash-stable(Q)  {}\mRightarrow{}  \00D9(P)  {}\mRightarrow{}  True  {}\mRightarrow{}  \{Q  \mwedge{}  \00D9(P)  \mwedge{}  (\mforall{}n:\mBbbN{}.  Q)\})


By

---

Latex:
(Auto  THEN  UnHalfSquash  THEN  Auto)

---

Home Index