diff --git a/Cslib.lean b/Cslib.lean
index c0269e0bb..1ff81659e 100644
--- a/Cslib.lean
+++ b/Cslib.lean
@@ -31,7 +31,9 @@ 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.SingleTapeTuring.Basic
+public import Cslib.Computability.Machines.Turing.SingleTape.Defs
+public import Cslib.Computability.Machines.Turing.SingleTape.Deterministic
+public import Cslib.Computability.Machines.Turing.SingleTape.NonDeterministic
 public import Cslib.Computability.URM.Basic
 public import Cslib.Computability.URM.Computable
 public import Cslib.Computability.URM.Defs
@@ -80,6 +82,7 @@ public import Cslib.Foundations.Semantics.LTS.Divergence
 public import Cslib.Foundations.Semantics.LTS.Execution
 public import Cslib.Foundations.Semantics.LTS.HasTau
 public import Cslib.Foundations.Semantics.LTS.LTSCat.Basic
+public import Cslib.Foundations.Semantics.LTS.Map
 public import Cslib.Foundations.Semantics.LTS.Notation
 public import Cslib.Foundations.Semantics.LTS.OmegaExecution
 public import Cslib.Foundations.Semantics.LTS.Relation
diff --git a/Cslib/Computability/Automata/EpsilonNA/Basic.lean b/Cslib/Computability/Automata/EpsilonNA/Basic.lean
index e001d98c2..a5fa79012 100644
--- a/Cslib/Computability/Automata/EpsilonNA/Basic.lean
+++ b/Cslib/Computability/Automata/EpsilonNA/Basic.lean
@@ -46,9 +46,8 @@ namespace FinAcc
 that trace from the start state. -/
 @[scoped grind =]
 instance : Acceptor (FinAcc State Symbol) Symbol where
-  Accepts (a : FinAcc State Symbol) (xs : List Symbol) :=
-    ∃ s ∈ a.εClosure a.start, ∃ s' ∈ a.accept,
-    a.saturate.MTr s (xs.map (some ·)) s'
+    Accepts (a : FinAcc State Symbol) (xs : List Symbol) :=
+  ∃ s ∈ a.start, ∃ s' ∈ a.accept, a.SMTr s (xs.map Option.some) s'
 
 end FinAcc
 
diff --git a/Cslib/Computability/Automata/EpsilonNA/ToNA.lean b/Cslib/Computability/Automata/EpsilonNA/ToNA.lean
index d0299dc92..74c94d3c1 100644
--- a/Cslib/Computability/Automata/EpsilonNA/ToNA.lean
+++ b/Cslib/Computability/Automata/EpsilonNA/ToNA.lean
@@ -7,32 +7,13 @@ Authors: Fabrizio Montesi
 module
 
 public import Cslib.Computability.Automata.EpsilonNA.Basic
+public import Cslib.Foundations.Semantics.LTS.Map
 
 /-! # Translation of εNA into NA -/
 
 @[expose] public section
 
-namespace Cslib
-
-/-- Converts an `LTS` with Option labels into an `LTS` on the carried label type, by removing all
-ε-transitions. -/
-@[local grind =]
-def LTS.noε (lts : LTS State (Option Label)) : LTS State Label where
-  Tr s μ s' := lts.Tr s (some μ) s'
-
-@[local grind .]
-private lemma LTS.noε_saturate_tr
-  {lts : LTS State (Option Label)} {h : μ = some μ'} :
-  lts.saturate.Tr s μ s' ↔ lts.saturate.noε.Tr s μ' s' := by
-  grind
-
-@[scoped grind =]
-lemma LTS.noε_saturate_mTr {lts : LTS State (Option Label)} :
-  lts.saturate.MTr s (μs.map some) = lts.saturate.noε.MTr s μs := by
-  ext s'
-  induction μs generalizing s <;> grind [<= LTS.MTr.stepL]
-
-namespace Automata.εNA.FinAcc
+namespace Cslib.Automata.εNA.FinAcc
 
 variable {State Symbol : Type*}
 
@@ -41,21 +22,39 @@ variable {State Symbol : Type*}
 def toNAFinAcc (a : εNA.FinAcc State Symbol) : NA.FinAcc State Symbol where
   start := a.εClosure a.start
   accept := a.accept
-  Tr := a.saturate.noε.Tr
+  toLTS := a.saturate.mapLabel Option.some
 
 open Acceptor in
-open scoped NA.FinAcc in
+open scoped NA.FinAcc LTS LTS.MTr LTS.STr LTS.SMTr in
 /-- Correctness of `toNAFinAcc`. -/
-@[scoped grind _=_]
-theorem toNAFinAcc_language_eq {ena : εNA.FinAcc State Symbol} :
-    language ena.toNAFinAcc = language ena := by
+@[scoped grind =]
+theorem toNAFinAcc_language_eq {a : εNA.FinAcc State Symbol} :
+    language a.toNAFinAcc = language a := by
   ext xs
-  have : ∀ s s', ena.saturate.MTr s (xs.map some) s' = ena.saturate.noε.MTr s xs s' := by
-    simp [LTS.noε_saturate_mTr]
-  #adaptation_note
-  /-- A grind regression found moving to nightly-2026-03-31 (changes from lean#13166) -/
-  grind [Accepts]
-
-end Automata.εNA.FinAcc
-
-end Cslib
+  apply Iff.intro <;> intro h <;> rcases h with ⟨s, hs, s', hs', h⟩
+  case mp =>
+    have h_start : ∃ sStart ∈ a.start, a.τSTr sStart s := by
+      simp only [toNAFinAcc, εClosure, LTS.τClosure, LTS.setImage, Set.mem_iUnion,
+        exists_prop] at hs
+      rcases hs with ⟨sStart, h_sStart, hs⟩
+      exists sStart
+      apply And.intro h_sStart
+      simp only [LTS.image, LTS.saturate, Set.mem_setOf_eq] at hs
+      grind only [LTS.sTr_τSTr_iff]
+    rcases h_start with ⟨sStart, h_sStart, h_start⟩
+    exists sStart
+    apply And.intro (by grind)
+    exists s'
+    apply And.intro (by grind)
+    apply LTS.SMTr.comp (μs₁ := []) (s₂ := s) <;> grind
+  case mpr =>
+    cases xs with
+    | nil =>
+      exists s'
+      simp only [toNAFinAcc, LTS.saturate, LTS.τClosure]
+      grind [cases LTS.SMTr]
+    | cons x xs =>
+      exists s
+      grind
+
+end Cslib.Automata.εNA.FinAcc
diff --git a/Cslib/Computability/Machines/Turing/SingleTape/Defs.lean b/Cslib/Computability/Machines/Turing/SingleTape/Defs.lean
new file mode 100644
index 000000000..47aac95e5
--- /dev/null
+++ b/Cslib/Computability/Machines/Turing/SingleTape/Defs.lean
@@ -0,0 +1,41 @@
+/-
+Copyright (c) 2026 Fabrizio Montesi. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Fabrizio Montesi, Bolton Bailey
+-/
+
+module
+
+public import Cslib.Foundations.Data.BiTape
+
+/-! # Basic definitions for Turing Machines (TMs) -/
+
+@[expose] public section
+
+namespace Cslib.Computability.Turing.SingleTape
+
+/-- The transition labels used by a single-tape Turing Machine. -/
+structure TrLabel (State Symbol : Type*) where
+  /-- Symbol to read from the tape. -/
+  read : Option Symbol
+  /-- Symbol to write on the tape. -/
+  write : Option Symbol
+  /-- Head movement of the tape. -/
+  move : Option Turing.Dir
+
+/-- Configuration of a single-tape Turing machine. -/
+structure Cfg (State Symbol : Type*) where
+  /-- The state that the machine is in. -/
+  state : State
+  /-- Tape of the machine (memory). -/
+  tape : Turing.BiTape Symbol
+
+/-- Helper builder for a configuration with a given tape content. -/
+def Cfg.mk₁ (s : State) (xs : List Symbol) : Cfg State Symbol where
+  state := s
+  tape := Turing.BiTape.mk₁ xs
+
+/-- The space used by a configuration is the space used by its tape. -/
+def Cfg.spaceUsed (cfg : Cfg State Symbol) : ℕ := cfg.tape.spaceUsed
+
+end Cslib.Computability.Turing.SingleTape
diff --git a/Cslib/Computability/Machines/SingleTapeTuring/Basic.lean b/Cslib/Computability/Machines/Turing/SingleTape/Deterministic.lean
similarity index 99%
rename from Cslib/Computability/Machines/SingleTapeTuring/Basic.lean
rename to Cslib/Computability/Machines/Turing/SingleTape/Deterministic.lean
index debad7d43..79c4ae530 100644
--- a/Cslib/Computability/Machines/SingleTapeTuring/Basic.lean
+++ b/Cslib/Computability/Machines/Turing/SingleTape/Deterministic.lean
@@ -62,11 +62,12 @@ We also provide ways of constructing polynomial-runtime TMs
 
 @[expose] public section
 
-open Cslib Relation
+open Relation
 
-namespace Turing
+namespace Cslib.Turing
 
 open BiTape StackTape
+open _root_.Turing
 
 variable {Symbol : Type}
 
@@ -503,4 +504,4 @@ end PolyTimeComputable
 
 end SingleTapeTM
 
-end Turing
+end Cslib.Turing
diff --git a/Cslib/Computability/Machines/Turing/SingleTape/NonDeterministic.lean b/Cslib/Computability/Machines/Turing/SingleTape/NonDeterministic.lean
new file mode 100644
index 000000000..c3f2971f4
--- /dev/null
+++ b/Cslib/Computability/Machines/Turing/SingleTape/NonDeterministic.lean
@@ -0,0 +1,59 @@
+/-
+Copyright (c) 2026 Fabrizio Montesi. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Fabrizio Montesi
+-/
+
+module
+
+public import Cslib.Foundations.Data.Relation
+public import Cslib.Computability.Automata.NA.Basic
+public import Cslib.Foundations.Data.BiTape
+public import Cslib.Computability.Machines.Turing.SingleTape.Defs
+
+/-! # Single-Tape Nondeterministic Turing Machines (NTMs)
+
+Nondeterministic Turing Machines (NTMs), defined as nondeterministic automata (`NA`) that act on a
+bidirectional tape (`BiTape`).
+-/
+
+@[expose] public section
+
+namespace Cslib.Computability.Turing.SingleTape
+
+open Automata
+
+/-- A (single-tape) Nondeterministic Turing Machine (NTM) is a nondeterministic automaton equipped
+with a set of accepting halting states. -/
+structure SingleTapeNTM (State Symbol : Type*)
+    extends NA State (SingleTape.TrLabel State Symbol) where
+  /-- The set of accepting states. -/
+  accept : Set State
+  /-- Proof that all accepting states are halting states. -/
+  accept_halting (hmem : s ∈ accept) : ¬∃ μ s', Tr s μ s'
+
+variable {State Symbol : Type*}
+
+/-- An NTM yields a small-step operational semantics on configurations, which codifies an execution
+step. -/
+@[scoped grind =]
+def SingleTapeNTM.Red (m : SingleTapeNTM State Symbol)
+    (c c' : Cfg State Symbol) : Prop :=
+  ∃ μ, m.Tr c.state μ c'.state ∧ -- The controller can perform the move
+    μ.read = c.tape.head ∧ -- The tape has the expected symbol to be read
+    c'.tape = (c.tape.write μ.write).optionMove μ.move -- Write effect on the tape
+
+/-- Multistep execution of an NTM, defined as the reflexive and transitive closure of one-step
+execution.
+-/
+@[scoped grind =]
+def SingleTapeNTM.MRed (m : SingleTapeNTM State Symbol) :=
+  Relation.ReflTransGen m.Red
+
+/-- An NTM is an acceptor of finite lists of symbols. -/
+@[simp, scoped grind =]
+instance : Acceptor (SingleTapeNTM State Symbol) Symbol where
+  Accepts (m : SingleTapeNTM State Symbol) (xs : List Symbol) :=
+    ∃ s ∈ m.start, ∃ c', c'.state ∈ m.accept ∧ m.MRed (Cfg.mk₁ s xs) c'
+
+end Cslib.Computability.Turing.SingleTape
diff --git a/Cslib/Foundations/Data/BiTape.lean b/Cslib/Foundations/Data/BiTape.lean
index e61272d57..b1729a43d 100644
--- a/Cslib/Foundations/Data/BiTape.lean
+++ b/Cslib/Foundations/Data/BiTape.lean
@@ -38,13 +38,13 @@ will not collide.
 
 @[expose] public section
 
-namespace Turing
+namespace Cslib.Turing
 
 /--
 A structure for bidirectionally-infinite Turing machine tapes
 that eventually take on blank `none` values
 -/
-structure BiTape (Symbol : Type) where
+structure BiTape (Symbol : Type*) where
   /-- The symbol currently under the tape head -/
   head : Option Symbol
   /-- The contents to the left of the head -/
@@ -54,7 +54,7 @@ structure BiTape (Symbol : Type) where
 
 namespace BiTape
 
-variable {Symbol : Type}
+variable {Symbol : Type*}
 
 /-- The empty `BiTape` -/
 def nil : BiTape Symbol := ⟨none, ∅, ∅⟩
@@ -92,6 +92,8 @@ Move the head right by shifting the right StackTape under the head.
 def moveRight (t : BiTape Symbol) : BiTape Symbol :=
   ⟨t.right.head, StackTape.cons t.head t.left, t.right.tail⟩
 
+open _root_.Turing
+
 /--
 Move the head to the left or right, shifting the tape underneath it.
 -/
@@ -102,7 +104,7 @@ def move (t : BiTape Symbol) : Dir → BiTape Symbol
 /--
 Optionally perform a `move`, or do nothing if `none`.
 -/
-def optionMove : BiTape Symbol → Option Dir → BiTape Symbol
+def optionMove : BiTape Symbol → Option Turing.Dir → BiTape Symbol
   | t, none => t
   | t, some d => t.move d
 
@@ -138,11 +140,11 @@ lemma spaceUsed_mk₁ (l : List Symbol) :
   | nil => simp [mk₁, spaceUsed, nil, StackTape.length_nil]
   | cons h t => simp [mk₁, spaceUsed, StackTape.length_nil, StackTape.length_mapSome]; omega
 
-lemma spaceUsed_move (t : BiTape Symbol) (d : Dir) :
+lemma spaceUsed_move (t : BiTape Symbol) (d : Turing.Dir) :
     (t.move d).spaceUsed ≤ t.spaceUsed + 1 := by
   cases d <;> grind [moveLeft, moveRight, move,
     spaceUsed, StackTape.length_tail_le, StackTape.length_cons_le]
 
 end BiTape
 
-end Turing
+end Cslib.Turing
diff --git a/Cslib/Foundations/Data/StackTape.lean b/Cslib/Foundations/Data/StackTape.lean
index a252582b0..18b884559 100644
--- a/Cslib/Foundations/Data/StackTape.lean
+++ b/Cslib/Foundations/Data/StackTape.lean
@@ -38,7 +38,7 @@ advantages and disadvantages.
 
 @[expose] public section
 
-namespace Turing
+namespace Cslib.Turing
 
 /--
 An infinite tape representation using a list of `Option` values,
@@ -46,7 +46,7 @@ where the list is eventually `none`.
 
 Represented as a `List (Option Symbol)` that does not end with `none`.
 -/
-structure StackTape (Symbol : Type) where
+structure StackTape (Symbol : Type*) where
   /-- The underlying list representation -/
   toList : List (Option Symbol)
   /--
@@ -59,7 +59,7 @@ attribute [scoped grind! .] StackTape.toList_getLast?_ne_some_none
 
 namespace StackTape
 
-variable {Symbol : Type}
+variable {Symbol : Type*}
 
 /-- The empty `StackTape` -/
 @[scoped grind]
@@ -178,4 +178,4 @@ end Length
 
 end StackTape
 
-end Turing
+end Cslib.Turing
diff --git a/Cslib/Foundations/Semantics/LTS/Bisimulation.lean b/Cslib/Foundations/Semantics/LTS/Bisimulation.lean
index 21ffd67eb..b8a506042 100644
--- a/Cslib/Foundations/Semantics/LTS/Bisimulation.lean
+++ b/Cslib/Foundations/Semantics/LTS/Bisimulation.lean
@@ -853,7 +853,7 @@ theorem IsSWBisimulation.follow_internal_fst
     obtain ⟨sb2', htrsb2', hrb'⟩ := h
     exists sb2'
     constructor
-    · simp only [sTr_τSTr] at htrsb htrsb2'
+    · simp only [sTr_τSTr_iff] at htrsb htrsb2'
       exact Relation.ReflTransGen.trans htrsb2 htrsb2'
     · exact hrb'
 
@@ -874,7 +874,7 @@ theorem IsSWBisimulation.follow_internal_snd
     obtain ⟨sb2', htrsb2', hrb'⟩ := h
     exists sb2'
     constructor
-    · simp only [sTr_τSTr] at htrsb htrsb2'
+    · simp only [sTr_τSTr_iff] at htrsb htrsb2'
       exact Relation.ReflTransGen.trans htrsb2 htrsb2'
     · exact hrb'
 
@@ -890,13 +890,13 @@ theorem isWeakBisimulation_iff_isSWBisimulation
     case left =>
       intro s₁' htr
       specialize h hr μ
-      have h' := h.1 s₁' (STr.single lts₁ htr)
+      have h' := h.1 s₁' (STr.single htr)
       obtain ⟨s₂', htr2, hr2⟩ := h'
       exists s₂'
     case right =>
       intro s₂' htr
       specialize h hr μ
-      have h' := h.2 s₂' (STr.single lts₂ htr)
+      have h' := h.2 s₂' (STr.single htr)
       obtain ⟨s₁', htr1, hr1⟩ := h'
       exists s₁'
   case mpr =>
@@ -910,15 +910,15 @@ theorem isWeakBisimulation_iff_isSWBisimulation
         constructor; constructor
         exact hr
       case tr sb sb' hstr1 htr hstr2 =>
-        rw [←sTr_τSTr] at hstr1 hstr2
-        simp only [sTr_τSTr] at hstr1 hstr2
+        rw [←sTr_τSTr_iff] at hstr1 hstr2
+        simp only [sTr_τSTr_iff] at hstr1 hstr2
         obtain ⟨sb1, hstr1b, hrb⟩ := IsSWBisimulation.follow_internal_fst h hr hstr1
         obtain ⟨sb2', hstr1b', hrb'⟩ := (h hrb μ).left _ htr
         obtain ⟨s₁', hstr1', hrb2⟩ := IsSWBisimulation.follow_internal_fst h hrb' hstr2
-        rw [←sTr_τSTr] at hstr1' hstr1b
+        rw [←sTr_τSTr_iff] at hstr1' hstr1b
         exists s₁'
         constructor
-        · exact STr.comp lts₂ hstr1b hstr1b' hstr1'
+        · exact STr.comp hstr1b hstr1b' hstr1'
         · exact hrb2
     case right =>
       intro s₂' hstr
@@ -928,15 +928,15 @@ theorem isWeakBisimulation_iff_isSWBisimulation
         constructor; constructor
         exact hr
       case tr sb sb' hstr1 htr hstr2 =>
-        rw [←sTr_τSTr] at hstr1 hstr2
-        simp only [sTr_τSTr] at hstr1 hstr2
+        rw [←sTr_τSTr_iff] at hstr1 hstr2
+        simp only [sTr_τSTr_iff] at hstr1 hstr2
         obtain ⟨sb1, hstr1b, hrb⟩ := IsSWBisimulation.follow_internal_snd h hr hstr1
         obtain ⟨sb2', hstr1b', hrb'⟩ := (h hrb μ).right _ htr
         obtain ⟨s₁', hstr1', hrb2⟩ := IsSWBisimulation.follow_internal_snd h hrb' hstr2
-        rw [←sTr_τSTr] at hstr1' hstr1b
+        rw [←sTr_τSTr_iff] at hstr1' hstr1b
         exists s₁'
         constructor
-        · exact STr.comp lts₁ hstr1b hstr1b' hstr1'
+        · exact STr.comp hstr1b hstr1b' hstr1'
         · exact hrb2
 
 theorem IsWeakBisimulation.isSwBisimulation
diff --git a/Cslib/Foundations/Semantics/LTS/HasTau.lean b/Cslib/Foundations/Semantics/LTS/HasTau.lean
index 9deb34d44..abe6bf699 100644
--- a/Cslib/Foundations/Semantics/LTS/HasTau.lean
+++ b/Cslib/Foundations/Semantics/LTS/HasTau.lean
@@ -31,8 +31,8 @@ def τSTr [HasTau Label] (lts : LTS State Label) : State → State → Prop :=
 
 /-- Saturated transition relation. -/
 inductive STr [HasTau Label] (lts : LTS State Label) : State → Label → State → Prop where
-| refl : lts.STr s HasTau.τ s
-| tr : lts.τSTr s1 s2 → lts.Tr s2 μ s3 → lts.τSTr s3 s4 → lts.STr s1 μ s4
+  | refl : lts.STr s HasTau.τ s
+  | tr : lts.τSTr s1 s2 → lts.Tr s2 μ s3 → lts.τSTr s3 s4 → lts.STr s1 μ s4
 
 /-- The `LTS` obtained by saturating the transition relation in `lts`. -/
 @[scoped grind =]
@@ -44,14 +44,14 @@ theorem saturate_tr_sTr [HasTau Label] {lts : LTS State Label} :
   lts.saturate.Tr = lts.STr := by rfl
 
 /-- Any transition is also a saturated transition. -/
-theorem STr.single [HasTau Label] (lts : LTS State Label) :
+theorem STr.single [HasTau Label] {lts : LTS State Label} :
     lts.Tr s μ s' → lts.STr s μ s' := by
   intro h
   apply STr.tr .refl h .refl
 
 /-- STr transitions labeled by HasTau.τ are exactly the τSTr transitions. -/
-theorem sTr_τSTr [HasTau Label] (lts : LTS State Label) :
-  lts.STr s HasTau.τ s' ↔ lts.τSTr s s' := by
+theorem sTr_τSTr_iff [HasTau Label] (lts : LTS State Label) :
+    lts.STr s HasTau.τ s' ↔ lts.τSTr s s' := by
   apply Iff.intro <;> intro h
   case mp =>
     cases h
@@ -64,14 +64,14 @@ theorem sTr_τSTr [HasTau Label] (lts : LTS State Label) :
     case tail _ h1 h2 => exact STr.tr h1 h2 .refl
 
 /-- In a saturated LTS, the transition and saturated transition relations are the same. -/
-theorem saturate_τSTr_τSTr [hHasTau : HasTau Label] (lts : LTS State Label)
-  : lts.saturate.τSTr s = lts.τSTr s := by
-  ext s''
+theorem saturate_τsTr_τSTr_iff [hHasTau : HasTau Label] (lts : LTS State Label) :
+    lts.saturate.τSTr = lts.τSTr := by
+  ext s s'
   apply Iff.intro <;> intro h
   case mp =>
     induction h
     case refl => constructor
-    case tail _ _ _ h2 h3 => exact Relation.ReflTransGen.trans h3 ((sTr_τSTr _).mp h2)
+    case tail _ _ _ h2 h3 => exact Relation.ReflTransGen.trans h3 ((sTr_τSTr_iff _).mp h2)
   case mpr =>
     cases h
     case refl => constructor
@@ -82,31 +82,31 @@ theorem saturate_τSTr_τSTr [hHasTau : HasTau Label] (lts : LTS State Label)
 /-- Saturated transitions labelled by τ can be composed. -/
 @[scoped grind .]
 theorem STr.trans_τ
-  [HasTau Label] (lts : LTS State Label)
-  (h1 : lts.STr s1 HasTau.τ s2) (h2 : lts.STr s2 HasTau.τ s3) :
-  lts.STr s1 HasTau.τ s3 := by
-  rw [sTr_τSTr _] at h1 h2
-  rw [sTr_τSTr _]
+    [HasTau Label] {lts : LTS State Label}
+    (h1 : lts.STr s1 HasTau.τ s2) (h2 : lts.STr s2 HasTau.τ s3) :
+    lts.STr s1 HasTau.τ s3 := by
+  rw [sTr_τSTr_iff _] at h1 h2
+  rw [sTr_τSTr_iff _]
   apply Relation.ReflTransGen.trans h1 h2
 
 /-- Saturated transitions can be composed. -/
 theorem STr.comp
-  [HasTau Label] (lts : LTS State Label)
-  (h1 : lts.STr s1 HasTau.τ s2)
-  (h2 : lts.STr s2 μ s3)
-  (h3 : lts.STr s3 HasTau.τ s4) :
+    [HasTau Label] {lts : LTS State Label}
+    (h1 : lts.STr s1 HasTau.τ s2)
+    (h2 : lts.STr s2 μ s3)
+    (h3 : lts.STr s3 HasTau.τ s4) :
   lts.STr s1 μ s4 := by
-  rw [sTr_τSTr _] at h1 h3
+  rw [sTr_τSTr_iff _] at h1 h3
   cases h2
   case refl =>
-    rw [sTr_τSTr _]
+    rw [sTr_τSTr_iff _]
     apply Relation.ReflTransGen.trans h1 h3
   case tr _ _ hτ1 htr hτ2 =>
     exact STr.tr (Relation.ReflTransGen.trans h1 hτ1) htr (Relation.ReflTransGen.trans hτ2 h3)
 
 /-- In a saturated LTS, the transition and saturated transition relations are the same. -/
 theorem saturate_tr_saturate_sTr [hHasTau : HasTau Label] (lts : LTS State Label)
-  (hμ : μ = hHasTau.τ) : lts.saturate.Tr s μ = lts.saturate.STr s μ := by
+    (hμ : μ = hHasTau.τ) : lts.saturate.Tr s μ = lts.saturate.STr s μ := by
   ext s'
   apply Iff.intro <;> intro h
   case mp =>
@@ -119,20 +119,123 @@ theorem saturate_tr_saturate_sTr [hHasTau : HasTau Label] (lts : LTS State Label
     cases h
     case refl => constructor
     case tr hstr1 htr hstr2 =>
-      rw [saturate_τSTr_τSTr lts] at hstr1 hstr2
-      rw [←sTr_τSTr lts] at hstr1 hstr2
-      exact STr.comp lts hstr1 htr hstr2
+      rw [saturate_τsTr_τSTr_iff lts] at hstr1 hstr2
+      rw [←sTr_τSTr_iff lts] at hstr1 hstr2
+      exact STr.comp hstr1 htr hstr2
 
 /-- In a saturated LTS, every state is in its τ-image. -/
 @[scoped grind .]
 theorem mem_saturate_image_τ [HasTau Label] (lts : LTS State Label) :
   s ∈ lts.saturate.image s HasTau.τ := STr.refl
 
+/-- `setImage` on `HasTau.τ` preserves membership. -/
+@[scoped grind .]
+lemma mem_saturate_setImage_τ [HasTau Label] (lts : LTS State Label) (h : s ∈ S) :
+    s ∈ lts.saturate.setImage S HasTau.τ := by
+  simp only [setImage, Set.mem_iUnion, exists_prop]
+  exists s
+  grind
+
+/-- Monotonicity of `setImage` on `HasTau.τ`. -/
+@[scoped grind .]
+lemma subset_saturate_setImage_τ [HasTau Label] (lts : LTS State Label) :
+    S ⊆ lts.saturate.setImage S HasTau.τ := by
+  simp only [Subset, LE.le, Set.Subset, setImage, Set.mem_iUnion, exists_prop]
+  intro s h
+  grind
+
+/-- `setImage` preserves (non-)emptyness. -/
+@[scoped grind =]
+lemma empty_saturate_setImage_τ [HasTau Label] (lts : LTS State Label) :
+    lts.saturate.setImage S HasTau.τ = ∅ ↔ S = ∅:= by grind
+
 /-- The `τ`-closure of a set of states `S` is the set of states reachable by any state in `S`
 by performing only `τ`-transitions. -/
 def τClosure [HasTau Label] (lts : LTS State Label) (S : Set State) : Set State :=
   lts.saturate.setImage S HasTau.τ
 
+/-- `τClosure` preserves membership. -/
+@[scoped grind .]
+lemma τClosure_mem [HasTau Label] (lts : LTS State Label) (h : s ∈ S) :
+    s ∈ lts.τClosure S := by grind [= τClosure]
+
+/-- Monotonicity of `setImage` on `HasTau.τ`. -/
+@[scoped grind .]
+lemma τClosure_subset [HasTau Label] (lts : LTS State Label) :
+    S ⊆ lts.τClosure S := by grind
+
+/-- Saturated multistep transition relation. -/
+inductive SMTr [HasTau Label] (lts : LTS State Label) : State → List Label → State → Prop where
+  | τ : lts.STr s HasTau.τ s' → lts.SMTr s [] s'
+  | stepL : lts.STr s1 μ s2 → lts.SMTr s2 μs s3 → lts.SMTr s1 (μ :: μs) s3
+
+/-- The saturated multistep transition relation is reflexive. -/
+@[scoped grind .]
+theorem SMTr.refl [HasTau Label] (lts : LTS State Label) (s : State) :
+    lts.SMTr s [] s := by grind [LTS.STr, LTS.SMTr]
+
+open scoped LTS.STr
+
+/-- The saturated multistep transition relation is transitive. -/
+@[scoped grind .]
+theorem SMTr.comp [HasTau Label] {lts : LTS State Label}
+    (h₁ : lts.SMTr s₁ μs₁ s₂) (h₂ : lts.SMTr s₂ μs₂ s₃) : lts.SMTr s₁ (μs₁ ++ μs₂) s₃ := by
+  induction h₁
+  case τ s₁ s₂ htr =>
+    cases h₂
+    case τ htr' => grind [SMTr]
+    case stepL _ _ _ μ s₂' μs hstr hmstr =>
+      have hstr' : lts.STr s₁ μ s₂' := by
+        apply STr.comp htr hstr STr.refl
+      simp only [List.nil_append]
+      apply stepL hstr' hmstr
+  case stepL s₁ μ s₁' μs s₂ hstr hmstr ih =>
+    apply stepL hstr (ih h₂)
+
+/-- A multistep transition implies a saturated multistep transition. -/
+@[scoped grind .]
+theorem SMTr.fromMTr [HasTau Label] {lts : LTS State Label}
+    (h : lts.MTr s μs s') : lts.SMTr s μs s' := by
+  induction μs generalizing s s'
+  case nil => grind [LTS.STr, LTS.SMTr]
+  case cons x xs ih =>
+    cases h
+    case stepL sb htr hmtr => exact SMTr.stepL (STr.single htr) (ih hmtr)
+
+@[scoped grind =]
+theorem sMTr_τSTr_iff [HasTau Label] {lts : LTS State Label} :
+    lts.τSTr s s' ↔ lts.SMTr s [] s' := by grind only [=_ sTr_τSTr_iff, SMTr]
+
+/-- A saturated multistep transition with a nonempty label list implies a multistep transition. -/
+@[scoped grind =]
+theorem saturate_mTr_sMTr_not_nil_iff [HasTau Label] {lts : LTS State Label}
+    (hμs : μs ≠ []) : lts.saturate.MTr s μs s' ↔ lts.SMTr s μs s' := by
+  induction μs generalizing s
+  case nil => contradiction
+  case cons x xs ih =>
+    apply Iff.intro <;> intro h
+    case mp =>
+      cases h
+      case stepL sb htr hmtr =>
+        cases xs with
+        | nil =>
+          cases hmtr
+          apply LTS.SMTr.stepL htr (by grind only [SMTr.fromMTr, MTr.refl])
+        | cons x' xs' =>
+          exact LTS.SMTr.stepL htr ((ih (by simp)).mp hmtr)
+    case mpr =>
+      cases h
+      case stepL sb htr hmtr =>
+        cases xs with
+        | nil =>
+          cases hmtr
+          case τ h_τ =>
+            exact LTS.MTr.stepL
+              (LTS.STr.comp LTS.STr.refl htr h_τ)
+              LTS.MTr.refl
+        | cons x' xs' =>
+          exact LTS.MTr.stepL htr ((ih (by simp)).mpr hmtr)
+
 end LTS
 
 end Cslib
diff --git a/Cslib/Foundations/Semantics/LTS/Map.lean b/Cslib/Foundations/Semantics/LTS/Map.lean
new file mode 100644
index 000000000..e5c4c6600
--- /dev/null
+++ b/Cslib/Foundations/Semantics/LTS/Map.lean
@@ -0,0 +1,39 @@
+/-
+Copyright (c) 2026 Fabrizio Montesi. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Fabrizio Montesi
+-/
+
+module
+
+public import Cslib.Foundations.Semantics.LTS.Basic
+
+
+/-!
+# Map operation for LTS.
+-/
+
+@[expose] public section
+
+namespace Cslib.LTS
+
+section MapLabel
+
+/-- Constructs an LTS by mapping its labels into those of an existing LTS. -/
+def mapLabel (lts : LTS State Label₁) (f : Label₂ → Label₁) : LTS State Label₂ where
+  Tr s μ s' := lts.Tr s (f μ) s'
+
+@[scoped grind =]
+theorem mapLabel_tr {lts : LTS State Label₁} {f : Label₂ → Label₁} :
+    (lts.mapLabel f).Tr s μ s' ↔ lts.Tr s (f μ) s' := by rfl
+
+@[scoped grind =]
+theorem mapLabel_mTr {lts : LTS State Label₁} {f : Label₂ → Label₁} :
+    (lts.mapLabel f).MTr s μs s' ↔ lts.MTr s (μs.map f) s' := by
+  induction μs generalizing s with
+  | nil => grind
+  | cons μ μs ih => grind [=_ mapLabel_tr (f := f)]
+
+end MapLabel
+
+end Cslib.LTS