Skip to main content

lemma_encode_utf8_len_strictly_monotonic

vstd::utf8

Function lemma_encode_utf8_len_strictly_monotonic 

Source 
pub proof fn lemma_encode_utf8_len_strictly_monotonic(s: Seq<char>, i: int, j: int)
Expand description
requires
0 <= i < j <= s.len(),
ensures
encode_utf8(s.subrange(0, i)).len() < encode_utf8(s.subrange(0, j)).len(),

Growing a prefix by at least one char strictly increases its encoded byte length.