proposition: Lemma step_ordered_dynamic_failure_tot_one_mapped_simulation_star_1 : step_ordered_dynamic_failure_tot_s_net_handlers_eq -> forall net failed tr, step_ordered_dynamic_failure_star step_ordered_dynamic_failure_init (failed, net) tr -> forall d, net.(odnwState) me = Some d -> exists tr', @step_s_star _ single init_handler (tot_s_map_data d) tr'.
proof: Proof. Proof using map_congr. move => H_net_eq net failed tr H_st. have ->: net = snd (failed, net) by []. remember step_ordered_dynamic_failure_init as y in H_st. move: Heqy. induction H_st using refl_trans_1n_trace_n1_ind => /= H_init; first by rewrite H_init. concludes. rewrite H_init {H_init x} in H_st1 H_st2. case: x' H IHH_st1 H_st1 => failed' net'. case: x'' H_st2 => failed'' net''. rewrite /=. move => H_step2 H IHH_step1 H_step1 d H_eq. case H_eq': (odnwState net' me) => [d'|]; last first. exists []. have H_eq_i := step_ordered_dynamic_failure_tot_one_mapped_simulation_1_init H H_eq' H_eq. rewrite H_eq_i. exact: RT1nTBase. have [tr' H_star] := IHH_step1 _ H_eq'. have H_st := step_ordered_dynamic_failure_tot_one_mapped_simulation_1 H_net_eq H_step1 H H_eq' H_eq. case: H_st => H_st; first by rewrite -H_st; exists tr'. have [tr'' H_st'] := H_st. exists (tr' ++ tr''). apply: (refl_trans_1n_trace_trans H_star). have ->: tr'' = tr'' ++ [] by rewrite app_nil_r. apply RT1nTStep with (x' := (tot_s_map_data d)) => //. exact: RT1nTBase. Qed.
imports: Verdi(Verdi DynamicNetLemmas) Verdi(Ssrexport)