proposition: Lemma fstep (s t : nat * vec nat (S n)) (s' : TM_facts.mconfig Σ (state P) (S n)) : sss_step (@mma_sss _) (1, M) s t -> sync s s' -> exists t', clos_trans _ step2 s' t' /\ sync t t'.
proof: Proof. Proof using M_mon. move=> [?] [l] [instr] [r] [{}v] [[<- HM]] [->]. move E: ((1 + (length l), v)) => st H. case: H HM E. - move=> ? x ? HM [<- <-]. move: s' => [p ts] /syncE [Hvts [E0 ->]]. exists (TM_facts.mk_mconfig (toState false (1 + (1 + (length l)))) (inc_bs x ts)). split; [apply: t_trans; (apply: t_step; split)|]. + cbn. have := to_nat_toAddress HM. by case: (toAddress (S (length l))). + by rewrite /TM_facts.step /= (to_nat_toAddress HM) (split_nth_error HM). + done. + by rewrite /TM_facts.step /= (to_nat_toAddress HM) (split_nth_error HM). + rewrite vec_pos_nth_eq. by apply: sync_inc. - move=> ? x q v' Hx HM [<- ?]. subst v'. rewrite vec_pos_nth_eq in Hx. move: s' => [p ts] /syncE [Hvts [E0 ->]]. exists (TM_facts.mk_mconfig (toState false (1 + (1 + (length l)))) (dec_bs x ts)). move: (HM) => /M_mon ?. split; [apply: t_trans; (apply: t_step; split)|]. + cbn. have := to_nat_toAddress HM. by case: (toAddress (S (length l))). + by rewrite /TM_facts.step /= (to_nat_toAddress HM) (split_nth_error HM). + done. + rewrite /TM_facts.step /= (to_nat_toAddress HM) (split_nth_error HM). rewrite current_chars_act. have [? ->] := Vector_nth_tapes x Hvts. by rewrite Hx /=. + by apply: sync_dec_0. - move=> ? x q v' ? Hx HM [<- ?]. subst v'. rewrite vec_pos_nth_eq in Hx. move: s' => [p ts] /syncE [Hvts [E0 ->]]. exists (TM_facts.mk_mconfig (toState false q) (dec_bs x ts)). move: (HM) => /M_mon ?. split; [apply: t_trans; (apply: t_step; split)|]. + cbn. have := to_nat_toAddress HM. by case: (toAddress (S (length l))). + by rewrite /TM_facts.step /= (to_nat_toAddress HM) (split_nth_error HM). + done. + rewrite /TM_facts.step /= (to_nat_toAddress HM) (split_nth_error HM). rewrite current_chars_act. have [? ->] := Vector_nth_tapes x Hvts. by rewrite Hx /=. + by apply: sync_dec_S. Qed.
imports: Undecidability.TM(TM) Undecidability.MinskyMachines(MM MMA.mma_defs Reductions.MMA_computable_to_MMA_mon_computable) Undecidability.Shared.Libs.DLW(Vec.pos Vec.vec Code.sss Code.subcode) Undecidability.Shared.Libs.PSL.FiniteTypes.FinTypesDef Undecidability.Shared.Libs.PSL(CompoundFinTypes) Undecidability.Shared.Libs.PSL.EqDec List Lia PeanoNat Compare_dec Relations ssreflect ssrbool ssrfun