Function ber_real_decimal_nr3_wf 

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

{
    match ber_real_decimal_significand(bytes) {
        Some((before, mark, after, end)) => {
            if end < bytes.len() && exponent_mark(bytes[end as int]) {
                let exponent_sign = end + 1;
                let exponent = exponent_sign + 1;
                let exponent_end = scan_ascii_digits(bytes, exponent);
                &&& exponent_sign < bytes.len()
                &&& (bytes[exponent_sign as int] == ASCII_PLUS
                    || bytes[exponent_sign as int] == ASCII_MINUS)
                &&& exponent < exponent_end
                &&& exponent_end == bytes.len()
                &&& ber_real_decimal_mantissa_nonzero(bytes, before, mark, after, end)

            } else {
                false
            }
        }
        None => false,
    }
}