Function lemma_decode_encode_bmp_string 

pub proof fn lemma_decode_encode_bmp_string(chars: Seq<char>)

requires

is_valid_bmp_chars(chars),

ensures

decode_bmp_string(encode_bmp_string(chars)) == chars,