fact: Fixpoint insertKnownSymbols {n : nat} (readSymbols : Vector.t (option sig) n) (i : Fin.t n) (newSymbols : list (option sig)) : Vector.t (option sig) n := match newSymbols with | nil => readSymbols | s :: newSymbols' => match finSucc_opt i with | Some i' => insertKnownSymbols (insertKnownSymbol readSymbols i s) i' newSymbols' | None => insertKnownSymbol readSymbols i s end end.
imports: Undecidability.TM.Basic.Mono Undecidability.TM.Combinators.Combinators Undecidability.TM.Code.Code Undecidability.TM.Single.EncodeTapes Undecidability.TM.Compound(TMTac MoveToSymbol Multi Shift)