---

Step * of Lemma firstn-filter

∀[T:Type]. ∀P:T ⟶ 𝔹. ∀L:T List. ∀n:ℕ.  ∃m:ℕ||L|| + 1. (firstn(n;filter(P;L)) = filter(P;firstn(m;L)) ∈ (T List))
BY
{ (InductionOnList
   THEN Reduce 0
   THEN Try (AutoSplit)
   THEN (RecUnfold `firstn` 0
         THEN Reduce 0
         THEN Try (RecFold `firstn` 0)
         THEN Auto
         THEN Try ((With ⌜0⌝ (D 0)⋅ THEN Complete (Auto))))) }

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 : ℕ
⊢ ∃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))

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

---

Latex:

---

Latex:
\mforall{}[T:Type]
    \mforall{}P:T  {}\mrightarrow{}  \mBbbB{}.  \mforall{}L:T  List.  \mforall{}n:\mBbbN{}.    \mexists{}m:\mBbbN{}||L||  +  1.  (firstn(n;filter(P;L))  =  filter(P;firstn(m;L)))


By

---

Latex:
(InductionOnList
  THEN  Reduce  0
  THEN  Try  (AutoSplit)
  THEN  (RecUnfold  `firstn`  0
              THEN  Reduce  0
              THEN  Try  (RecFold  `firstn`  0)
              THEN  Auto
              THEN  Try  ((With  \mkleeneopen{}0\mkleeneclose{}  (D  0)\mcdot{}  THEN  Complete  (Auto)))))

---

Home Index