proposition: Lemma transition_0_0 : (terminating (1, (0, 0))) + (non_terminating (1, (0, 0))) + (exists a', reaches (1, (0, 0)) (1, (S a', 0))) + (exists b', reaches (1, (0, 0)) (1, (0, S b'))) + (exists a' b', reaches (1, (0, 0)) (1, (S a', S b'))).
proof: Proof. Proof using HM. have [y [/reaches'_incl H'y]] := reaches'I (1, (0, 0)). have [[[pz [az bz]]] Hyz|]:= mm2_sig_step_dec M y; first last. { move=> Hy _. do 4 left. move: H'y => /mm2_steps_terminates_l. apply. by apply: mm2_stop_terminates. } have H0z : reaches_plus (1, (0, 0)) (pz, (az, bz)). { by apply: clos_rt_t; [|apply: t_step]; eassumption. } move=> /(_ _ Hyz). case /(eq_or_inf Nat.eq_dec); first last. { move=> H'z. do 4 left. eexists. by split; [apply: clos_rt_clos_t|]; eassumption. } move=> /= ?. subst pz. move: az bz H0z {Hyz} => [|az] [|bz] H0z. - do 3 left. right. by apply: mm2_loop_not_terminates. - do 1 left. right. exists bz. by apply /clos_rt_clos_t. - do 2 left. right. exists az. by apply /clos_rt_clos_t. - right. exists az, bz. by apply /clos_rt_clos_t. Qed.
imports: List PeanoNat Lia Relation_Operators Operators_Properties Transitive_Closure Undecidability.MinskyMachines.MM2 Undecidability.MinskyMachines.Util.MM2_facts ssreflect ssrbool ssrfun