proposition: Lemma step_async_outputs_m : forall net net' tr, step_async net net' tr -> (inputs_m tr = [] /\ (outputs_m tr = [] /\ nwState net Primary = nwState net' Primary)) \/ (inputs_m tr = [] /\ exists os, outputs_m tr = [os]) \/ (exists i, inputs_m tr = [i]).
proof: Proof. Proof using. intros. invc H; simpl; break_match; auto; repeat rewrite app_nil_r in *; simpl in *; try find_apply_lem_hyp PB_net_defn; try find_apply_lem_hyp PB_input_handler_defn; intuition; subst. - rewrite inputs_m_inr_singleton. rewrite update_eq by auto. auto. - rewrite inputs_m_inr_singleton. rewrite update_eq by auto. auto. - break_exists. intuition; break_match. + intuition. subst. rewrite inputs_m_inr_singleton. simpl. eauto. + break_exists. intuition. subst. rewrite inputs_m_inr_singleton. simpl. eauto. - rewrite inputs_m_inr_singleton. rewrite update_diff by auto. auto. - rewrite inputs_m_inr_singleton. rewrite update_diff by auto. auto. - break_exists. intuition; subst; rewrite inputs_m_primary_inl; eauto. - rewrite inputs_m_inl_read. rewrite update_eq by auto. auto. - rewrite inputs_m_inl_read. rewrite update_diff by auto. auto. - rewrite inputs_m_backup. rewrite update_diff by auto. auto. Qed.
imports: Verdi(Verdi HandlerMonad)