---

Step * 1 1 of Lemma firstn-filter


1. [T] : Type
2. P : T ⟶ 𝔹
3. u : T
4. v : T List
5. ∀n:ℕ. ∃m:ℕ||v|| + 1. (firstn(n;filter(P;v)) = filter(P;firstn(m;v)) ∈ (T List))
6. ↑(P u)
7. n : ℕ
8. 0 < n
⊢ ∃m:ℕ(||v|| + 1) + 1
   ([u / firstn(n - 1;filter(P;v))] = filter(P;if 0 <z m then [u / firstn(m - 1;v)] else [] fi ) ∈ (T List))
BY
{ ((With ⌜n - 1⌝ (D (-4))⋅ THENA Auto) THEN ExRepD THEN With ⌜m + 1⌝ (D 0)⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  P  :  T  {}\mrightarrow{}  \mBbbB{}
3.  u  :  T
4.  v  :  T  List
5.  \mforall{}n:\mBbbN{}.  \mexists{}m:\mBbbN{}||v||  +  1.  (firstn(n;filter(P;v))  =  filter(P;firstn(m;v)))
6.  \muparrow{}(P  u)
7.  n  :  \mBbbN{}
8.  0  <  n
\mvdash{}  \mexists{}m:\mBbbN{}(||v||  +  1)  +  1
      ([u  /  firstn(n  -  1;filter(P;v))]  =  filter(P;if  0  <z  m  then  [u  /  firstn(m  -  1;v)]  else  []  fi  ))


By

---

Latex:
((With  \mkleeneopen{}n  -  1\mkleeneclose{}  (D  (-4))\mcdot{}  THENA  Auto)  THEN  ExRepD  THEN  With  \mkleeneopen{}m  +  1\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto)

---

Home Index