Nuprl Definition : bm_N
bm_N(k;v;m1;m2) ==
binary_map_case(m1;binary_map_case(m2;bm_T(k;v;1;bm_E();bm_E());key,value,cnt,left,right.bm_T(k;v;1 + cnt;bm_E();m2));
key,value,cnt,left,right.binary_map_case(m2;bm_T(k;v;1 + cnt;m1;bm_E());key',value',cnt',left',right'.
bm_T(k;v;1 + cnt + cnt';m1;m2)))
Definitions occuring in Statement :
binary_map_case: binary_map_case(m;E;key,value,cnt,left,right.F[key; value; cnt; left; right]),
bm_T: bm_T(key;value;cnt;left;right),
bm_E: bm_E(),
add: n + m,
natural_number: $n
FDL editor aliases :
bm_N
bm\_N(k;v;m1;m2) ==
binary\_map\_case(m1;binary\_map\_case(m2;bm\_T(k;v;1;bm\_E();bm\_E());key,value,cnt,left,right.
bm\_T(k;v;1 + cnt;bm\_E();m2));key,value,cnt,left,right.
binary\_map\_case(m2;bm\_T(k;v;1 + cnt;m1;bm\_E());key',value',cnt',left',right'.
bm\_T(k;v;1 + cnt + cnt';m1;m2)))
Date html generated:
2015_07_17-AM-08_18_53
Last ObjectModification:
2012_08_20-PM-07_11_35
Home
Index