proposition: Fact mma_sss_progress_DEC_0 P i x k v st : (i,DECₐ x k::nil) <sc P -> v#>x = O -> P // (1+i,v) ->> st -> P // (i,v) -+> st.
proof: Proof. intros H1 H2 H3. apply sss_progress_compute_trans with (2 := H3). apply subcode_sss_progress with (1 := H1). exists 1; split; auto; apply sss_steps_1. apply in_sss_step with (l := nil). + simpl; lia. + constructor; auto. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils pos vec subcode sss)