Nuprl Definition : bm_cnt_prop0
bm_cnt_prop0(m) ==
binary_map_ind(m;<0, tt>;key,value,cnt,left,right,recL,recR.<cnt, (cnt =z 1 + (fst(recL)) + (fst(recR))) ∧b (snd(recL)\000C) ∧b (snd(recR))>)
Definitions occuring in Statement :
binary_map_ind: binary_map_ind(v;E;key,value,cnt,left,right,rec1,rec2.T[key;value;cnt;left;right;rec1;rec2]),
band: p ∧b q,
eq_int: (i =z j),
btrue: tt,
pi1: fst(t),
pi2: snd(t),
pair: <a, b>,
add: n + m,
natural_number: $n
FDL editor aliases :
bm_cnt_prop0
bm\_cnt\_prop0(m) ==
binary\_map\_ind(m;ɘ, tt>key,value,cnt,left,right,recL,recR.<cnt
, (cnt =\msubz{} 1 + (fst(recL)) + (fst(recR)))
\mwedge{}\msubb{} (snd(recL))
\mwedge{}\msubb{} (snd(recR))
>)
Date html generated:
2015_07_17-AM-08_18_00
Last ObjectModification:
2012_08_21-AM-10_41_57
Home
Index