proposition: Lemma simulation_step {instr p1 cs1 p2 cs2 ts1} : (p1, [instr]) <sc (1, M) -> mma_sss instr (p1, cs1) (p2, cs2) -> encodes_counters cs1 ts1 -> exists ts2, TM_facts.step (M := P) (TM_facts.mk_mconfig (toState p1) ts1) = TM_facts.mk_mconfig (toState p2) ts2 /\ encodes_counters cs2 ts2.
proof: Proof. rewrite /TM_facts.step /= /trans'. move=> /read_instr [q [-> [-> ->]]]. move E1: (S q, cs1) => p1cs1. move E2: (p2, cs2) => p2cs2 H. case: H E1 E2. - move=> ? i ? [<- <-] [-> ->] Hcs1ts1. eexists. split; first done. elim: Hcs1ts1 i. { move=> i. by case: (pos_O_inv i). } move=> m c t cs ts Hct Hcsts IH i. have [->|[i' ->]] := pos_S_inv i. + move=> /=. constructor; last by rewrite TM_facts.doAct_nop. rewrite /TM_facts.doAct. case: Hct => [[|?]|[|?] ?| |>]. all: by eauto with counters nocore. + by constructor; [rewrite doAct_nop_1|apply: IH]. - move=> ? i p' v Hcs1i [<- ?] [-> ->] Hcs1ts1. subst v. rewrite (read_current_char Hcs1ts1 Hcs1i). eexists. by split; [done|rewrite TM_facts.doAct_nop]. - move=> ? i p' v k Hcs1i [_ ?] [-> ->] Hcs1ts1. subst v. move=> [:H]. have [->|->] := (read_current_char Hcs1ts1 Hcs1i); eexists; split; [done|abstract: H|done|by apply: H]. elim: Hcs1ts1 i Hcs1i. { move=> i. by case: (pos_O_inv i). } move=> m c t cs ts Hct Hcsts IH i. have [->|[i' ->]] := pos_S_inv i. + move=> /= Hc. constructor; last by rewrite TM_facts.doAct_nop. rewrite /TM_facts.doAct. case: Hct Hc => [//|? [|?]| |[|?]] [<-]. all: by eauto with counters nocore. + move=> ?. by constructor; [rewrite doAct_nop_1|apply: IH]. Qed.
imports: Undecidability.MinskyMachines(MM MMA.mma_defs) Undecidability.Shared.Libs.DLW(Vec.pos Vec.vec Code.sss Code.subcode) Undecidability.Shared.Libs.PSL.FiniteTypes.FinTypesDef Undecidability.Shared.Libs.PSL.EqDec List Vector Lia PeanoNat Compare_dec ssreflect ssrbool ssrfun