fun ddest(outnum,value) { rmap_write(outnum,value?cast(unsigned[64])?bits(32,63),inum); rmap_write(outnum+1,value?cast(unsigned[64])?bits(32),inum); }