Nuprl Definition : bm_T'

bm_T'(k;v;m1;m2) ==
  binary_map_case(m1;binary_map_case(m2;bm_T(k;v;1;bm_E();bm_E());key2,value2,cnt2,left2,right2.
                                     binary_map_case(left2;binary_map_case(right2;bm_T(k;v;2;bm_E();m2);
                                                                           key2r,value2r,cnt2r,left2r,right2r.
                                                                           bm_single_L(k;v;m1;m2));
                                                     key2l,value2l,cnt2l,left2l,right2l.
                                                     binary_map_case(right2;bm_double_L(k;v;m1;m2);
                                                                     key2r,value2r,cnt2r,left2r,right2r.
                                                                     if cnt2l <z cnt2r
                                                                     then bm_single_L(k;v;m1;m2)
                                                                     else bm_double_L(k;v;m1;m2)
                                                                     fi )));key1,value1,cnt1,left1,right1.
                  binary_map_case(m2;binary_map_case(left1;binary_map_case(right1;bm_T(k;v;2;m1;bm_E());
                                                                           key1r,value1r,cnt1r,left1r,right1r.
                                                                           bm_double_R(k;v;m1;m2));
                                                     key1l,value1l,cnt1l,left1l,right1l.
                                                     binary_map_case(right1;bm_single_R(k;v;m1;m2);
                                                                     key1r,value1r,cnt1r,left1r,right1r.
                                                                     if cnt1r <z cnt1l
                                                                     then bm_single_R(k;v;m1;m2)
                                                                     else bm_double_R(k;v;m1;m2)
                                                                     fi ));key2,value2,cnt2,left2,right2.
                                  if bm_wt(cnt1) ≤z cnt2
                                    then if bm_numItems(left2) <z bm_numItems(right2)
                                         then bm_single_L(k;v;m1;m2)
                                         else bm_double_L(k;v;m1;m2)
                                         fi 
                                  if bm_wt(cnt2) ≤z cnt1
                                    then if bm_numItems(right1) <z bm_numItems(left1)
                                         then bm_single_R(k;v;m1;m2)
                                         else bm_double_R(k;v;m1;m2)
                                         fi 
                                  else bm_T(k;v;cnt1 + cnt2 + 1;m1;m2)
                                  fi ))


Definitions occuring in Statement :  bm_double_R: bm_double_R(c;cv;m;z),  bm_double_L: bm_double_L(a;av;w;m),  bm_single_R: bm_single_R(b;bv;m;z),  bm_single_L: bm_single_L(a;av;x;m),  bm_numItems: bm_numItems(m),  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(),  bm_wt: bm_wt(i),  le_int: i ≤z j,  ifthenelse: if b then t else f fi ,  lt_int: i <z j,  add: n + m,  natural_number: $n
FDL editor aliases :  bm_T'
bm\_T'(k;v;m1;m2)  ==
    binary\_map\_case(m1;
                                    binary\_map\_case(m2;bm\_T(k;v;1;bm\_E();bm\_E());key2,value2,cnt2,left2,right2.
                                                                    binary\_map\_case(left2;
                                                                                                    ...;key2l,value2l,cnt2l,left2l,right2l.
                                                                                                    ...));key1,value1,cnt1,left1,right1.
                                    binary\_map\_case(m2;
                                                                    binary\_map\_case(left1;
                                                                                                    ...;key1l,value1l,cnt1l,left1l,right1l.
                                                                                                    ...);key2,value2,cnt2,left2,right2.
                                                                    if  bm\_wt(cnt1)  \mleq{}z  cnt2
                                                                        then  if  bm\_numItems(left2)  <z  bm\_numItems(right2)
                                                                                  then  bm\_single\_L(k;v;m1;m2)
                                                                                  else  bm\_double\_L(k;v;m1;m2)
                                                                                  fi 
                                                                    if  bm\_wt(cnt2)  \mleq{}z  cnt1
                                                                        then  if  bm\_numItems(right1)  <z  bm\_numItems(left1)
                                                                                  then  bm\_single\_R(k;v;m1;m2)
                                                                                  else  bm\_double\_R(k;v;m1;m2)
                                                                                  fi 
                                                                    else  bm\_T(k;v;cnt1  +  cnt2  +  1;m1;m2)
                                                                    fi  ))


Date html generated: 2015_07_17-AM-08_19_04
Last ObjectModification: 2012_08_21-PM-06_34_08

Home Index