fact: Definition seq_num_input_handlers (h : name) (inp : input) (state : seq_num_data) : (list output) * seq_num_data * list (name * seq_num_msg) := let '(out, data', pkts) := input_handlers h inp (tdData state) in let (n', tpkts) := processPackets (tdNum state) pkts in (out, mkseq_num_data n' (tdSeen state) data', tpkts).
imports: Verdi(Verdi)