---

Step * of Lemma bm_insert_if_not_in_wf

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

---

Latex:


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


By

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

---

Home Index