---

Step * of Lemma bm_double_R_wf

∀[T,Key:Type]. ∀[c:Key]. ∀[cv:T]. ∀[m,z:binary-map(T;Key)].
  (bm_double_R(c;cv;m;z) ∈ binary-map(T;Key)) supposing ((↑bm_T?(bm_T-right(m))) and (↑bm_T?(m)))
BY
{ (Auto
   THEN All (RepUR ``binary-map bm_double_R``)
   THEN Fold `binary-map` 0
   THEN DVarSets
   THEN (DVar `m' THEN All Reduce THEN Try (Trivial) THEN DVar `m5' THEN All Reduce THEN Try (Trivial))
   THEN RWO "bm_cnt_prop_T" (-5)
   THEN Auto
   THEN MemTypeCD
   THEN Auto) }

---

Latex:


\mforall{}[T,Key:Type].  \mforall{}[c:Key].  \mforall{}[cv:T].  \mforall{}[m,z:binary-map(T;Key)].
    (bm\_double\_R(c;cv;m;z)  \mmember{}  binary-map(T;Key))  supposing  ((\muparrow{}bm\_T?(bm\_T-right(m)))  and  (\muparrow{}bm\_T?(m)))


By

(Auto
  THEN  All  (RepUR  ``binary-map  bm\_double\_R``)
  THEN  Fold  `binary-map`  0
  THEN  DVarSets
  THEN  (DVar  `m'
              THEN  All  Reduce
              THEN  Try  (Trivial)
              THEN  DVar  `m5'
              THEN  All  Reduce
              THEN  Try  (Trivial))
  THEN  RWO  "bm\_cnt\_prop\_T"  (-5)
  THEN  Auto
  THEN  MemTypeCD
  THEN  Auto)

---

Home Index