---

Step * 2 of Lemma firstn-filter


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

---

Latex:

---

Latex:

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


By

---

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

---

Home Index