Function is_valid_printable_string_spec 

pub open spec fn is_valid_printable_string_spec(bytes: Seq<u8>) -> bool

{ forall |i: int| 0 <= i < bytes.len() ==> is_printable_byte(#[trigger] bytes[i]) }