---

Step * of Lemma collect_accm_wf

∀[A:Type]. ∀[P:{L:A List| 0 < ||L||}  ─→ 𝔹]. ∀[num:A ─→ ℕ].
  (collect_accm(v.P[v];v.num[v]) ∈ (ℤ × {L:A List| 0 < ||L|| ⇒ (¬↑P[L])}  × ({L:A List| 0 < ||L|| ∧ (↑P[L])}  + Top))
   ─→ A
   ─→ (ℤ × {L:A List| 0 < ||L|| ⇒ (¬↑P[L])}  × ({L:A List| 0 < ||L|| ∧ (↑P[L])}  + Top)))
BY
{ ProveWfLemma }

---

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{}  (\mBbbZ{}
                                                                      \mtimes{}  \{L:A  List|  0  <  ||L||  {}\mRightarrow{}  (\mneg{}\muparrow{}P[L])\} 
                                                                      \mtimes{}  (\{L:A  List|  0  <  ||L||  \mwedge{}  (\muparrow{}P[L])\}    +  Top))
      {}\mrightarrow{}  A
      {}\mrightarrow{}  (\mBbbZ{}  \mtimes{}  \{L:A  List|  0  <  ||L||  {}\mRightarrow{}  (\mneg{}\muparrow{}P[L])\}    \mtimes{}  (\{L:A  List|  0  <  ||L||  \mwedge{}  (\muparrow{}P[L])\}    +  Top)))


By

ProveWfLemma

---

Home Index