proposition: Lemma terminating_orI p a b x y : reaches' (p, (S a, S b)) x -> step x y -> mm2_stop M y -> (forall a', terminating (p, (S a', 0))) + (forall b', terminating (p, (0, S b'))).
proof: Proof. rewrite (mm2_state_eta x). case: (index x) => [|px]. { move=> _ Hxy _. exfalso. by move: Hxy => [?] [/mm2_instr_at_pos]. } case Hi: (nth_error M px) => [i|]; first last. { move=> _ Hxy _. exfalso. move: Hxy => [?] [/nth_error_Some_mm2_instr_at_iff]. by rewrite Hi. } move: i Hi => []. - move=> /nth_error_Some_mm2_instr_at_iff Hi Hx H'x Hy. left=> a'. move: Hx => /reaches'E [n] [m] /= [?] [?]. move=> /(_ (S a') 0 ltac:(lia) ltac:(lia)). move=> /reaches'_incl /mm2_steps_terminates_l. apply. have ? := mm2_step_intro Hi (S a' + n) m. apply: mm2_steps_terminates_l. + apply: rt_step. eassumption. + apply: mm2_stop_terminates. apply: mm2_stop_index_eq; [eassumption|]. move: H'x => [?] [/mm2_instr_at_unique H'i Hxy]. move: Hi => /H'i ?. by inversion Hxy; subst. - move=> /nth_error_Some_mm2_instr_at_iff Hi Hx H'x Hy. right=> b'. move: Hx => /reaches'E [n] [m] /= [?] [?]. move=> /(_ 0 (S b') ltac:(lia) ltac:(lia)). move=> /reaches'_incl /mm2_steps_terminates_l. apply. have ? := mm2_step_intro Hi n (S b' + m). apply: mm2_steps_terminates_l. + apply: rt_step. eassumption. + apply: mm2_stop_terminates. apply: mm2_stop_index_eq; [eassumption|]. move: H'x => [?] [/mm2_instr_at_unique H'i Hxy]. move: Hi => /H'i ?. by inversion Hxy; subst. - move=> q /nth_error_Some_mm2_instr_at_iff Hi Hx H'x Hy. left=> a'. move: Hx => /reaches'E [n] [m] /= [?] [?]. move=> /(_ (S a') 0 ltac:(lia) ltac:(lia)). move=> /reaches'_incl /mm2_steps_terminates_l. apply. have ? := mm2_step_intro Hi (S (a' + n)) m. apply: mm2_steps_terminates_l. + apply: rt_step. eassumption. + apply: mm2_stop_terminates. apply: mm2_stop_index_eq; [eassumption|]. move: H'x => [?] [/mm2_instr_at_unique H'i Hxy]. move: Hi => /H'i ?. inversion Hxy; subst; by [|cbn; congruence]. - move=> q /nth_error_Some_mm2_instr_at_iff Hi Hx H'x Hy. right=> b'. move: Hx => /reaches'E [n] [m] /= [?] [?]. move=> /(_ 0 (S b') ltac:(lia) ltac:(lia)). move=> /reaches'_incl /mm2_steps_terminates_l. apply. have ? := mm2_step_intro Hi n (S (b' + m)). apply: mm2_steps_terminates_l. + apply: rt_step. eassumption. + apply: mm2_stop_terminates. apply: mm2_stop_index_eq; [eassumption|]. move: H'x => [?] [/mm2_instr_at_unique H'i Hxy]. move: Hi => /H'i ?. inversion Hxy; subst; by [|cbn; congruence]. Qed.
imports: List PeanoNat Lia Relation_Operators Operators_Properties Transitive_Closure Undecidability.MinskyMachines.MM2 Undecidability.MinskyMachines.Util.MM2_facts ssreflect ssrbool ssrfun