proposition: Fact bsm_sss_stall : forall P s, sss_step_stall (@bsm_sss n) P s -> out_code (fst s) P.
proof: Proof. intros (i,P) (q,v) H; unfold fst. red in H. destruct (in_out_code_dec q (i,P)) as [ H1 | ]; auto; exfalso. apply in_code_subcode in H1. destruct H1 as (ii & l & r & H1 & H2). simpl in H1. destruct (bsm_sss_total ii (q,v)) as (t & Ht). apply (H t); subst; apply in_sss_step; auto. Qed.
imports: List Arith Lia Bool Undecidability.Shared.Libs.DLW(utils list_bool pos vec subcode sss)