proposition: Lemma target_index_b p q : nth_error M p = Some (mm2_dec_b q) -> q = 1 \/ (forall a b, mm2_stop M (q, (a, b))).
proof: Proof. Proof using HM. move: q => [|[|q]]. - move=> _. right => ??. apply /mm2_stop_index_iff. by left. - move=> _. by left. - move=> /nth_error_Some_mm2_instr_at_iff Hq. right. move=> a b z [?] [/mm2_instr_at_bounds /= ? _]. case Hi: (nth_error M q) => [i|]; first last. { move: Hi => /nth_error_None. lia. } move: Hi => /nth_error_Some_mm2_instr_at_iff. case: i => > Hi. + suff: (S p, (1, 1)) = (S q, (0, 0)) by done. apply: (HM). * eexists. by split; [eassumption|constructor]. * eexists. by split; [eassumption|constructor]. + suff: (S p, (0, 2)) = (S q, (0, 0)) by done. apply: (HM). * eexists. by split; [eassumption|constructor]. * eexists. by split; [eassumption|constructor]. + suff: (S p, (0, 1)) = (S q, (0, 0)) by done. apply: (HM). * eexists. by split; [eassumption|constructor]. * eexists. by split; [eassumption|constructor]. + suff: (S p, (0, 1)) = (S q, (0, 0)) by done. apply: (HM). * eexists. by split; [eassumption|constructor]. * eexists. by split; [eassumption|constructor]. Qed.
imports: List PeanoNat Lia Relation_Operators Operators_Properties Transitive_Closure Undecidability.MinskyMachines.MM2 Undecidability.MinskyMachines.Util.MM2_facts ssreflect ssrbool ssrfun