proposition: Lemma mm_self_loop_no_term_1 i x s v : (i,DEC x i::nil) <sc (1,P) -> s = (i,v) -> v#>x = 0 -> ~ (1,P) // s ↓.
proof: Proof. intros H1 H2 H3 (s0 & H4). revert i x v H1 H2 H3. pattern s; revert H4; apply mm_term_ind. + intros Hs0 i x v H1 H2 H3. subst s0. revert Hs0; apply in_out_code. apply subcode_in_code with (1 := H1). simpl; lia. + intros i ρ v j w H1 H2 H3 IH3 k x p G1 G2 G3. inversion G2; subst p k. generalize (subcode_cons_inj _ _ _ _ H1 G1); intros; subst. apply mm_sss_DEC0_inv in H2; auto. destruct H2; subst j w. apply (IH3 _ _ _ G1 eq_refl); auto. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils pos vec subcode sss) Undecidability.MinskyMachines.MM(mm_defs)