---

Step * of Lemma sq_stable_and_decidable

∀[P:ℙ]. (Dec(P) ⇒ (∀[Q:⋂x:P. ℙ]. (SqStable(P) ⇒ (P ⇒ SqStable(Q)) ⇒ SqStable(P ∧ Q))))
BY
{ (RepeatFor 2 ((D 0 THENA Auto)) THEN D (-1)) }

1
1. [P] : ℙ
2. P@i
⊢ ∀[Q:⋂x:P. ℙ]. (SqStable(P) ⇒ (P ⇒ SqStable(Q)) ⇒ SqStable(P ∧ Q))

2
1. [P] : ℙ
2. ¬P@i
⊢ ∀[Q:⋂x:P. ℙ]. (SqStable(P) ⇒ (P ⇒ SqStable(Q)) ⇒ SqStable(P ∧ Q))

---

Latex:

---

Latex:
\mforall{}[P:\mBbbP{}].  (Dec(P)  {}\mRightarrow{}  (\mforall{}[Q:\mcap{}x:P.  \mBbbP{}].  (SqStable(P)  {}\mRightarrow{}  (P  {}\mRightarrow{}  SqStable(Q))  {}\mRightarrow{}  SqStable(P  \mwedge{}  Q))))


By

---

Latex:
(RepeatFor  2  ((D  0  THENA  Auto))  THEN  D  (-1))

---

Home Index