proposition: Lemma inputs_1_m_revert : forall net tr, step_async_star (params := PB_multi_params) step_async_init net tr -> inputs_m tr = inputs_1 (revert_trace tr) ++ queue (nwState net Primary).
proof: Proof. Proof using. intros. find_apply_lem_hyp refl_trans_1n_n1_trace. prep_induction H. induction H; intros; subst. - simpl. auto. - repeat concludes. rewrite inputs_m_app. rewrite revert_trace_app. rewrite inputs_1_app. rewrite IHrefl_trans_n1_trace. repeat rewrite <- app_assoc. f_equal. invc H1; simpl in *. + find_apply_lem_hyp PB_net_defn. intuition; subst; simpl in *; rewrite (inputs_m_inr_singleton); rewrite app_nil_r. * rewrite update_nop. auto. * repeat find_rewrite. rewrite update_nop. auto. * break_exists. break_let. { intuition; subst. - repeat find_rewrite. rewrite app_nil_r. simpl. rewrite update_eq by auto. auto. - break_exists. intuition. subst. repeat find_rewrite. simpl. rewrite update_eq by auto. auto. } * break_exists. intuition. repeat find_rewrite. rewrite update_diff by auto. auto. + find_apply_lem_hyp PB_input_handler_defn. intuition; subst; simpl in *. * break_exists. intuition; subst; rewrite (inputs_m_primary_inl); rewrite update_eq; auto. * rewrite (inputs_m_inl_read). rewrite inputs_m_inr_singleton. rewrite app_nil_r. rewrite update_nop. auto. * rewrite (inputs_m_backup). rewrite inputs_m_inr_singleton. rewrite app_nil_r. rewrite update_nop. auto. Qed.
imports: Verdi(Verdi HandlerMonad)