Function der_real_special_wf 

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

{
    bytes.len() == 1
        && (bytes[0] == REAL_PLUS_INFINITY || bytes[0] == REAL_MINUS_INFINITY
            || bytes[0] == REAL_NOT_A_NUMBER || bytes[0] == REAL_MINUS_ZERO)
}