fact: Definition seq_num_net_handlers (dst : name) (src : name) (m : seq_num_msg) (state : seq_num_data) : list output * seq_num_data * list (name * seq_num_msg) := let seen_src := assoc_default name_eq_dec (tdSeen state) src [] in if member (tmNum m) seen_src then ([], state, []) else let '(out, data', pkts) := net_handlers dst src (tmMsg m) (tdData state) in let (n', tpkts) := processPackets (tdNum state) pkts in (out, mkseq_num_data n' (assoc_set name_eq_dec (tdSeen state) src (tmNum m :: seen_src)) data', tpkts).
imports: Verdi(Verdi)