---

Step * of Lemma bm_N_wf

∀[T,Key:Type]. ∀[k:Key]. ∀[v:T]. ∀[m1,m2:binary-map(T;Key)].  (bm_N(k;v;m1;m2) ∈ binary-map(T;Key))
BY
{ (Auto
   THEN All (RepUR ``binary-map bm_N``)
   THEN DVarSets
   THEN MemTypeCD
   THEN Auto
   THEN OnVar `m1' BinaryMapCase 
   THEN OnVar `m2' BinaryMapCase 
   THEN (RWO "bm_cnt_prop_T" 0 THENA Auto)
   THEN Try ((RWO "bm_cnt_prop_E" 0 THENA Auto))
   THEN Try ((RWO "bm_numItems_E" 0 THENA Auto))
   THEN Try ((RWO "bm_numItems_T" 0 THENA Auto))
   THEN Reduce 0
   THEN Auto) }

---

Latex:


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


By

(Auto
  THEN  All  (RepUR  ``binary-map  bm\_N``)
  THEN  DVarSets
  THEN  MemTypeCD
  THEN  Auto
  THEN  OnVar  `m1'  BinaryMapCase 
  THEN  OnVar  `m2'  BinaryMapCase 
  THEN  (RWO  "bm\_cnt\_prop\_T"  0  THENA  Auto)
  THEN  Try  ((RWO  "bm\_cnt\_prop\_E"  0  THENA  Auto))
  THEN  Try  ((RWO  "bm\_numItems\_E"  0  THENA  Auto))
  THEN  Try  ((RWO  "bm\_numItems\_T"  0  THENA  Auto))
  THEN  Reduce  0
  THEN  Auto)

---

Home Index