add postcondition for normal cases
remove old file
rename Bitstream predicates
fix old include
rename files and function and adapt proofs
use shorter  predicate names for Bitstream