proposition: Lemma transition_0_Sb : (forall b, terminating (1, (0, S b))) + (forall b, non_terminating (1, (0, S b))) + (forall b, reaches (1, (0, S b)) (1, (0, 0))) + (forall b, exists a', reaches (1, (0, S b)) (1, (S a', 0))) + (forall b, exists a' b', reaches (1, (0, S b)) (1, (S a', S b'))).
proof: Proof. Proof using HM. have [x' [Hx']] := reaches'I (1, (0, 1)). have [[y']|] := mm2_sig_step_dec M x'; first last. { move=> ??. do 4 left. move=> b. move: Hx' => /reaches'_None_terminating. apply=> /=; by [assumption|lia]. } move=> /[dup] Hx'y' + H => /H{H}. case /(eq_or_inf Nat.eq_dec); first last. { move: Hx' Hx'y' => /reaches'_Some_terminating H /H {}H /H {}H. do 4 left. move=> b. apply: H => /=; lia. } move: y' Hx'y' => [py' [[|ay'] by']] + /= Hy'; subst py'. { move: by' => [|by'] H'x'. - do 2 left. right. move=> b. elim: (S b); first by apply: rt_refl. move=> {}b IH. move: Hx' => /reaches'E. move=> [n'] [m'] /= [Hax] [Hbx] /(_ 0 (S b) ltac:(lia) ltac:(lia)). move=> /reaches'_incl Hk. apply: (rt_trans Hk). move: H'x' => /(mm2_step_parallel (index x', (n', S b + m'))) /= /(_ ltac:(lia)). move=> [[pz [az bz]]] /= [/rt_step] H [?] ?. apply: (rt_trans H). subst pz. move: IH. congr reaches. congr (_, (_, _)); lia. - do 3 left. right. move=> b. apply: transition_loop => a' b' ??. move: Hx' H'x' => /reaches'E [n] [m] /= [?] [?]. move=> /(_ a' b' ltac:(lia) ltac:(lia)) /reaches'_incl Hk'. move=> /(mm2_step_parallel (index x', (a' + n, b' + m))) /=. move=> /(_ ltac:(lia)) [[pz [az bz]]] [/t_step Hz] /= [? ?]. subst pz. exists az, bz. split; last by lia. apply: clos_rt_t; by eassumption. } move: by' => [|by'] H'x'; first last. { right. move=> b. move: Hx' => /reaches'E [n] [m] /= [Hax'] [Hbx']. move=> /(_ 0 (S b) ltac:(lia) ltac:(lia)) /reaches'_incl. move: H'x' => /(mm2_step_parallel (index x', (n, S b + m))) /=. move=> /(_ ltac:(lia)) [[pz' [az' bz']]] /= [/rt_step Hz'] [? ?] Hx'. exists (az' - 1), (bz' - 1). apply /(rt_trans Hx'). move: Hz'. congr reaches. congr (_, (_, _)); lia. } have := reaches'I (1, (1, 1)). move=> [x] [Hx]. have [[y]|] := mm2_sig_step_dec M x; first last. { move=> ??. do 4 left. move=> b. move: Hx => /reaches'_None_terminating. apply => /=; by [assumption|lia]. } move=> /[dup] Hxy + H => /H{H}. case /(eq_or_inf Nat.eq_dec); first last. { move=> Hy. move: (Hx) (Hxy) (Hy) => /terminating_orI => H /H {}H /H {H} [HS|?]; last by (do 4 left). do 4 left. move=> [|b]. { apply: (mm2_steps_terminates_l _ (HS ay')). by apply: (rt_trans (reaches'_incl Hx') (rt_step H'x')). } move: Hx' => /reaches'E [n] [m] /= [?] [?]. move=> /(_ 0 (S (S b)) ltac:(lia) ltac:(lia)). move=> /reaches'_incl /mm2_steps_terminates_l. apply. move: H'x' => /(mm2_step_parallel (index x', (n, S (S b) + m))) /=. move=> /(_ ltac:(lia)) [[pz' [az' bz']]] /= [Hz'] [?] ?. move: Hz' => /rt_step /mm2_steps_terminates_l. apply. subst pz'. move: Hx => /reaches'E [n'] [m'] /= [?] [?]. move=> /(_ az' bz' ltac:(lia) ltac:(lia)). move=> /reaches'_incl /mm2_steps_terminates_l. apply. move: Hxy => /(mm2_step_parallel (index x, (az' + n', bz' + m'))) /=. move=> /(_ ltac:(lia)) [z] [Hz] [?] ?. move: Hz => /rt_step /mm2_steps_terminates_l. apply. apply: mm2_stop_terminates. by apply: mm2_stop_index_eq; eassumption. } move=> H0y. move Ha'y: (value1 y) => a'y. move Hb'y: (value2 y) => b'y. move: a'y Ha'y => [|a'y] H1y. { exfalso. apply: rev_dec_unique. + apply: (proj1 (dec_stepI Hxy H0y)). move: Hx => /reaches'E [n] [m] /= [?] [?]. lia. + apply: (proj2 (dec_stepI H'x' ltac:(done))). move: Hx' => /reaches'E [n] [m] /= [?] [?]. lia. } move: b'y Hb'y => [|b'y] H2y. - do 1 left. right. move=> b. move: Hx' => /reaches'E [n] [m] /= [?] [?]. move=> /(_ 0 (S b) ltac:(lia) ltac:(lia)) /reaches'_incl Hk'. move: H'x' => /(mm2_step_parallel (index x', (n, S b + m))) /=. move=> /(_ ltac:(lia)) [y'] [/rt_step Hy'] [H0y'] ?. move: Hx Hxy => /dec_b_0 H. rewrite (mm2_state_eta y) H0y H1y H2y. move=> /H {H} => /(_ (S ay') b) Hk''. exists (b * a'y + ay'). apply /(rt_trans Hk') /(rt_trans Hy'). rewrite (mm2_state_eta y'). move: Hk''. congr reaches; congr (_, (_, _)); lia. - do 3 left. right. move=> b. apply: dec_loop; [eassumption|]. move: Hxy. rewrite (mm2_state_eta y) H0y H1y H2y. apply. Qed.
imports: List PeanoNat Lia Relation_Operators Operators_Properties Transitive_Closure Undecidability.MinskyMachines.MM2 Undecidability.MinskyMachines.Util.MM2_facts ssreflect ssrbool ssrfun