---

Step * of Lemma bm_find_wf

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

---

Latex:


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


By

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

---

Home Index