is_ascii_chars_concat

vstd::utf8

Function is_ascii_chars_concat 

Source 
pub broadcast proof fn is_ascii_chars_concat(c1: Seq<char>, c2: Seq<char>, c3: Seq<char>)
Expand description
requires
c1 =~= c2 + c3,
ensures
is_ascii_chars(c1) <==> is_ascii_chars(c2) && is_ascii_chars(c3),

Ensures that an ASCII character sequence is formed by the concatenation of two ASCII character sequences.