Step
*
1
2
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. ([] = filter(P;if 0 <z m then [u / firstn(m - 1;v)] else [] fi ) ∈ (T List))
BY
{ ((With ⌜0⌝ (D 0)⋅ THENA Auto) THEN Reduce 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.  \mneg{}0  <  n
\mvdash{}  \mexists{}m:\mBbbN{}(||v||  +  1)  +  1.  ([]  =  filter(P;if  0  <z  m  then  [u  /  firstn(m  -  1;v)]  else  []  fi  ))
By
Latex:
((With  \mkleeneopen{}0\mkleeneclose{}  (D  0)\mcdot{}  THENA  Auto)  THEN  Reduce  0  THEN  Auto)
Home
Index