---

Step * of Lemma weak-Markov-principle

∀a,b:ℕ ⟶ ℕ.
  ((∀c:ℕ ⟶ ℕ. ((¬¬(∃n:ℕ. (¬((a n) = (c n) ∈ ℤ)))) ∨ (¬¬(∃n:ℕ. (¬((b n) = (c n) ∈ ℤ))))))
  ⇒ (∃n:ℕ. (¬((a n) = (b n) ∈ ℤ))))
BY
{ (InstLemma `weak-Markov-principle-alt` []
   THEN RepeatFor 6 ((ParallelLast' THENW Auto))
   THEN (RWO "-1" 0 THEN Auto)
   THEN (D 0 THENA Auto)
   THEN ExRepD
   THEN D -1
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}a,b:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.
    ((\mforall{}c:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.  ((\mneg{}\mneg{}(\mexists{}n:\mBbbN{}.  (\mneg{}((a  n)  =  (c  n)))))  \mvee{}  (\mneg{}\mneg{}(\mexists{}n:\mBbbN{}.  (\mneg{}((b  n)  =  (c  n)))))))
    {}\mRightarrow{}  (\mexists{}n:\mBbbN{}.  (\mneg{}((a  n)  =  (b  n)))))


By

---

Latex:
(InstLemma  `weak-Markov-principle-alt`  []
  THEN  RepeatFor  6  ((ParallelLast'  THENW  Auto))
  THEN  (RWO  "-1"  0  THEN  Auto)
  THEN  (D  0  THENA  Auto)
  THEN  ExRepD
  THEN  D  -1
  THEN  Auto)

---

Home Index