---

Step * of Lemma collect_filter-wf2

∀[A:Type]. ∀[P:{L:A List| 0 < ||L||}  ─→ 𝔹].
  (collect_filter() ∈ {s:ℤ × {L:A List| 0 < ||L|| ⇒ (¬↑P[L])}  × ({L:A List| 0 < ||L|| ∧ (↑P[L])}  + Top)| 
                       (↑isl(snd(snd(s)))) ⇒ (1 ≤ (fst(s)))}  ─→ bag(ℕ × {L:A List| 0 < ||L|| ∧ (↑P[L])} ))
BY
{ (Auto
   THEN Unfold `collect_filter` 0
   THEN MemCD
   THEN Try ((D (-1) THEN RepeatFor 3 (D -2)))
   THEN All Reduce
   THEN (ThinTrivial THEN Auto)⋅) }

---

Latex:


\mforall{}[A:Type].  \mforall{}[P:\{L:A  List|  0  <  ||L||\}    {}\mrightarrow{}  \mBbbB{}].
    (collect\_filter()  \mmember{}  \{s:\mBbbZ{}
                                              \mtimes{}  \{L:A  List|  0  <  ||L||  {}\mRightarrow{}  (\mneg{}\muparrow{}P[L])\} 
                                              \mtimes{}  (\{L:A  List|  0  <  ||L||  \mwedge{}  (\muparrow{}P[L])\}    +  Top)| 
                                              (\muparrow{}isl(snd(snd(s))))  {}\mRightarrow{}  (1  \mleq{}  (fst(s)))\}    {}\mrightarrow{}  bag(\mBbbN{}  \mtimes{}  \{L:A  List|  0  <  ||L||  \mwedge{}  (\muparrow{}P\000C[L])\}  ))


By

(Auto
  THEN  Unfold  `collect\_filter`  0
  THEN  MemCD
  THEN  Try  ((D  (-1)  THEN  RepeatFor  3  (D  -2)))
  THEN  All  Reduce
  THEN  (ThinTrivial  THEN  Auto)\mcdot{})

---

Home Index