---

Step * of Lemma bm_foldl_wf

∀[T,U,Key:Type]. ∀[f:T ─→ U ─→ U]. ∀[m:binary-map(T;Key)]. ∀[init:U].  (bm_foldl(f;init;m) ∈ U)
BY
{ ProveWfLemma }

---

Latex:


\mforall{}[T,U,Key:Type].  \mforall{}[f:T  {}\mrightarrow{}  U  {}\mrightarrow{}  U].  \mforall{}[m:binary-map(T;Key)].  \mforall{}[init:U].    (bm\_foldl(f;init;m)  \mmember{}  U)


By

ProveWfLemma

---

Home Index