---

Step * 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. 0 < ||filter(λa.P[a];as)||
⊢ (hd(filter(λa.P[a];as)) ∈ T) c∧ ((hd(filter(λa.P[a];as)) ∈ as) ∧ (↑P[hd(filter(λa.P[a];as))]))
BY
{ xxx(MoveToConcl (-1) THEN GenConclTerm ⌜filter(λa.P[a];as)⌝⋅ THEN 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
⊢ (hd(v) ∈ as)

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) ∈ as)
⊢ ↑P[hd(v)]

---

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.  0  <  ||filter(\mlambda{}a.P[a];as)||
\mvdash{}  (hd(filter(\mlambda{}a.P[a];as))  \mmember{}  T)  c\mwedge{}  ((hd(filter(\mlambda{}a.P[a];as))  \mmember{}  as)  \mwedge{}  (\muparrow{}P[hd(filter(\mlambda{}a.P[a];as))]))


By

---

Latex:
xxx(MoveToConcl  (-1)  THEN  GenConclTerm  \mkleeneopen{}filter(\mlambda{}a.P[a];as)\mkleeneclose{}\mcdot{}  THEN  Auto)xxx

---

Home Index