Function generalized_mainend 

pub exec fn generalized_mainend(bytes: &[u8], zone_start: usize) -> usize

requires

generalized_time_bytes_wf::<false>(bytes@),

zone_start == generalized_zone_start(bytes@),

returns

generalized_main_end(bytes@, zone_start),

Verified executable implementation of generalized_main_end.