proposition: Lemma lb_step_execution_lb_step_ordered_failure_pt_map_onet_infseq : forall s, lb_step_execution lb_step_ordered_failure s -> lb_step_execution lb_step_ordered_failure (map pt_map_onet_event s).
proof: Proof. Proof using name_map_bijective multi_map_lb_congr multi_map_congr label_eq_dec. cofix c. move => s H_exec. rewrite -pt_map_onet_event_Map_unfold {1}/pt_map_onet_event /=. inversion H_exec; subst => /=. rewrite -pt_map_onet_event_Map_unfold /= /pt_map_onet_event /=. case (label_eq_dec (tot_map_label (evt_l e)) label_silent) => H_eq. apply: Cons_lb_step_exec. - rewrite H_eq. destruct e, e'. destruct evt_a, evt_a0. simpl in *. by eapply lb_step_ordered_failure_pt_mapped_simulation_1_silent; eauto. - destruct e, e'. destruct evt_a, evt_a0. apply (lb_step_ordered_failure_pt_mapped_simulation_1_silent H_eq) in H. break_and. simpl in *. rewrite H0 filterMap_app. by aggressive_rewrite_goal. - pose s' := Cons e' s0. rewrite (pt_map_onet_event_Map_unfold s'). exact: c. apply: Cons_lb_step_exec => /=. - destruct e, e'. destruct evt_a, evt_a0. simpl in *. by eapply lb_step_ordered_failure_pt_mapped_simulation_1_non_silent; eauto. - by rewrite H0 filterMap_app. - pose s' := Cons e' s0. rewrite (pt_map_onet_event_Map_unfold s'). exact: c. Qed.
imports: Verdi(Verdi LabeledNet) Verdi(TotalMapSimulations PartialMapSimulations) Verdi(TotalMapExecutionSimulations) InfSeqExt(infseq map exteq) Coq(FunctionalExtensionality) Verdi(Ssrexport) Coq(ssrbool)