---

Step * of Lemma bm_insert'_wf

∀[T,Key:Type]. ∀[compare:bm_compare(Key)]. ∀[p:Key × T]. ∀[m:binary-map(T;Key)].
  (bm_insert'(compare;p;m) ∈ binary-map(T;Key))
BY
{ ProveWfLemma }

---

Latex:

---

Latex:
\mforall{}[T,Key:Type].  \mforall{}[compare:bm\_compare(Key)].  \mforall{}[p:Key  \mtimes{}  T].  \mforall{}[m:binary-map(T;Key)].
    (bm\_insert'(compare;p;m)  \mmember{}  binary-map(T;Key))


By

---

Latex:
ProveWfLemma

---

Home Index