Nuprl Lemma : bm_count_prop
∀[T,Key:Type]. ∀[m:binary_map(T;Key)]. bm_numItems(m) = bm_count(m) ∈ ℤ supposing ↑bm_cnt_prop(m)
Proof
Definitions occuring in Statement :
bm_count: bm_count(m),
bm_numItems: bm_numItems(m),
bm_cnt_prop: bm_cnt_prop(m),
binary_map: binary_map(T;Key),
assert: ↑b,
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
int: ℤ,
universe: Type,
equal: s = t ∈ T
Lemmas :
binary_map-induction,
isect_wf,
assert_wf,
bm_cnt_prop_wf,
equal_wf,
bm_numItems_wf,
bm_count_wf,
bm_numItems_E_reduce_lemma,
bm_count_E_reduce_lemma,
bm_cnt_prop_E,
btrue_wf,
bm_numItems_T,
bm_count_T,
bm_cnt_prop_T,
bm_T_wf,
iff_weakening_equal,
binary_map_wf,
add_functionality_wrt_eq
\mforall{}[T,Key:Type]. \mforall{}[m:binary\_map(T;Key)]. bm\_numItems(m) = bm\_count(m) supposing \muparrow{}bm\_cnt\_prop(m)
Date html generated:
2015_07_17-AM-08_18_46
Last ObjectModification:
2015_02_03-PM-09_47_45
Home
Index