proposition: Corollary step_async_pt_mapped_simulation_star_1 : forall net tr, @step_async_star _ multi_fst step_async_init net tr -> exists tr', @step_async_star _ multi_snd step_async_init (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. move => net tr H_step. remember step_async_init as y in *. move: Heqy. induction H_step using refl_trans_1n_trace_n1_ind => H_init /=. rewrite H_init. rewrite /step_async_init /= /pt_map_net /=. rewrite pt_init_handlers_fun_eq. exists []. split => //. exact: RT1nTBase. concludes. rewrite H_init in H_step2 H_step1. apply step_async_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 _ _ _ _ (pt_map_net x'')) => //. exact: RT1nTBase. * by rewrite 2!filterMap_app H_eq_tr filterMap_app. move: H => [H_eq H_eq']. rewrite H_eq. 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)