proposition: Theorem step_async_tot_mapped_simulation_1 : forall net net' tr, @step_async _ multi_fst net net' tr -> @step_async _ multi_snd (tot_map_net net) (tot_map_net net') (map tot_map_trace_occ tr).
proof: Proof. Proof using name_map_bijective multi_map_congr. move => net net' tr. case => {net net' tr}. - move => net net' p ms ms' out d l H_eq H_hnd H_eq'. rewrite /tot_map_trace_occ /=. have ->: tot_map_name (pDst p) = pDst (tot_map_packet p) by case: p H_eq H_hnd H_eq' => src dst m H_eq H_hnd H_eq'. apply (@StepAsync_deliver _ _ _ _ _ (map tot_map_packet ms) (map tot_map_packet ms') (map tot_map_output out) (tot_map_data d) (tot_map_name_msgs l)). * by rewrite /tot_map_net /= H_eq /= map_app. * rewrite /=. case: p H_eq H_hnd H_eq' => /= src dst m H_eq H_hnd H_eq'. have H_q := tot_net_handlers_eq dst src m (nwState net dst). rewrite /tot_mapped_net_handlers in H_q. rewrite H_hnd in H_q. rewrite H_q. by rewrite tot_map_name_inv_inverse. * rewrite /= H_eq' /= /tot_map_net /=. rewrite -tot_map_update_packet_eq. rewrite 2!map_app. destruct p. by rewrite tot_map_packet_map_eq. - move => h net net' out inp d l H_hnd H_eq. apply (@StepAsync_input _ _ _ _ _ _ _ (tot_map_data d) (tot_map_name_msgs l)). rewrite /=. have H_q := tot_input_handlers_eq h inp (nwState net h). rewrite /tot_mapped_input_handlers /= in H_q. rewrite H_hnd in H_q. rewrite H_q. by rewrite tot_map_name_inv_inverse. rewrite /= H_eq /= /tot_map_net /=. by rewrite -tot_map_update_eq map_app tot_map_packet_map_eq. Qed.
imports: Verdi(Verdi DynamicNetLemmas) Coq(FunctionalExtensionality) Coq(Sorting.Permutation Sumbool) Verdi(Ssrexport)