Nuprl Lemma : bm_count_T
∀[key,value,cnt,left,right:Top]. (bm_count(bm_T(key;value;cnt;left;right)) ~ 1 + bm_count(left) + bm_count(right))
Proof
Definitions occuring in Statement :
bm_count: bm_count(m),
bm_T: bm_T(key;value;cnt;left;right),
uall: ∀[x:A]. B[x],
top: Top,
add: n + m,
natural_number: $n,
sqequal: s ~ t
Lemmas :
top_wf
\mforall{}[key,value,cnt,left,right:Top].
(bm\_count(bm\_T(key;value;cnt;left;right)) \msim{} 1 + bm\_count(left) + bm\_count(right))
Date html generated:
2015_07_17-AM-08_18_45
Last ObjectModification:
2015_01_27-PM-00_39_46
Home
Index