Skip to main content

lemma_decode_encode_universal_string

vest_lib::asn1::universalstring

Function lemma_decode_encode_universal_string 

Source 
pub proof fn lemma_decode_encode_universal_string(chars: Seq<char>)
Expand description
ensures
decode_universal_string(encode_universal_string(chars)) == chars,