---

Step * 1 2 1 1 1 of Lemma unbounded-decidable-nset-infinite


1. d : ℕ ⟶ 𝔹
2. n : ℕ
3. ∀j:ℕ. (-1 < j ⇒ (↑(d j)) ⇒ (n ≤ j))
4. ∀m:ℕ. (¬(m ∈ filter(d;upto(n))))
⊢ ||filter(d;upto(n))|| = 0 ∈ ℕ
BY
{ ((MoveToConcl (-1) THEN (GenConcl ⌜filter(d;upto(n)) = L ∈ (ℕ List)⌝⋅ THENA Auto))
   THEN All Thin
   THEN DVar `L'
   THEN Reduce 0
   THEN Auto
   THEN (D -1 With ⌜u⌝  THENA Auto)
   THEN D -1
   THEN Auto) }

---

Latex:

---

Latex:

1.  d  :  \mBbbN{}  {}\mrightarrow{}  \mBbbB{}
2.  n  :  \mBbbN{}
3.  \mforall{}j:\mBbbN{}.  (-1  <  j  {}\mRightarrow{}  (\muparrow{}(d  j))  {}\mRightarrow{}  (n  \mleq{}  j))
4.  \mforall{}m:\mBbbN{}.  (\mneg{}(m  \mmember{}  filter(d;upto(n))))
\mvdash{}  ||filter(d;upto(n))||  =  0


By

---

Latex:
((MoveToConcl  (-1)  THEN  (GenConcl  \mkleeneopen{}filter(d;upto(n))  =  L\mkleeneclose{}\mcdot{}  THENA  Auto))
  THEN  All  Thin
  THEN  DVar  `L'
  THEN  Reduce  0
  THEN  Auto
  THEN  (D  -1  With  \mkleeneopen{}u\mkleeneclose{}    THENA  Auto)
  THEN  D  -1
  THEN  Auto)

---

Home Index