---

Step * 1 2 of Lemma weak-Markov-principle2


1. a : ℕ*
2. ∀c:ℕ*. ((¬¬(∃n:ℕ. (¬((a n) = (c n) ∈ ℤ)))) ∨ (¬¬(∃n:ℕ. (¬(0 = (c n) ∈ ℤ)))))
3. c : ℕ ⟶ ℕ
4. ¬¬(∃n:ℕ. (¬(0 = (nat-star-retract(c) n) ∈ ℤ)))
⊢ ∃i:ℕ
   (((i = 0 ∈ ℤ) ⇒ (¬¬(∃n:ℕ. (¬((a n) = (nat-star-retract(c) n) ∈ ℤ)))))
   ∧ ((¬(i = 0 ∈ ℤ)) ⇒ (¬¬(∃n:ℕ. (¬(0 = (nat-star-retract(c) n) ∈ ℤ))))))
BY
{ (D 0 With ⌜1⌝  THEN Auto) }

---

Latex:

---

Latex:

1.  a  :  \mBbbN{}*
2.  \mforall{}c:\mBbbN{}*.  ((\mneg{}\mneg{}(\mexists{}n:\mBbbN{}.  (\mneg{}((a  n)  =  (c  n)))))  \mvee{}  (\mneg{}\mneg{}(\mexists{}n:\mBbbN{}.  (\mneg{}(0  =  (c  n))))))
3.  c  :  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}
4.  \mneg{}\mneg{}(\mexists{}n:\mBbbN{}.  (\mneg{}(0  =  (nat-star-retract(c)  n))))
\mvdash{}  \mexists{}i:\mBbbN{}
      (((i  =  0)  {}\mRightarrow{}  (\mneg{}\mneg{}(\mexists{}n:\mBbbN{}.  (\mneg{}((a  n)  =  (nat-star-retract(c)  n))))))
      \mwedge{}  ((\mneg{}(i  =  0))  {}\mRightarrow{}  (\mneg{}\mneg{}(\mexists{}n:\mBbbN{}.  (\mneg{}(0  =  (nat-star-retract(c)  n)))))))


By

---

Latex:
(D  0  With  \mkleeneopen{}1\mkleeneclose{}    THEN  Auto)

---

Home Index