fact: Definition MoveL_rel {Σ : finType} D (n : nat) : Vector.t (tape Σ) 1 -> unit * Vector.t (tape Σ) 1 -> Prop := fun t '(_, t') => t' = Vector.map (Nat.iter n (fun t => @tape_move Σ t D)) t.
imports: Undecidability.TM.Compound.TMTac Undecidability.TM.Basic.Mono Undecidability.TM.Compound.Multi Undecidability.TM.Combinators.Combinators Undecidability.TM.Compound.WriteString