Function lemma_encode_decode_bmp_string 

pub proof fn lemma_encode_decode_bmp_string(bytes: Seq<u8>)

requires

is_valid_bmp_string(bytes),

ensures

encode_bmp_string(decode_bmp_string(bytes)) == bytes,