---

Step * of Lemma bm_insert_wf

∀[T,Key:Type]. ∀[compare:bm_compare(Key)]. ∀[m:binary-map(T;Key)]. ∀[x:Key]. ∀[v:T].
  (bm_insert(compare;m;x;v) ∈ binary-map(T;Key))
BY
{ (Auto
   THEN Unfold `binary-map` (-3)
   THEN DVarSets
   THEN BinMapInd `m'
   THEN (RepUR ``bm_insert`` 0 THEN Try (Fold `bm_insert` 0))
   THEN Try (((CallByValueReduce 0 THENA Auto) THEN OnSomeHyp (\h. RWO "bm_cnt_prop_T" h THEN Auto)))
   THEN Auto
   THEN BLemma `bm_T-wf2`
   THEN Auto) }

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  Unfold  `binary-map`  (-3)
  THEN  DVarSets
  THEN  BinMapInd  `m'
  THEN  (RepUR  ``bm\_insert``  0  THEN  Try  (Fold  `bm\_insert`  0))
  THEN  Try  (((CallByValueReduce  0  THENA  Auto)  THEN  OnSomeHyp  (\mbackslash{}h.  RWO  "bm\_cnt\_prop\_T"  h  THEN  Auto)))
  THEN  Auto
  THEN  BLemma  `bm\_T-wf2`
  THEN  Auto)

---

Home Index