Function is_valid_numeric_string 

pub open spec fn is_valid_numeric_string(chars: Seq<char>) -> bool

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