Nuprl Lemma : bm_numItems_is_cnt_prop0
∀[T,Key:Type]. ∀[m:binary_map(T;Key)]. (bm_numItems(m) ~ fst(bm_cnt_prop0(m)))
Proof
Definitions occuring in Statement :
bm_numItems: bm_numItems(m),
bm_cnt_prop0: bm_cnt_prop0(m),
binary_map: binary_map(T;Key),
uall: ∀[x:A]. B[x],
pi1: fst(t),
universe: Type,
sqequal: s ~ t
Lemmas :
subtype_base_sq,
int_subtype_base,
binary_map-ext,
eq_atom_wf,
bool_wf,
eqtt_to_assert,
assert_of_eq_atom,
atom_subtype_base,
unit_wf2,
unit_subtype_base,
it_wf,
bm_numItems_E,
bm_cnt_prop0_E_reduce_lemma,
eqff_to_assert,
equal_wf,
bool_cases_sqequal,
bool_subtype_base,
assert-bnot,
neg_assert_of_eq_atom,
bm_numItems_T_reduce_lemma,
bm_cnt_prop0_T,
binary_map_wf
\mforall{}[T,Key:Type]. \mforall{}[m:binary\_map(T;Key)]. (bm\_numItems(m) \msim{} fst(bm\_cnt\_prop0(m)))
Date html generated:
2015_07_17-AM-08_18_34
Last ObjectModification:
2015_01_27-PM-00_40_02
Home
Index