proposition: Lemma current_chars_act k (ts : Vector.t (tape Σ) k) i actions action : Vector.nth (TM_facts.current_chars (TM_facts.doAct_multi ts (vec_change actions i action))) i = current (TM_facts.doAct (Vector.nth ts i) action).
proof: Proof. elim: ts i actions. { by apply: Fin.case0. } move=> t ? ts IH i actions. rewrite (Vector.eta actions). have [->|[j ->]] := pos_S_inv i. - done. - by apply: IH. 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