Function ber_real_bytes_wf 

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

{
    ||| bytes.len() == 0
    ||| der_real_special_wf(bytes)
    ||| ber_real_binary_wf(bytes)
    ||| ber_real_decimal_wf(bytes)

}

Complete BER predicate for REAL contents octets.