proposition: Theorem pbj_NOABT : forall net tr, step_async_star (params:=PB_multi_params) step_async_init net tr -> no_output_at_backup_trace tr.
proof: Proof. Proof using. intros. find_apply_lem_hyp refl_trans_1n_n1_trace. prep_induction H. induction H; intros. - auto using NOABT_nil. - subst. repeat concludes. apply NOABT_app; auto. invc H1; simpl in *. + find_apply_lem_hyp PB_net_defn'. intuition; subst; repeat find_rewrite; auto using NOABT_singleton_inr_nil, NOABT_singleton_primary. + rewrite cons_cons_app. apply NOABT_app. * auto using NOABT_singleton_inl. * find_apply_lem_hyp PB_input_handler_defn. intuition; break_exists; intuition; subst; auto using NOABT_singleton_inr_nil, NOABT_singleton_inr_read_response. Qed.
imports: Verdi(Verdi HandlerMonad)