proposition: Lemma uniform_representative_decision v : In v representatives -> (forall ab, RZ v ab -> terminating (1, ab)) + (forall ab, RZ v ab -> non_terminating (1, ab)).
proof: Proof. Proof using HM. move: v. have: { L & incl L representatives & (forall v, In v representatives -> (forall ab, RZ v ab -> terminating (1, ab)) + (forall ab, RZ v ab -> non_terminating (1, ab)) + { w | In w L /\ (forall ab, RZ v ab -> exists a'b', RZ w a'b' /\ reaches_plus (1, ab) (1, a'b')) } ) }. { exists representatives; first done. by apply: uniform_transition. } case. elim. { move=> _ H v /H /= [[|]|]; [tauto|tauto|]. by move=> [?] []. } move=> v0 L IH /(@incl_cons_inv (nat*nat)) [Hv0 HL] HRZ. apply: IH; first done. move=> v /HRZ. move=> [[|]|]; [tauto|tauto|]. have HE := @eq_or_inf (nat * nat) ltac:(by do ? decide equality). move=> [w] /= [/HE [|]]; first last. { move=> ??. right. by exists w. } move=> <-. move: Hv0 => /HRZ [[|]|]. - move=> Hv0 Hv. left. left=> ab /Hv [a'b'] [/Hv0]. by move=> /mm2_steps_terminates_l H /clos_rt_clos_t /H. - move=> Hv0 Hv. left. right=> ab /Hv [a'b'] [/Hv0]. by move=> /mm2_steps_not_terminates_l H /clos_rt_clos_t /H. - move=> [w'] /= [/HE [|]]. + move=> <- /RZ_loop Hv0 Hv. left. right=> ab /Hv [a'b'] [/Hv0]. by move=> /mm2_steps_not_terminates_l H /clos_rt_clos_t /H. + move=> ? Hv0 Hv. right. exists w'. split; first done. move=> ab /Hv [a'b'] [/Hv0] [a''b''] [? HSk'] HSk. exists a''b''. split; first done. by apply: t_trans; eassumption. Qed.
imports: List PeanoNat Lia Relation_Operators Operators_Properties Transitive_Closure Undecidability.MinskyMachines.MM2 Undecidability.MinskyMachines.Util.MM2_facts ssreflect ssrbool ssrfun