diff --git a/Cslib.lean b/Cslib.lean
index a4d250711..3a915908e 100644
--- a/Cslib.lean
+++ b/Cslib.lean
@@ -74,6 +74,7 @@ public import Cslib.Foundations.Data.DecidableEqZero
 public import Cslib.Foundations.Data.FinFun.Basic
 public import Cslib.Foundations.Data.FinFun.Update
 public import Cslib.Foundations.Data.HasFresh
+public import Cslib.Foundations.Data.List.IsChainFromTo
 public import Cslib.Foundations.Data.Nat.Segment
 public import Cslib.Foundations.Data.OmegaSequence.Defs
 public import Cslib.Foundations.Data.OmegaSequence.Flatten
diff --git a/Cslib/Computability/Machines/Turing/SingleTape/Deterministic.lean b/Cslib/Computability/Machines/Turing/SingleTape/Deterministic.lean
index 29f379d5a..77ce68176 100644
--- a/Cslib/Computability/Machines/Turing/SingleTape/Deterministic.lean
+++ b/Cslib/Computability/Machines/Turing/SingleTape/Deterministic.lean
@@ -445,7 +445,7 @@ def TimeComputable.comp {f g : List Symbol → List Symbol}
         (hg.timeBound (f a).length) hg_outputsFun
     -- Therefore, the computer reduces a to g (f a) in the sum of those times.
     have h_a_reducesTo_g_f_a := RelatesWithinSteps.trans h_a_reducesTo_f_a h_f_a_reducesTo_g_f_a
-    apply RelatesWithinSteps.of_le h_a_reducesTo_g_f_a
+    refine RelatesWithinSteps.mono ?_ h_a_reducesTo_g_f_a
     refine Nat.add_le_add_left ?_ (hf.timeBound a.length)
     · apply h_mono
       -- Use the lemma about output length being bounded by input length + time
diff --git a/Cslib/Foundations/Data/List/IsChainFromTo.lean b/Cslib/Foundations/Data/List/IsChainFromTo.lean
new file mode 100644
index 000000000..cb39d18b7
--- /dev/null
+++ b/Cslib/Foundations/Data/List/IsChainFromTo.lean
@@ -0,0 +1,194 @@
+/-
+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.Init
+public import Mathlib.Data.List.Chain
+public import Mathlib.Data.List.Nodup
+public import Mathlib.Logic.Relation
+
+/-! # Chains with a designated start and end
+
+This file defines `List.IsChainFromTo`, a variant of `List.IsChain` that also fixes the first and
+last element of the chain. Such a chain is an explicit witness for the fact that its end point is
+reachable from its start point, and its length bounds the number of steps that are needed.
+
+## Main definitions
+
+* `List.IsChainFromTo r chain a b`: `chain` is a non-empty list whose adjacent elements are related
+  by `r`, whose first element is `a` and whose last element is `b`.
+
+## Main results
+
+* `List.IsChainFromTo.reflTransGen`: the start and the end of a chain are related by
+  `Relation.ReflTransGen`.
+* `List.IsChainFromTo.head_induction_on`: induction on a chain, peeling off elements at the start.
+* `List.IsChainFromTo.exists_length_lt_of_not_nodup`: a chain with duplicates can always be
+  shortened.
+* `List.IsChainFromTo.exists_nodup`: iterating the above yields a chain without duplicates.
+-/
+
+@[expose] public section
+
+variable {α : Type*} {r : α → α → Prop} {chain : List α} {a b c : α}
+
+/-- A "chain from to" is a list of elements where adjacent elements relate to each other
+(cf. `List.IsChain`) and start and end with specific elements. -/
+structure List.IsChainFromTo {α : Type*} (r : α → α → Prop) (chain : List α) (a b : α) : Prop where
+  isChain : chain.IsChain r
+  ne_nil : chain ≠ []
+  head_eq : chain.head ne_nil = a
+  getLast_eq : chain.getLast ne_nil = b
+
+attribute [grind →] List.IsChainFromTo.head_eq List.IsChainFromTo.getLast_eq
+
+/-- A chain has at least one element. -/
+@[grind →]
+lemma List.IsChainFromTo.length_pos (hc : chain.IsChainFromTo r a b) : 0 < chain.length :=
+  List.length_pos_iff.mpr hc.ne_nil
+
+/-- The first element of an `r`-chain from `a` to `b` is `a`. -/
+@[grind →]
+lemma List.IsChainFromTo.getElem_zero (hc : chain.IsChainFromTo r a b) :
+    chain[0]'hc.length_pos = a := by
+  rw [List.getElem_zero]
+  exact hc.head_eq
+
+/-- The last element of an `r`-chain from `a` to `b` is `b`. -/
+@[grind →]
+lemma List.IsChainFromTo.getElem_length_sub_one (hc : chain.IsChainFromTo r a b) :
+    chain[chain.length - 1]'(by have := hc.length_pos; lia) = b := by
+  rw [List.getElem_length_sub_one_eq_getLast]
+  exact hc.getLast_eq
+
+/-- The start and the end of an `r`-chain are reflexively-transitively related by `r`. -/
+theorem List.IsChainFromTo.reflTransGen (hc : chain.IsChainFromTo r a b) :
+    Relation.ReflTransGen r a b := by
+  simpa [hc.head_eq, hc.getLast_eq] using
+    List.relationReflTransGen_of_exists_isChain chain hc.isChain hc.ne_nil
+
+/-- Create a `List.IsChainFromTo` from a non-empty `List.IsChain`. -/
+theorem List.IsChain.isChainFromTo_of_ne_nil
+    {chain : List α} (hc : chain.IsChain r) (h_ne_nil : chain ≠ []) :
+    List.IsChainFromTo r chain (chain.head h_ne_nil) (chain.getLast h_ne_nil) :=
+  ⟨hc, h_ne_nil, rfl, rfl⟩
+
+/-- A one-element list is an `r`-chain from that element to itself. -/
+@[simp, grind ←]
+lemma List.isChainFromTo_singleton : List.IsChainFromTo r [a] a a :=
+  ⟨List.IsChain.singleton a, by simp, rfl, rfl⟩
+
+/-- Prepend an `r`-related element to the start of the chain. -/
+lemma List.IsChainFromTo.cons (h : r a b) (hc : chain.IsChainFromTo r b c) :
+    (a :: chain).IsChainFromTo r a c where
+  isChain := hc.isChain.cons_of_ne_nil hc.ne_nil (hc.head_eq.symm ▸ h)
+  ne_nil := cons_ne_nil a chain
+  head_eq := head_cons
+  getLast_eq := hc.getLast_eq ▸ chain.getLast_cons hc.ne_nil
+
+/-- A two-element list of `r`-related elements is an `r`-chain from the first to the second. -/
+@[simp, grind ←]
+lemma List.isChainFromTo_pair (h : r a b) : List.IsChainFromTo r [a, b] a b :=
+  ⟨by simp [h], by simp, rfl, rfl⟩
+
+/-- Removing the head yields a valid chain. -/
+lemma List.IsChainFromTo.of_cons_cons {x y : α} (hc : (x :: y :: chain).IsChainFromTo r a b) :
+    (y :: chain).IsChainFromTo r y b :=
+  ⟨hc.isChain.of_cons, cons_ne_nil _ _, head_cons, by grind⟩
+
+/-- Appending a chain and the tail of a second one whose start point equals the end point of the
+first yields a valid chain. -/
+lemma List.IsChainFromTo.append_tail (hc : chain.IsChainFromTo r a b) {chain' : List α}
+    (hc' : chain'.IsChainFromTo r b c) : (chain ++ chain'.tail).IsChainFromTo r a c where
+  isChain := by
+    have hb : chain.dropLast ++ [b] = chain :=
+      hc.getLast_eq ▸ chain.dropLast_append_getLast hc.ne_nil
+    have hb' : [b] ++ chain'.tail = chain' := by simp [←hc'.head_eq]
+    rw [←hb] at hc ⊢
+    exact hc.isChain.append_overlap (l₃ := chain'.tail) (hb'.symm ▸ hc'.isChain) (cons_ne_nil b [])
+  ne_nil := append_ne_nil_of_left_ne_nil hc.ne_nil _
+  head_eq := head_append_left hc.ne_nil |>.trans hc.head_eq
+  getLast_eq := by grind
+
+/-- Add an `r`-related element to the end of the chain. -/
+lemma List.IsChainFromTo.snoc (hc : chain.IsChainFromTo r a b) (h : r b c) :
+    (chain ++ [c]).IsChainFromTo r a c :=
+  append_tail hc (chain' := [b, c]) (by simp [h])
+
+/-- Appending a chain, dropping its last element and another chain whose start point equals
+the end point of the first chain yields a valid chain. -/
+lemma List.IsChainFromTo.append_dropLast (hc : chain.IsChainFromTo r a b) {chain' : List α}
+    (hc' : chain'.IsChainFromTo r b c) : (chain.dropLast ++ chain').IsChainFromTo r a c := by
+  convert hc.append_tail hc' using 1
+  nth_rw 1 [←chain'.cons_head_tail hc'.ne_nil, hc'.head_eq, append_cons, ←hc.getLast_eq,
+    dropLast_concat_getLast hc.ne_nil]
+
+/-- Taking the first `i + 1` elements of a chain yields a chain from the same start point to
+`chain[i]`. -/
+lemma List.IsChainFromTo.take (hc : chain.IsChainFromTo r a b) {i : ℕ} (hi : i < chain.length) :
+    (chain.take (i + 1)).IsChainFromTo r a chain[i] := by
+  have : chain.take (i + 1) ≠ [] := by grind [ne_nil_iff_length_pos, length_take]
+  exact ⟨hc.isChain.take _, this, by grind, by grind [chain.getLast_take this]⟩
+
+/-- Dropping the first `i` elements of a chain yields a chain from `chain[i]` to the same end
+point. -/
+lemma List.IsChainFromTo.drop (hc : chain.IsChainFromTo r a b) {i : ℕ} (hi : i < chain.length) :
+    (chain.drop i).IsChainFromTo r chain[i] b := by
+  have : chain.drop i ≠ [] := ne_nil_iff_length_pos.mpr <| chain.lt_length_drop hi
+  refine ⟨hc.isChain.drop _, this, chain.head_drop this, hc.getLast_eq ▸ chain.getLast_drop this⟩
+
+@[elab_as_elim]
+lemma List.IsChainFromTo.head_induction_on
+    {motive : ∀ {chain : List α} {a b : α}, chain.IsChainFromTo r a b → Prop}
+    (h_refl : ∀ {a : α}, motive (isChainFromTo_singleton (r := r) (a := a)))
+    (h_head : ∀ {a b c : α} {chain : List α} (hab : r a b) (hc : chain.IsChainFromTo r b c),
+      motive hc → motive (hc.cons hab))
+    {chain : List α} {a b : α} (hc : chain.IsChainFromTo r a b) : motive hc := by
+  induction htail : chain.tail generalizing chain a with
+  | nil =>
+    obtain rfl : chain = [a] := by grind
+    grind
+  | cons a' tail ih =>
+    obtain rfl : chain = a :: a' :: tail := by grind
+    obtain ⟨hrel, hchain⟩ := isChain_cons_cons.mp hc.isChain
+    have : (a' :: tail).IsChainFromTo r a' b := hc.of_cons_cons
+    exact h_head hrel this (ih this rfl)
+
+/-- Any element of an `r`-chain from `a` to `b` is reflexively-transitively related from `a`. -/
+lemma List.IsChainFromTo.reflTransGen_of_mem (hc : chain.IsChainFromTo r a b) {x : α}
+    (mem : x ∈ chain) :
+    Relation.ReflTransGen r a x := by
+  obtain ⟨i, hi, rfl⟩ := List.getElem_of_mem mem
+  exact (hc.take hi).reflTransGen
+
+/-- If there is an `r`-chain from `a` to `b` with duplicates, then there is a shorter `r`-chain
+from `a` to `b` (the one that skips the part between the duplicates). -/
+lemma List.IsChainFromTo.exists_length_lt_of_not_nodup
+    (hc : chain.IsChainFromTo r a b)
+    (h_dup : ¬ chain.Nodup) :
+    ∃ chain' : List α, chain'.IsChainFromTo r a b ∧ chain'.length < chain.length := by
+  simp only [nodup_iff_getElem?_ne_getElem?, not_forall, not_not] at h_dup
+  obtain ⟨i, j, h_ij, h_lt, h_eq⟩ := h_dup
+  use chain.take i ++ chain.drop j
+  split_ands
+  · apply IsChainFromTo.mk ..
+    · apply (hc.isChain.take _).append (hc.isChain.drop _)
+      grind [List.head?_drop, hc.isChain.getElem (i := i - 1)]
+    · grind [append_eq_nil_iff, drop_eq_nil_iff]
+    · grind
+    · grind
+  · grind
+
+/-- For any `r`-chain from `a` to `b` there is one without duplicates. -/
+lemma List.IsChainFromTo.exists_nodup (hc : chain.IsChainFromTo r a b) :
+    ∃ chain' : List α, chain'.IsChainFromTo r a b ∧ chain'.Nodup := by
+  induction hn : chain.length using Nat.strong_induction_on generalizing chain with
+  | h n ih =>
+    by_cases h_dup : chain.Nodup
+    · use chain, hc, h_dup
+    · obtain ⟨chain', hc', hlen⟩ := hc.exists_length_lt_of_not_nodup h_dup
+      exact ih chain'.length (hn ▸ hlen) hc' rfl
diff --git a/Cslib/Foundations/Data/RelatesInSteps.lean b/Cslib/Foundations/Data/RelatesInSteps.lean
index 052e52c98..2d896c2db 100644
--- a/Cslib/Foundations/Data/RelatesInSteps.lean
+++ b/Cslib/Foundations/Data/RelatesInSteps.lean
@@ -7,18 +7,28 @@ Authors: Bolton Bailey
 module
 
 public import Cslib.Init
+public import Cslib.Foundations.Data.List.IsChainFromTo
+public import Mathlib.Data.Set.Card
 public import Mathlib.Logic.Relation
 
 /-! # Relations Across Steps
 
 This file defines `Relation.RelatesInSteps` (and `Relation.RelatesWithinSteps`).
-These are inductively defines propositions that communicate whether a relation forms a
+These are inductively defined propositions that communicate whether a relation forms a
 chain of length `n` (or at most `n`) between two elements.
+
+The lemma `RelatesInSteps.exists_isChainFromTo` allows to obtain a chain
+(`List.IsChainFromTo`) of related elements that witness the reachability, and
+`List.IsChainFromTo.relatesInSteps` is the converse direction.
+`Relation.relatesInSteps_iff_exists_isChainFromTo` combines both.
+
+Another result is `Relation.ReflTransGen.relatesInSteps_lt_encard`, which states that any element
+reachable from `a` is reachable in fewer steps than there are elements reachable from `a`.
 -/
 
 @[expose] public section
 
-variable {α : Type*} {r : α → α → Prop} {a b c : α}
+variable {α : Type*} {r : α → α → Prop} {a b c : α} {n m : ℕ}
 
 namespace Relation
 
@@ -37,6 +47,8 @@ theorem RelatesInSteps.reflTransGen (h : RelatesInSteps r a b n) : ReflTransGen
   | refl => rfl
   | tail _ _ _ _ h ih => exact .tail ih h
 
+/-- If `b` is reachable from `a` via `r`, then they relate to each other for some number
+of steps. -/
 theorem ReflTransGen.relatesInSteps (h : ReflTransGen r a b) : ∃ n, RelatesInSteps r a b n := by
   induction h with
   | refl => exact ⟨0, .refl a⟩
@@ -100,9 +112,8 @@ lemma RelatesInSteps.succ_iff {a b : α} {n : ℕ} :
   · rintro ⟨t', h_steps, h_red⟩
     exact .tail _ t' b n h_steps h_red
 
-lemma RelatesInSteps.succ' {a b : α} : ∀ {n : ℕ}, RelatesInSteps r a b (n + 1) →
+lemma RelatesInSteps.succ' {a b : α} {n : ℕ} (h : RelatesInSteps r a b (n + 1)) :
     ∃ t', r a t' ∧ RelatesInSteps r t' b n := by
-  intro n h
   obtain ⟨t', hsteps, hstep⟩ := succ h
   cases n with
   | zero =>
@@ -147,6 +158,50 @@ lemma RelatesInSteps.map {α α' : Type*}
   | tail t' t'' m _ hstep ih =>
     exact .tail (g _) (g t') (g t'') m ih (hg t' t'' hstep)
 
+/-! ## Translating between `RelatesInSteps` and chains (`List.IsChainFromTo`) -/
+
+/-- If `b` is related to `a` via `r` in `n` steps, then there is an `r`-chain of `n + 1` elements
+starting at `a` and ending at `b`.
+This is similar to `List.exists_isChain_ne_nil_of_relationReflTransGen`, but also provides
+a length guarantee. -/
+lemma RelatesInSteps.exists_isChainFromTo {a b : α} {n : ℕ} (h : RelatesInSteps r a b n) :
+    ∃ chain : List α, chain.IsChainFromTo r a b ∧ chain.length = n + 1 := by
+  induction h using RelatesInSteps.head_induction_on with
+  | hrefl => exact ⟨[b], List.isChainFromTo_singleton, rfl⟩
+  | @hhead a c n h' h ih =>
+    obtain ⟨l, hchain, hlen⟩ := ih
+    use a :: l, hchain.cons h'
+    simpa
+
+/-- Any two elements along an `r`-chain are related in as many steps as their distance in the
+chain. -/
+lemma _root_.List.IsChain.relatesInSteps_getElem {chain : List α} (hc : chain.IsChain r)
+    (i k : ℕ) (hik : i + k < chain.length) :
+    RelatesInSteps r chain[i] chain[i + k] k := by
+  induction k with
+  | zero => exact .refl _
+  | succ k ih =>
+    apply RelatesInSteps.tail _ (chain[i + k]) _ k (ih (by lia))
+    apply List.IsChain.getElem hc
+
+/-- If there is an `r`-chain of `n + 1` elements from `a` to `b`, then `a` and `b` are related
+to each other in `n` steps. -/
+lemma _root_.List.IsChainFromTo.relatesInSteps {chain : List α} {n : ℕ}
+    (hc : chain.IsChainFromTo r a b) (hlen : chain.length = n + 1) :
+    RelatesInSteps r a b n := by
+  have hrel := _root_.List.IsChain.relatesInSteps_getElem hc.isChain 0 n (by lia)
+  simp only [Nat.zero_add] at hrel
+  have hlast : chain[n]'(by lia) = b := by simpa [hlen] using hc.getElem_length_sub_one
+  rwa [hc.getElem_zero, hlast] at hrel
+
+/-- `a` and `b` are related in `n` steps exactly when there is an `r`-chain of `n + 1` elements
+from `a` to `b`. -/
+lemma relatesInSteps_iff_exists_isChainFromTo :
+    RelatesInSteps r a b n ↔ ∃ chain : List α, chain.IsChainFromTo r a b ∧ chain.length = n + 1 :=
+  ⟨RelatesInSteps.exists_isChainFromTo, fun ⟨_, hc, hlen⟩ => hc.relatesInSteps hlen⟩
+
+/-! ## RelatesWithinSteps - only requires an upper bound on the number of steps -/
+
 /--
 `RelatesWithinSteps` is a variant of `RelatesInSteps` that allows for a loose bound.
 It states that `a` relates to `b` in *at most* `n` steps.
@@ -166,10 +221,8 @@ lemma RelatesWithinSteps.single {a b : α} (h : r a b) : RelatesWithinSteps r a
   RelatesWithinSteps.of_relatesInSteps (RelatesInSteps.single h)
 
 lemma RelatesWithinSteps.zero {a b : α} (h : RelatesWithinSteps r a b 0) : a = b := by
-  obtain ⟨m, hm, hevals⟩ := h
-  have : m = 0 := Nat.le_zero.mp hm
-  subst this
-  exact RelatesInSteps.zero hevals
+  obtain ⟨_, hm, hevals⟩ := h
+  simp_all
 
 @[simp]
 lemma RelatesWithinSteps.zero_iff {a b : α} : RelatesWithinSteps r a b 0 ↔ a = b := by
@@ -186,22 +239,20 @@ lemma RelatesWithinSteps.trans {a b c : α} {n₁ n₂ : ℕ}
     RelatesWithinSteps r a c (n₁ + n₂) := by
   obtain ⟨m₁, hm₁, hevals₁⟩ := h₁
   obtain ⟨m₂, hm₂, hevals₂⟩ := h₂
-  use m₁ + m₂
-  constructor
-  · lia
-  · exact RelatesInSteps.trans hevals₁ hevals₂
+  exact ⟨m₁ + m₂, by lia, hevals₁.trans hevals₂⟩
 
-lemma RelatesWithinSteps.of_le {a b : α} {n₁ n₂ : ℕ}
-    (h : RelatesWithinSteps r a b n₁) (hn : n₁ ≤ n₂) :
-    RelatesWithinSteps r a b n₂ := by
-  obtain ⟨m, hm, hevals⟩ := h
+/-- If two elements `a` and `b` are related in at most `n₁` steps in the relation `r` and
+`n₁ ≤ n₂`, then they are also related in at most `n₂` steps. -/
+lemma RelatesWithinSteps.mono {a b : α} : Monotone (RelatesWithinSteps r a b ·) := by
+  intro n₁ n₂ hn ⟨m, hm, hevals⟩
   exact ⟨m, Nat.le_trans hm hn, hevals⟩
 
 /-- If `h : α → ℕ` increases by at most 1 on each step of `r`,
 then the value of `h` at the output is at most `h` at the input plus the step bound. -/
-lemma RelatesWithinSteps.apply_le_apply_add {a b : α} {m : ℕ} (hevals : RelatesWithinSteps r a b m)
-    (h : α → ℕ) (h_step : ∀ a b, r a b → h b ≤ h a + 1)
-    :
+lemma RelatesWithinSteps.apply_le_apply_add {a b : α} {m : ℕ}
+    (hevals : RelatesWithinSteps r a b m)
+    (h : α → ℕ)
+    (h_step : ∀ a b, r a b → h b ≤ h a + 1) :
     h b ≤ h a + m := by
   obtain ⟨m, hm, hevals_m⟩ := hevals
   have := RelatesInSteps.apply_le_apply_add hevals_m h h_step
@@ -218,4 +269,29 @@ lemma RelatesWithinSteps.map {α α' : Type*} {r : α → α → Prop} {r' : α'
   obtain ⟨m, hm, hevals⟩ := h
   exact ⟨m, hm, RelatesInSteps.map g hg hevals⟩
 
+/-! ## Reachability under a bound on the number of reachable elements -/
+
+/-- A more precise version of `ReflTransGen.relatesInSteps`: if `b` is reachable from `a`, then it
+is related to `a` in fewer steps than there are elements reachable from `a`.
+Note that this cardinality is an `ℕ∞`, and if it is infinite, no bound on the number of steps
+is stated. -/
+theorem ReflTransGen.relatesInSteps_lt_encard {b : α} (h : ReflTransGen r a b) :
+    ∃ n, RelatesInSteps r a b n ∧ (n : ℕ∞) < {x | ReflTransGen r a x}.encard := by
+  classical
+  -- Take any chain from `a` to `b` and remove its duplicates.
+  obtain ⟨n₀, hn₀⟩ := h.relatesInSteps
+  obtain ⟨chain₀, hc₀, -⟩ := hn₀.exists_isChainFromTo
+  obtain ⟨chain, hc, h_nodup⟩ := hc₀.exists_nodup
+  obtain ⟨n, hlen⟩ : ∃ n, chain.length = n + 1 := ⟨chain.length - 1, by have := hc.length_pos; lia⟩
+  refine ⟨n, hc.relatesInSteps hlen, ?_⟩
+  -- All elements of the chain are reachable from `a`, and they are pairwise distinct,
+  -- so the chain has at most as many elements as there are reachable elements.
+  have hsub : {x | x ∈ chain} ⊆ {x | ReflTransGen r a x} := fun _ hx => hc.reflTransGen_of_mem hx
+  have h_le : (chain.length : ℕ∞) ≤ {x | ReflTransGen r a x}.encard := by
+    rw [← List.coe_toFinset] at hsub
+    have := Set.encard_le_encard hsub
+    rwa [Set.encard_coe_eq_coe_finsetCard, List.toFinset_card_of_nodup h_nodup] at this
+  -- The chain has one more element than the number of steps.
+  exact lt_of_lt_of_le (by rw [hlen]; exact_mod_cast Nat.lt_succ_self n) h_le
+
 end Relation