proposition: Theorem step_ordered_failure_tot_mapped_simulation_1 : forall net net' failed failed' tr, @step_ordered_failure _ _ overlay_fst fail_msg_fst (failed, net) (failed', net') tr -> @step_ordered_failure _ _ overlay_snd fail_msg_snd (map tot_map_name failed, tot_map_onet net) (map tot_map_name failed', tot_map_onet net') (map tot_map_trace tr).
proof: Proof. Proof using overlay_map_congr name_map_bijective multi_map_congr fail_msg_map_congr. move => net net' failed failed' tr H_step. invcs H_step. - rewrite /tot_map_onet /=. apply (@StepOrderedFailure_deliver _ _ _ _ _ _ _ _ (tot_map_msg m) (map tot_map_msg ms) (map tot_map_output out) (tot_map_data d) (tot_map_name_msgs l) (tot_map_name from) (tot_map_name to)). * by rewrite /tot_map_net /= 2!tot_map_name_inv_inverse /= H3. * exact: not_in_failed_not_in. * rewrite /= tot_map_name_inv_inverse -tot_net_handlers_eq /tot_mapped_net_handlers /=. repeat break_let. by find_inversion. * by rewrite /= tot_map_update_eq collate_tot_map_update2_eq. * by rewrite map_tot_map_trace_eq. - rewrite /tot_map_onet /=. apply (@StepOrderedFailure_input _ _ _ _ (tot_map_name h) _ _ _ _ (map tot_map_output out) (tot_map_input inp) (tot_map_data d) (tot_map_name_msgs l)). * exact: not_in_failed_not_in. * rewrite /= tot_map_name_inv_inverse -tot_input_handlers_eq /tot_mapped_input_handlers. repeat break_let. by find_inversion. * by rewrite /= /tot_map_onet /= tot_map_update_eq collate_tot_map_eq. * by rewrite map_tot_map_trace_eq. - rewrite /tot_map_onet /=. set l := map2snd _ _. have H_nd: NoDup (map fst (tot_map_name_msgs l)). rewrite /tot_map_name_msgs /=. rewrite /l {l} /=. eapply NoDup_map_snd_fst. apply (@nodup_tot_map msg_fail); first exact: in_map2snd_snd. apply NoDup_map2snd. apply NoDup_remove_all. exact: no_dup_nodes. move => nm nm' H_in H_in'. have H_fail := tot_map_in_snd _ _ _ _ H_in. have H_fail' := tot_map_in_snd _ _ _ _ H_in'. by rewrite H_fail H_fail'. have H_pm := map_msg_fail_eq h failed. have H_eq := NoDup_Permutation_collate_eq _ _ name_eq_dec _ _ _ _ H_nd H_pm. rewrite /l /tot_map_name_msgs in H_eq. apply: StepOrderedFailure_fail. * exact: not_in_failed_not_in. * rewrite /=. rewrite /l collate_tot_map_eq /tot_map_name_msgs. by rewrite H_eq. Qed.
imports: Verdi(Verdi DynamicNetLemmas) Coq(FunctionalExtensionality) Coq(Sorting.Permutation Sumbool) Verdi(Ssrexport)