---

Step * 1 1 of Lemma hd-filter


1. [T] : Type
2. P : T ⟶ 𝔹
3. as : T List
4. ∃a:T. ((a ∈ as) ∧ (↑P[a]))
5. filter(λa.P[a];as) ∈ {x:T| ↑((λa.P[a]) x)}  List
6. v : {x:T| ↑((λa.P[a]) x)}  List
7. filter(λa.P[a];as) = v ∈ ({x:T| ↑((λa.P[a]) x)}  List)
8. 0 < ||v||
9. hd(v) ∈ T
⊢ (hd(v) ∈ as)
BY
{ xxx(Assert (hd(v) ∈ v) BY
            Auto)xxx }

1
1. T : Type
2. P : T ⟶ 𝔹
3. as : T List
4. ∃a:T. ((a ∈ as) ∧ (↑P[a]))
5. filter(λa.P[a];as) ∈ {x:T| ↑((λa.P[a]) x)}  List
6. v : {x:T| ↑((λa.P[a]) x)}  List
7. filter(λa.P[a];as) = v ∈ ({x:T| ↑((λa.P[a]) x)}  List)
8. 0 < ||v||
9. hd(v) ∈ T
⊢ ¬↑null(v)

2
1. [T] : Type
2. P : T ⟶ 𝔹
3. as : T List
4. ∃a:T. ((a ∈ as) ∧ (↑P[a]))
5. filter(λa.P[a];as) ∈ {x:T| ↑((λa.P[a]) x)}  List
6. v : {x:T| ↑((λa.P[a]) x)}  List
7. filter(λa.P[a];as) = v ∈ ({x:T| ↑((λa.P[a]) x)}  List)
8. 0 < ||v||
9. hd(v) ∈ T
10. (hd(v) ∈ v)
⊢ (hd(v) ∈ as)

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  P  :  T  {}\mrightarrow{}  \mBbbB{}
3.  as  :  T  List
4.  \mexists{}a:T.  ((a  \mmember{}  as)  \mwedge{}  (\muparrow{}P[a]))
5.  filter(\mlambda{}a.P[a];as)  \mmember{}  \{x:T|  \muparrow{}((\mlambda{}a.P[a])  x)\}    List
6.  v  :  \{x:T|  \muparrow{}((\mlambda{}a.P[a])  x)\}    List
7.  filter(\mlambda{}a.P[a];as)  =  v
8.  0  <  ||v||
9.  hd(v)  \mmember{}  T
\mvdash{}  (hd(v)  \mmember{}  as)


By

---

Latex:
xxx(Assert  (hd(v)  \mmember{}  v)  BY
                    Auto)xxx

---

Home Index