---

Step * of Lemma collect_filter_wf

∀[A:Type]. ∀[P:{L:A List| 0 < ||L||}  ⟶ 𝔹].
  (collect_filter() ∈ (ℤ × {L:A List| 0 < ||L|| ⇒ (¬↑P[L])}  × ({L:A List| 0 < ||L|| ∧ (↑P[L])}  + Top))
   ⟶ bag(ℤ × {L:A List| 0 < ||L|| ∧ (↑P[L])} ))
BY
{ ProveWfLemma }

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[P:\{L:A  List|  0  <  ||L||\}    {}\mrightarrow{}  \mBbbB{}].
    (collect\_filter()  \mmember{}  (\mBbbZ{}
      \mtimes{}  \{L:A  List|  0  <  ||L||  {}\mRightarrow{}  (\mneg{}\muparrow{}P[L])\} 
      \mtimes{}  (\{L:A  List|  0  <  ||L||  \mwedge{}  (\muparrow{}P[L])\}    +  Top))  {}\mrightarrow{}  bag(\mBbbZ{}  \mtimes{}  \{L:A  List|  0  <  ||L||  \mwedge{}  (\muparrow{}P[L])\}  ))


By

---

Latex:
ProveWfLemma

---

Home Index