make Bit8 function non-inline
make Bit64 non-inline
change bitposition -> bitpos
remove unnecessary use of \old
add predicate NormalBitsequence
add more precise assigns clauses