---

Step * 2 of Lemma DNS-iff-not-not-GMP


1. A : ℕ ⟶ ℙ
2. ¬¬GMPi.A[i])@i
⊢ DNSi.A[i]
BY
{ (D 0 THEN Auto THEN ParallelOp 2 THEN D 0 THEN Auto THEN RepeatFor 2 ((D -1 THEN Auto))) }

---

Latex:

---

Latex:

1.  A  :  \mBbbN{}  {}\mrightarrow{}  \mBbbP{}
2.  \mneg{}\mneg{}GMPi.A[i])@i
\mvdash{}  DNSi.A[i]


By

---

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

---

Home Index