---

Step * of Lemma bm_single_R_wf

∀[T,Key:Type]. ∀[b:Key]. ∀[bv:T]. ∀[m,z:binary-map(T;Key)].
  bm_single_R(b;bv;m;z) ∈ binary-map(T;Key) supposing ↑bm_T?(m)
BY
{ (Auto
   THEN All (RepUR ``binary-map bm_single_R``)
   THEN DVarSets
   THEN DVar `m'
   THEN All Reduce⋅
   THEN Try (Trivial)
   THEN (RWO "bm_cnt_prop_T" (-4) THENA Auto)
   THEN RepUR ``binary_map_case`` 0
   THEN Fold `binary-map` 0
   THEN Auto) }

---

Latex:


\mforall{}[T,Key:Type].  \mforall{}[b:Key].  \mforall{}[bv:T].  \mforall{}[m,z:binary-map(T;Key)].
    bm\_single\_R(b;bv;m;z)  \mmember{}  binary-map(T;Key)  supposing  \muparrow{}bm\_T?(m)


By

(Auto
  THEN  All  (RepUR  ``binary-map  bm\_single\_R``)
  THEN  DVarSets
  THEN  DVar  `m'
  THEN  All  Reduce\mcdot{}
  THEN  Try  (Trivial)
  THEN  (RWO  "bm\_cnt\_prop\_T"  (-4)  THENA  Auto)
  THEN  RepUR  ``binary\_map\_case``  0
  THEN  Fold  `binary-map`  0
  THEN  Auto)

---

Home Index