---

Step * 1 of Lemma member-filter-witness_wf


1. T : Type
2. P : T ⟶ 𝔹
3. L : T List
4. x : {x:T| ↑(P x)} 
5. i : ℕ
6. t2 : i < ||L||
7. t3 : x = L[i] ∈ T
⊢ <filter-index(P;L) i, ⋅, ⋅> ∈ (x ∈ filter(P;L))
BY
{ TACTIC:GenConclAtAddr [2;1] }

1
1. T : Type
2. P : T ⟶ 𝔹
3. L : T List
4. x : {x:T| ↑(P x)} 
5. i : ℕ
6. t2 : i < ||L||
7. t3 : x = L[i] ∈ T
8. v : {j:ℕ||filter(P;L)||| filter(P;L)[j] = L[i] ∈ T} 
9. (filter-index(P;L) i) = v ∈ {j:ℕ||filter(P;L)||| filter(P;L)[j] = L[i] ∈ T} 
⊢ <v, ⋅, ⋅> ∈ (x ∈ filter(P;L))

---

Latex:

---

Latex:

1.  T  :  Type
2.  P  :  T  {}\mrightarrow{}  \mBbbB{}
3.  L  :  T  List
4.  x  :  \{x:T|  \muparrow{}(P  x)\} 
5.  i  :  \mBbbN{}
6.  t2  :  i  <  ||L||
7.  t3  :  x  =  L[i]
\mvdash{}  <filter-index(P;L)  i,  \mcdot{},  \mcdot{}>  \mmember{}  (x  \mmember{}  filter(P;L))


By

---

Latex:
TACTIC:GenConclAtAddr  [2;1]

---

Home Index