---

Step * 1 1 1 1 1 1 of Lemma fset-find_wf


1. T : Type
2. eq : EqDecider(T)
3. P : T ⟶ 𝔹
4. s : Base
5. s ∈ T List
6. ∃x:T. ((x ∈ s) ∧ (↑(P x)))
⊢ hd(filter(P;s)) ∈ {x:T| (x ∈ s) ∧ (↑(P x))} 
BY
{ ((InstLemma `filter_type` [⌜{x:T| (x ∈ s)} ⌝;⌜P⌝;⌜s⌝]⋅ THENA Auto)
   THEN SubsumeC ⌜{x:{x:T| (x ∈ s)} | ↑(P x)} ⌝⋅
   THEN Auto
   THEN Try (((D 0 THENA Auto) THEN D -1 THEN D -2 THEN Complete (Auto)))) }

1
1. T : Type
2. eq : EqDecider(T)
3. P : T ⟶ 𝔹
4. s : Base
5. s ∈ T List
6. ∃x:T. ((x ∈ s) ∧ (↑(P x)))
7. filter(P;s) ∈ {x:{x:T| (x ∈ s)} | ↑(P x)}  List
⊢ ||filter(P;s)|| ≥ 1 

---

Latex:

---

Latex:

1.  T  :  Type
2.  eq  :  EqDecider(T)
3.  P  :  T  {}\mrightarrow{}  \mBbbB{}
4.  s  :  Base
5.  s  \mmember{}  T  List
6.  \mexists{}x:T.  ((x  \mmember{}  s)  \mwedge{}  (\muparrow{}(P  x)))
\mvdash{}  hd(filter(P;s))  \mmember{}  \{x:T|  (x  \mmember{}  s)  \mwedge{}  (\muparrow{}(P  x))\} 


By

---

Latex:
((InstLemma  `filter\_type`  [\mkleeneopen{}\{x:T|  (x  \mmember{}  s)\}  \mkleeneclose{};\mkleeneopen{}P\mkleeneclose{};\mkleeneopen{}s\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  SubsumeC  \mkleeneopen{}\{x:\{x:T|  (x  \mmember{}  s)\}  |  \muparrow{}(P  x)\}  \mkleeneclose{}\mcdot{}
  THEN  Auto
  THEN  Try  (((D  0  THENA  Auto)  THEN  D  -1  THEN  D  -2  THEN  Complete  (Auto))))

---

Home Index