proposition: Corollary step_failure_pt_mapped_simulation_star_1 : forall net failed tr, @step_failure_star _ _ fail_fst step_failure_init (failed, net) tr -> exists tr', @step_failure_star _ _ fail_snd step_failure_init (map tot_map_name failed, pt_map_net net) tr' /\ filterMap trace_non_empty_out (filterMap pt_map_trace_occ tr) = filterMap trace_non_empty_out tr'.
proof: Proof. Proof using name_map_bijective multi_map_congr fail_map_congr. move => net failed tr H_step. remember step_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_failure_init /= /pt_map_net /=. rewrite -pt_init_handlers_fun_eq. exists []. split => //. 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_failure_pt_mapped_simulation_1 in H. case: H => H. move: IHH_step1 => [tr' [H_star H_eq_tr]]. exists (tr' ++ filterMap pt_map_trace_occ tr2). split. * have H_trans := refl_trans_1n_trace_trans H_star. apply: H_trans. rewrite -(app_nil_r (filterMap pt_map_trace_occ _)). apply: (@RT1nTStep _ _ _ _ (map tot_map_name failed'', pt_map_net net'')) => //. exact: RT1nTBase. * by rewrite 3!filterMap_app H_eq_tr. move: H => [H_eq_n [H_eq_f H_eq]]. rewrite H_eq_n -H_eq_f. move: IHH_step1 => [tr' [H_star H_tr]]. exists tr'. split => //. rewrite 2!filterMap_app. by rewrite H_eq app_nil_r. Qed.
imports: Verdi(Verdi DynamicNetLemmas TotalMapSimulations) Coq(FunctionalExtensionality) Coq(Sumbool Sorting.Permutation) Verdi(DynamicNetLemmas) Verdi(Ssrexport)