proposition: Lemma step_ordered_dynamic_failure_deserialized_simulation : forall net net' failed failed' tr, NoDup (odnwNodes net) -> @step_ordered_dynamic_failure _ _ serialized_name_overlay_params serialized_new_msg_params serialized_fail_msg_params (failed, net) (failed', net') tr -> @step_ordered_dynamic_failure _ _ orig_name_overlay_params orig_new_msg_params orig_fail_msg_params (failed, deserialize_odnet net) (failed', deserialize_odnet net') tr \/ deserialize_odnet net = deserialize_odnet net' /\ failed = failed' /\ tr = [].
proof: Proof. Proof using. move => net net' failed failed' tr H_nd H_st. eapply step_ordered_dynamic_failure_pt_mapped_simulation_1 in H_st; last by []. case: H_st => H_st. have H_eq_n: failed = map (@tot_map_name _ _ _ _ multi_params_orig_name_tot_map) failed by rewrite /tot_map_name /= map_id. rewrite {1}H_eq_n. have H_eq_n': failed' = map (@tot_map_name _ _ _ _ multi_params_orig_name_tot_map) failed' by rewrite /tot_map_name /= map_id. rewrite {1}H_eq_n'. left. rewrite -2!pt_map_odnet_deserialize_odnet. have ->: tr = filterMap (@pt_map_trace_ev _ _ _ _ _ orig_multi_params_name_tot_map) tr. rewrite /pt_map_trace_ev /= /id. clear. elim: tr => //=. case => a; case => b l IH; first by rewrite -IH. by rewrite -IH. exact: H_st. right. move: H_st => [H_eq_net [H_eq_f H_eq_tr]]. split; first by rewrite -2!pt_map_odnet_deserialize_odnet. split => //. move: H_eq_tr. rewrite /pt_map_trace_ev /= /id. set f := fun _ => _. clear. elim => //=. elim: tr => //=. case => n; case => /= [i|o] l IH. * by rewrite -IH. * by rewrite -IH. Qed.
imports: StructTact(Util) Verdi(Verdi) Coq(FunctionalExtensionality) Verdi(TotalMapSimulations PartialMapSimulations) Cheerios(Cheerios) Verdi(SerializedMsgParams) Verdi(Ssrexport)