Nuprl Definition : bm_count

bm_count(m) ==  binary_map_ind(m;0;key,value,cnt,left,right,recL,recR.1 recL 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]) add: m natural_number: $n
FDL editor aliases :  bm_count

Latex:
bm\_count(m)  ==    binary\_map\_ind(m;0;key,value,cnt,left,right,recL,recR.1  +  recL  +  recR)



Date html generated: 2016_05_17-PM-01_39_02
Last ObjectModification: 2012_08_21-AM-09_50_00

Theory : binary-map


Home Index