proposition: Corollary mm_env_compute_DEC_0 P i x k v st : (i,DEC x k::nil) <sc P -> v⇢x = O -> P // (k,v) ->> st -> P // (i,v) ->> st.
proof: Proof. intros; apply sss_progress_compute; eapply mm_env_progress_DEC_0; eauto. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils subcode sss) Undecidability.MinskyMachines.MMenv(env)