proposition: Theorem decision (c: mm2_state) : (terminating c) + (not (terminating c)).
proof: Proof. Proof using HM. have [y [/reaches'_incl Hk]] := reaches'I c. have [[[pz [az bz]] Hyz]|] := mm2_sig_step_dec M y; first last. { move=> ??. left. apply: (mm2_steps_terminates_l Hk). by apply: mm2_stop_terminates. } have Hcz : reaches c (pz, (az, bz)). { apply: rt_trans; [|apply: rt_step]; by eassumption. } move=> /(_ _ Hyz). case /(eq_or_inf Nat.eq_dec); first last. { move=> ?. left. move: Hcz => /mm2_steps_terminates_l. apply. by apply: mm2_stop_terminates. } move=> /= ?. subst pz. case: (uniform_decision_0 az bz). - move=> /mm2_steps_terminates_l H'z. left. by apply: H'z. - move=> /mm2_steps_not_terminates_l H'z. right. by apply: H'z. Qed.
imports: List PeanoNat Lia Relation_Operators Operators_Properties Transitive_Closure Undecidability.MinskyMachines.MM2 Undecidability.MinskyMachines.Util.MM2_facts ssreflect ssrbool ssrfun