proposition: Fact sss_step_stall_inv P st : sss_step_stall P st -> { ii | (fst st,ii::nil) <sc P /\ sss_stall ii st } + { out_code (fst st) P }.
proof: Proof. intros H. destruct (in_out_code_dec (fst st) P) as [ H1 | H1 ]. 2: tauto. destruct P as (iP,cP). destruct st as (j,d). simpl in H1. destruct (@list_pick _ cP (j-iP)) as (ii & l & r & H2 & H3). lia. left; exists ii; simpl; split. exists l, r; split; auto; lia. intros st' H4. apply (H st'). subst; apply in_sss_step; auto. simpl; lia. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(Utils.utils Code.subcode)