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