---

Step * of Lemma collect_accum_wf

∀[A,B:Type]. ∀[P:B ⟶ 𝔹]. ∀[num:A ⟶ ℕ]. ∀[init:B]. ∀[f:B ⟶ A ⟶ B].
  (collect_accum(x.num[x];init;a,v.f[a;v];a.P[a]) ∈ (ℤ × B × (B + Top)) ⟶ A ⟶ (ℤ × B × (B + Top)))
BY
{ ProveWfLemma }

---

Latex:

---

Latex:
\mforall{}[A,B:Type].  \mforall{}[P:B  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[num:A  {}\mrightarrow{}  \mBbbN{}].  \mforall{}[init:B].  \mforall{}[f:B  {}\mrightarrow{}  A  {}\mrightarrow{}  B].
    (collect\_accum(x.num[x];init;a,v.f[a;v];a.P[a])  \mmember{}  (\mBbbZ{}  \mtimes{}  B  \mtimes{}  (B  +  Top))  {}\mrightarrow{}  A  {}\mrightarrow{}  (\mBbbZ{}  \mtimes{}  B  \mtimes{}  (B  +  Top)))


By

---

Latex:
ProveWfLemma

---

Home Index