---

Step * of Lemma bm_mapi_wf

∀[T,Key:Type]. ∀[f:Key ─→ T ─→ T]. ∀[m:binary-map(T;Key)].  (bm_mapi(f;m) ∈ binary-map(T;Key))
BY
{ ((Auto THEN D -1)
   THEN BinMapInd `m'
   THEN RepUR ``bm_mapi`` 0
   THEN Try (Fold `bm_mapi` 0)
   THEN Try (BLemma `bm_E-wf2`)
   THEN Auto
   THEN (RWO "bm_cnt_prop_T" (-1) THENA Auto)
   THEN DVarSets
   THEN BLemma `bm_T-wf2`
   THEN Auto
   THEN BinMapCase `left'
   THEN BinMapCase `m5'
   THEN RepUR ``bm_mapi`` 0
   THEN Auto) }

---

Latex:


\mforall{}[T,Key:Type].  \mforall{}[f:Key  {}\mrightarrow{}  T  {}\mrightarrow{}  T].  \mforall{}[m:binary-map(T;Key)].    (bm\_mapi(f;m)  \mmember{}  binary-map(T;Key))


By

((Auto  THEN  D  -1)
  THEN  BinMapInd  `m'
  THEN  RepUR  ``bm\_mapi``  0
  THEN  Try  (Fold  `bm\_mapi`  0)
  THEN  Try  (BLemma  `bm\_E-wf2`)
  THEN  Auto
  THEN  (RWO  "bm\_cnt\_prop\_T"  (-1)  THENA  Auto)
  THEN  DVarSets
  THEN  BLemma  `bm\_T-wf2`
  THEN  Auto
  THEN  BinMapCase  `left'
  THEN  BinMapCase  `m5'
  THEN  RepUR  ``bm\_mapi``  0
  THEN  Auto)

---

Home Index