proposition: Lemma uniform_transition ab : In ab representatives -> (forall a'b', RZ ab a'b' -> terminating (1, a'b')) + (forall a'b', RZ ab a'b' -> non_terminating (1, a'b')) + {v | In v representatives /\ (forall a'b', RZ ab a'b' -> exists w, RZ v w /\ reaches_plus (1, a'b') (1, w)) }.
proof: Proof. Proof using HM. rewrite /representatives /=. have HE := @eq_or_inf (nat * nat) ltac:(by do ? decide equality). case /HE; [|case /HE; [|case /HE; [|case /HE; last done]]] => <-. - have [[[[|]|]|]|] := transition_0_0. + move=> ?. left. left=> - [a' b'] /= ?. have ->: a' = 0 by lia. have ->: b' = 0 by lia. done. + move=> ?. left. right=> - [a' b'] /= ?. have ->: a' = 0 by lia. have ->: b' = 0 by lia. done. + move=> H. right. exists (1, 0). split; first by tauto. move: H => [a'' Hk] [a' b'] /= ?. have ->: a' = 0 by lia. have ->: b' = 0 by lia. exists (S a'', 0). split; [lia|by apply: (reaches_neq_incl Hk)]. + move=> H. right. exists (0, 1). split; first by tauto. move: H => [b'' Hk] [a' b'] /= ?. have ->: a' = 0 by lia. have ->: b' = 0 by lia. exists (0, S b''). split; [lia|by apply: (reaches_neq_incl Hk)]. + move=> H. right. exists (1, 1). split; first by tauto. move: H => [a'' [b'' Hk]] [a' b'] /= ?. have ->: a' = 0 by lia. have ->: b' = 0 by lia. exists (S a'', S b''). split; [lia|by apply: (reaches_neq_incl Hk)]. - have [[[[|]|]|]|] := transition_Sa_0. + move=> ?. left. left=> - [a' b'] /= ?. have ->: a' = S (a' - 1) by lia. have ->: b' = 0 by lia. done. + move=> ?. left. right=> - [a' b'] /= ?. have ->: a' = S (a' - 1) by lia. have ->: b' = 0 by lia. done. + move=> H. right. exists (0, 0). split; first by tauto. move=> [a' b'] /= ?. have ->: a' = S (a' - 1) by lia. have ->: b' = 0 by lia. have Hk := H (a'-1). exists (0, 0). split; [lia|by apply: (reaches_neq_incl Hk)]. + move=> H. right. exists (0, 1). split; first by tauto. move=> [a' b'] /= ?. have ->: a' = S (a' - 1) by lia. have ->: b' = 0 by lia. have [b'' Hk] := H (a'-1). exists (0, S b''). split; [lia|by apply: (reaches_neq_incl Hk)]. + move=> H. right. exists (1, 1). split; first by tauto. move=> [a' b'] /= ?. have ->: a' = S (a' - 1) by lia. have ->: b' = 0 by lia. have [a'' [b'' Hk]] := H (a'-1). exists (S a'', S b''). split; [lia|by apply: (reaches_neq_incl Hk)]. - have [[[[|]|]|]|] := transition_0_Sb. + move=> ?. left. left=> - [a' b'] /= ?. have ->: a' = 0 by lia. have ->: b' = S (b' - 1) by lia. done. + move=> ?. left. right=> - [a' b'] /= ?. have ->: a' = 0 by lia. have ->: b' = S (b' - 1) by lia. done. + move=> H. right. exists (0, 0). split; first by tauto. move=> [a' b'] /= ?. have ->: a' = 0 by lia. have ->: b' = S (b' - 1) by lia. have Hk := H (b'-1). exists (0, 0). split; [lia|by apply: (reaches_neq_incl Hk)]. + move=> H. right. exists (1, 0). split; first by tauto. move=> [a' b'] /= ?. have ->: a' = 0 by lia. have ->: b' = S (b' - 1) by lia. have [a'' Hk] := H (b'-1). exists (S a'', 0). split; [lia|by apply: (reaches_neq_incl Hk)]. + move=> H. right. exists (1, 1). split; first by tauto. move=> [a' b'] /= ?. have ->: a' = 0 by lia. have ->: b' = S (b' - 1) by lia. have [a'' [b'' Hk]] := H (b'-1). exists (S a'', S b''). split; [lia|by apply: (reaches_neq_incl Hk)]. - have [[[[|]|]|]|] := transition_Sa_Sb. + move=> ?. left. left=> - [a' b'] /= ?. have ->: a' = S (a' - 1) by lia. have ->: b' = S (b' - 1) by lia. done. + move=> ?. left. right=> - [a' b'] /= ?. have ->: a' = S (a' - 1) by lia. have ->: b' = S (b' - 1) by lia. done. + move=> H. right. exists (0, 0). split; first by tauto. move=> [a' b'] /= ?. have ->: a' = S (a' - 1) by lia. have ->: b' = S (b' - 1) by lia. have Hk := H (a'-1) (b'-1). exists (0, 0). split; [lia|by apply: (reaches_neq_incl Hk)]. + move=> H. right. exists (1, 0). split; first by tauto. move=> [a' b'] /= ?. have ->: a' = S (a' - 1) by lia. have ->: b' = S (b' - 1) by lia. have [a'' Hk] := H (a'-1) (b'-1). exists (S a'', 0). split; [lia|by apply: (reaches_neq_incl Hk)]. + move=> H. right. exists (0, 1). split; first by tauto. move=> [a' b'] /= ?. have ->: a' = S (a' - 1) by lia. have ->: b' = S (b' - 1) by lia. have [b'' Hk] := H (a'-1) (b'-1). exists (0, S b''). split; [lia|by apply: (reaches_neq_incl Hk)]. Qed.
imports: List PeanoNat Lia Relation_Operators Operators_Properties Transitive_Closure Undecidability.MinskyMachines.MM2 Undecidability.MinskyMachines.Util.MM2_facts ssreflect ssrbool ssrfun