Function lemma_decoded_bmp_string_valid 

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

requires

is_valid_bmp_string(bytes),

ensures

is_valid_bmp_chars(decode_bmp_string(bytes)),