proposition: Lemma step_ordered_dynamic_failure_star_lb_step_reachable : step_star_lb_step_reachable lb_step_ordered_dynamic_failure step_ordered_dynamic_failure step_ordered_dynamic_failure_init.
proof: Proof. Proof using. rewrite /step_star_lb_step_reachable. case => failed net l. case => failed' net' tr tr' H_star H_st. invcs H_st. - set net' := {| odnwNodes := _ ; odnwPackets := _ ; odnwState := _ |}. apply (@refl_trans_1n_trace_trans _ _ _ _ (failed', net)) => //. rewrite -(app_nil_r (map2fst _ _)). apply: (@RT1nTStep _ _ _ _ (failed', net')); last exact: RT1nTBase. apply: (StepOrderedDynamicFailure_deliver _ _ _ _ _ H5 H6) => //. rewrite /net_handlers /= /unlabeled_net_handlers /=. repeat break_let. by tuple_inversion. - set net' := {| odnwNodes := _ ; odnwPackets := _ ; odnwState := _ |}. apply (@refl_trans_1n_trace_trans _ _ _ _ (failed', net)) => //. rewrite -(app_nil_r (_ :: _)). apply: (@RT1nTStep _ _ _ _ (failed', net')); last exact: RT1nTBase. apply: (StepOrderedDynamicFailure_input _ _ _ _ H5) => //. rewrite /input_handlers /= /unlabeled_input_handlers /=. repeat break_let. by tuple_inversion. - by have ->: tr' ++ [] = tr' by auto with datatypes. Qed.
imports: Verdi(Verdi) InfSeqExt(infseq exteq) Verdi(Ssrexport)