Function der_real_bytes_wf 

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

{
    ||| bytes.len() == 0
    ||| der_real_special_wf(bytes)
    ||| der_real_binary_wf(bytes)
    ||| der_real_decimal_wf(bytes)

}

Complete canonical DER predicate for REAL contents octets.