---

Step * of Lemma bm_T-wf2

∀[T,Key:Type]. ∀[key:Key]. ∀[value:T]. ∀[cnt:ℤ]. ∀[left,right:binary-map(T;Key)].
  bm_T(key;value;cnt;left;right) ∈ binary-map(T;Key) supposing cnt = (1 + bm_numItems(left) + bm_numItems(right)) ∈ ℤ
BY
{ (Auto THEN MemTypeCD THEN Auto THEN BLemma `bm_cnt_prop_T` THEN Auto) }

---

Latex:


\mforall{}[T,Key:Type].  \mforall{}[key:Key].  \mforall{}[value:T].  \mforall{}[cnt:\mBbbZ{}].  \mforall{}[left,right:binary-map(T;Key)].
    bm\_T(key;value;cnt;left;right)  \mmember{}  binary-map(T;Key) 
    supposing  cnt  =  (1  +  bm\_numItems(left)  +  bm\_numItems(right))


By

(Auto  THEN  MemTypeCD  THEN  Auto  THEN  BLemma  `bm\_cnt\_prop\_T`  THEN  Auto)

---

Home Index