---

Step * of Lemma bm_lookup_wf

∀[T,Key:Type]. ∀[compare:bm_compare(Key)]. ∀[x:Key]. ∀[m:binary-map(T;Key)].
  bm_lookup(compare;m;x) ∈ T supposing ↑bm_inDomain(compare;m;x)
BY
{ (Auto
   THEN Unfold `binary-map` (-2)
   THEN DVarSets
   THEN BinaryMapInd (-3)
   THEN RepUR ``bm_inDomain bm_lookup`` 0
   THEN Try (Folds ``bm_inDomain bm_lookup`` 0)
   THEN Try ((BLemma `bm_T-wf2` THEN Auto))
   THEN Try (CallByValueReduce 0)
   THEN Auto) }

---

Latex:


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


By

(Auto
  THEN  Unfold  `binary-map`  (-2)
  THEN  DVarSets
  THEN  BinaryMapInd  (-3)
  THEN  RepUR  ``bm\_inDomain  bm\_lookup``  0
  THEN  Try  (Folds  ``bm\_inDomain  bm\_lookup``  0)
  THEN  Try  ((BLemma  `bm\_T-wf2`  THEN  Auto))
  THEN  Try  (CallByValueReduce  0)
  THEN  Auto)

---

Home Index