Function oid_from_subidentifiers 

pub open spec fn oid_from_subidentifiers(
    first_subidentifier: UInt,
    rest: Seq<UInt>,
) -> ObjectIdentifierSpec

{
    if first_subidentifier < 40 {
        ObjectIdentifierSpec {
            first: 0,
            second: first_subidentifier,
            rest,
        }
    } else if first_subidentifier < 80 {
        ObjectIdentifierSpec {
            first: 1,
            second: (first_subidentifier - 40u64) as UInt,
            rest,
        }
    } else {
        ObjectIdentifierSpec {
            first: 2,
            second: (first_subidentifier - 80u64) as UInt,
            rest,
        }
    }
}