fact: Definition step_ordered_dynamic_failure_tot_s_net_handlers_eq := forall net failed tr src m ms d out st' ps out' st'', step_ordered_dynamic_failure_star step_ordered_dynamic_failure_init (failed, net) tr -> odnwPackets net src me = m :: ms -> ~ In me failed -> odnwState net me = Some d -> net_handlers me src m d = (out, st', ps) -> input_handler (tot_s_map_msg me src m) (tot_s_map_data d) = (out', st'') -> map tot_s_map_output out = out' /\ tot_s_map_data st' = st''.
imports: Verdi(Verdi DynamicNetLemmas) Verdi(Ssrexport)