proposition: Lemma pt_map_odnet_tot_map_labeled_event_state_continuously_enabled : forall l, tot_map_label l <> label_silent -> forall s, lb_step_execution lb_step_ordered_dynamic_failure s -> weak_fairness lb_step_ordered_dynamic_failure label_silent s -> continuously (now (enabled lb_step_ordered_dynamic_failure (tot_map_label l))) (map pt_map_odnet_event s) -> continuously (now (enabled lb_step_ordered_dynamic_failure l)) s.
proof: Proof. Proof using lb_step_ordered_dynamic_failure_weak_fairness_always_enabled_pt_map_onet_continuously. move => l H_neq s H_exec H_fair. have H_a: ((lb_step_execution lb_step_ordered_dynamic_failure) /\_ (weak_fairness lb_step_ordered_dynamic_failure label_silent)) s by auto. move: H_a {H_exec H_fair}. apply: eventually_map_conv_ext => {s}. - apply extensional_always. exact: extensional_now. - apply extensional_always. exact: extensional_now. - apply extensional_and_tl. * exact: lb_step_execution_extensional. * exact: weak_fairness_extensional. - rewrite /and_tl /=. move => x s [H_e H_w]. apply lb_step_execution_invar in H_e. by apply weak_fairness_invar in H_w. - case => x s [H_a H_w] H_al. simpl in *. exact: lb_step_ordered_dynamic_failure_weak_fairness_always_enabled_pt_map_onet_continuously. Qed.
imports: Verdi(Verdi LabeledNet) Verdi(TotalMapSimulations PartialMapSimulations) Verdi(TotalMapExecutionSimulations) InfSeqExt(infseq map exteq) Coq(FunctionalExtensionality) Verdi(Ssrexport) Coq(ssrbool)