Function ber_real_decimal_nr1_wf 

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

{
    let start = after_optional_sign(bytes, skip_ascii_spaces(bytes, 1));
    let end = scan_ascii_digits(bytes, start);
    &&& start < end
    &&& end == bytes.len()
    &&& ascii_digits_have_nonzero(bytes, start as int, end as int)

}