diff --git a/Cslib.lean b/Cslib.lean
index 982b94f5d..5cb58db9d 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
 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.lean b/Cslib/Foundations/Data/List.lean
new file mode 100644
index 000000000..b2e247d94
--- /dev/null
+++ b/Cslib/Foundations/Data/List.lean
@@ -0,0 +1,67 @@
+/-
+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
+
+/-! # 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.
+
+The lemma `List.IsChainFromTo.exists_length_lt_of_not_nodup` shows that a chain with duplicates can
+always be shortened.
+-/
+
+@[expose] public section
+
+variable {α : Type*} {r : α → α → Prop} {chain : List α} {a b : α}
+
+/-- 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
+
+/-- Restatement of `head_eq`, but tagged with grind. -/
+@[grind →]
+lemma List.IsChainFromTo_head_eq (hc : chain.IsChainFromTo r a b) :
+    chain.head hc.ne_nil = a :=
+  hc.head_eq
+
+/-- Restatement of `getLast_eq`, but tagged with grind. -/
+@[grind →]
+lemma List.IsChainFromTo_getLast_eq (hc : chain.IsChainFromTo r a b) :
+    chain.getLast hc.ne_nil = b :=
+  hc.getLast_eq
+
+@[simp, grind ←]
+lemma List.IsChainFromTo.singleton {a : α} : List.IsChainFromTo r [a] a a :=
+  ⟨List.IsChain.singleton a, by simp, rfl, rfl⟩
+
+/-- 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).
+Note that applying this method iteratively does not necessarily lead to the shortest `r`-chain
+from `a` to `b`, since we always keep the initial and final segment. -/
+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
+  rw [nodup_iff_getElem?_ne_getElem?] at h_dup
+  push Not at h_dup
+  obtain ⟨i, j, h_ij, h_lt, h_eq⟩ := h_dup
+  use chain.take i ++ chain.drop j
+  refine ⟨⟨?_, by simp; omega, by grind, by grind⟩, by grind⟩
+  · refine (hc.isChain.take _).append (hc.isChain.drop _) ?_
+    intro x hx y hy
+    rw [List.head?_drop] at hy
+    have := hc.isChain.getElem (i := i - 1) (by omega)
+    grind
diff --git a/Cslib/Foundations/Data/RelatesInSteps.lean b/Cslib/Foundations/Data/RelatesInSteps.lean
index 052e52c98..7c0bc1c01 100644
--- a/Cslib/Foundations/Data/RelatesInSteps.lean
+++ b/Cslib/Foundations/Data/RelatesInSteps.lean
@@ -7,18 +7,27 @@ Authors: Bolton Bailey
 module
 
 public import Cslib.Init
+public import Cslib.Foundations.Data.List
+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
+`RelatesInSteps.of_isChainFromTo` is the converse direction.
+
+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 +46,9 @@ 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.
+See `ReflTransGen.relatesInSteps_lt_encard` for a bound on the 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,48 @@ lemma RelatesInSteps.map {α α' : Type*}
   | tail t' t'' m _ hstep ih =>
     exact .tail (g _) (g t') (g t'') m ih (hg t' t'' hstep)
 
+/-! ## Lemmas to translate between RelatesInSteps and the existence of a chain (`List.IsChain`) -/
+
+/-- 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 with
+  | refl => exact ⟨[a], by simp, rfl⟩
+  | tail t' t'' m _ hstep ih =>
+    obtain ⟨l, hchain, hlen⟩ := ih
+    use l ++ [t'']
+    refine ⟨⟨?_, by simp, ?_, by simp⟩, by grind⟩
+    · exact hchain.isChain.append (by simp) (by grind)
+    · grind
+
+/-- Any two elements along an `r`-chain are related in as many steps as their distance in the
+chain. -/
+lemma RelatesInSteps.of_isChain {chain : List α}
+    (hc : chain.IsChain r)
+    (p k : ℕ)
+    (hpk : p + k < chain.length) :
+    RelatesInSteps r chain[p] chain[p + k] k := by
+  induction k with
+  | zero => exact .refl _
+  | succ k ih =>
+    refine .tail _ (chain[p + k]) _ k (ih (by lia)) ?_
+    apply List.IsChain.getElem hc
+
+/-- If there is an `r`-chain from `a` to `b`, then `a` and `b` are related to each other with
+a number of steps equal to the length of the chain minus one. -/
+lemma RelatesInSteps.of_isChainFromTo {chain : List α} (hc : chain.IsChainFromTo r a b) :
+    RelatesInSteps r a b (chain.length - 1) := by
+  have h_ne : chain.length > 0 := by grind
+  have hrel := RelatesInSteps.of_isChain hc.isChain 0 (chain.length - 1) (by omega)
+  have h0 : chain[0] = a := by grind
+  have hl : chain[chain.length - 1] = b := by grind
+  simpa [h0, hl] using hrel
+
+/-! ## 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 +219,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 +237,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 +267,39 @@ 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
+  -- Let us use the shortest chain from `a` to `b`.
+  have hex : ∃ n, RelatesInSteps r a b n := h.relatesInSteps
+  refine ⟨Nat.find hex, Nat.find_spec hex, ?_⟩
+  obtain ⟨chain, hc, hlen⟩ := (Nat.find_spec hex).exists_isChainFromTo
+  -- All elements in the chain are reachable from `a`.
+  have hsub : {x | x ∈ chain} ⊆ {x | ReflTransGen r a x} := by
+    simp only [Set.subset_def, Set.mem_ofPred_eq]
+    intro y hy
+    obtain ⟨i, hi, rfl⟩ := List.getElem_of_mem hy
+    have := RelatesInSteps.of_isChain hc.isChain 0 i (by omega)
+    grind [RelatesInSteps.reflTransGen]
+  -- Now assume, for the sake of contradiction, that the minimal chain has at least as many
+  -- elements as there are reachable elements.
+  by_contra hcard
+  push Not at hcard
+  -- Then there is at least one duplicate element.
+  have h_dup : ¬chain.Nodup := by
+    intro h_nodup
+    have hle := (Set.encard_le_encard hsub).trans hcard
+    rw [← List.coe_toFinset, Set.encard_coe_eq_coe_finsetCard] at hle
+    grind [List.toFinset_card_of_nodup, Nat.cast_le]
+  -- But then we can shorten the chain which contradicts the fact that it is minimal.
+  obtain ⟨chain', hc', hlt⟩ := hc.exists_length_lt_of_not_nodup h_dup
+  have := List.length_pos_iff.mpr hc'.ne_nil
+  exact Nat.find_min hex (m := chain'.length - 1) (by omega) (RelatesInSteps.of_isChainFromTo hc')
+
 end Relation