proposition: Corollary step_ordered_failure_pt_mapped_simulation_star_1 : forall net failed tr, @step_ordered_failure_star _ _ overlay_fst fail_msg_fst step_ordered_failure_init (failed, net) tr -> @step_ordered_failure_star _ _ overlay_snd fail_msg_snd step_ordered_failure_init (map tot_map_name failed, pt_map_onet net) (filterMap pt_map_trace_ev tr).
proof: Proof. Proof using overlay_map_congr name_map_bijective multi_map_congr fail_msg_map_congr. move => net failed tr H_step. remember step_ordered_failure_init as y in *. have H_eq_f: failed = fst (failed, net) by []. have H_eq_n: net = snd (failed, net) by []. rewrite H_eq_f {H_eq_f}. rewrite {2}H_eq_n {H_eq_n}. move: Heqy. induction H_step using refl_trans_1n_trace_n1_ind => H_init /=. rewrite H_init. rewrite /step_ordered_failure_init /= /pt_map_onet /=. rewrite -pt_init_handlers_fun_eq. exact: RT1nTBase. concludes. rewrite H_init {H_init x} in H_step2 H_step1. case: x' H IHH_step1 H_step1 => failed' net'. case: x'' H_step2 => failed'' net''. rewrite /=. move => H_step2 H IHH_step1 H_step1. apply step_ordered_failure_pt_mapped_simulation_1 in H. rewrite filterMap_app. case: H => H. have H_trans := refl_trans_1n_trace_trans IHH_step1. apply: H_trans. rewrite -(app_nil_r (filterMap pt_map_trace_ev _)). apply: (@RT1nTStep _ _ _ _ (map tot_map_name failed'', pt_map_onet net'')) => //. exact: RT1nTBase. move: H => [H_eq_n [H_eq_f H_eq]]. by rewrite H_eq_n -H_eq_f H_eq app_nil_r. Qed.
imports: Verdi(Verdi DynamicNetLemmas TotalMapSimulations) Coq(FunctionalExtensionality) Coq(Sumbool Sorting.Permutation) Verdi(DynamicNetLemmas) Verdi(Ssrexport)