---

Step * of Lemma hd-filter

∀[T:Type]
  ∀P:T ⟶ 𝔹. ∀as:T List.
    ((∃a:T. ((a ∈ as) ∧ (↑P[a])))
    ⇒ ((hd(filter(λa.P[a];as)) ∈ T) c∧ ((hd(filter(λa.P[a];as)) ∈ as) ∧ (↑P[hd(filter(λa.P[a];as))]))))
BY
{ xxx((xxxUnivCDxxx THENA Auto)
      THEN (InstLemma `filter_type` [⌜T⌝;⌜λa.P[a]⌝;⌜as⌝]⋅ THENA Auto)
      THEN (InstLemma `length-filter-pos` [⌜T⌝;⌜λa.P[a]⌝;⌜as⌝]⋅ THENA (Auto THEN BLemma `l_exists_iff` 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. 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))]))

---

Latex:

---

Latex:
\mforall{}[T:Type]
    \mforall{}P:T  {}\mrightarrow{}  \mBbbB{}.  \mforall{}as:T  List.
        ((\mexists{}a:T.  ((a  \mmember{}  as)  \mwedge{}  (\muparrow{}P[a])))
        {}\mRightarrow{}  ((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((xxxUnivCDxxx  THENA  Auto)
        THEN  (InstLemma  `filter\_type`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}\mlambda{}a.P[a]\mkleeneclose{};\mkleeneopen{}as\mkleeneclose{}]\mcdot{}  THENA  Auto)
        THEN  (InstLemma  `length-filter-pos`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}\mlambda{}a.P[a]\mkleeneclose{};\mkleeneopen{}as\mkleeneclose{}]\mcdot{}
                    THENA  (Auto  THEN  BLemma  `l\_exists\_iff`  THEN  Auto)
                    ))xxx

---

Home Index