proposition: Theorem step_ordered_failure_tot_one_mapped_simulation_1 : step_ordered_failure_tot_s_net_handlers_eq -> forall net net' failed failed' tr tr', step_ordered_failure_star step_ordered_failure_init (failed, net) tr -> step_ordered_failure (failed, net) (failed', net') tr' -> net.(onwState) me = net'.(onwState) me \/ exists tr'', @step_s _ single (tot_s_map_data (net.(onwState) me)) (tot_s_map_data (net'.(onwState) me)) tr''.
proof: Proof. Proof using map_congr. move => H_net_eq net net' failed failed' tr tr' H_star H_step. invcs H_step. - rewrite /update. break_if; last by left. right. subst_max. destruct (input_handler (tot_s_map_msg me from m) (tot_s_map_data (onwState net me))) eqn:?. have H_eq := H_net_eq _ _ _ _ _ _ _ _ _ _ _ H_star H3 H4 H5 Heqp. break_and. exists (inl (tot_s_map_msg me from m) :: (map inr l0)). apply: SST_deliver => //=. by rewrite Heqp H0. - rewrite /update. break_if; last by left. right. subst_max. destruct (input_handler (tot_s_map_input me inp) (tot_s_map_data (onwState net me))) eqn:?. have H_eq_inp := @tot_s_input_handlers_eq _ _ _ _ _ _ map_congr _ _ _ _ _ _ _ H4 Heqp. break_and. exists (inl (tot_s_map_input me inp) :: map inr l0). apply: SST_deliver => //=. by rewrite Heqp H0. - by left. Qed.
imports: Verdi(Verdi DynamicNetLemmas) Verdi(Ssrexport)