diff --git a/.gitignore b/.gitignore
index 94f4582b..85b216ae 100644
--- a/.gitignore
+++ b/.gitignore
@@ -14,3 +14,4 @@
 /docs/Std-manifest.json.hash
 /docs/Std-manifest.json.trace
 .DS_Store
+.claude
diff --git a/Cslib/Computability/Machines/SingleTapeTuring/Basic.lean b/Cslib/Computability/Machines/SingleTapeTuring/Basic.lean
new file mode 100644
index 00000000..a5756591
--- /dev/null
+++ b/Cslib/Computability/Machines/SingleTapeTuring/Basic.lean
@@ -0,0 +1,605 @@
+/-
+Copyright (c) 2025 Bolton Bailey. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Bolton Bailey TODO add the authors of the mathlib file this is based on
+-/
+
+module
+
+public import Cslib.Foundations.Data.OTape
+public import Cslib.Foundations.Semantics.ReductionSystem.Basic
+public import Mathlib.Algebra.Polynomial.Eval.Defs
+
+@[expose] public section
+
+/-!
+# Single-Tape Turing Machine
+
+Defines a single-tape Turing machine over the alphabet of `Option α`,
+where `none` represents a blank `OTape` symbol.
+
+## TODOs
+
+- encoding?
+- refactor polynomial time to another file?
+
+-/
+
+open Cslib
+
+namespace Turing
+
+variable {α : Type}
+
+namespace SingleTapeTM
+
+-- TODO make into a structure?
+/--
+A Turing machine "statement" is just a `Option`al command to move left or right,
+and write a symbol on the `OTape`.
+-/
+def Stmt (α : Type) := Option α × Option Dir
+deriving Inhabited
+
+def Stmt.symbol : Stmt α → Option α
+  | (symbol, _) => symbol
+
+def Stmt.movement : Stmt α → Option Dir
+  | (_, movement) => movement
+
+end SingleTapeTM
+
+/-- A SingleTapeTM over the alphabet of Option α (none is blank OTape symbol). -/
+structure SingleTapeTM α where
+  /-- Inhabited instance for the alphabet -/
+  [Inhabitedα : Inhabited α]
+  /-- Finiteness of the alphabet -/
+  [Fintypeα : Fintype α]
+  /-- type of state labels -/
+  (Λ : Type)
+  /-- finiteness of the state type -/
+  [FintypeΛ : Fintype Λ]
+  /-- Initial state -/
+  (q₀ : Λ)
+  /-- Transition function, mapping a state and a head symbol
+  to a Stmt to invoke, and optionally a new state (none for halt) -/
+  (M : Λ → (Option α) → (Turing.SingleTapeTM.Stmt α × Option Λ))
+
+namespace SingleTapeTM
+
+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 (tm : SingleTapeTM α)
+
+instance : Inhabited tm.Λ :=
+  ⟨tm.q₀⟩
+
+instance : Fintype tm.Λ :=
+  tm.FintypeΛ
+
+instance inhabitedStmt : Inhabited (Stmt α) := inferInstance
+
+/--
+The configurations of a Turing machine consist of an `Option`al state
+(or none for the halting state)
+and an OTape representing the tape contents.
+-/
+structure Cfg : Type where
+  /-- the state of the TM (or none for the halting state) -/
+  state : Option tm.Λ
+  /-- the OTape contents -/
+  OTape : OTape α
+deriving Inhabited
+
+/-- The step function corresponding to this TM. -/
+@[simp]
+def step : tm.Cfg → Option tm.Cfg :=
+  fun ⟨q, t⟩ =>
+    match q with
+    -- If in the halting state, there is no next configuration
+    | none => none
+    -- If in state q'
+    | some q' =>
+      -- Look up the transition function
+      match tm.M q' t.head with
+      | ⟨(wr, dir), q''⟩ =>
+          -- enter a new configuration
+          some ⟨
+            -- With state q'' (or none for halting)
+            q'',
+            -- And OTape updated according to the Stmt
+            (t.write wr).move? dir⟩
+
+/-- The initial configuration corresponding to a list in the input alphabet. -/
+def initCfg (tm : SingleTapeTM α) (s : List α) : tm.Cfg := ⟨some tm.q₀, OTape.mk₁ s⟩
+
+/-- The final configuration corresponding to a list in the output alphabet.
+(We demand that the head halts at the leftmost position of the output.)
+-/
+def haltCfg (tm : SingleTapeTM α) (s : List α) : tm.Cfg := ⟨none, OTape.mk₁ s⟩
+
+def Cfg.space_used (tm : SingleTapeTM α) (cfg : tm.Cfg) : ℕ :=
+  cfg.OTape.space_used
+
+lemma Cfg.space_used_initCfg (tm : SingleTapeTM α) (s : List α) :
+    (tm.initCfg s).space_used = max 1 s.length := by
+  simp only [space_used, initCfg, OTape.space_used_mk₁]
+
+lemma Cfg.space_used_haltCfg (tm : SingleTapeTM α) (s : List α) :
+    (tm.haltCfg s).space_used = max 1 s.length := by
+  simp [haltCfg, Cfg.space_used, OTape.space_used_mk₁]
+
+lemma Cfg.space_used_step {tm : SingleTapeTM α} (cfg cfg' : tm.Cfg)
+    (hstep : tm.step cfg = some cfg') : cfg'.space_used ≤ cfg.space_used + 1 := by
+  obtain ⟨_ | q, tape⟩ := cfg
+  · simp [step] at hstep
+  · simp only [step] at hstep
+    generalize hM : tm.M q tape.head = result at hstep
+    obtain ⟨⟨wr, dir⟩, q''⟩ := result
+    cases hstep; cases dir with
+    | none => simp [Cfg.space_used, OTape.move?, OTape.space_used_write]
+    | some d =>
+      have := OTape.space_used_move (tape.write wr) d
+      simp only [Cfg.space_used, OTape.move?, OTape.space_used_write] at this ⊢; exact this
+
+end Cfg
+
+/--
+The `TerminalReductionSystem` corresponding to a `SingleTapeTM α`
+is defined by the `step` function,
+which maps a configuration to its next configuration if it exists.
+-/
+def TerminalReductionSystem (tm : SingleTapeTM α) : Cslib.TerminalReductionSystem (tm.Cfg) :=
+  TerminalReductionSystem.Option tm.step
+
+/-- A proof of tm outputting l' when given l. -/
+def Outputs (tm : SingleTapeTM α) (l : List α) (l' : List α) : Prop :=
+  tm.TerminalReductionSystem.MRed (initCfg tm l) (haltCfg tm l')
+
+/-- A proof of tm outputting l' when given l in at most m steps. -/
+def OutputsWithinTime (tm : SingleTapeTM α) (l : List α) (l' : List α)
+    (m : ℕ) :=
+  tm.TerminalReductionSystem.reducesToWithinSteps (initCfg tm l) (haltCfg tm l') m
+
+/--
+This lemma bounds the size blow-up of the output of a Turing machine.
+It states that the increase in length of the output over the input is bounded by the runtime.
+This is important for guaranteeing that composition of polynomial time Turing machines
+remains polynomial time, as the input to the second machine
+is bounded by the output length of the first machine.
+-/
+lemma output_length_le_input_length_add_time (tm : SingleTapeTM α) (l l' : List α) (t : ℕ)
+    (h : tm.OutputsWithinTime l l' t) :
+    l'.length ≤ max 1 l.length + t := by
+  simp only [OutputsWithinTime] at h
+  obtain ⟨steps, hsteps_le, hevals⟩ := h
+  replace hevals := hevals.bounded_increase
+  specialize hevals (Cfg.space_used tm)
+  simp only [Cfg.space_used_initCfg, Cfg.space_used_haltCfg] at hevals
+  suffices l'.length ≤ max 1 l.length + steps
+    by omega
+  specialize hevals fun a b hstep ↦ Cfg.space_used_step a b (Option.mem_def.mp hstep)
+  omega
+
+/-- A Turing machine + a proof it outputsInTime `f`. -/
+structure Computable (f : List α → List α) where
+  /-- the underlying bundled SingleTapeTM -/
+  tm : SingleTapeTM α
+  /-- a proof this machine outputsInTime `f` -/
+  outputsFun : ∀ a, tm.Outputs a (f a)
+
+/-- A Turing machine + a time function +
+a proof it outputsInTime `f` in at most `time(input.length)` steps. -/
+structure TimeComputable (f : List α → List α) where
+  /-- the underlying bundled SingleTapeTM -/
+  tm : SingleTapeTM α
+  /-- a time function -/
+  time : ℕ → ℕ
+  /-- proof this machine outputsInTime `f` in at most `time(input.length)` steps -/
+  outputsFun : ∀ a, tm.OutputsWithinTime a (f a) (time a.length)
+
+section
+
+variable [Inhabited α] [Fintype α]
+
+/-- A Turing machine computing the identity. -/
+def idComputer : SingleTapeTM α where
+  Λ := PUnit
+  q₀ := PUnit.unit
+  M := fun _ b => ⟨(b, none), none⟩
+
+-- TODO switch to where syntax
+/-- A proof that the identity map on α is computable in time. -/
+def TimeComputable.id : TimeComputable (α := α) id :=
+  ⟨idComputer, fun _ => 1, fun x => by
+    refine ⟨1, le_refl 1, ?_⟩
+    -- Need to show reducesToInSteps for 1 step
+    refine Cslib.ReductionSystem.reducesToInSteps.cons _ _ _ 0 ?_
+      (Cslib.ReductionSystem.reducesToInSteps.refl _)
+    -- Show the single step reduction: step (init x) = some (halt x)
+    simp only [TerminalReductionSystem, Cslib.TerminalReductionSystem.Option, initCfg, haltCfg,
+      idComputer, step, OTape.move?]
+    congr 1⟩
+
+def compComputer {f : List α → List α} {g : List α → List α}
+    (hf : TimeComputable f)
+    (hg : TimeComputable g) :
+    SingleTapeTM α :=
+  {
+    Λ := hf.tm.Λ ⊕ hg.tm.Λ
+    q₀ := Sum.inl hf.tm.q₀
+    M := fun q h =>
+      match q with
+      -- If we are in the first machine's states, run that machine
+      | Sum.inl ql => match hf.tm.M ql (h) with
+        -- The action should be the same, and the state should either be the corresponding state
+        -- in the first machine, or transition to the start state of the second machine if halting
+        | (ql', stmt) => (ql',
+            match stmt with
+            -- If it halts, transition to the start state of the second machine
+            | none => some (Sum.inr hg.tm.q₀)
+            -- Otherwise continue as normal
+            | _ => Option.map Sum.inl stmt)
+      -- If we are in the second machine's states, run that machine
+      | Sum.inr qr =>
+        match hg.tm.M qr (h) with
+        -- The action should be the same, and the state should be the corresponding state
+        -- in the second machine, or halting if the second machine halts
+        | (qr', stmt) => (qr',
+            match stmt with
+            -- If it halts, transition to the halting state
+            | none => none
+            -- Otherwise continue as normal
+            | _ => Option.map Sum.inr stmt)
+  }
+
+lemma compComputer_q₀_eq (f : List α → List α) (g : List α → List α)
+  (hf : TimeComputable f) (hg : TimeComputable g) :
+    (compComputer hf hg).q₀ = Sum.inl hf.tm.q₀ :=
+  rfl
+
+/-- Lift a config over a tm to a config over the comp -/
+def liftCompCfg_left {f : List α → List α} {g : List α → List α}
+    (hf : TimeComputable f) (hg : TimeComputable g)
+    (cfg : hf.tm.Cfg) :
+    (compComputer hf hg).Cfg :=
+  {
+    state := Option.map Sum.inl cfg.state
+    OTape := cfg.OTape
+  }
+
+def liftCompCfg_right {f : List α → List α} {g : List α → List α}
+    (hf : TimeComputable f) (hg : TimeComputable g)
+    (cfg : hg.tm.Cfg) :
+    (compComputer hf hg).Cfg :=
+  {
+    state := Option.map Sum.inr cfg.state
+    OTape := cfg.OTape
+  }
+
+theorem map_liftCompCfg_left_step
+    {f : List α → List α} {g : List α → List α}
+    (hf : TimeComputable f) (hg : TimeComputable g)
+    (x : hf.tm.Cfg) (hx : ∀ cfg, hf.tm.step x = some cfg → cfg.state.isSome) :
+    Option.map (liftCompCfg_left hf hg) (hf.tm.step x) =
+      (compComputer hf hg).step (liftCompCfg_left hf hg x) := by
+  cases x with
+  | mk state OTape =>
+    cases state with
+    | none =>
+      -- x is already in halting state, step returns none on both sides
+      simp only [step, liftCompCfg_left, Option.map_none, compComputer]
+    | some q =>
+      simp only [step, liftCompCfg_left, compComputer, Option.map_some]
+      -- Get the transition result
+      generalize hM : hf.tm.M q OTape.head = result
+      obtain ⟨⟨wr, dir⟩, nextState⟩ := result
+      simp only
+      -- Case on whether the next state is none (halting) or some
+      cases nextState with
+      | none =>
+        -- The first machine halts, but hx says the result has state.isSome
+        simp only [step, hM] at hx
+        have := hx ⟨none, (OTape.write wr).move? dir⟩ rfl
+        simp at this
+      | some q' =>
+        -- Normal step case - both sides produce the lifted config
+        simp only [hM, Option.map_some, liftCompCfg_left]
+
+/-- Helper lemma: liftCompCfg_right commutes with step for the second machine -/
+theorem map_liftCompCfg_right_step
+    {f : List α → List α} {g : List α → List α}
+    (hf : TimeComputable f) (hg : TimeComputable g)
+    (x : hg.tm.Cfg) :
+    Option.map (liftCompCfg_right hf hg) (hg.tm.step x) =
+      (compComputer hf hg).step (liftCompCfg_right hf hg x) := by
+  cases x with
+  | mk state OTape =>
+    cases state with
+    | none =>
+      simp only [step, liftCompCfg_right, Option.map_none, compComputer]
+    | some q =>
+      simp only [step, liftCompCfg_right, compComputer, Option.map_some]
+      generalize hM : hg.tm.M q OTape.head = result
+      obtain ⟨⟨wr, dir⟩, nextState⟩ := result
+      cases nextState with
+      | none => simp only [hM, Option.map_some, liftCompCfg_right, Option.map_none]
+      | some q' => simp only [hM, Option.map_some, liftCompCfg_right]
+
+theorem comp_transition_to_right {f : List α → List α} {g : List α → List α}
+    (hf : TimeComputable f) (hg : TimeComputable g)
+    (tp : OTape α)
+    (q : hf.tm.Λ)
+    (hM : (hf.tm.M q tp.head).2 = none) :
+    (compComputer hf hg).step { state := some (Sum.inl q), OTape := tp } =
+      some { state := some (Sum.inr hg.tm.q₀),
+             OTape := (tp.write (hf.tm.M q tp.head).1.symbol).move?
+                        (hf.tm.M q tp.head).1.movement } := by
+  simp only [step, compComputer, hM, Stmt.symbol, Stmt.movement]
+  generalize hfM_eq : hf.tm.M q tp.head = result
+  obtain ⟨⟨wr, dir⟩, nextState⟩ := result
+  simp only [hfM_eq]
+
+/-- Helper: lifting to Sum.inl and transitioning to Sum.inr on halt -/
+def liftCompCfg_left_or_right {f : List α → List α} {g : List α → List α}
+    (hf : TimeComputable f) (hg : TimeComputable g)
+    (cfg : hf.tm.Cfg) :
+    (compComputer hf hg).Cfg :=
+  match cfg.state with
+  | some q => { state := some (Sum.inl q), OTape := cfg.OTape }
+  | none => { state := some (Sum.inr hg.tm.q₀), OTape := cfg.OTape }
+
+/-- The lifting function commutes with step, converting halt to transition -/
+theorem map_liftCompCfg_left_or_right_step
+    {f : List α → List α} {g : List α → List α}
+    (hf : TimeComputable f) (hg : TimeComputable g)
+    (x : hf.tm.Cfg)
+    (hx : x.state.isSome) :
+    Option.map (liftCompCfg_left_or_right hf hg) (hf.tm.step x) =
+      (compComputer hf hg).step (liftCompCfg_left_or_right hf hg x) := by
+  cases x with
+  | mk state OTape =>
+    cases state with
+    | none => simp at hx
+    | some q =>
+      simp only [step, liftCompCfg_left_or_right, compComputer]
+      generalize hM : hf.tm.M q OTape.head = result
+      obtain ⟨⟨wr, dir⟩, nextState⟩ := result
+      cases nextState with
+      | none => simp only [hM, Option.map_some, liftCompCfg_left_or_right]
+      | some q' => simp only [hM, Option.map_some, liftCompCfg_left_or_right]
+
+/-- General simulation: if the first machine goes from cfg to halt, the composed machine
+    goes from lifted cfg to Sum.inr hg.tm.q₀ -/
+theorem comp_left_simulation_general {f : List α → List α} {g : List α → List α}
+    (hf : TimeComputable f) (hg : TimeComputable g)
+    (cfg : hf.tm.Cfg)
+    (hcfg : cfg.state.isSome)
+    (haltCfg : hf.tm.Cfg)
+    (steps : ℕ)
+    (h : hf.tm.TerminalReductionSystem.reducesToInSteps cfg haltCfg steps) :
+    (compComputer hf hg).TerminalReductionSystem.reducesToInSteps
+      (liftCompCfg_left_or_right hf hg cfg)
+      (liftCompCfg_left_or_right hf hg haltCfg)
+      steps := by
+  -- Proof by induction on steps.
+  -- Key insight: liftCompCfg_left_or_right maps:
+  --   { state := some q, OTape } -> { state := some (Sum.inl q), OTape }
+  --   { state := none, OTape }   -> { state := some (Sum.inr hg.tm.q₀), OTape }
+  -- For non-halting configs, the composed machine simulates exactly.
+  -- When the first machine halts, the composed machine transitions to Sum.inr hg.tm.q₀.
+  induction steps generalizing cfg haltCfg with
+  | zero =>
+    simp only [ReductionSystem.reducesToInSteps.zero_iff] at h ⊢
+    rw [h]
+  | succ n ih =>
+    -- Use the decomposition lemma: cfg evals to some intermediate c in n steps,
+    -- and then c steps to haltCfg
+    -- obtain ⟨c, hc_n, hc_step⟩ := EvalsToInTime.succ_decompose hf.tm.step cfg haltCfg n h
+    rw [ReductionSystem.reducesToInSteps.succ'_iff] at h ⊢
+    obtain ⟨c, hc_n, hc_step⟩ := h
+    use liftCompCfg_left_or_right hf hg c
+    constructor
+    · apply ih
+      · exact hcfg
+      · exact hc_n
+    · cases c with
+      | mk state OTape =>
+        cases state with
+        | none =>
+          -- c is in halting state, but step of halting state is none, contradiction
+          simp only [TerminalReductionSystem, Cslib.TerminalReductionSystem.Option, step] at hc_step
+          cases hc_step
+        | some q =>
+          -- Use the lifting lemma
+          have h1 := map_liftCompCfg_left_or_right_step hf hg ⟨some q, OTape⟩ (by simp)
+          simp only [TerminalReductionSystem, Cslib.TerminalReductionSystem.Option] at hc_step ⊢
+          rw [hc_step, Option.map_some] at h1
+          exact h1.symm
+
+
+/--
+Simulation for the first phase of the composed computer.
+When the first machine runs from start to halt, the composed machine
+runs from start (with Sum.inl state) to Sum.inr hg.tm.q₀ (the start of the second phase).
+This takes the same number of steps because the halt transition becomes a transition to the
+second machine.
+-/
+theorem comp_left_simulation {f : List α → List α} {g : List α → List α}
+    (hf : TimeComputable f) (hg : TimeComputable g)
+    (a : List α)
+    (hf_outputsFun :
+      hf.tm.TerminalReductionSystem.reducesToWithinSteps
+        { state := some hf.tm.q₀, OTape := OTape.mk₁ a }
+        ({ state := none, OTape := OTape.mk₁ (f a) })
+        (hf.time a.length)) :
+    (compComputer hf hg).TerminalReductionSystem.reducesToWithinSteps
+      { state := some (Sum.inl hf.tm.q₀), OTape := OTape.mk₁ a }
+      ({ state := some (Sum.inr hg.tm.q₀), OTape := OTape.mk₁ (f a) })
+      (hf.time a.length) := by
+  obtain ⟨steps, hsteps_le, hsteps_eval⟩ := hf_outputsFun
+  use steps
+  constructor
+  · exact hsteps_le
+  · have := comp_left_simulation_general hf hg
+      { state := some hf.tm.q₀, OTape := OTape.mk₁ a }
+      (by simp)
+      { state := none, OTape := OTape.mk₁ (f a) }
+      steps
+      hsteps_eval
+    simp only [liftCompCfg_left_or_right] at this
+    exact this
+
+/-- Simulation lemma for the second machine in the composed computer -/
+theorem comp_right_simulation
+    {f : List α → List α} {g : List α → List α}
+    (hf : TimeComputable f) (hg : TimeComputable g)
+    (x : hg.tm.Cfg) (y : hg.tm.Cfg) (m : ℕ)
+    (h : hg.tm.TerminalReductionSystem.reducesToWithinSteps x y m) :
+    (compComputer hf hg).TerminalReductionSystem.reducesToWithinSteps
+      (liftCompCfg_right hf hg x)
+      ((liftCompCfg_right hf hg) y)
+      m := by
+  refine Cslib.ReductionSystem.reducesToWithinSteps.map (liftCompCfg_right hf hg) ?_ h
+  intro a b hab
+  have h1 := map_liftCompCfg_right_step hf hg a
+  rw [hab, Option.map_some] at h1
+  exact h1.symm
+
+/--
+A composition for TimeComputable.
+
+If f and g are computed by turing machines M₁ and M₂
+then we can construct a turing machine M which computes g ∘ f by first running M₁
+and then, when M₁ halts, transitioning to the start state of M₂ and running M₂.
+
+This results in time bounded by the amount of time taken by M₁ plus the maximum time taken by M₂ on
+inputs of length of the maximum output length of M₁ for that input size (which is itself bounded by
+the time taken by M₁).
+
+Note that we require the time function of the second machine to be monotone;
+this is to ensure that if the first machine returns an output
+which is shorter than the maximum possible length of output for that input size,
+then the time bound for the second machine still holds for that shorter input to the second machine.
+
+TODO refactor out the definition of the composed TM.
+Prove separately that it
+evals to the intermediate state from the start state and
+then from the intermediate state to the final state.
+-/
+def TimeComputable.comp
+    {f : List α → List α} {g : List α → List α}
+    (hf : TimeComputable f) (hg : TimeComputable g)
+    (h_mono : Monotone hg.time) :
+    (TimeComputable (g ∘ f)) where
+  tm := compComputer hf hg
+  time l := (hf.time l) + hg.time (max 1 l + hf.time l)
+  outputsFun a := by
+    have hf_outputsFun := hf.outputsFun a
+    have hg_outputsFun := hg.outputsFun (f a)
+    simp only [OutputsWithinTime, initCfg, compComputer_q₀_eq, Function.comp_apply,
+      haltCfg] at hg_outputsFun hf_outputsFun ⊢
+    -- The computer reduces a to f a in time hf.time a
+    have h_a_reducesTo_f_a :
+        (compComputer hf hg).TerminalReductionSystem.reducesToWithinSteps
+          { state := some (Sum.inl hf.tm.q₀), OTape := OTape.mk₁ a }
+          { state := some (Sum.inr hg.tm.q₀), OTape := OTape.mk₁ (f a) }
+          (hf.time a.length) :=
+      comp_left_simulation hf hg a hf_outputsFun
+    have h_f_a_reducesTo_g_f_a :
+        (compComputer hf hg).TerminalReductionSystem.reducesToWithinSteps
+          { state := some (Sum.inr hg.tm.q₀), OTape := OTape.mk₁ (f a) }
+          { state := none, OTape := OTape.mk₁ (g (f a)) }
+          (hg.time (f a).length) := by
+      -- Use the simulation lemma for the second machine
+      have := comp_right_simulation hf hg
+        { state := some hg.tm.q₀, OTape := OTape.mk₁ (f a) }
+        { state := none, OTape := OTape.mk₁ (g (f a)) }
+        (hg.time (f a).length)
+        hg_outputsFun
+      simp only [liftCompCfg_right] at this
+      exact this
+    have h_a_reducesTo_g_f_a :=
+      Cslib.ReductionSystem.reducesToWithinSteps.trans
+        h_a_reducesTo_f_a h_f_a_reducesTo_g_f_a
+    apply Cslib.ReductionSystem.reducesToWithinSteps.mono_steps h_a_reducesTo_g_f_a
+    apply add_le_add
+    · omega
+    · apply h_mono
+      -- Use the lemma about output length being bounded by input length + time
+      exact output_length_le_input_length_add_time hf.tm _ _ _ (hf.outputsFun a)
+
+end
+
+/-!
+## Polynomial Time Computability
+
+This section defines polynomial time computable functions on Turing machines,
+and proves that
+* The identity function is polynomial time computable
+* The composition of two polynomial time computable functions is polynomial time computable
+
+### TODO
+
+Use of mathlib's `Polynomial` type leads to noncomputable definitions here.
+Perhaps we could switch to a computable polynomial representation?
+-/
+
+section PolyTime
+
+variable [Inhabited α] [Fintype α]
+
+
+/-- A Turing machine + a polynomial time function +
+a proof it outputsInTime `f` in at most `time(input.length)` steps. -/
+structure PolyTimeComputable (f : List α → List α) extends TimeComputable f where
+  /-- a polynomial time bound -/
+  poly : Polynomial ℕ
+  /-- proof that this machine outputsInTime `f` in at most `time(input.length)` steps -/
+  bounds : ∀ n, time n ≤ poly.eval n
+
+/-- A proof that the identity map on α is computable in polytime. -/
+noncomputable def PolyTimeComputable.id : @PolyTimeComputable (α := α) id where
+  toTimeComputable := TimeComputable.id
+  poly := 1
+  bounds n := by simp only [TimeComputable.id, Polynomial.eval_one, le_refl]
+
+/--
+A proof that the composition of two polytime computable functions is polytime computable.
+-/
+noncomputable def PolyTimeComputable.comp
+    {f : List α → List α} {g : List α → List α}
+    (hf : PolyTimeComputable f)
+    (hg : PolyTimeComputable g)
+    -- all Nat polynomials are monotone, but the tighter internal bound maybe is not, awkwardly
+    (h_mono : Monotone hg.time) :
+    PolyTimeComputable (g ∘ f) where
+  toTimeComputable := TimeComputable.comp hf.toTimeComputable hg.toTimeComputable h_mono
+
+  poly := hf.poly + hg.poly.comp (1 + Polynomial.X + hf.poly)
+  bounds n := by
+    simp only [TimeComputable.comp, Polynomial.eval_add, Polynomial.eval_comp, Polynomial.eval_X,
+      Polynomial.eval_one]
+    apply add_le_add
+    · exact hf.bounds n
+    · have : hg.time (max 1 n + hf.time n) ≤ hg.time (1 + n + hf.poly.eval n) := by
+        apply h_mono
+        apply add_le_add
+        · omega
+        · exact hf.bounds n
+      apply le_trans this _
+      exact hg.bounds (1 + n + hf.poly.eval n)
+
+end PolyTime
+
+end SingleTapeTM
+
+end Turing
diff --git a/Cslib/Foundations/Data/OList.lean b/Cslib/Foundations/Data/OList.lean
new file mode 100644
index 00000000..c3c724ca
--- /dev/null
+++ b/Cslib/Foundations/Data/OList.lean
@@ -0,0 +1,98 @@
+/-
+Copyright (c) 2025 Bolton Bailey. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Bolton Bailey
+-/
+
+module
+
+public import Mathlib.Data.List.Basic
+
+@[expose] public section
+
+/-!
+# OList: Lists of Options that don't end with none
+
+This file defines `OList`, a list of option values where the list cannot end with `none`.
+This is useful for representing tape contents where trailing blanks are not stored.
+-/
+
+namespace Turing
+
+/--
+List of option values that don't end with none
+-/
+structure OList (α : Type) where
+  (asList : List (Option α))
+  -- The list can be empty (i.e. none), but if it is not empty, the last element is not (some) none
+  (h : asList.getLast? ≠ some none)
+
+def OList.empty {α} : OList α := { asList := [], h := by simp }
+
+def OList.map_some {α} (l : List α) : OList α := { asList := l.map some, h := by simp }
+
+instance {α : Type} : Inhabited (OList α) where
+  default := OList.empty
+
+
+def OList.length {α} (l : OList α) : ℕ := l.asList.length
+
+def OList.cons {α} : Option α -> OList α -> OList α
+| none, l => { asList := [], h := by simp }
+| some a, l => {
+    asList := some a :: l.asList,
+    h := by
+      cases hl : l.asList with
+      | nil => simp
+      | cons hd tl =>
+        simp only [List.getLast?_cons_cons]
+        rw [← hl]
+        exact l.h
+       }
+
+def OList.tail {α} (l : OList α) : OList α :=
+  match hl : l.asList with
+  | [] => OList.empty
+  | hd :: t => { asList := t, h := by
+                  match t with
+                  | [] => simp
+                  | hd' :: t' =>
+                    have lh := l.h
+                    rw [hl] at lh
+                    simp only [List.getLast?_cons_cons] at lh
+                    have := l.h
+                    rw [hl, List.getLast?_cons_cons] at this
+                    exact this
+  }
+
+def OList.head {α} (l : OList α) : Option α :=
+  match l.asList with
+  | [] => none
+  | h :: _ => h
+
+lemma OList.length_tail_le {α} (l : OList α) : l.tail.length ≤ l.length := by
+  unfold tail length
+  split
+  · simp [empty]
+  · next heq => simp [heq]
+
+lemma OList.length_cons_none {α} (l : OList α) : (OList.cons none l).length = 0 := by
+  simp [cons, length]
+
+lemma OList.length_cons_some {α} (a : α) (l : OList α) :
+    (OList.cons (some a) l).length = l.length + 1 := by
+  simp [cons, length]
+
+lemma OList.length_cons_le {α} (o : Option α) (l : OList α) :
+    (OList.cons o l).length ≤ l.length + 1 := by
+  cases o with
+  | none => simp [length_cons_none]
+  | some a => simp [length_cons_some]
+
+lemma OList.length_map_some {α} (l : List α) : (OList.map_some l).length = l.length := by
+  simp [map_some, length]
+
+lemma OList.length_empty {α} : (OList.empty : OList α).length = 0 := by
+  simp [empty, length]
+
+end Turing
diff --git a/Cslib/Foundations/Data/OTape.lean b/Cslib/Foundations/Data/OTape.lean
new file mode 100644
index 00000000..cad574d1
--- /dev/null
+++ b/Cslib/Foundations/Data/OTape.lean
@@ -0,0 +1,112 @@
+/-
+Copyright (c) 2025 Bolton Bailey. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Bolton Bailey
+-/
+
+module
+
+public import Cslib.Foundations.Data.OList
+public import Mathlib.Computability.TuringMachine
+
+@[expose] public section
+
+/-!
+# OTape: Tape representation using OList
+
+This file defines `OTape`, a tape representation for Turing machines
+in the form of an `List` of `Option` values,
+with the additional property that the list cannot end with `none`.
+
+## Design
+
+Note that Mathlib has a `Tape` type, but it requires the alphabet type to be inhabited,
+and considers the ends of the tape to be filled with default values.
+
+The design that requires the tape elements to be `Option` values ensures that
+Lists of the base alphabet, rendered directly onto the tape by mapping over `some`,
+will not collide.
+
+## Main definitions
+
+* `OTape`: A tape with a head symbol and left/right contents stored as `OList`
+* `OTape.move`: Move the tape head left or right
+* `OTape.write`: Write a symbol at the current head position
+* `OTape.space_used`: The space used by the tape
+-/
+
+namespace Turing
+
+/--
+I find this more convenient than mathlib's Tape type,
+because that requires the type tobe inhabited,
+and it is easy to confuse a list representing one thing with a list representing another,
+if the representations are the same except for a sequence of default values at the end.
+
+The head of the machine is the current symbol under the tape head.
+We do not assume here, but could add, that the ends of the tape are never none.
+The move function should guarantee this, so that two tapes are equal
+even if one has written none to the side
+-/
+structure OTape (α : Type) where
+  (head : Option α)
+  (left : OList α)
+  (right : OList α)
+deriving Inhabited
+
+def OTape.mk₁ {α} (l : List α) : OTape α :=
+  match l with
+  | [] => { head := none, left := OList.empty, right := OList.empty }
+  | h :: t => { head := some h, left := OList.empty, right := OList.map_some t }
+
+def OTape.move {α} : Turing.OTape α → Dir → Turing.OTape α
+  | t, .left =>
+    match t.left, t.head, t.right with
+    | l, h, r => { head := l.head, left := l.tail, right := OList.cons h r }
+  | t, .right =>
+    match t.left, t.head, t.right with
+    | l, h, r => { head := r.head, left := OList.cons h l, right := r.tail }
+
+
+def OTape.move? {α} : Turing.OTape α → Option Dir → Turing.OTape α
+  | t, none => t
+  | t, some d => t.move d
+
+def OTape.write {α} : Turing.OTape α → Option α → Turing.OTape α
+  | t, a => { t with head := a }
+
+/--
+The space used by a OTape is the number of symbols
+between and including the head, and leftmost and rightmost non-blank symbols on the OTape
+-/
+def OTape.space_used {α} (t : Turing.OTape α) : ℕ :=
+  1 + t.left.length + t.right.length
+
+lemma OTape.space_used_write {α} (t : Turing.OTape α) (a : Option α) :
+    (t.write a).space_used = t.space_used := by
+  rfl
+
+lemma OTape.space_used_mk₁ (l : List α) :
+    (OTape.mk₁ l).space_used = max 1 l.length := by
+  cases l with
+  | nil =>
+    simp [mk₁, space_used, OList.length_empty]
+  | cons h t =>
+    simp [mk₁, space_used, OList.length_empty, OList.length_map_some]
+    omega
+
+lemma OTape.space_used_move {α} (t : Turing.OTape α) (d : Dir) :
+    (t.move d).space_used ≤ t.space_used + 1 := by
+  cases d with
+  | left =>
+    simp only [move, space_used]
+    have h1 := OList.length_tail_le t.left
+    have h2 := OList.length_cons_le t.head t.right
+    omega
+  | right =>
+    simp only [move, space_used]
+    have h1 := OList.length_cons_le t.head t.left
+    have h2 := OList.length_tail_le t.right
+    omega
+
+end Turing
diff --git a/Cslib/Foundations/Semantics/ReductionSystem/Basic.lean b/Cslib/Foundations/Semantics/ReductionSystem/Basic.lean
index 5aad8a38..b1b8127c 100644
--- a/Cslib/Foundations/Semantics/ReductionSystem/Basic.lean
+++ b/Cslib/Foundations/Semantics/ReductionSystem/Basic.lean
@@ -29,6 +29,11 @@ structure ReductionSystem (Term : Type u) where
   /-- The reduction relation. -/
   Red : Term → Term → Prop
 
+structure TerminalReductionSystem (Term : Type u) extends ReductionSystem Term where
+  /-- The terminal terms. -/
+  Terminal : Term → Prop
+  /-- A terminal term cannot be further reduced. -/
+  terminal_not_reducible : ∀ t t', Terminal t → ¬ Red t t'
 
 section MultiStep
 
@@ -50,6 +55,213 @@ theorem ReductionSystem.MRed.single (rs : ReductionSystem Term) (h : rs.Red a b)
 
 end MultiStep
 
+section Steps
+
+inductive ReductionSystem.reducesToInSteps
+    (rs : ReductionSystem Term) : Term → Term → ℕ → Prop
+  | refl (t : Term) : reducesToInSteps rs t t 0
+  | cons (t t' t'' : Term) (n : ℕ) (h₁ : rs.Red t t') (h₂ : reducesToInSteps rs t' t'' n) :
+      reducesToInSteps rs t t'' (n + 1)
+
+lemma ReductionSystem.reducesToInSteps.trans {rs : ReductionSystem Term} {a b c : Term} {n m : ℕ}
+    (h₁ : reducesToInSteps rs a b n) (h₂ : reducesToInSteps rs b c m) :
+    reducesToInSteps rs a c (n + m) := by
+  induction h₁ with
+  | refl _ => simp only [Nat.zero_add]; exact h₂
+  | cons t t' t'' k h_red _ ih =>
+    simp only [Nat.add_right_comm]
+    exact reducesToInSteps.cons t t' c (k + m) h_red (ih h₂)
+
+lemma ReductionSystem.reducesToInSteps.zero {rs : ReductionSystem Term} {a b : Term}
+    (h : reducesToInSteps rs a b 0) :
+    a = b := by
+  cases h
+  rfl
+
+@[simp]
+lemma ReductionSystem.reducesToInSteps.zero_iff {rs : ReductionSystem Term} {a b : Term} :
+    reducesToInSteps rs a b 0 ↔ a = b := by
+  constructor
+  · exact reducesToInSteps.zero
+  · intro h; subst h; exact reducesToInSteps.refl a
+
+
+lemma ReductionSystem.reducesToInSteps.succ {rs : ReductionSystem Term} {a b : Term} {n : ℕ}
+    (h : reducesToInSteps rs a b (n + 1)) :
+    ∃ t', rs.Red a t' ∧ reducesToInSteps rs t' b n := by
+  cases h with
+  | cons _ t' _ _ h_red h_steps => exact ⟨t', h_red, h_steps⟩
+
+lemma ReductionSystem.reducesToInSteps.succ_iff {rs : ReductionSystem Term} {a b : Term} {n : ℕ} :
+    reducesToInSteps rs a b (n + 1) ↔ ∃ t', rs.Red a t' ∧ reducesToInSteps rs t' b n := by
+  constructor
+  · exact ReductionSystem.reducesToInSteps.succ
+  · rintro ⟨t', h_red, h_steps⟩
+    exact ReductionSystem.reducesToInSteps.cons a t' b n h_red h_steps
+
+lemma ReductionSystem.reducesToInSteps.succ' {rs : ReductionSystem Term} {a b : Term} {n : ℕ}
+    (h : reducesToInSteps rs a b (n + 1)) :
+    ∃ t', reducesToInSteps rs a t' n ∧ rs.Red t' b := by
+  induction n generalizing a b with
+  | zero =>
+    obtain ⟨t', h_red, h_steps⟩ := succ h
+    rw [zero_iff] at h_steps
+    subst h_steps
+    exact ⟨a, reducesToInSteps.refl a, h_red⟩
+  | succ k ih =>
+    obtain ⟨t', h_red, h_steps⟩ := succ h
+    obtain ⟨t'', h_steps', h_red'⟩ := ih h_steps
+    exact ⟨t'', reducesToInSteps.cons a t' t'' k h_red h_steps', h_red'⟩
+
+lemma ReductionSystem.reducesToInSteps.succ'_iff
+    {rs : ReductionSystem Term} {a b : Term} {n : ℕ} :
+    reducesToInSteps rs a b (n + 1) ↔ ∃ t', reducesToInSteps rs a t' n ∧ rs.Red t' b := by
+  constructor
+  · exact succ'
+  · rintro ⟨t', h_steps, h_red⟩
+    have h_one : reducesToInSteps rs t' b 1 := cons t' b b 0 h_red (refl b)
+    have := trans h_steps h_one
+    simp only [Nat.add_one] at this
+    exact this
+
+lemma ReductionSystem.reducesToInSteps.bounded_increase
+    {rs : ReductionSystem Term} {a b : Term} (h : Term → ℕ)
+    (h_step : ∀ a b, rs.Red a b → h b ≤ h a + 1)
+    (m : ℕ)
+    (hevals : rs.reducesToInSteps a b m) :
+    h b ≤ h a + m := by
+  induction hevals with
+  | refl _ => simp
+  | cons t t' t'' k h_red _ ih =>
+    have h_step' := h_step t t' h_red
+    omega
+
+/--
+If `g` is a homomorphism from `rs` to `rs'` (i.e., it preserves the reduction relation),
+then `reducesToInSteps` is preserved under `g`.
+-/
+lemma ReductionSystem.reducesToInSteps.map {Term Term' : Type*}
+    {rs : ReductionSystem Term} {rs' : ReductionSystem Term'}
+    (g : Term → Term') (hg : ∀ a b, rs.Red a b → rs'.Red (g a) (g b))
+    {a b : Term} {n : ℕ}
+    (h : reducesToInSteps rs a b n) :
+    reducesToInSteps rs' (g a) (g b) n := by
+  induction h with
+  | refl t => exact reducesToInSteps.refl (g t)
+  | cons t t' t'' m h_red h_steps ih =>
+    exact reducesToInSteps.cons (g t) (g t') (g t'') m (hg t t' h_red) ih
+
+/--
+`reducesToWithinSteps` is a variant of `reducesToInSteps` that allows for a loose bound.
+It states that a term `a` reduces to a term `b` in *at most* `n` steps.
+-/
+def ReductionSystem.reducesToWithinSteps (rs : ReductionSystem Term)
+    (a b : Term) (n : ℕ) : Prop :=
+  ∃ m ≤ n, reducesToInSteps rs a b m
+
+/-- Reflexivity of `reducesToWithinSteps` in 0 steps. -/
+lemma ReductionSystem.reducesToWithinSteps.refl {rs : ReductionSystem Term} (a : Term) :
+    reducesToWithinSteps rs a a 0 := by
+  use 0
+  exact ⟨Nat.le_refl 0, reducesToInSteps.refl a⟩
+
+/-- Transitivity of `reducesToWithinSteps` in the sum of the step bounds. -/
+@[trans]
+lemma ReductionSystem.reducesToWithinSteps.trans {rs : ReductionSystem Term}
+    {a b c : Term} {n₁ n₂ : ℕ}
+    (h₁ : reducesToWithinSteps rs a b n₁) (h₂ : reducesToWithinSteps rs b c n₂) :
+    reducesToWithinSteps rs a c (n₁ + n₂) := by
+  obtain ⟨m₁, hm₁, hevals₁⟩ := h₁
+  obtain ⟨m₂, hm₂, hevals₂⟩ := h₂
+  use m₁ + m₂
+  constructor
+  · omega
+  · exact reducesToInSteps.trans hevals₁ hevals₂
+
+/-- Monotonicity of `reducesToWithinSteps` in the step bound. -/
+lemma ReductionSystem.reducesToWithinSteps.mono_steps {rs : ReductionSystem Term}
+    {a b : Term} {n₁ n₂ : ℕ}
+    (h : reducesToWithinSteps rs a b n₁) (hn : n₁ ≤ n₂) :
+    reducesToWithinSteps rs a b n₂ := by
+  obtain ⟨m, hm, hevals⟩ := h
+  use m
+  constructor
+  · omega
+  · exact hevals
+
+/-- If `h : Term → ℕ` increases by at most 1 on each step of `rs`,
+then the value of `h` at the output is at most `h` at the input plus the step bound. -/
+lemma ReductionSystem.reducesToWithinSteps.bounded_increase {rs : ReductionSystem Term}
+    {a b : Term} (h : Term → ℕ)
+    (h_step : ∀ a b, rs.Red a b → h b ≤ h a + 1)
+    (n : ℕ)
+    (hevals : reducesToWithinSteps rs a b n) :
+    h b ≤ h a + n := by
+  obtain ⟨m, hm, hevals_m⟩ := hevals
+  have := reducesToInSteps.bounded_increase h h_step m hevals_m
+  omega
+
+/--
+If `g` is a homomorphism from `rs` to `rs'` (i.e., it preserves the reduction relation),
+then `reducesToWithinSteps` is preserved under `g`.
+-/
+lemma ReductionSystem.reducesToWithinSteps.map {Term Term' : Type*}
+    {rs : ReductionSystem Term} {rs' : ReductionSystem Term'}
+    (g : Term → Term') (hg : ∀ a b, rs.Red a b → rs'.Red (g a) (g b))
+    {a b : Term} {n : ℕ}
+    (h : reducesToWithinSteps rs a b n) :
+    reducesToWithinSteps rs' (g a) (g b) n := by
+  obtain ⟨m, hm, hevals⟩ := h
+  exact ⟨m, hm, reducesToInSteps.map g hg hevals⟩
+
+/-- A single reduction step gives `reducesToWithinSteps` with bound 1. -/
+lemma ReductionSystem.reducesToWithinSteps.single {rs : ReductionSystem Term}
+    {a b : Term} (h : rs.Red a b) :
+    reducesToWithinSteps rs a b 1 := by
+  use 1
+  constructor
+  · exact Nat.le_refl 1
+  · exact reducesToInSteps.cons a b b 0 h (reducesToInSteps.refl b)
+
+/-- `reducesToInSteps` implies `reducesToWithinSteps` with the same bound. -/
+lemma ReductionSystem.reducesToWithinSteps.of_reducesToInSteps {rs : ReductionSystem Term}
+    {a b : Term} {n : ℕ}
+    (h : reducesToInSteps rs a b n) :
+    reducesToWithinSteps rs a b n :=
+  ⟨n, Nat.le_refl n, h⟩
+
+/-- Zero steps means the terms are equal. -/
+lemma ReductionSystem.reducesToWithinSteps.zero {rs : ReductionSystem Term} {a b : Term}
+    (h : reducesToWithinSteps rs a b 0) :
+    a = b := by
+  obtain ⟨m, hm, hevals⟩ := h
+  have : m = 0 := Nat.le_zero.mp hm
+  subst this
+  exact reducesToInSteps.zero hevals
+
+@[simp]
+lemma ReductionSystem.reducesToWithinSteps.zero_iff {rs : ReductionSystem Term} {a b : Term} :
+    reducesToWithinSteps rs a b 0 ↔ a = b := by
+  constructor
+  · exact reducesToWithinSteps.zero
+  · intro h
+    subst h
+    exact reducesToWithinSteps.refl a
+
+end Steps
+
+/--
+Given a map σ → Option σ, we can construct a terminal reduction system on `σ` where:
+* a term is terminal if it maps to `none` under the given function,
+* and otherwise is reducible to its `some` value under the given function.
+-/
+def TerminalReductionSystem.Option {σ : Type*} (f : σ → Option σ) : TerminalReductionSystem σ where
+  Red := fun a b => f a = some b
+  Terminal := fun a => f a = none
+  terminal_not_reducible := by
+    intros t t' h_terminal h_red
+    simp [h_terminal] at h_red
+
 open Lean Elab Meta Command Term
 
 -- thank you to Kyle Miller for this: