pub broadcast proof fn is_ascii_concat(s1: &str, s2: &str, s3: &str)Expand description
requires
s1@ =~= s2@ + s3@,is_ascii(s1) <==> is_ascii(s2) && is_ascii(s3),