---

Step * of Lemma collect_accm-wf2

∀[A:Type]. ∀[P:{L:A List| 0 < ||L||}  ─→ 𝔹]. ∀[num:A ─→ ℕ].
  (collect_accm(v.P[v];v.num[v]) ∈ {s:ℤ × {L:A List| 0 < ||L|| ⇒ (¬↑P[L])}  × ({L:A List| 0 < ||L|| ∧ (↑P[L])}  + Top)|\000C 
                                    (↑isl(snd(snd(s)))) ⇒ (1 ≤ (fst(s)))} 
   ─→ A
   ─→ {s:ℤ × {L:A List| 0 < ||L|| ⇒ (¬↑P[L])}  × ({L:A List| 0 < ||L|| ∧ (↑P[L])}  + Top)| 
       (↑isl(snd(snd(s)))) ⇒ (1 ≤ (fst(s)))} )
BY
{ (ProveWfLemma THEN (MemTypeCD THEN Auto THEN Reduce 0 THEN Auto)⋅) }

---

Latex:


\mforall{}[A:Type].  \mforall{}[P:\{L:A  List|  0  <  ||L||\}    {}\mrightarrow{}  \mBbbB{}].  \mforall{}[num:A  {}\mrightarrow{}  \mBbbN{}].
    (collect\_accm(v.P[v];v.num[v])  \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{}  A
      {}\mrightarrow{}  \{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)))\}  )


By

(ProveWfLemma  THEN  (MemTypeCD  THEN  Auto  THEN  Reduce  0  THEN  Auto)\mcdot{})

---

Home Index