---

Step * 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 : ℕ
⊢ ∃m:ℕ(||v|| + 1) + 1
   (if 0 <z n then [u / firstn(n - 1;filter(P;v))] else [] fi 
   = filter(P;if 0 <z m then [u / firstn(m - 1;v)] else [] fi )
   ∈ (T List))
BY
{ AutoSplit }

1
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))

2
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. ([] = filter(P;if 0 <z m then [u / firstn(m - 1;v)] else [] fi ) ∈ (T List))

---

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{}
\mvdash{}  \mexists{}m:\mBbbN{}(||v||  +  1)  +  1
      (if  0  <z  n  then  [u  /  firstn(n  -  1;filter(P;v))]  else  []  fi 
      =  filter(P;if  0  <z  m  then  [u  /  firstn(m  -  1;v)]  else  []  fi  ))


By

---

Latex:
AutoSplit

---

Home Index