proposition: Lemma P_init {k k'} {M : list (mm_instr (pos (1+k+k')))} {v : Vector.t nat k} : @TM_facts.step _ _ (P M) (TM_facts.mk_mconfig (true, pos0) (niltape ## Vector.append (Vector.map enc v) (Vector.const niltape k'))) = TM_facts.mk_mconfig (toState M false 1) (enc 0 ## Vector.append (Vector.map enc v) (Vector.const (enc 0) k')).
proof: Proof. cbn. congr TM_facts.mk_mconfig. congr Vector.cons. elim: v. - cbn. elim: (k'). { done. } by move=> > /= ->. - by move=> > /= ->. 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