---

Step * of Lemma bm_delete'_wf

∀[T,Key:Type]. ∀[m1,m2:binary-map(T;Key)].  (bm_delete'(m1;m2) ∈ binary-map(T;Key))
BY
{ (Auto
   THEN RepUR ``bm_delete'`` 0
   THEN BinMapCase `m1'
   THEN BinMapCase `m2'
   THEN GenConclAtAddr [2;1]
   THEN DVar `v'
   THEN Reduce 0
   THEN Auto
   THEN MemTypeCD
   THEN Auto) }

---

Latex:


\mforall{}[T,Key:Type].  \mforall{}[m1,m2:binary-map(T;Key)].    (bm\_delete'(m1;m2)  \mmember{}  binary-map(T;Key))


By

(Auto
  THEN  RepUR  ``bm\_delete'``  0
  THEN  BinMapCase  `m1'
  THEN  BinMapCase  `m2'
  THEN  GenConclAtAddr  [2;1]
  THEN  DVar  `v'
  THEN  Reduce  0
  THEN  Auto
  THEN  MemTypeCD
  THEN  Auto)

---

Home Index