---

Step * 1 of Lemma weak-Markov-principle2

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

1
1. a : ℕ*
2. ∀c:ℕ*. ((¬¬(∃n:ℕ. (¬((a n) = (c n) ∈ ℤ)))) ∨ (¬¬(∃n:ℕ. (¬(0 = (c n) ∈ ℤ)))))
3. c : ℕ ⟶ ℕ
4. ¬¬(∃n:ℕ. (¬((a n) = (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) ∈ ℤ))))))

2
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) ∈ ℤ))))))

---

Latex:

---

Latex:
.....assertion..... 
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))))))
\mvdash{}  \mforall{}c:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}
        \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  THENA  Auto)  THEN  (InstHyp  [\mkleeneopen{}nat-star-retract(c)\mkleeneclose{}]  2\mcdot{}  THENA  Auto)  THEN  D  -1)

---

Home Index