Function generalized_main_end 

pub open spec fn generalized_main_end(bytes: Seq<u8>, zone_start: usize) -> usize

{
    if generalized_candidate_wf::<false>(bytes, 10, zone_start) {
        10
    } else if generalized_candidate_wf::<false>(bytes, 12, zone_start) {
        12
    } else {
        14
    }
}

Spec function identifying the end index of the main date-time prefix (YYYYMMDDhh[mm[ss]]).