---

Step * of Lemma bm_try_remove_wf

∀[T,Key:Type]. ∀[compare:bm_compare(Key)]. ∀[x:Key]. ∀[m:binary-map(T;Key)].
  (bm_try_remove(compare;m;x) ∈ binary-map(T;Key) × (T?))
BY
{ (Auto
   THEN Unfold `binary-map` (-1)
   THEN DVarSets
   THEN BinaryMapInd (-2)
   THEN DVarSets
   THEN RepUR ``bm_try_remove`` 0
   THEN Try (Fold `bm_try_remove` 0)
   THEN Auto
   THEN BLemma `bm_E-wf2`
   THEN Auto) }

---

Latex:


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


By

(Auto
  THEN  Unfold  `binary-map`  (-1)
  THEN  DVarSets
  THEN  BinaryMapInd  (-2)
  THEN  DVarSets
  THEN  RepUR  ``bm\_try\_remove``  0
  THEN  Try  (Fold  `bm\_try\_remove`  0)
  THEN  Auto
  THEN  BLemma  `bm\_E-wf2`
  THEN  Auto)

---

Home Index