Nuprl Lemma : bm_cnt_prop0_T
∀[key,value,cnt,left,right:Top].
(bm_cnt_prop0(bm_T(key;value;cnt;left;right)) ~ <cnt
, (cnt =z 1 + (fst(bm_cnt_prop0(left))) + (fst(bm_cnt_prop0(right))))
∧b (snd(bm_cnt_prop0(left)))
∧b (snd(bm_cnt_prop0(right)))
>)
Proof
Definitions occuring in Statement :
bm_cnt_prop0: bm_cnt_prop0(m),
bm_T: bm_T(key;value;cnt;left;right),
band: p ∧b q,
eq_int: (i =z j),
uall: ∀[x:A]. B[x],
top: Top,
pi1: fst(t),
pi2: snd(t),
pair: <a, b>,
add: n + m,
natural_number: $n,
sqequal: s ~ t
Lemmas :
top_wf
\mforall{}[key,value,cnt,left,right:Top].
(bm\_cnt\_prop0(bm\_T(key;value;cnt;left;right)) \msim{} <cnt
, (cnt =\msubz{} 1
+ (fst(bm\_cnt\_prop0(left)))
+ (fst(bm\_cnt\_prop0(right))))
\mwedge{}\msubb{} (snd(bm\_cnt\_prop0(left)))
\mwedge{}\msubb{} (snd(bm\_cnt\_prop0(right)))
>)
Date html generated:
2015_07_17-AM-08_18_04
Last ObjectModification:
2015_01_27-PM-00_39_47
Home
Index