fact: Definition ReadCurrentSymbols_steps (n : nat) (T : tapes sig n) := match T with | [| |] => ReadCurrentSymbols_Loop_steps_nil | tp ::: T' => 2 + ReadCurrentSymbols_Loop_steps_cons (vector_to_list T') tp 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)