proposition: Lemma step_ordered_failure_serialize_simulation_star : forall net failed tr, @step_ordered_failure_star _ _ orig_name_overlay_params orig_fail_msg_params step_ordered_failure_init (failed, net) tr -> @step_ordered_failure_star _ _ serialized_name_overlay_params serialized_fail_msg_params step_ordered_failure_init (failed, serialize_onet net) tr.
proof: Proof. Proof using. move => net failed tr H_st. have ->: failed = map (@tot_map_name _ _ _ _ orig_multi_params_name_tot_map) failed by rewrite /tot_map_name /= map_id. have ->: tr = map (@tot_map_trace _ _ _ _ _ orig_multi_params_name_tot_map) tr. rewrite /tot_map_trace /= /id /= {H_st}. elim: tr => //=. by case => a; case => [i|o] l IH; rewrite -IH. exact: step_ordered_failure_tot_mapped_simulation_star_1. Qed.
imports: StructTact(Util) Verdi(Verdi) Coq(FunctionalExtensionality) Verdi(TotalMapSimulations PartialMapSimulations) Cheerios(Cheerios) Verdi(SerializedMsgParams) Verdi(Ssrexport)