---

Step * of Lemma bm_single_L_wf

∀[T,Key:Type]. ∀[a:Key]. ∀[av:T]. ∀[x,m:binary-map(T;Key)].
  bm_single_L(a;av;x;m) ∈ binary-map(T;Key) supposing ↑bm_T?(m)
BY
{ (Auto
   THEN All (RepUR ``binary-map bm_single_L``)
   THEN DVarSets
   THEN D -3
   THEN All Reduce⋅
   THEN Try (Trivial)
   THEN (RWO "bm_cnt_prop_T" (-2) THENA Auto)
   THEN RepUR ``binary_map_case`` 0
   THEN Fold `binary-map` 0
   THEN Auto) }

---

Latex:


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


By

(Auto
  THEN  All  (RepUR  ``binary-map  bm\_single\_L``)
  THEN  DVarSets
  THEN  D  -3
  THEN  All  Reduce\mcdot{}
  THEN  Try  (Trivial)
  THEN  (RWO  "bm\_cnt\_prop\_T"  (-2)  THENA  Auto)
  THEN  RepUR  ``binary\_map\_case``  0
  THEN  Fold  `binary-map`  0
  THEN  Auto)

---

Home Index