diff --git a/Cslib.lean b/Cslib.lean
index c0269e0bbb..7dd907cd62 100644
--- a/Cslib.lean
+++ b/Cslib.lean
@@ -31,6 +31,7 @@ public import Cslib.Computability.Languages.Language
 public import Cslib.Computability.Languages.OmegaLanguage
 public import Cslib.Computability.Languages.OmegaRegularLanguage
 public import Cslib.Computability.Languages.RegularLanguage
+public import Cslib.Computability.Machines.MultiTapeTuring.Basic
 public import Cslib.Computability.Machines.SingleTapeTuring.Basic
 public import Cslib.Computability.URM.Basic
 public import Cslib.Computability.URM.Computable
diff --git a/Cslib/Computability/Machines/MultiTapeTuring/Basic.lean b/Cslib/Computability/Machines/MultiTapeTuring/Basic.lean
new file mode 100644
index 0000000000..e63f8becf1
--- /dev/null
+++ b/Cslib/Computability/Machines/MultiTapeTuring/Basic.lean
@@ -0,0 +1,418 @@
+/-
+Copyright (c) 2026 Christian Reitwiessner. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Christian Reitwiessner
+-/
+
+module
+
+public import Mathlib.Data.Finset.Max
+public import Mathlib.Algebra.Order.BigOperators.Group.Finset
+public import Mathlib.Computability.Language
+public import Cslib.Foundations.Data.BiTape
+public import Cslib.Foundations.Data.RelatesInSteps
+
+/-!
+# Multi-Tape Turing Machines
+
+Defines Turing machines with a read-only input tape, `k` work tapes and one write-only output tape.
+The tapes contain symbols from `Option Symbol` for a finite alphabet `Symbol` (where `none` is the
+blank symbol).
+
+## Design
+
+The multi-tape Turing machine uses a read-only input tape, `k` work tapes and a write-only output
+tape.
+The input head can move freely on the input, but any move attempt beyond one cell outside the input
+results in no movement.
+The transition function can optionally output one symbol, which models the write-only output tape.
+Because of these restrictions, the input and output tapes do not count towards the space usage of
+the machine. The space usage of the work tapes is the number of cells the head accessed.
+
+## Important Declarations
+
+We define a number of structures and concepts related to multi-tape Turing machine computation:
+
+* `MultiTapeTM`: the TM itself
+* `Cfg`: the configuration of a TM, including internal state, the tapes and the output so far
+* `spaceUsed`: the number of work tape cells touched by the head until a certain step
+* `TransitionRelation`: the transition relation from one configuration to the next
+* `ComputesInTimeAndSpace`: a proof that a TM computes an output from an input in a certain number
+    of steps and using a certain number of tape cells
+* `ComputesFunInTimeAndSpace`: a proof that a TM computes a function (on strings) respecting a
+    time and space bound in the input length
+* `DecidesLanguageInTimeAndSpace`: a proof that a TM decides a language within a certain time
+    and space bound
+
+There are two ways to talk about the behaviour of a multi-tape Turing machine, and they are
+proven to be equivalent.
+
+* `MultiTapeTM.configs`: a sequence of configurations by execution step
+* `RelatesInSteps tm.TransitionRelation cfg cfg' t`: a proof that `tm` transforms the configuration
+    `cfg` into `cfg'` in exactly `t` steps
+
+-/
+
+@[expose] public section
+
+open Cslib Relation
+
+namespace Turing
+
+open BiTape StackTape
+
+variable {Symbol : Type}
+
+variable {k : ℕ}
+
+/-- The output of the transition function. -/
+structure TransitionOut (k : ℕ) (Symbol State : Type) where
+  /-- The movement (attempt) of the input head. -/
+  inputMove : Option Dir
+  /-- Actions on the work tapes: optionally a symbol to write and the head movement. -/
+  stmts : Fin k → (Option (Option Symbol)) × (Option Dir)
+  /-- An optional symbol to output. -/
+  outS : Option Symbol
+  /-- The successor state or none to halt. -/
+  q' : Option State
+
+/--
+A multi-tape Turing machine with `k` work tapes over the alphabet of `Option Symbol` (where `none`
+is the blank `BiTape` symbol).
+-/
+structure MultiTapeTM k Symbol [Inhabited Symbol] [Fintype Symbol] where
+  /-- type of state labels -/
+  State : Type
+  /-- finiteness of the state type -/
+  [stateFintype : Fintype State]
+  /-- initial state -/
+  q₀ : State
+  /-- transition function, mapping a state, the current input symbol and a tuple of head symbols
+  to a movement for the input head, actions on the work tape, optionally a symbol to output and
+  the successor state -/
+  tr : State → (Option Symbol) → (Fin k → Option Symbol) → TransitionOut k Symbol State
+
+namespace MultiTapeTM
+
+section Cfg
+
+/-!
+## Configurations of a Turing Machine
+
+This section defines the configurations of a Turing machine,
+the step function that lets the machine transition from one configuration to the next,
+and the intended initial and final configurations.
+-/
+
+variable [Inhabited Symbol] [Fintype Symbol] (tm : MultiTapeTM k Symbol)
+
+/--
+The configurations of a Turing machine consist of:
+- an `Option`al state (or none for the halting state),
+- `BiTape`s representing the tape contents and
+- the output so far.
+-/
+@[ext]
+structure Cfg : Type where
+  /-- the state of the TM (or none for the halting state) -/
+  state : Option tm.State
+  /-- the input -/
+  input : List Symbol
+  /-- the position of the input head, shifted by one -/
+  inputPos : Fin (input.length + 2)
+  /-- the work tape -/
+  workTapes : Fin k → BiTape Symbol
+  /-- the output so far -/
+  output : List Symbol
+deriving Inhabited
+
+/-- Attempt to move the input tape head.
+The machine can only read one empty cell outside of the input,
+any attempted movement beyond that results in no movement. -/
+@[scoped grind =]
+def moveInputPos {n : ℕ} (pos : Fin (n + 2)) (m : Option Dir) : Fin (n + 2) :=
+  let p := (pos + optionDirToInt m).toNat
+  if h : p < n + 2 then ⟨p, h⟩ else ⟨n + 1, by omega⟩
+
+@[simp, scoped grind =]
+lemma moveInputPos_none (pos : Fin (n + 2)) : moveInputPos pos none = pos := by
+  simp [moveInputPos, optionDirToInt]
+
+/-- The output of the transition function applied to a state and the set of topes. -/
+def transitionOutput (q : tm.State) (inputSymbol : Option Symbol) (work : Fin k → BiTape Symbol) :
+    TransitionOut k Symbol tm.State :=
+  tm.tr q inputSymbol (fun i => (work i).head)
+
+/-- The symbol currently under the input tape head. -/
+@[scoped grind =]
+def inputSymbol (cfg : tm.Cfg) : Option Symbol :=
+  if h₁ : cfg.inputPos = 0 then none
+  else if h₂ : cfg.inputPos = cfg.input.length + 1 then none
+  else cfg.input[cfg.inputPos.val - 1]'(by grind)
+
+@[simp]
+lemma inputSymbolInner {cfg : tm.Cfg} (p : ℕ)
+    (h₁ : cfg.inputPos.val = 1 + p)
+    (h₂ : p < cfg.input.length) :
+    tm.inputSymbol cfg = some cfg.input[p] := by
+  simp [inputSymbol, h₁]
+  grind
+
+/-- The step function corresponding to a `MultiTapeTM`. -/
+def step (cfg : tm.Cfg) : Option tm.Cfg :=
+  match cfg.state with
+  | none => none
+  | some q =>
+    let {inputMove, stmts, outS, q'} := tm.transitionOutput q (tm.inputSymbol cfg) cfg.workTapes
+    some {
+      state := q',
+      input := cfg.input,
+      inputPos := moveInputPos cfg.inputPos inputMove,
+      workTapes i := match stmts i with
+        | (none, m) =>  cfg.workTapes i |>.optionMove m
+        | (some s, m) => cfg.workTapes i |>.write s |>.optionMove m
+      output := match outS with
+      | none => cfg.output
+      | some s => cfg.output ++ [s]
+    }
+
+/-- Any number of positive steps run from a halting configuration lead to `none`. -/
+@[simp, scoped grind =]
+lemma step_iter_none_eq_none (cfg : tm.Cfg) (n : ℕ) (h_halt : cfg.state = none) :
+    (Option.bind · tm.step)^[n + 1] (some cfg) = none := by
+  rw [Function.iterate_succ_apply]
+  induction n with
+  | zero => simp [step, h_halt]
+  | succ n ih => grind [Function.iterate_succ_apply']
+
+/-- The initial configuration corresponding to a list in the input alphabet. -/
+@[simp]
+def initCfg (s : List Symbol) : tm.Cfg :=
+  ⟨some tm.q₀, s, 1, default, []⟩
+
+/-- The sequence of configurations of the Turing machine starting from `cfg`.
+If the Turing machine halts, it will eventually get and stay `none` after reaching the halting
+configuration. -/
+def configs (cfg : tm.Cfg) (t : ℕ) : Option tm.Cfg :=
+  (Option.bind · tm.step)^[t] cfg
+
+lemma configs_succ' (cfg : tm.Cfg) (t : ℕ) :
+    tm.configs cfg (t + 1) = (Option.bind · tm.step) (tm.configs cfg t) := by
+  simp [configs, Function.iterate_succ_apply']
+
+lemma configs_succ (cfg : tm.Cfg) (t : ℕ) :
+    tm.configs cfg (t + 1) = tm.configs cfg t >>= tm.step := by
+  simp [configs, Function.iterate_succ_apply']
+
+end Cfg
+
+section Space
+/-! Now we define space usage and add some helper lemmas. -/
+
+variable [Inhabited Symbol] [Fintype Symbol] (tm : MultiTapeTM k Symbol)
+
+/-- Convert an "optional movement" to an integer where positive is "right". -/
+@[simp, grind]
+def optionDirToInt : Option Dir → ℤ
+  | some .left => -1
+  | none => 0
+  | some .right => 1
+
+/-- The movements of the work tape heads after configuration `cfg`. -/
+def headMovements (cfg : tm.Cfg) : Fin k → ℤ
+  | i => match cfg.state with
+    | none => 0
+    | some q => optionDirToInt
+      (tm.transitionOutput q (tm.inputSymbol cfg) cfg.workTapes |>.stmts i |>.2)
+
+/-- The head positions of the work tapes as a function of the number of steps, relative to
+the starting position in `cfg`. -/
+def headPositions (cfg : tm.Cfg) (t : ℕ) : Fin k → ℤ
+  | i => ∑ t' ∈ Finset.range t, (tm.configs cfg t').elim 0 (tm.headMovements · i)
+
+/--
+The number of work tape cells touched by the head of tape `i` in the computation starting from
+configuration `cfg` up to step `t`.
+-/
+def spaceUsedByTape (cfg : tm.Cfg) (t : ℕ) (i : Fin k) : ℕ :=
+  let positions := (Finset.range (t + 1)).image (fun t' => tm.headPositions cfg t' i)
+  have ne := Finset.image_nonempty.mpr ⟨0, by simp⟩
+  (positions.max' ne - positions.min' ne).toNat + 1
+
+/--
+The number of work tape cells touched by a computation starting from configuration
+`cfg` up to step `t`.
+-/
+def spaceUsed (cfg : tm.Cfg) (t : ℕ) : ℕ := ∑ i, tm.spaceUsedByTape cfg t i
+
+/-- A zero-tape Turing machine uses zero space. -/
+@[simp]
+lemma spaceUsed_zero_tapes_eq_zero (cfg : tm.Cfg) (t : ℕ) (h_zero : k = 0) :
+    tm.spaceUsed cfg t = 0 := by
+  unfold spaceUsed
+  subst h_zero
+  simp
+
+@[scoped grind .]
+lemma OptionDirToInt_bound (d : Option Dir) :
+    -1 ≤ optionDirToInt d ∧ optionDirToInt d ≤ 1 := by
+  rcases d with _ | d
+  · decide
+  · rcases d <;> decide
+
+/-- A single step moves each work tape head by at most one cell. -/
+lemma step_head_movement_bound (cfg : tm.Cfg) (t : ℕ) (i : Fin k) :
+    -1 ≤ (tm.configs cfg t).elim 0 (tm.headMovements · i)
+      ∧ (tm.configs cfg t).elim 0 (tm.headMovements · i) ≤ 1 := by
+  unfold headMovements
+  dsimp
+  rcases h : tm.configs cfg t <;>
+  grind
+
+/-- The head position changes by the corresponding head movement on each step. -/
+lemma headPositions_succ (cfg : tm.Cfg) (t : ℕ) (i : Fin k) :
+    tm.headPositions cfg (t + 1) i
+      = tm.headPositions cfg t i + (tm.configs cfg t).elim 0 (tm.headMovements · i) := by
+  simp only [headPositions, Finset.sum_range_succ]
+
+/--
+Inserting one new point `a`, adjacent to an existing point `q` of `s`, widens the spanned
+interval `max' - min'` by at most one cell.
+-/
+private lemma span_insert_le {s S : Finset ℤ} (hs : s.Nonempty) (hS : S.Nonempty)
+    {a q : ℤ} (hSeq : S = insert a s) (hq : q ∈ s) (h1 : a ≤ q + 1) (h2 : q ≤ a + 1) :
+    (S.max' hS - S.min' hS).toNat ≤ (s.max' hs - s.min' hs).toNat + 1 := by
+  subst hSeq
+  rw [Finset.max'_insert _ _ hs, Finset.min'_insert _ _ hs]
+  have hm := Finset.min'_le _ _ hq
+  have hM := Finset.le_max' _ _ hq
+  grind
+
+/-- The number of cells touched by a single work tape grows by at most one each step. -/
+lemma spaceUsedByTape_succ_le (cfg : tm.Cfg) (t : ℕ) (i : Fin k) :
+    tm.spaceUsedByTape cfg (t + 1) i ≤ tm.spaceUsedByTape cfg t i + 1 := by
+  unfold spaceUsedByTape
+  have hs := tm.headPositions_succ cfg t i
+  have step_bound := tm.step_head_movement_bound cfg t i
+  apply Nat.add_le_add_right
+  refine span_insert_le _ _
+    (by rw [Finset.range_add_one, Finset.image_insert])
+    (by exact Finset.mem_image_of_mem _ (Finset.mem_range.mpr (Nat.lt_succ_self t)))
+    (by grind)
+    (by grind)
+
+/--
+The space used by a configuration grows by at most `k` each step.
+-/
+lemma spaceUsed_linear (cfg : tm.Cfg) (t : ℕ) :
+    tm.spaceUsed cfg (t + 1) ≤ tm.spaceUsed cfg t + k := by
+  calc tm.spaceUsed cfg (t + 1)
+      ≤ ∑ i, (tm.spaceUsedByTape cfg t i + 1) :=
+        Finset.sum_le_sum fun i _ => tm.spaceUsedByTape_succ_le cfg t i
+    _ = (∑ i, tm.spaceUsedByTape cfg t i) + k := by simp [Finset.sum_add_distrib]
+
+end Space
+
+open Cfg
+
+variable [Inhabited Symbol] [Fintype Symbol]
+
+/--
+The `TransitionRelation` corresponding to a `MultiTapeTM k Symbol`
+is defined by the `step` function,
+which maps a configuration to its next configuration, if it exists.
+-/
+@[scoped grind =]
+def TransitionRelation (tm : MultiTapeTM k Symbol) (c₁ c₂ : tm.Cfg) : Prop :=
+  tm.step c₁ = some c₂
+
+/-- A proof that the Turing machine `tm` on input `input` outputs `output` in exactly `t` steps
+and uses at most `s` space. -/
+def ComputesInTimeAndSpace
+    (tm : MultiTapeTM k Symbol)
+    (input output : List Symbol)
+    (t s : ℕ) : Prop :=
+  ∃ cfg,
+  cfg.state = none ∧
+  cfg.output = output ∧
+  RelatesInSteps tm.TransitionRelation (tm.initCfg input) cfg t ∧
+  tm.spaceUsed (tm.initCfg input) t = s
+
+/-- A proof that the Turing machine `tm` computes the function `f` such that on all inputs of
+length `n` it uses at most `t n` steps and `s n` space. -/
+def ComputesFunInTimeAndSpace
+    (tm : MultiTapeTM k Symbol)
+    (f : List Symbol → List Symbol)
+    (t s : ℕ → ℕ) : Prop :=
+  ∀ input, ∃ t' ≤ t input.length, ∃ s' ≤ s input.length,
+  ComputesInTimeAndSpace tm input (f input) t' s'
+
+open Classical in
+/-- The indicator function of a language. -/
+noncomputable def indicator (L : Language Symbol) : List Symbol → List Symbol
+  | x => if x ∈ L then [default] else []
+
+/-- A proof that a Turing machine `tm` decides a language `l` with time and space bounds. -/
+def DecidesLanguageInTimeAndSpace
+    (tm : MultiTapeTM k Symbol)
+    (L : Language Symbol)
+    (t s : ℕ → ℕ) : Prop :=
+  ComputesFunInTimeAndSpace tm (indicator L) t s
+
+/-- This lemma translates between the relational notion and the iterated step notion. The latter
+can be more convenient especially for deterministic machines as we have here. -/
+@[scoped grind =]
+lemma relatesInSteps_iff_step_iter_eq_some
+    (tm : MultiTapeTM k Symbol)
+    (cfg₁ cfg₂ : tm.Cfg)
+    (t : ℕ) :
+  RelatesInSteps tm.TransitionRelation cfg₁ cfg₂ t ↔
+    (Option.bind · tm.step)^[t] cfg₁ = .some cfg₂ := by
+  induction t generalizing cfg₁ cfg₂ with
+  | zero => simp
+  | succ t ih =>
+    rw [RelatesInSteps.succ_iff, Function.iterate_succ_apply']
+    constructor
+    · grind
+    · intro h_configs
+      cases h : (Option.bind · tm.step)^[t] cfg₁ with
+      | none => grind
+      | some cfg' =>
+        use cfg'
+        grind
+
+/-- The Turing machine `tm` halts after exactly `t` steps on input `input`. -/
+def haltsAtStep (tm : MultiTapeTM k Symbol) (input : List Symbol) (t : ℕ) : Bool :=
+  match (tm.configs (tm.initCfg input) t) with
+  | some ⟨none, _, _, _, _⟩ => true
+  | _ => false
+
+/-- If a Turing machine halts, the time step is uniquely determined. -/
+lemma halting_step_unique
+    {tm : MultiTapeTM k Symbol}
+    {input : List Symbol}
+    {t₁ t₂ : ℕ}
+    (h_halts₁ : tm.haltsAtStep input t₁)
+    (h_halts₂ : tm.haltsAtStep input t₂) :
+    t₁ = t₂ := by
+  wlog h : t₁ ≤ t₂
+  · exact (this h_halts₂ h_halts₁ (Nat.le_of_not_le h)).symm
+  obtain ⟨d, rfl⟩ := Nat.exists_eq_add_of_le h
+  cases d with
+  | zero => rfl
+  | succ d =>
+    unfold haltsAtStep configs at h_halts₁ h_halts₂
+    rw [Nat.add_comm t₁ (d + 1), Function.iterate_add_apply] at h_halts₂
+    grind
+
+/-- At the halting step, the configuration sequence of a Turing machine is still `some`. -/
+lemma configs_isSome_of_haltsAtStep
+    {tm : MultiTapeTM k Symbol} {input : List Symbol} {t : ℕ}
+    (h_halts : tm.haltsAtStep input t) :
+    (tm.configs (tm.initCfg input) t).isSome := by
+  grind [haltsAtStep]
+
+
+end MultiTapeTM
+
+end Turing
diff --git a/Cslib/Computability/Machines/MultiTapeTuring/Simulations.lean b/Cslib/Computability/Machines/MultiTapeTuring/Simulations.lean
new file mode 100644
index 0000000000..daf485a9cb
--- /dev/null
+++ b/Cslib/Computability/Machines/MultiTapeTuring/Simulations.lean
@@ -0,0 +1,147 @@
+/-
+Copyright (c) 2026 Christian Reitwiessner. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Christian Reitwiessner
+-/
+
+module
+
+public import Cslib.Computability.Machines.SingleTapeTuring.Basic
+public import Cslib.Computability.Machines.MultiTapeTuring.Basic
+public import Mathlib.Computability.DFA
+public import Mathlib.Data.Fin.VecNotation
+public import Mathlib.Tactic.FinCases
+
+/-!
+# Simulations between different machines
+
+
+-/
+
+@[expose] public section
+
+open Cslib Relation Turing.BiTape Turing.MultiTapeTM.Cfg
+
+namespace Turing
+
+variable {Symbol : Type} [Inhabited Symbol] [Fintype Symbol]
+
+namespace MultiTapeTM
+
+section SingleTapeTMSimulation
+/-! Simulation of a single-tape TM by a multi-tape TM. -/
+
+variable (tm : SingleTapeTM Symbol)
+
+-- Stages of simulating a single-tape TM in a multi-tape TM:
+-- 1. copy input to work tape
+-- 2. move to start of work tape
+-- 3. run single-tape-tm on work tape
+-- 4. copy output to output tape and halt
+
+
+inductive SimState where
+  | copyInput -- copy from the input tape to the work tape
+  | moveToStart -- move to the start of the work tape
+  | runSingleTape (q : tm.State) -- simulate single-tape TM on work tape
+  | copyOutput -- copy output to output tape
+deriving Fintype
+
+def SimTr :
+    (SimState tm) → (Option Symbol) → (Fin 1 → Option Symbol) → TransitionOut 1 Symbol (SimState tm)
+  | .copyInput => fun input _ => match input with
+    | none => ⟨none, fun _ => ⟨none, some .left⟩, none, some .moveToStart⟩
+    | some c => ⟨some .right, fun _ => ⟨some (some c), some .right⟩, none, some .copyInput⟩
+  | .moveToStart => fun _ syms => match syms 0 with
+    | some _ => ⟨none, fun _ => ⟨none, some .left⟩, none, some .moveToStart⟩
+    | none => ⟨none, fun _ => ⟨none, some .right⟩, none, some (.runSingleTape tm.q₀)⟩
+  | .runSingleTape q => fun _ syms => match tm.tr q (syms 0) with
+    | ⟨⟨w, m⟩, some q'⟩ => ⟨none, fun _ => ⟨some w, m⟩, none, some (.runSingleTape q')⟩
+    | ⟨⟨w, m⟩, none⟩ => ⟨none, fun _ => ⟨some w, m⟩, none, some .copyOutput⟩
+  | .copyOutput => fun _ syms => match syms 0 with
+    | some c => ⟨none, fun _ => ⟨none, some .right⟩, some c, some .copyOutput⟩
+    | none => ⟨none, fun _ => ⟨none, none⟩, none, none⟩
+
+def MultiFromSingle : MultiTapeTM (k := 1) Symbol where
+  State := SimState tm
+  q₀ := .copyInput
+  tr := SimTr tm
+
+-- TODO re-prove this using RelatesInSteps?
+
+lemma copyInput_innerStep
+    (input : List Symbol) (t : ℕ) (h_lt : t ≤ input.length) :
+    (MultiFromSingle tm).configs ((MultiFromSingle tm).initCfg input) t =
+      some ⟨some .copyInput, input, ⟨1 + t, by omega⟩,
+            fun _ => (BiTape.mk₁ (input.take t)).moveInt t, []⟩ := by
+  induction t with
+  | zero =>
+    simp [configs, Function.iterate_zero, initCfg, MultiFromSingle, moveInt]
+  | succ t ih =>
+    have hinput (work : BiTape Symbol) : (MultiFromSingle tm).inputSymbol
+        ⟨some .copyInput, input, ⟨1 + t, by omega⟩, fun _ => work, []⟩ = some input[t] := by
+      grind
+    have htransitionOut (work : BiTape Symbol) :
+        (MultiFromSingle tm).transitionOutput .copyInput (some input[t]) (fun _ => work) =
+        ⟨some .right, fun _ => ⟨some input[t], some .right⟩, none, some .copyInput⟩ := by
+      unfold MultiFromSingle SimTr
+      simp [transitionOutput]
+    have htape : (((mk₁ (List.take t input)).moveInt ↑t).write (some input[t])).move Dir.right =
+        (mk₁ (List.take (t + 1) input)).moveInt (↑t + 1) := by
+      ext1 i
+      simp [Function.update]
+      grind
+    rw [configs_succ, ih (by omega)]
+    simp [step, hinput, htransitionOut, moveInputPos, htape]
+    grind
+
+lemma copyInput_lastStep
+    (input : List Symbol) (work : BiTape Symbol) :
+    (MultiFromSingle tm).step
+      ⟨some .copyInput, input, ⟨1 + input.length, by omega⟩, fun _ => work, []⟩ =
+      some ⟨some .moveToStart, input, ⟨1 + input.length, by omega⟩,
+          fun _ => work.moveLeft, []⟩ := by
+  have hinput : (MultiFromSingle tm).inputSymbol
+      ⟨some .copyInput, input, ⟨1 + input.length, by omega⟩, fun _ => work, []⟩ = none := by
+    grind
+  have htransitionOut :
+      (MultiFromSingle tm).transitionOutput .copyInput none (fun _ => work) =
+      ⟨none, fun _ => ⟨none, some .left⟩, none, some .moveToStart⟩ := by
+    unfold MultiFromSingle SimTr
+    simp [transitionOutput]
+  simp [step, hinput, htransitionOut]
+  grind
+
+lemma moveToStart_semantics (input work : List Symbol) (ip : Fin (input.length + 2))
+    (h_ip : ip ≠ 0 ∧ ip ≠ input.length + 1)
+    (t : ℕ) (h_lt : t < work.length - 1) :
+    RelatesInSteps (MultiFromSingle tm).TransitionRelation
+      ⟨some .moveToStart, input, ip, fun _ => (BiTape.mk₁ work).moveInt (t - 1), []⟩
+      ⟨some .moveToStart, input, ip, fun _ => (BiTape.mk₁ work).moveInt (-1), []⟩
+      t := by
+  induction t with
+  | zero => simp [RelatesInSteps.zero_iff]
+  | succ t ih =>
+    specialize ih (by omega)
+    rw [RelatesInSteps.succ'_iff]
+    refine ⟨⟨some .moveToStart, input, ip, fun _ => (BiTape.mk₁ work).moveInt (t - 1), []⟩, ?_, ih⟩
+    have h_inputSymbol : (MultiFromSingle tm).inputSymbol
+        ⟨some .moveToStart, input, ip, fun _ => (BiTape.mk₁ work).moveInt t, []⟩ ≠ none := by
+      unfold inputSymbol
+      simp [h_ip]
+    have htout (c : Option Symbol) (h_c : c ≠ none) : (MultiFromSingle tm).transitionOutput
+          .moveToStart c (fun _ => (BiTape.mk₁ work).moveInt t) =
+        ⟨none, fun _ => ⟨none, some .left⟩, none, some .moveToStart⟩ := by
+      unfold MultiFromSingle SimTr
+      simp [transitionOutput]
+      grind
+    simp [TransitionRelation, step, move_eq_moveInt, BiTape.optionDirToInt, htout _ h_inputSymbol]
+    grind
+
+
+
+end SingleTapeTMSimulation
+
+end MultiTapeTM
+
+end Turing
diff --git a/Cslib/Foundations/Data/BiTape.lean b/Cslib/Foundations/Data/BiTape.lean
index e61272d57d..256bf1e29d 100644
--- a/Cslib/Foundations/Data/BiTape.lean
+++ b/Cslib/Foundations/Data/BiTape.lean
@@ -56,6 +56,8 @@ namespace BiTape
 
 variable {Symbol : Type}
 
+-- TODO remove this definition, just use `default`.
+
 /-- The empty `BiTape` -/
 def nil : BiTape Symbol := ⟨none, ∅, ∅⟩
 
@@ -68,6 +70,9 @@ instance : EmptyCollection (BiTape Symbol) :=
 @[simp]
 lemma empty_eq_nil : (∅ : BiTape Symbol) = nil := rfl
 
+@[simp]
+lemma nil_eq_default : (default : BiTape Symbol) = nil := rfl
+
 /--
 Given a `List` of `Symbol`s, construct a `BiTape` by mapping the list to `some` elements
 and laying them out to the right side,
@@ -78,6 +83,47 @@ def mk₁ (l : List Symbol) : BiTape Symbol :=
   | [] => ∅
   | h :: t => { head := some h, left := ∅, right := StackTape.mapSome t }
 
+@[simp, scoped grind =]
+lemma mk₁_nil : mk₁ ([] : List Symbol) = nil := rfl
+
+open scoped Int in
+/-- Returns the tape symbol at positon `p` relative to the head, where
+positive numbers are right of the head and negative are left of the head. -/
+@[scoped grind]
+def get (t : BiTape Symbol) : ℤ → Option Symbol
+  | 0 => t.head
+  | (p' + 1 : Nat) => t.right.toList[p']?.getD none
+  | -[p'+1] => t.left.toList[p']?.getD none
+
+/-- Two tapes are equal if and only if their `get` functions are equal. This allows to view
+tapes as functions `ℤ → Option Symbol`. -/
+@[ext]
+lemma ext_get (t₁ t₂ : BiTape Symbol) (h_get_eq : ∀ p, t₁.get p = t₂.get p) : t₁ = t₂ := by
+  cases t₁
+  congr
+  · simpa [get] using h_get_eq 0
+  · apply StackTape.ext_get
+    intro p
+    simpa [get] using h_get_eq (Int.negSucc p)
+  · apply StackTape.ext_get
+    intro p
+    sorry --simpa [get] using h_get_eq (p + 1)
+
+/-- Simplification lemma that explains the contents of each of the cells after tape
+construction using mk₁. -/
+@[simp, scoped grind =]
+lemma get_mk₁ (l : List Symbol) (p : ℤ) :
+  (mk₁ l).get p = if p < 0 then none else l[p.toNat]? := by
+  match p with
+  | Int.ofNat 0 => cases l <;> simp [mk₁, get, nil]
+  | Int.ofNat (n + 1) =>
+    cases l with
+    | nil => simp [mk₁, get, nil]
+    | cons h t =>
+      simp only [mk₁, get, StackTape.mapSome]
+      grind
+  | Int.negSucc n => cases l <;> simp [mk₁, get, nil]
+
 section Move
 
 /--
@@ -95,6 +141,7 @@ def moveRight (t : BiTape Symbol) : BiTape Symbol :=
 /--
 Move the head to the left or right, shifting the tape underneath it.
 -/
+@[scoped grind =]
 def move (t : BiTape Symbol) : Dir → BiTape Symbol
   | .left => t.moveLeft
   | .right => t.moveRight
@@ -102,6 +149,7 @@ def move (t : BiTape Symbol) : Dir → BiTape Symbol
 /--
 Optionally perform a `move`, or do nothing if `none`.
 -/
+@[simp, scoped grind =]
 def optionMove : BiTape Symbol → Option Dir → BiTape Symbol
   | t, none => t
   | t, some d => t.move d
@@ -114,6 +162,101 @@ lemma moveLeft_moveRight (t : BiTape Symbol) : t.moveLeft.moveRight = t := by
 lemma moveRight_moveLeft (t : BiTape Symbol) : t.moveRight.moveLeft = t := by
   simp [moveLeft, moveRight]
 
+/-- Translate an optional direction into a head movement offset, where the positive
+direction is to the right. -/
+@[scoped grind =]
+def optionDirToInt (d : Option Dir) : ℤ :=
+  match d with
+  | none => 0
+  | some .left => -1
+  | some .right => 1
+
+@[simp, scoped grind =]
+lemma get_moveLeft (t : BiTape Symbol) (p : ℤ) : t.moveLeft.get p = t.get (p - 1) := by
+  unfold moveLeft get
+  match p with
+  | Int.ofNat 0 =>
+    simp [StackTape.head_eq_getD]
+    rfl
+  | Int.ofNat 1 => simp
+  | Int.ofNat (n + 2) =>
+    rw [show Int.ofNat (n + 2) - 1 = Int.ofNat (n + 1) by lia]
+    simp
+  | Int.negSucc n => simp
+
+@[simp, scoped grind =]
+lemma get_move_right (t : BiTape Symbol) (p : ℤ) : t.moveRight.get p = t.get (p + 1) := by
+  unfold moveRight get
+  match p with
+  | Int.ofNat n =>
+    rw [show Int.ofNat n + 1 = Int.ofNat (n + 1) by lia]
+    cases n <;> simp [StackTape.head_eq_getD]
+  | Int.negSucc 0 => simp
+  | Int.negSucc (n + 1) =>
+    rw [show Int.negSucc (n + 1) + 1 = Int.negSucc n from rfl]
+    simp
+
+@[simp, scoped grind =]
+lemma get_optionMove (t : BiTape Symbol) (d : Option Dir) (p : ℤ) :
+    (t.optionMove d).get p = t.get (p + optionDirToInt d) := by
+  unfold optionMove optionDirToInt
+  grind [move]
+
+@[simp, scoped grind =]
+lemma get_move (t : BiTape Symbol) (d : Dir) (p : ℤ) :
+    (t.move d).get p = t.get (p + optionDirToInt (some d)) := by
+  cases d <;> grind
+
+@[simp, scoped grind =]
+lemma get_moveRight_iterate (t : BiTape Symbol) (n : ℕ) (p : ℤ) :
+    (moveRight^[n] t).get p = t.get (p + n):= by
+  induction n generalizing t p with
+  | zero => simp
+  | succ n ih => simp [Function.iterate_succ_apply, ih, Int.add_assoc]
+
+@[simp, scoped grind =]
+lemma get_moveLeft_iterate (t : BiTape Symbol) (n : ℕ) (p : ℤ) :
+    (moveLeft^[n] t).get p = t.get (p - n):= by
+  induction n generalizing t p with
+  | zero => simp
+  | succ n ih =>
+    have : p - n - 1 = p - (n + 1) := by lia
+    simp [Function.iterate_succ_apply, ih, this]
+
+/-- Move the tape head by an integer amount where positive numbers move the head to the right and
+negative to the left. -/
+def moveInt (t : BiTape Symbol) (Δ : ℤ) : BiTape Symbol :=
+  if Δ ≥ 0 then
+    .moveRight^[Δ.toNat] t
+  else
+    .moveLeft^[(-Δ).toNat] t
+
+/-- Simplification lemma that connects `moveInt` and the function view via `get`. -/
+@[simp, scoped grind =]
+lemma get_moveInt (t : BiTape Symbol) (Δ p : ℤ) :
+  (moveInt t Δ).get p = t.get (p + Δ) := by
+  grind [moveInt]
+
+@[simp, scoped grind =]
+lemma moveInt_head (t : BiTape Symbol) (Δ : ℤ) :
+  (moveInt t Δ).head = t.get Δ := by
+  rw [show (moveInt t Δ).head = (moveInt t Δ).get 0 from rfl]
+  grind [moveInt]
+
+@[simp, scoped grind =]
+lemma moveInt_moveInt (t : BiTape Symbol) (Δ₁ Δ₂ : ℤ) :
+  (t.moveInt Δ₁).moveInt Δ₂ = t.moveInt (Δ₁ + Δ₂) := by
+  sorry
+
+lemma move_eq_moveInt (t : BiTape Symbol) (d : Dir) : t.move d = t.moveInt (optionDirToInt (some d)) := by
+  sorry
+
+lemma moveLeft_eq_moveInt (t : BiTape Symbol) : t.moveLeft = t.moveInt (-1) := by
+  sorry
+
+lemma moveRight_eq_moveInt (t : BiTape Symbol) : t.moveRight = t.moveInt 1 := by
+  sorry
+
 end Move
 
 /--
@@ -121,6 +264,16 @@ Write a value under the head of the `BiTape`.
 -/
 def write (t : BiTape Symbol) (a : Option Symbol) : BiTape Symbol := { t with head := a }
 
+@[simp, scoped grind =]
+lemma get_write (t : BiTape Symbol) (a : Option Symbol) :
+    (t.write a).get = Function.update t.get 0 a := by
+  unfold write get Function.update
+  funext p
+  match p with
+  | Int.ofNat 0 => simp
+  | Int.ofNat (n + 1) => grind
+  | Int.negSucc n => simp
+
 /--
 The space used by a `BiTape` is the number of symbols
 between and including the head, and leftmost and rightmost non-blank symbols on the `BiTape`.
diff --git a/Cslib/Foundations/Data/StackTape.lean b/Cslib/Foundations/Data/StackTape.lean
index a252582b02..94383a1706 100644
--- a/Cslib/Foundations/Data/StackTape.lean
+++ b/Cslib/Foundations/Data/StackTape.lean
@@ -106,6 +106,25 @@ def head (l : StackTape Symbol) : Option Symbol :=
   | [] => none
   | h :: _ => h
 
+@[scoped grind =]
+lemma head_eq_getD (s : StackTape Symbol) : s.head = s.toList[0]?.getD none := by
+  unfold head; cases s.toList <;> simp
+
+@[simp, scoped grind =]
+lemma tail_getElem? (s : StackTape Symbol) (n : ℕ) :
+    s.tail.toList[n]? = s.toList[n + 1]? := by
+  cases s with | mk l h => cases l <;> simp [tail, nil]
+
+@[simp, scoped grind =]
+lemma cons_getD_zero (x : Option Symbol) (s : StackTape Symbol) :
+    (cons x s).toList[0]?.getD none = x := by
+  cases x <;> (cases s with | mk l h => cases l <;> simp [cons])
+
+@[simp, scoped grind =]
+lemma cons_getD_succ (x : Option Symbol) (s : StackTape Symbol) (n : ℕ) :
+    (cons x s).toList[n + 1]?.getD none = s.toList[n]?.getD none := by
+  cases x <;> (cases s with | mk l h => cases l <;> simp [cons])
+
 lemma eq_iff (l1 l2 : StackTape Symbol) :
     l1 = l2 ↔ l1.head = l2.head ∧ l1.tail = l2.tail := by
   constructor
@@ -115,13 +134,23 @@ lemma eq_iff (l1 l2 : StackTape Symbol) :
     cases l2 with | mk as2 h2 =>
     cases as1 <;> cases as2 <;> grind
 
+@[ext]
+lemma ext (t₁ t₂ : StackTape Symbol) (h_toList_eq : t₁.toList = t₂.toList) : t₁ = t₂ := by
+  obtain ⟨t₁, h₁⟩ := t₁
+  obtain ⟨t₂, h₂⟩ := t₂
+  simpa using h_toList_eq
+
+@[ext]
+lemma ext_get (t₁ t₂ : StackTape Symbol)
+    (h_get_eq : ∀ p : ℕ, t₁.toList[p]?.getD none = t₂.toList[p]?.getD none) :
+    t₁ = t₂ := by
+  obtain ⟨l₁, h₁⟩ := t₁
+  obtain ⟨l₂, h₂⟩ := t₂
+  sorry --grind [List.ext_getElem]
+
 @[simp]
 lemma head_cons (o : Option Symbol) (l : StackTape Symbol) : (cons o l).head = o := by
-  cases o with
-  | none =>
-    cases l with | mk toList hl =>
-    cases toList <;> grind
-  | some a => grind
+  grind
 
 @[simp]
 lemma tail_cons (o : Option Symbol) (l : StackTape Symbol) : (cons o l).tail = l := by