proposition: Lemma pt_map_onet_tot_map_labeled_event_inf_often_enabled : forall l, tot_map_label l <> label_silent -> forall s, lb_step_execution lb_step_ordered_failure s -> strong_fairness lb_step_ordered_failure label_silent s -> inf_often (now (enabled lb_step_ordered_failure (tot_map_label l))) (map pt_map_onet_event s) -> inf_often (now (enabled lb_step_ordered_failure l)) s.
proof: Proof. Proof using lb_step_ordered_failure_strong_fairness_enabled_pt_map_onet_eventually. move => l H_neq s H_exec H_fair. have H_a: ((lb_step_execution lb_step_ordered_failure) /\_ (strong_fairness lb_step_ordered_failure label_silent)) s by auto. move: H_a {H_exec H_fair}. apply: always_map_conv_ext => {s}. rewrite /and_tl /=. move => x s0 [H_e H_w]. apply lb_step_execution_invar in H_e. by apply strong_fairness_invar in H_w. apply: eventually_map_conv_ext. - exact: extensional_now. - exact: extensional_now. - apply extensional_and_tl. * exact: lb_step_execution_extensional. * exact: strong_fairness_extensional. - rewrite /and_tl /=. move => x s [H_e H_w]. apply lb_step_execution_invar in H_e. by apply strong_fairness_invar in H_w. - rewrite /and_tl. case => /= x s [H_a H_w] H_en. exact: lb_step_ordered_failure_strong_fairness_enabled_pt_map_onet_eventually. Qed.
imports: Verdi(Verdi LabeledNet) Verdi(TotalMapSimulations PartialMapSimulations) Verdi(TotalMapExecutionSimulations) InfSeqExt(infseq map exteq) Coq(FunctionalExtensionality) Verdi(Ssrexport) Coq(ssrbool)