---

Step * of Lemma bm_double_L_wf

∀[T,Key:Type]. ∀[a:Key]. ∀[av:T]. ∀[w,m:binary-map(T;Key)].
  (bm_double_L(a;av;w;m) ∈ binary-map(T;Key)) supposing ((↑bm_T?(bm_T-left(m))) and (↑bm_T?(m)))
BY
{ (Auto
   THEN All (RepUR ``binary-map bm_double_L``)
   THEN DVarSets
   THEN Fold `binary-map` 0
   THEN DVar `m'
   THEN All Reduce
   THEN Try (Trivial)
   THEN ThinTrivial
   THEN DVar `left'
   THEN All Reduce
   THEN Try (Trivial)
   THEN ThinTrivial
   THEN (RWO "bm_cnt_prop_T" (-1) THENA Auto)
   THEN RepUR ``binary_map_case`` 0
   THEN Auto
   THEN RWO "bm_cnt_prop_T" (-2)
   THEN Auto) }

---

Latex:


\mforall{}[T,Key:Type].  \mforall{}[a:Key].  \mforall{}[av:T].  \mforall{}[w,m:binary-map(T;Key)].
    (bm\_double\_L(a;av;w;m)  \mmember{}  binary-map(T;Key))  supposing  ((\muparrow{}bm\_T?(bm\_T-left(m)))  and  (\muparrow{}bm\_T?(m)))


By

(Auto
  THEN  All  (RepUR  ``binary-map  bm\_double\_L``)
  THEN  DVarSets
  THEN  Fold  `binary-map`  0
  THEN  DVar  `m'
  THEN  All  Reduce
  THEN  Try  (Trivial)
  THEN  ThinTrivial
  THEN  DVar  `left'
  THEN  All  Reduce
  THEN  Try  (Trivial)
  THEN  ThinTrivial
  THEN  (RWO  "bm\_cnt\_prop\_T"  (-1)  THENA  Auto)
  THEN  RepUR  ``binary\_map\_case``  0
  THEN  Auto
  THEN  RWO  "bm\_cnt\_prop\_T"  (-2)
  THEN  Auto)

---

Home Index