---

Step * of Lemma filter-index_wf

No Annotations
∀[T:Type]. ∀[P:T ⟶ 𝔹]. ∀[L:T List].  (filter-index(P;L) ∈ i:{i:ℕ||L||| ↑(P L[i])}  ⟶ {j:ℕ||filter(P;L)||| filter(P;L)[\000Cj] = L[i] ∈ T} )
BY
{ (Auto
   THEN (ExtWith [`i'] [⌜Void ⟶ Void⌝]⋅ THENA Auto)
   THEN D -1
   THEN RepeatFor 2 (MoveToConcl (-1))
   THEN ListInd (-1)
   THEN Reduce 0
   THEN (D 0 THENA Auto)) }

1
1. T : Type
2. P : T ⟶ 𝔹
3. i : ℕ0
⊢ (↑(P ⊥)) ⇒ (filter-index(P;[]) i ∈ {j:ℕ0| ⊥ = ⊥ ∈ T} )

2
1. T : Type
2. P : T ⟶ 𝔹
3. u : T
4. v : T List
5. ∀i:ℕ||v||. ((↑(P v[i])) ⇒ (filter-index(P;v) i ∈ {j:ℕ||filter(P;v)||| filter(P;v)[j] = v[i] ∈ T} ))
6. i : ℕ||v|| + 1
⊢ (↑(P [u / v][i]))
⇒ (filter-index(P;[u / v]) i ∈ {j:ℕ||if P u then [u / filter(P;v)] else filter(P;v) fi ||| 
                                 if P u then [u / filter(P;v)] else filter(P;v) fi [j] = [u / v][i] ∈ T} )

---

Latex:

---

Latex:
No  Annotations
\mforall{}[T:Type].  \mforall{}[P:T  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[L:T  List].
    (filter-index(P;L)  \mmember{}  i:\{i:\mBbbN{}||L|||  \muparrow{}(P  L[i])\}    {}\mrightarrow{}  \{j:\mBbbN{}||filter(P;L)|||  filter(P;L)[j]  =  L[i]\}  )


By

---

Latex:
(Auto
  THEN  (ExtWith  [`i']  [\mkleeneopen{}Void  {}\mrightarrow{}  Void\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  D  -1
  THEN  RepeatFor  2  (MoveToConcl  (-1))
  THEN  ListInd  (-1)
  THEN  Reduce  0
  THEN  (D  0  THENA  Auto))

---

Home Index