proposition: Fact mm_env_steps_INC_inv k P i x v st : (i,INC x::nil) <sc P -> k <> 0 -> P // (i,v) -[k]-> st -> exists k', k' < k /\ P // (1+i,v⦃x⇠S(v⇢x)⦄) -[k']-> st.
proof: Proof. intros H1 H2 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. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils subcode sss) Undecidability.MinskyMachines.MMenv(env)