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);
    }