---

Step * of Lemma bm_delmin_wf

∀[T,Key:Type]. ∀[m:binary-map(T;Key)].  bm_delmin(m) ∈ binary-map(T;Key) supposing ↑bm_T?(m)
BY
{ (Auto
   THEN Unfold `binary-map` (-2)
   THEN DVarSets
   THEN BinMapInd `m'
   THEN RepUR ``bm_delmin`` 0
   THEN Fold `bm_delmin` 0
   THEN (RWO "bm_cnt_prop_T" (-1) THENA Auto)
   THEN RepD
   THEN DVarSets
   THEN BinMapCase `left'
   THEN Try (Complete ((MemTypeCD THEN Auto)))
   THEN Auto) }

---

Latex:


\mforall{}[T,Key:Type].  \mforall{}[m:binary-map(T;Key)].    bm\_delmin(m)  \mmember{}  binary-map(T;Key)  supposing  \muparrow{}bm\_T?(m)


By

(Auto
  THEN  Unfold  `binary-map`  (-2)
  THEN  DVarSets
  THEN  BinMapInd  `m'
  THEN  RepUR  ``bm\_delmin``  0
  THEN  Fold  `bm\_delmin`  0
  THEN  (RWO  "bm\_cnt\_prop\_T"  (-1)  THENA  Auto)
  THEN  RepD
  THEN  DVarSets
  THEN  BinMapCase  `left'
  THEN  Try  (Complete  ((MemTypeCD  THEN  Auto)))
  THEN  Auto)

---

Home Index