proposition: Corollary step_ordered_dynamic_failure_pt_mapped_simulation_star_1 : forall net failed tr, @step_ordered_dynamic_failure_star _ _ overlay_fst new_msg_fst fail_msg_fst step_ordered_dynamic_failure_init (failed, net) tr -> @step_ordered_dynamic_failure_star _ _ overlay_snd new_msg_snd fail_msg_snd step_ordered_dynamic_failure_init (map tot_map_name failed, pt_map_odnet net) (filterMap pt_map_trace_ev tr).
proof: Proof. Proof using overlay_map_congr new_msg_map_congr name_map_bijective multi_map_congr fail_msg_map_congr. move => net failed tr H_step. remember step_ordered_dynamic_failure_init as y in *. change failed with (fst (failed, net)). change net with (snd (failed, net)) at 2. move: Heqy. induction H_step using refl_trans_1n_trace_n1_ind => H_init /=. rewrite H_init /step_ordered_dynamic_failure_init /= /step_ordered_failure_init. exact: RT1nTBase. concludes. repeat find_rewrite. destruct x'. destruct x''. rewrite /=. find_apply_lem_hyp step_ordered_dynamic_failure_pt_mapped_simulation_1; last by move: H_step1; apply: ordered_dynamic_nodes_no_dup. simpl in *. 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 l0, pt_map_odnet o0)) => //. 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)