proposition: Theorem pbj_0_or_1 : forall net tr, step_async_star (params:=PB_multi_params) step_async_init net tr -> zero_or_one_outputs_per_step_trace tr.
proof: Proof. Proof using. intros. find_apply_lem_hyp refl_trans_1n_n1_trace. prep_induction H. induction H; intros; subst. - auto using ZOOOPST_nil. - repeat concludes. apply ZOOOPST_app; auto. invc H1; simpl in *. + find_apply_lem_hyp PB_net_defn. intuition; subst; auto using ZOOOPST_singleton_nil. break_exists. break_and. break_match. intuition; subst; auto using ZOOOPST_singleton_singleton. + rewrite cons_cons_app. apply ZOOOPST_app. * auto using ZOOOPST_singleton_inl. * find_apply_lem_hyp PB_input_handler_defn; intuition; subst; auto using ZOOOPST_singleton_nil, ZOOOPST_singleton_singleton. Qed.
imports: Verdi(Verdi HandlerMonad)