reformulate post condition to be similar of _Write
remove LeftBitInSequence predicate