---

Step * 1 of Lemma nat-inf-limit


1. p : ℕ∞ ⟶ 𝔹
2. ∀n:ℕ. p n∞ = ff
3. ↑(p ∞)
⊢ ∀f:ℕ ⟶ 𝔹. Dec(∀n:ℕ. f n = ff)
BY
{ (Intro
   THEN (Assert λn.(¬b(∃i<n + 1.f i)_b) ∈ ℕ∞ BY
               (MemTypeCD
                THEN Reduce 0
                THEN Auto
                THEN (RW assert_pushdownC (-1) THENA Auto)
                THEN RWO "assert-b-exists" (-1)
                THEN Auto
                THEN RWO "assert-b-exists" 0
                THEN Auto
                THEN RepeatFor 2 (ParallelLast)))
   ) }

1
1. p : ℕ∞ ⟶ 𝔹
2. ∀n:ℕ. p n∞ = ff
3. ↑(p ∞)
4. f : ℕ ⟶ 𝔹
5. λn.(¬b(∃i<n + 1.f i)_b) ∈ ℕ∞
⊢ Dec(∀n:ℕ. f n = ff)

---

Latex:

---

Latex:

1.  p  :  \mBbbN{}\minfty{}  {}\mrightarrow{}  \mBbbB{}
2.  \mforall{}n:\mBbbN{}.  p  n\minfty{}  =  ff
3.  \muparrow{}(p  \minfty{})
\mvdash{}  \mforall{}f:\mBbbN{}  {}\mrightarrow{}  \mBbbB{}.  Dec(\mforall{}n:\mBbbN{}.  f  n  =  ff)


By

---

Latex:
(Intro
  THEN  (Assert  \mlambda{}n.(\mneg{}\msubb{}(\mexists{}i<n  +  1.f  i)\_b)  \mmember{}  \mBbbN{}\minfty{}  BY
                          (MemTypeCD
                            THEN  Reduce  0
                            THEN  Auto
                            THEN  (RW  assert\_pushdownC  (-1)  THENA  Auto)
                            THEN  RWO  "assert-b-exists"  (-1)
                            THEN  Auto
                            THEN  RWO  "assert-b-exists"  0
                            THEN  Auto
                            THEN  RepeatFor  2  (ParallelLast)))
  )

---

Home Index