Nuprl Lemma : bm

∀[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)) ∈ ℤ

Proof

Definitions occuring in Statement : bm_numItems: bm_numItems(m), binary-map: binary-map(T;Key), bm_T: bm_T(key;value;cnt;left;right), uimplies: b supposing a, uall: ∀[x:A]. B[x], member: t ∈ T, add: n + m, natural_number: $n, int: ℤ, universe: Type, equal: s = t ∈ T
Lemmas : bm_cnt_prop_T, assert_elim, bm_cnt_prop_wf, subtype_base_sq, bool_wf, bool_subtype_base, assert_wf, equal-wf-base-T, int_subtype_base, bm_numItems_wf, binary-map_wf
\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)) Date html generated: 2015_07_17-AM-08_18_38 Last ObjectModification: 2015_01_27-PM-00_40_09 Home Index