proposition: Lemma sync_init {k k'} {M : list (mm_instr (pos (1+k+k')))} {v : Vector.t nat k} : @sync _ M (1, Vector.append (0 ## v) (Vector.const 0 k')) (TM_facts.mk_mconfig (toState M false 1) (Vector.append ((enc 0) ## Vector.map enc v) (Vector.const (enc 0) k'))).
proof: Proof. apply: sync_intro; [|done] => /=. constructor. { by apply: (encodes_counter_intro _ 0). } apply: vec_Forall2_append. - elim: v. { by constructor. } move=> *. constructor; [|done]. by apply: (encodes_counter_intro _ 0). - clear. elim: k'. { by constructor. } move=> *. constructor; [|done]. by apply: (encodes_counter_intro _ 0). 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