Function oid_first_subidentifier 

pub open spec fn oid_first_subidentifier(v: ObjectIdentifierSpec) -> UInt

{
    if !v.wf() {
        0
    } else if v.first < 2 {
        (v.first * 40 + v.second) as UInt
    } else {
        (80 + v.second) as UInt
    }
}