proposition: Lemma backup_plus_network_eq_primary : forall net tr, step_async_star (params := Counter_MultiParams) step_async_init net tr -> nwState net backup + inc_in_flight_to_backup (nwPackets net) = nwState net primary.
proof: Proof. intros. remember step_async_init as y in *. revert Heqy. induction H using refl_trans_1n_trace_n1_ind; intros; subst. - reflexivity. - concludes. match goal with | [ H : step_async _ _ _ |- _ ] => invc H end; simpl. + find_apply_lem_hyp net_handlers_NetHandler. find_copy_apply_lem_hyp NetHandler_inc_in_flight_to_backup_preserved. repeat find_rewrite. rewrite cons_is_app in IHrefl_trans_1n_trace1. repeat rewrite inc_in_flight_to_backup_app in *. destruct (pDst p) eqn:?; try rewrite update_same; try rewrite update_diff by congruence; unfold send_packets in *; simpl in *. * erewrite PrimaryNetHandler_no_msgs with (ms := l) in * by eauto. rewrite inc_in_flight_to_backup_cons_primary_dst in * by auto. simpl in *. rewrite inc_in_flight_to_backup_nil in *. auto with *. * lia. + find_apply_lem_hyp input_handlers_InputHandlers. find_copy_apply_lem_hyp InputHandler_inc_in_flight_to_backup_preserved. unfold send_packets in *. simpl in *. rewrite inc_in_flight_to_backup_app. subst. destruct h eqn:?; try rewrite update_same; try rewrite update_diff by congruence. * lia. * erewrite InputHandler_backup_no_msgs with (l := l) by eauto. simpl. rewrite inc_in_flight_to_backup_nil. lia. Qed.
imports: Verdi(Verdi HandlerMonad)