proposition: Theorem step_ordered_dynamic_failure_tot_one_mapped_simulation_1 : step_ordered_dynamic_failure_tot_s_net_handlers_eq -> forall net net' failed failed' tr tr', step_ordered_dynamic_failure_star step_ordered_dynamic_failure_init (failed, net) tr -> step_ordered_dynamic_failure (failed, net) (failed', net') tr' -> forall d, net.(odnwState) me = Some d -> forall d', net'.(odnwState) me = Some d' -> d = d' \/ exists tr'', @step_s _ single (tot_s_map_data d) (tot_s_map_data d') tr''.
proof: Proof. Proof using map_congr. move => H_net_eq net net' failed failed' tr tr' H_star H_step d H_eq d' H_eq'. invcs H_step. - left. have H_neq: h <> me. move => H_n. rewrite -H_n in H_eq. have H_eq_n := ordered_dynamic_uninitialized_state H_star _ H4. by congruence. move: H_eq'. rewrite /update. break_if; first by find_rewrite. by congruence. - move: H_eq'. rewrite /update. break_if => H_eq'; last by left; congruence. right. find_injection. rewrite H_eq in H5. find_injection. destruct (input_handler (tot_s_map_msg me from m) (tot_s_map_data d0)) eqn:?. have H_eq_st := H_net_eq _ _ _ _ _ _ _ _ _ _ _ _ H_star H6 H3 H_eq H7 Heqp. break_and. exists (inl (tot_s_map_msg me from m) :: (map inr l0)). apply: SST_deliver => //=. by rewrite Heqp H0. - move: H_eq'. rewrite /update. break_if => H_eq'; last by left; rewrite H_eq in H_eq'; find_injection. right. find_injection. rewrite H_eq in H5. find_injection. destruct (input_handler (tot_s_map_input me inp) (tot_s_map_data d0)) eqn:?. have H_eq_inp := @tot_s_input_handlers_eq _ _ _ _ _ _ map_congr _ _ _ _ _ _ _ H6 Heqp. break_and. exists (inl (tot_s_map_input me inp) :: map inr l0). apply: SST_deliver => //=. by rewrite Heqp H0. - left. find_rewrite. by find_injection. Qed.
imports: Verdi(Verdi DynamicNetLemmas) Verdi(Ssrexport)