proposition: Lemma transition_Sa_Sb : (forall a b, terminating (1, (S a, S b))) + (forall a b, non_terminating (1, (S a, S b))) + (forall a b, reaches (1, (S a, S b)) (1, (0, 0))) + (forall a b, exists a', reaches (1, (S a, S b)) (1, (S a', 0))) + (forall a b, exists b', reaches (1, (S a, S b)) (1, (0, S b'))).
proof: Proof. Proof using HM. have := reaches'I (1, (1, 1)). move=> [x] [H0x]. have [[y H'x]|] := mm2_sig_step_dec M x; first last. { move=> Hy _. do 4 left. move=> a b. move: H0x Hy => /reaches'_None_terminating /[apply] /=. apply; lia. } move=> /(_ _ H'x). case /(eq_or_inf Nat.eq_dec); first last. { move: H0x H'x => /reaches'_Some_terminating /[apply] /[apply] H. do 4 left. move=> a b. apply: H => /=; lia. } move: y H'x => [py' [[|ay'] [|by']]] H'x /= Hy'; subst py'. - by move: H0x H'x => /not_transition_1_1_to_0_0 /[apply]. - right. move=> a b. move: H0x H'x => /dec_a_0 H /H /(_ (S a) (S b)) Hk'. exists (S a * by' + S b - 1). move: Hk'. congr reaches. congr (_, (_, _)); lia. - do 1 left. right. move=> a b. move: H0x H'x => /dec_b_0 H /H /(_ (S a) (S b)) Hk'. exists (S b * ay' + S a - 1). move: Hk'. congr reaches. congr (_, (_, _)); lia. - do 3 left. right. move=> a b. apply: dec_loop; by eassumption. Qed.
imports: List PeanoNat Lia Relation_Operators Operators_Properties Transitive_Closure Undecidability.MinskyMachines.MM2 Undecidability.MinskyMachines.Util.MM2_facts ssreflect ssrbool ssrfun