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
Definitions unfolded in proof : 
uall: ∀[x:A]. B[x]
, 
member: t ∈ T
, 
so_lambda: λ2x.t[x]
, 
uimplies: b supposing a
, 
prop: ℙ
, 
so_apply: x[s]
, 
implies: P 
⇒ Q
, 
all: ∀x:A. B[x]
, 
top: Top
, 
uiff: uiff(P;Q)
, 
and: P ∧ Q
, 
guard: {T}
, 
iff: P 
⇐⇒ Q
, 
rev_implies: P 
⇐ Q
Latex:
\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:
2016_05_17-PM-01_39_14
Last ObjectModification:
2015_12_28-PM-08_10_44
Theory : binary-map
Home
Index