Function generalized_time_len 

pub open spec fn generalized_time_len(value: GeneralizedTimeSpec) -> nat

{
    10 as nat + if value.precision == TimePrecision::Hour { 0 as nat } else { 2 as nat }
        + if value.precision == TimePrecision::Second { 2 as nat } else { 0 as nat }
        + if value.fraction.len() == 0 { 0 as nat } else { 1 + value.fraction.len() }
        + if value.zone == TimeZone::Utc { 1 as nat } else { 0 as nat }
}