proposition: Fact mm_env_steps_DEC_0_inv k P i x p v st : (i,DEC x p::nil) <sc P -> k <> 0 -> v⇢x = 0 -> P // (i,v) -[k]-> st -> exists k', k' < k /\ P // (p,v) -[k']-> st.
proof: Proof. intros H1 H2 H3 H4. apply sss_steps_inv in H4. destruct H4 as [ (? & ?) | (k' & st2 & ? & H4 & H5) ]; subst; auto. destruct H2; auto. apply sss_step_subcode_inv with (1 := H1) in H4. exists k'; split. lia. inversion H4; subst; auto. rewrite H3 in H9; discriminate. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils subcode sss) Undecidability.MinskyMachines.MMenv(env)