proposition: Corollary mm_compute_DEC_S P i x k v u st : (i,DEC x k::nil) <sc P -> v#>x = S u -> P // (1+i,v[u/x]) ->> st -> P // (i,v) ->> st.
proof: Proof. intros; apply sss_progress_compute; eapply mm_progress_DEC_S; eauto. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils pos vec subcode sss)