---

Step * of Lemma baire-diff-from-diff

∀a:ℕ ⟶ ℕ. ∀n:ℕ.  (¬((a n) = (baire-diff-from(a;n) n) ∈ ℕ))
BY
{ (RepeatFor 2 ((D 0 THENA Auto))
   THEN RepUR ``baire-diff-from`` 0
   THEN AutoSplit
   THEN RepUR ``nat-pred`` 0
   THEN RepeatFor 2 (AutoSplit)) }

---

Latex:

---

Latex:
\mforall{}a:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.  \mforall{}n:\mBbbN{}.    (\mneg{}((a  n)  =  (baire-diff-from(a;n)  n)))


By

---

Latex:
(RepeatFor  2  ((D  0  THENA  Auto))
  THEN  RepUR  ``baire-diff-from``  0
  THEN  AutoSplit
  THEN  RepUR  ``nat-pred``  0
  THEN  RepeatFor  2  (AutoSplit))

---

Home Index