---

Step * of Lemma bm_inDomain_wf

∀[T,Key:Type]. ∀[compare:bm_compare(Key)]. ∀[x:Key]. ∀[m:binary-map(T;Key)].  (bm_inDomain(compare;m;x) ∈ 𝔹)
BY
{ (Auto
   THEN Unfold `binary-map` (-1)
   THEN DVarSets
   THEN BinMapInd `m'
   THEN RepUR ``bm_inDomain`` 0
   THEN Try ((Fold `bm_inDomain` 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\_inDomain(compare;m;x)  \mmember{}  \mBbbB{})


By

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

---

Home Index