proposition: Lemma Vector_nth_tapes {k v ts} (i : Fin.t k) : encodes_counters v ts -> exists m, Vector.nth ts i = midtape (repeat false m) false (repeat true (Vector.nth v i)).
proof: Proof. move=> H. elim: H i. { by apply: Fin.case0. } move=> > [] > ? IH i. have [->|[j ->]] := pos_S_inv i. - by eexists. - by apply: (IH j). 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