From 9300a03105cc75c2f9d137099d2862d4df129718 Mon Sep 17 00:00:00 2001
From: Samuel Schlesinger <sgschlesinger@gmail.com>
Date: Sat, 25 Jul 2026 17:47:16 +0200
Subject: [PATCH 1/5] fix(LTS): define acyclicity by well-founded termination

---
 Cslib/Foundations/Semantics/LTS/Basic.lean |  8 +++--
 CslibTests/LTS.lean                        | 41 ++++++++++++++++++++++
 2 files changed, 47 insertions(+), 2 deletions(-)

diff --git a/Cslib/Foundations/Semantics/LTS/Basic.lean b/Cslib/Foundations/Semantics/LTS/Basic.lean
index b1f864f89..e1ef7c5a0 100644
--- a/Cslib/Foundations/Semantics/LTS/Basic.lean
+++ b/Cslib/Foundations/Semantics/LTS/Basic.lean
@@ -356,9 +356,13 @@ attribute [instance] FinitelyBranching.image_finite FinitelyBranching.finite_sta
 /-- Every LTS with finite types for states and labels is also finitely branching. -/
 instance FinitelyBranching.of_finite [Finite State] [Finite Label] : lts.FinitelyBranching where
 
-/-- An LTS is acyclic if there are no infinite multistep transitions. -/
+/-- An LTS is acyclic if it admits no infinite execution.
+
+This is well-foundedness of the converse of the unlabelled transition relation. Unlike a global
+bound on execution length, it allows terminating systems whose finite executions are arbitrarily
+long. -/
 class Acyclic (lts : LTS State Label) where
-  acyclic : ∃ n, ∀ s1 μs s2, lts.MTr s1 μs s2 → μs.length < n
+  acyclic : WellFounded fun s2 s1 => ∃ μ, lts.Tr s1 μ s2
 
 /-- An LTS is finite if it is finite-state and acyclic.
 
diff --git a/CslibTests/LTS.lean b/CslibTests/LTS.lean
index 34f3c3db9..f644ac37c 100644
--- a/CslibTests/LTS.lean
+++ b/CslibTests/LTS.lean
@@ -8,6 +8,7 @@ import Cslib.Foundations.Semantics.LTS.Divergence
 import Cslib.Foundations.Semantics.LTS.Bisimulation
 import Mathlib.Algebra.Group.Even
 import Mathlib.Algebra.Ring.Parity
+import Mathlib.Order.WellFounded
 import Cslib.Foundations.Semantics.LTS.Notation
 
 namespace CslibTests
@@ -83,6 +84,46 @@ example : natDivLTS.Divergent n := by
     constructor
   · simp [natInfiniteExecution]
 
+-- A terminating LTS can have finite executions of unbounded length.
+
+def countdownLTS : LTS ℕ Unit where
+  Tr n _ m := n = m + 1
+
+instance : countdownLTS.Acyclic where
+  acyclic := by
+    apply Subrelation.wf _ Nat.lt_wfRel.wf
+    rintro s2 s1 ⟨μ, h⟩
+    change s2 < s1
+    simp only [countdownLTS] at h
+    omega
+
+private theorem countdownLTS_mTr (n : ℕ) :
+    countdownLTS.MTr n (List.replicate n ()) 0 := by
+  induction n with
+  | zero => exact .refl
+  | succ n ih =>
+      rw [List.replicate_succ]
+      exact .stepL (by simp [countdownLTS]) ih
+
+theorem countdownLTS_has_no_uniform_bound :
+    ¬ ∃ bound, ∀ s1 μs s2, countdownLTS.MTr s1 μs s2 → μs.length < bound := by
+  rintro ⟨bound, hbound⟩
+  have := hbound bound (List.replicate bound ()) 0 (countdownLTS_mTr bound)
+  simp at this
+
+-- An LTS with an infinite execution is not acyclic.
+
+def successorLTS : LTS ℕ Unit where
+  Tr n _ m := m = n + 1
+
+theorem successorLTS_not_acyclic : ¬ successorLTS.Acyclic := by
+  intro h
+  have hacyclic := h.acyclic
+  rw [wellFounded_iff_isEmpty_descending_chain] at hacyclic
+  exact hacyclic.false ⟨fun n => n, by
+    intro n
+    exact ⟨(), by simp [successorLTS]⟩⟩
+
 -- Examples on decidable LTSs
 def natTrF (n : ℕ) (μ : ℕ) (m : ℕ) : Bool :=
   match n, μ, m with

From 6b24928607c05aa6d631ebc19a7d4c98fa6a8ad6 Mon Sep 17 00:00:00 2001
From: Samuel Schlesinger <sgschlesinger@gmail.com>
Date: Wed, 29 Jul 2026 23:28:10 -0400
Subject: [PATCH 2/5] fix(LTS): separate boundedness, termination, and
 acyclicity

---
 Cslib/Foundations/Relation/Confluence.lean    |  4 +
 Cslib/Foundations/Relation/Defs.lean          |  4 +
 Cslib/Foundations/Semantics/LTS/Basic.lean    | 27 ++++--
 Cslib/Foundations/Semantics/LTS/Relation.lean | 35 ++++++++
 .../Semantics/LTS/Termination.lean            | 84 ++++++++++++++++++-
 CslibTests/LTS.lean                           | 42 +++++++---
 6 files changed, 178 insertions(+), 18 deletions(-)

diff --git a/Cslib/Foundations/Relation/Confluence.lean b/Cslib/Foundations/Relation/Confluence.lean
index cd23f5684..b6f57c79d 100644
--- a/Cslib/Foundations/Relation/Confluence.lean
+++ b/Cslib/Foundations/Relation/Confluence.lean
@@ -196,6 +196,10 @@ theorem Terminating.toTransGen (ht : Terminating r) : Terminating (TransGen r) :
   simp_rw [iff_forall_sn, SN.iff_transGen] at ht ⊢
   exact ht
 
+/-- A terminating relation is acyclic. -/
+theorem Terminating.toAcyclic (ht : Terminating r) : Acyclic r :=
+  ⟨fun x hx => ht.toTransGen.irrefl.irrefl x hx⟩
+
 theorem Terminating.ofTransGen : Terminating (TransGen r) → Terminating r := by
   simp_rw [iff_forall_sn, SN.iff_transGen]
   exact id
diff --git a/Cslib/Foundations/Relation/Defs.lean b/Cslib/Foundations/Relation/Defs.lean
index f649ed5dd..9760721b0 100644
--- a/Cslib/Foundations/Relation/Defs.lean
+++ b/Cslib/Foundations/Relation/Defs.lean
@@ -89,6 +89,10 @@ abbrev Normalizing (r : α → α → Prop) : Prop :=
 the inverse of `r`. -/
 abbrev SN (r : α → α → Prop) := Acc (fun a b => r b a)
 
+/-- A relation is acyclic if its transitive closure is irreflexive, equivalently if it admits no
+nonempty cycle. -/
+abbrev Acyclic (r : α → α → Prop) := Std.Irrefl (TransGen r)
+
 /-- A relation is terminating when the inverse of its transitive closure is well-founded.
   Note that this is also called Noetherian or strongly normalizing in the literature. -/
 abbrev Terminating (r : α → α → Prop) := WellFounded (fun a b => r b a)
diff --git a/Cslib/Foundations/Semantics/LTS/Basic.lean b/Cslib/Foundations/Semantics/LTS/Basic.lean
index e1ef7c5a0..e2f87eb20 100644
--- a/Cslib/Foundations/Semantics/LTS/Basic.lean
+++ b/Cslib/Foundations/Semantics/LTS/Basic.lean
@@ -6,7 +6,7 @@ Authors: Fabrizio Montesi
 
 module
 
-public import Cslib.Init
+public import Cslib.Foundations.Relation.Defs
 public import Mathlib.Data.Set.Finite.Basic
 public import Mathlib.Order.SetNotation
 
@@ -25,6 +25,9 @@ relation `Tr` between states. We follow the style and conventions in [Sangiorgi2
 - `LTS.MTr` extends the transition relation of any LTS to a multistep transition relation,
 formalising the inference system and admissible rules for such relations in [Montesi2023].
 
+- `LTS.Bounded`, `LTS.Terminating`, and `LTS.Acyclic` distinguish globally bounded execution
+length, absence of infinite executions, and absence of nonempty cycles.
+
 - Definitions for all the common classes of LTSs: image-finite, finitely branching, finite-state,
 finite, and deterministic.
 
@@ -63,6 +66,10 @@ structure LTS (State : Type u) (Label : Type v) where
 
 namespace LTS
 
+/-- The unlabelled transition relation underlying an LTS. -/
+def toRelation (lts : LTS State Label) : State → State → Prop :=
+  fun s1 s2 => ∃ μ, lts.Tr s1 μ s2
+
 section MultiStep
 
 /-! ## Multistep transitions and executions with finite traces
@@ -356,13 +363,21 @@ attribute [instance] FinitelyBranching.image_finite FinitelyBranching.finite_sta
 /-- Every LTS with finite types for states and labels is also finitely branching. -/
 instance FinitelyBranching.of_finite [Finite State] [Finite Label] : lts.FinitelyBranching where
 
-/-- An LTS is acyclic if it admits no infinite execution.
+/-- An LTS is bounded if there is a global bound on the length of all of its finite executions. -/
+class Bounded (lts : LTS State Label) where
+  bounded : ∃ n, ∀ s1 μs s2, lts.MTr s1 μs s2 → μs.length < n
 
-This is well-foundedness of the converse of the unlabelled transition relation. Unlike a global
-bound on execution length, it allows terminating systems whose finite executions are arbitrarily
-long. -/
+/-- An LTS is terminating if its underlying unlabelled transition relation is terminating,
+equivalently if it admits no infinite execution. -/
+class Terminating (lts : LTS State Label) where
+  terminating : Relation.Terminating lts.toRelation
+
+/-- An LTS is acyclic if its underlying unlabelled transition relation contains no nonempty
+cycle. -/
 class Acyclic (lts : LTS State Label) where
-  acyclic : WellFounded fun s2 s1 => ∃ μ, lts.Tr s1 μ s2
+  [acyclic : Relation.Acyclic lts.toRelation]
+
+attribute [instance] Acyclic.acyclic
 
 /-- An LTS is finite if it is finite-state and acyclic.
 
diff --git a/Cslib/Foundations/Semantics/LTS/Relation.lean b/Cslib/Foundations/Semantics/LTS/Relation.lean
index c087357b4..ba19e6978 100644
--- a/Cslib/Foundations/Semantics/LTS/Relation.lean
+++ b/Cslib/Foundations/Semantics/LTS/Relation.lean
@@ -32,6 +32,41 @@ labels `μs`. -/
 def MTr.toRelation (lts : LTS State Label) (μs : List Label) : State → State → Prop :=
   fun s1 s2 => lts.MTr s1 μs s2
 
+section Paths
+
+variable (lts : LTS State Label)
+
+/-- A multistep transition induces a reflexive-transitive path in the underlying unlabelled
+transition relation. -/
+theorem MTr.toReflTransGen (h : lts.MTr s1 μs s2) :
+    Relation.ReflTransGen lts.toRelation s1 s2 := by
+  induction h with
+  | refl => exact .refl
+  | stepL htr _ ih => exact ih.head ⟨_, htr⟩
+
+/-- A nonempty multistep transition induces a nonempty path in the underlying unlabelled
+transition relation. -/
+theorem MTr.toTransGen (h : lts.MTr s1 μs s2) (hne : μs ≠ []) :
+    Relation.TransGen lts.toRelation s1 s2 := by
+  cases h with
+  | refl => contradiction
+  | stepL htr hmtr => exact Relation.TransGen.head' ⟨_, htr⟩ (hmtr.toReflTransGen lts)
+
+/-- A nonempty path in the underlying unlabelled transition relation can be labelled to obtain a
+multistep transition. -/
+theorem exists_mTr_of_transGen (h : Relation.TransGen lts.toRelation s1 s2) :
+    ∃ μs, μs ≠ [] ∧ lts.MTr s1 μs s2 := by
+  induction h with
+  | single htr =>
+      obtain ⟨μ, htr⟩ := htr
+      exact ⟨[μ], by simp, MTr.single lts htr⟩
+  | tail _ htr ih =>
+      obtain ⟨μs, hne, hmtr⟩ := ih
+      obtain ⟨μ, htr⟩ := htr
+      exact ⟨μs ++ [μ], by simp, hmtr.stepR lts htr⟩
+
+end Paths
+
 /-! ### Calc tactic support for MTr -/
 
 /-- Transitions can be chained. -/
diff --git a/Cslib/Foundations/Semantics/LTS/Termination.lean b/Cslib/Foundations/Semantics/LTS/Termination.lean
index 2203737fb..79e2573dd 100644
--- a/Cslib/Foundations/Semantics/LTS/Termination.lean
+++ b/Cslib/Foundations/Semantics/LTS/Termination.lean
@@ -6,10 +6,15 @@ Authors: Fabrizio Montesi
 
 module
 
-public import Cslib.Foundations.Semantics.LTS.Basic
+public import Cslib.Foundations.Relation.Confluence
+public import Cslib.Foundations.Semantics.LTS.Relation
+public import Mathlib.Data.Fintype.Card
+public import Mathlib.Data.List.Chain
 
 /-!
 # Termination of LTS
+
+This module relates global execution bounds, well-founded termination, and acyclicity.
 -/
 
 @[expose] public section
@@ -20,6 +25,83 @@ universe u v
 
 variable {State : Type u} {Label : Type v} (lts : LTS State Label) (Terminated : State → Prop)
 
+/-- A multistep transition admits a chain of its visited states. -/
+private theorem exists_state_chain (h : lts.MTr s1 μs s2) :
+    ∃ states : List State,
+      (s1 :: states).length = μs.length + 1 ∧
+        (s1 :: states).IsChain lts.toRelation := by
+  induction h with
+  | refl => exact ⟨[], by simp⟩
+  | @stepL s1 μ s2 μs s3 htr hmtr ih =>
+      obtain ⟨states, hlength, hchain⟩ := ih
+      exact ⟨s2 :: states, by simp [hlength], .cons_cons ⟨μ, htr⟩ hchain⟩
+
+/-- Bounded LTSs are terminating. -/
+theorem Bounded.toTerminating (h : lts.Bounded) : lts.Terminating := by
+  constructor
+  change WellFounded (fun a b => lts.toRelation b a)
+  rw [wellFounded_iff_isEmpty_descending_chain]
+  constructor
+  rintro ⟨f, hf⟩
+  change ∀ n, lts.toRelation (f n) (f (n + 1)) at hf
+  obtain ⟨bound, hbound⟩ := h.bounded
+  have hpaths : ∀ n, ∃ μs, μs.length = n ∧ lts.MTr (f 0) μs (f n) := by
+    intro n
+    induction n with
+    | zero => exact ⟨[], rfl, .refl⟩
+    | succ n ih =>
+        obtain ⟨μs, hlength, hmtr⟩ := ih
+        obtain ⟨μ, htr⟩ := hf n
+        exact ⟨μs ++ [μ], by simp [hlength], hmtr.stepR lts htr⟩
+  obtain ⟨μs, hlength, hmtr⟩ := hpaths bound
+  have := hbound (f 0) μs (f bound) hmtr
+  omega
+
+/-- A bounded LTS is available as a terminating LTS through typeclass inference. -/
+instance bounded_terminating [lts.Bounded] : lts.Terminating :=
+  (inferInstance : lts.Bounded).toTerminating
+
+/-- Terminating LTSs are acyclic. -/
+theorem Terminating.toAcyclic (h : lts.Terminating) : lts.Acyclic where
+  acyclic := h.terminating.toAcyclic
+
+/-- A terminating LTS is available as an acyclic LTS through typeclass inference. -/
+instance terminating_acyclic [lts.Terminating] : lts.Acyclic :=
+  (inferInstance : lts.Terminating).toAcyclic
+
+/-- On a finite state space, acyclic LTSs are bounded. -/
+theorem Acyclic.toBounded [Finite State] (h : lts.Acyclic) : lts.Bounded := by
+  classical
+  letI := Fintype.ofFinite State
+  refine ⟨Fintype.card State, ?_⟩
+  intro s1 μs s2 hmtr
+  obtain ⟨states, hlength, hchain⟩ := exists_state_chain lts hmtr
+  have htransChain : (s1 :: states).IsChain (Relation.TransGen lts.toRelation) :=
+    hchain.imp_of_mem_imp fun _ _ _ _ htr => .single htr
+  letI : Std.Irrefl (Relation.TransGen lts.toRelation) := h.acyclic
+  have hnodup : (s1 :: states).Nodup := htransChain.pairwise.nodup
+  have hcard := hnodup.length_le_card
+  omega
+
+/-- On a finite state space, acyclic LTSs are terminating. -/
+theorem Acyclic.toTerminating [Finite State] (h : lts.Acyclic) : lts.Terminating :=
+  h.toBounded.toTerminating
+
+/-- An LTS is acyclic exactly when it has no nonempty multistep cycle. -/
+theorem acyclic_iff_no_nonempty_mTr :
+    lts.Acyclic ↔ ¬ ∃ s μs, lts.MTr s μs s ∧ 0 < μs.length := by
+  constructor
+  · rintro h ⟨s, μs, hmtr, hlength⟩
+    exact h.acyclic.irrefl s (hmtr.toTransGen lts (List.ne_nil_of_length_pos hlength))
+  · intro h
+    refine { acyclic := ⟨fun s hcycle => ?_⟩ }
+    obtain ⟨μs, hne, hmtr⟩ := exists_mTr_of_transGen lts hcycle
+    exact h ⟨s, μs, hmtr, List.length_pos_of_ne_nil hne⟩
+
+/-- Finite LTSs are bounded. -/
+instance finiteLTS_bounded [Finite State] [lts.FiniteLTS] : lts.Bounded :=
+  (inferInstance : lts.Acyclic).toBounded
+
 /-- A state 'may terminate' if it can reach a terminated state. The definition of `Terminated`
 is a parameter. -/
 def MayTerminate (s : State) : Prop := ∃ s', Terminated s' ∧ lts.CanReach s s'
diff --git a/CslibTests/LTS.lean b/CslibTests/LTS.lean
index f644ac37c..ad6f5718c 100644
--- a/CslibTests/LTS.lean
+++ b/CslibTests/LTS.lean
@@ -6,6 +6,7 @@ Authors: Fabrizio Montesi
 
 import Cslib.Foundations.Semantics.LTS.Divergence
 import Cslib.Foundations.Semantics.LTS.Bisimulation
+import Cslib.Foundations.Semantics.LTS.Termination
 import Mathlib.Algebra.Group.Even
 import Mathlib.Algebra.Ring.Parity
 import Mathlib.Order.WellFounded
@@ -84,19 +85,22 @@ example : natDivLTS.Divergent n := by
     constructor
   · simp [natInfiniteExecution]
 
--- A terminating LTS can have finite executions of unbounded length.
+-- The three execution properties are distinct on infinite-state LTSs.
 
 def countdownLTS : LTS ℕ Unit where
   Tr n _ m := n = m + 1
 
-instance : countdownLTS.Acyclic where
-  acyclic := by
+instance : countdownLTS.Terminating where
+  terminating := by
     apply Subrelation.wf _ Nat.lt_wfRel.wf
     rintro s2 s1 ⟨μ, h⟩
     change s2 < s1
     simp only [countdownLTS] at h
     omega
 
+example : countdownLTS.Acyclic := inferInstance
+example : Relation.Acyclic countdownLTS.toRelation := inferInstance
+
 private theorem countdownLTS_mTr (n : ℕ) :
     countdownLTS.MTr n (List.replicate n ()) 0 := by
   induction n with
@@ -105,25 +109,41 @@ private theorem countdownLTS_mTr (n : ℕ) :
       rw [List.replicate_succ]
       exact .stepL (by simp [countdownLTS]) ih
 
-theorem countdownLTS_has_no_uniform_bound :
-    ¬ ∃ bound, ∀ s1 μs s2, countdownLTS.MTr s1 μs s2 → μs.length < bound := by
+theorem countdownLTS_not_bounded : ¬ countdownLTS.Bounded := by
   rintro ⟨bound, hbound⟩
   have := hbound bound (List.replicate bound ()) 0 (countdownLTS_mTr bound)
   simp at this
 
--- An LTS with an infinite execution is not acyclic.
-
 def successorLTS : LTS ℕ Unit where
   Tr n _ m := m = n + 1
 
-theorem successorLTS_not_acyclic : ¬ successorLTS.Acyclic := by
+private theorem successorLTS_transGen_lt {n m : ℕ}
+    (h : Relation.TransGen successorLTS.toRelation n m) : n < m := by
+  apply Relation.transGen_minimal (r' := (· < ·)) at h
+  · exact h
+  · rintro n m ⟨μ, htr⟩
+    simp only [successorLTS] at htr
+    omega
+
+instance : successorLTS.Acyclic where
+  acyclic := ⟨fun n h => (Nat.lt_irrefl n) (successorLTS_transGen_lt h)⟩
+
+theorem successorLTS_not_terminating : ¬ successorLTS.Terminating := by
   intro h
-  have hacyclic := h.acyclic
-  rw [wellFounded_iff_isEmpty_descending_chain] at hacyclic
-  exact hacyclic.false ⟨fun n => n, by
+  have hterminating := h.terminating
+  change WellFounded (fun a b => successorLTS.toRelation b a) at hterminating
+  rw [wellFounded_iff_isEmpty_descending_chain] at hterminating
+  exact hterminating.false ⟨fun n => n, by
     intro n
     exact ⟨(), by simp [successorLTS]⟩⟩
 
+def selfLoopLTS : LTS Unit Unit where
+  Tr _ _ _ := True
+
+theorem selfLoopLTS_not_acyclic : ¬ selfLoopLTS.Acyclic := by
+  intro h
+  exact h.acyclic.irrefl () (.single ⟨(), trivial⟩)
+
 -- Examples on decidable LTSs
 def natTrF (n : ℕ) (μ : ℕ) (m : ℕ) : Bool :=
   match n, μ, m with

From 7f0087cff4bf62eaafa2a132e29e77e139e6ea85 Mon Sep 17 00:00:00 2001
From: Samuel Schlesinger <sgschlesinger@gmail.com>
Date: Wed, 29 Jul 2026 23:48:55 -0400
Subject: [PATCH 3/5] refactor(LTS): expose unlabelled path characterizations

---
 Cslib/Foundations/Semantics/LTS/Relation.lean | 50 +++++++++++++------
 .../Semantics/LTS/Termination.lean            |  2 +-
 2 files changed, 36 insertions(+), 16 deletions(-)

diff --git a/Cslib/Foundations/Semantics/LTS/Relation.lean b/Cslib/Foundations/Semantics/LTS/Relation.lean
index ba19e6978..57da4faa6 100644
--- a/Cslib/Foundations/Semantics/LTS/Relation.lean
+++ b/Cslib/Foundations/Semantics/LTS/Relation.lean
@@ -32,7 +32,7 @@ labels `μs`. -/
 def MTr.toRelation (lts : LTS State Label) (μs : List Label) : State → State → Prop :=
   fun s1 s2 => lts.MTr s1 μs s2
 
-section Paths
+section UnlabelledPaths
 
 variable (lts : LTS State Label)
 
@@ -52,20 +52,40 @@ theorem MTr.toTransGen (h : lts.MTr s1 μs s2) (hne : μs ≠ []) :
   | refl => contradiction
   | stepL htr hmtr => exact Relation.TransGen.head' ⟨_, htr⟩ (hmtr.toReflTransGen lts)
 
-/-- A nonempty path in the underlying unlabelled transition relation can be labelled to obtain a
-multistep transition. -/
-theorem exists_mTr_of_transGen (h : Relation.TransGen lts.toRelation s1 s2) :
-    ∃ μs, μs ≠ [] ∧ lts.MTr s1 μs s2 := by
-  induction h with
-  | single htr =>
-      obtain ⟨μ, htr⟩ := htr
-      exact ⟨[μ], by simp, MTr.single lts htr⟩
-  | tail _ htr ih =>
-      obtain ⟨μs, hne, hmtr⟩ := ih
-      obtain ⟨μ, htr⟩ := htr
-      exact ⟨μs ++ [μ], by simp, hmtr.stepR lts htr⟩
-
-end Paths
+/-- The reflexive-transitive closure of the underlying unlabelled transition relation is exactly
+reachability in the LTS. -/
+theorem reflTransGen_toRelation_iff :
+    Relation.ReflTransGen lts.toRelation s1 s2 ↔ lts.CanReach s1 s2 := by
+  constructor
+  · intro h
+    induction h with
+    | refl => exact ⟨[], .refl⟩
+    | tail _ htr ih =>
+        obtain ⟨μs, hmtr⟩ := ih
+        obtain ⟨μ, htr⟩ := htr
+        exact ⟨μs ++ [μ], hmtr.stepR lts htr⟩
+  · rintro ⟨μs, hmtr⟩
+    exact hmtr.toReflTransGen lts
+
+/-- The transitive closure of the underlying unlabelled transition relation is exactly the
+nonempty multistep transitions of the LTS. -/
+theorem transGen_toRelation_iff :
+    Relation.TransGen lts.toRelation s1 s2 ↔
+      ∃ μs, μs ≠ [] ∧ lts.MTr s1 μs s2 := by
+  constructor
+  · intro h
+    induction h with
+    | single htr =>
+        obtain ⟨μ, htr⟩ := htr
+        exact ⟨[μ], by simp, MTr.single lts htr⟩
+    | tail _ htr ih =>
+        obtain ⟨μs, hne, hmtr⟩ := ih
+        obtain ⟨μ, htr⟩ := htr
+        exact ⟨μs ++ [μ], by simp, hmtr.stepR lts htr⟩
+  · rintro ⟨μs, hne, hmtr⟩
+    exact hmtr.toTransGen lts hne
+
+end UnlabelledPaths
 
 /-! ### Calc tactic support for MTr -/
 
diff --git a/Cslib/Foundations/Semantics/LTS/Termination.lean b/Cslib/Foundations/Semantics/LTS/Termination.lean
index 79e2573dd..d9dd8603c 100644
--- a/Cslib/Foundations/Semantics/LTS/Termination.lean
+++ b/Cslib/Foundations/Semantics/LTS/Termination.lean
@@ -95,7 +95,7 @@ theorem acyclic_iff_no_nonempty_mTr :
     exact h.acyclic.irrefl s (hmtr.toTransGen lts (List.ne_nil_of_length_pos hlength))
   · intro h
     refine { acyclic := ⟨fun s hcycle => ?_⟩ }
-    obtain ⟨μs, hne, hmtr⟩ := exists_mTr_of_transGen lts hcycle
+    obtain ⟨μs, hne, hmtr⟩ := (transGen_toRelation_iff lts).mp hcycle
     exact h ⟨s, μs, hmtr, List.length_pos_of_ne_nil hne⟩
 
 /-- Finite LTSs are bounded. -/

From fefa027d61e0ae479ec2f28f8f91c0cac6dcd6f8 Mon Sep 17 00:00:00 2001
From: Samuel Schlesinger <sgschlesinger@gmail.com>
Date: Fri, 31 Jul 2026 00:54:34 -0400
Subject: [PATCH 4/5] refactor(LTS): address termination review feedback

---
 Cslib.lean                                    |  1 +
 Cslib/Foundations/Semantics/LTS/Basic.lean    | 19 +++--
 .../Semantics/LTS/ExampleTermination.lean     | 78 +++++++++++++++++++
 .../Foundations/Semantics/LTS/Execution.lean  |  5 ++
 .../Semantics/LTS/Termination.lean            | 55 ++++---------
 CslibTests/LTS.lean                           | 61 ---------------
 6 files changed, 110 insertions(+), 109 deletions(-)
 create mode 100644 Cslib/Foundations/Semantics/LTS/ExampleTermination.lean

diff --git a/Cslib.lean b/Cslib.lean
index 281dea9c2..0bda62972 100644
--- a/Cslib.lean
+++ b/Cslib.lean
@@ -93,6 +93,7 @@ public import Cslib.Foundations.Semantics.FLTS.Prod
 public import Cslib.Foundations.Semantics.LTS.Basic
 public import Cslib.Foundations.Semantics.LTS.Bisimulation
 public import Cslib.Foundations.Semantics.LTS.Divergence
+public import Cslib.Foundations.Semantics.LTS.ExampleTermination
 public import Cslib.Foundations.Semantics.LTS.Execution
 public import Cslib.Foundations.Semantics.LTS.HasTau
 public import Cslib.Foundations.Semantics.LTS.LTSCat.Basic
diff --git a/Cslib/Foundations/Semantics/LTS/Basic.lean b/Cslib/Foundations/Semantics/LTS/Basic.lean
index e2f87eb20..2c536f8bc 100644
--- a/Cslib/Foundations/Semantics/LTS/Basic.lean
+++ b/Cslib/Foundations/Semantics/LTS/Basic.lean
@@ -25,11 +25,12 @@ relation `Tr` between states. We follow the style and conventions in [Sangiorgi2
 - `LTS.MTr` extends the transition relation of any LTS to a multistep transition relation,
 formalising the inference system and admissible rules for such relations in [Montesi2023].
 
-- `LTS.Bounded`, `LTS.Terminating`, and `LTS.Acyclic` distinguish globally bounded execution
-length, absence of infinite executions, and absence of nonempty cycles.
+- `LTS.BoundedUpTo` records an explicit global execution-length bound. `LTS.Bounded`,
+`LTS.Terminating`, and `LTS.Acyclic` distinguish globally bounded execution length, absence of
+infinite executions, and absence of nonempty cycles.
 
 - Definitions for all the common classes of LTSs: image-finite, finitely branching, finite-state,
-finite, and deterministic.
+and deterministic.
 
 ## Main statements
 
@@ -363,9 +364,13 @@ attribute [instance] FinitelyBranching.image_finite FinitelyBranching.finite_sta
 /-- Every LTS with finite types for states and labels is also finitely branching. -/
 instance FinitelyBranching.of_finite [Finite State] [Finite Label] : lts.FinitelyBranching where
 
+/-- An LTS is bounded up to `n` if every finite execution has length strictly less than `n`. -/
+def BoundedUpTo (lts : LTS State Label) (n : ℕ) : Prop :=
+  ∀ s1 μs s2, lts.MTr s1 μs s2 → μs.length < n
+
 /-- An LTS is bounded if there is a global bound on the length of all of its finite executions. -/
 class Bounded (lts : LTS State Label) where
-  bounded : ∃ n, ∀ s1 μs s2, lts.MTr s1 μs s2 → μs.length < n
+  bounded : ∃ n, lts.BoundedUpTo n
 
 /-- An LTS is terminating if its underlying unlabelled transition relation is terminating,
 equivalently if it admits no infinite execution. -/
@@ -379,12 +384,6 @@ class Acyclic (lts : LTS State Label) where
 
 attribute [instance] Acyclic.acyclic
 
-/-- An LTS is finite if it is finite-state and acyclic.
-
-We call this `FiniteLTS` instead of just `Finite` to avoid confusion with the standard `Finite`
-class. -/
-class FiniteLTS [Finite State] (lts : LTS State Label) extends lts.Acyclic
-
 end Classes
 
 end LTS
diff --git a/Cslib/Foundations/Semantics/LTS/ExampleTermination.lean b/Cslib/Foundations/Semantics/LTS/ExampleTermination.lean
new file mode 100644
index 000000000..a381a1122
--- /dev/null
+++ b/Cslib/Foundations/Semantics/LTS/ExampleTermination.lean
@@ -0,0 +1,78 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+module
+
+public import Cslib.Foundations.Semantics.LTS.Termination
+public import Mathlib.Order.WellFounded
+
+/-!
+# Examples separating boundedness, termination, and acyclicity
+
+On infinite state spaces, boundedness, termination, and acyclicity are distinct properties.
+This file gives concrete LTSs witnessing that the converses in
+`Bounded → Terminating → Acyclic` do not hold in general.
+-/
+
+@[expose] public section
+
+namespace Cslib.LTS.Example
+
+/-- The countdown LTS takes a natural number to its predecessor. -/
+def countdownLTS : LTS ℕ Unit where
+  Tr n _ m := n = m + 1
+
+instance countdownLTS_terminating : countdownLTS.Terminating where
+  terminating := by
+    apply Subrelation.wf _ Nat.lt_wfRel.wf
+    rintro s2 s1 ⟨_, rfl⟩
+    exact Nat.lt_succ_self s2
+
+example : countdownLTS.Acyclic := inferInstance
+example : Relation.Acyclic countdownLTS.toRelation := inferInstance
+
+private theorem countdownLTS_mTr (n : ℕ) :
+    countdownLTS.MTr n (List.replicate n ()) 0 := by
+  induction n with
+  | zero => exact .refl
+  | succ n ih =>
+      simpa [List.replicate_succ] using MTr.stepL (by simp [countdownLTS]) ih
+
+/-- The countdown LTS is not bounded. -/
+theorem countdownLTS_not_bounded : ¬ countdownLTS.Bounded := by
+  rintro ⟨bound, hbound⟩
+  simpa using hbound bound (List.replicate bound ()) 0 (countdownLTS_mTr bound)
+
+/-- The successor LTS takes each natural number to its successor. -/
+def successorLTS : LTS ℕ Unit where
+  Tr n _ m := m = n + 1
+
+private theorem successorLTS_transGen_lt {n m : ℕ}
+    (h : Relation.TransGen successorLTS.toRelation n m) : n < m := by
+  apply Relation.transGen_minimal (r' := (· < ·)) at h
+  · exact h
+  · rintro n m ⟨μ, htr⟩
+    simp only [successorLTS] at htr
+    omega
+
+instance successorLTS_acyclic : successorLTS.Acyclic where
+  acyclic := ⟨fun n h => (Nat.lt_irrefl n) (successorLTS_transGen_lt h)⟩
+
+/-- The successor LTS is not terminating. -/
+theorem successorLTS_not_terminating : ¬ successorLTS.Terminating := by
+  intro h
+  exact (Relation.Terminating.iff_isEmpty_chain.mp h.terminating).false
+    ⟨fun n => n, fun n => ⟨(), by simp [successorLTS]⟩⟩
+
+/-- The self-loop LTS has a transition from its unique state to itself. -/
+def selfLoopLTS : LTS Unit Unit where
+  Tr _ _ _ := True
+
+/-- The self-loop LTS is not acyclic. -/
+theorem selfLoopLTS_not_acyclic : ¬ selfLoopLTS.Acyclic :=
+  fun h => h.acyclic.irrefl () (.single ⟨(), trivial⟩)
+
+end Cslib.LTS.Example
diff --git a/Cslib/Foundations/Semantics/LTS/Execution.lean b/Cslib/Foundations/Semantics/LTS/Execution.lean
index 51ced513d..d8b6a98bc 100644
--- a/Cslib/Foundations/Semantics/LTS/Execution.lean
+++ b/Cslib/Foundations/Semantics/LTS/Execution.lean
@@ -84,6 +84,11 @@ theorem Execution.to_mTr (hexec : lts.Execution s1 μs s2 ss) :
         apply this
       · grind
 
+/-- The states visited by an execution form a chain in the underlying unlabelled relation. -/
+theorem Execution.isChain (hexec : lts.Execution s1 μs s2 ss) :
+    ss.IsChain lts.toRelation := by
+  grind [Execution, List.isChain_iff_getElem, toRelation]
+
 open scoped Execution
 /-- Correspondence of multistep transitions and executions. -/
 @[scoped grind =]
diff --git a/Cslib/Foundations/Semantics/LTS/Termination.lean b/Cslib/Foundations/Semantics/LTS/Termination.lean
index d9dd8603c..6b8c2f14b 100644
--- a/Cslib/Foundations/Semantics/LTS/Termination.lean
+++ b/Cslib/Foundations/Semantics/LTS/Termination.lean
@@ -7,9 +7,10 @@ Authors: Fabrizio Montesi
 module
 
 public import Cslib.Foundations.Relation.Confluence
-public import Cslib.Foundations.Semantics.LTS.Relation
+public import Cslib.Foundations.Semantics.LTS.Execution
 public import Mathlib.Data.Fintype.Card
 public import Mathlib.Data.List.Chain
+public import Mathlib.SetTheory.Cardinal.Finite
 
 /-!
 # Termination of LTS
@@ -25,22 +26,10 @@ universe u v
 
 variable {State : Type u} {Label : Type v} (lts : LTS State Label) (Terminated : State → Prop)
 
-/-- A multistep transition admits a chain of its visited states. -/
-private theorem exists_state_chain (h : lts.MTr s1 μs s2) :
-    ∃ states : List State,
-      (s1 :: states).length = μs.length + 1 ∧
-        (s1 :: states).IsChain lts.toRelation := by
-  induction h with
-  | refl => exact ⟨[], by simp⟩
-  | @stepL s1 μ s2 μs s3 htr hmtr ih =>
-      obtain ⟨states, hlength, hchain⟩ := ih
-      exact ⟨s2 :: states, by simp [hlength], .cons_cons ⟨μ, htr⟩ hchain⟩
-
 /-- Bounded LTSs are terminating. -/
 theorem Bounded.toTerminating (h : lts.Bounded) : lts.Terminating := by
   constructor
-  change WellFounded (fun a b => lts.toRelation b a)
-  rw [wellFounded_iff_isEmpty_descending_chain]
+  rw [Relation.Terminating.iff_isEmpty_chain]
   constructor
   rintro ⟨f, hf⟩
   change ∀ n, lts.toRelation (f n) (f (n + 1)) at hf
@@ -69,39 +58,29 @@ theorem Terminating.toAcyclic (h : lts.Terminating) : lts.Acyclic where
 instance terminating_acyclic [lts.Terminating] : lts.Acyclic :=
   (inferInstance : lts.Terminating).toAcyclic
 
-/-- On a finite state space, acyclic LTSs are bounded. -/
-theorem Acyclic.toBounded [Finite State] (h : lts.Acyclic) : lts.Bounded := by
+/-- On a finite state space, an acyclic LTS has execution length strictly less than the number of
+states. -/
+theorem Acyclic.toBoundedUpTo [Finite State] (h : lts.Acyclic) :
+    lts.BoundedUpTo (Nat.card State) := by
   classical
   letI := Fintype.ofFinite State
-  refine ⟨Fintype.card State, ?_⟩
+  rw [Nat.card_eq_fintype_card]
   intro s1 μs s2 hmtr
-  obtain ⟨states, hlength, hchain⟩ := exists_state_chain lts hmtr
-  have htransChain : (s1 :: states).IsChain (Relation.TransGen lts.toRelation) :=
-    hchain.imp_of_mem_imp fun _ _ _ _ htr => .single htr
+  obtain ⟨states, hexec⟩ := Execution.of_mTr hmtr
+  have hchain : states.IsChain (Relation.TransGen lts.toRelation) :=
+    hexec.isChain.imp_of_mem_imp fun _ _ _ _ htr => .single htr
   letI : Std.Irrefl (Relation.TransGen lts.toRelation) := h.acyclic
-  have hnodup : (s1 :: states).Nodup := htransChain.pairwise.nodup
-  have hcard := hnodup.length_le_card
-  omega
+  have hcard := hchain.pairwise.nodup.length_le_card
+  grind [Execution]
+
+/-- On a finite state space, acyclic LTSs are bounded. -/
+theorem Acyclic.toBounded [Finite State] (h : lts.Acyclic) : lts.Bounded :=
+  ⟨Nat.card State, h.toBoundedUpTo⟩
 
 /-- On a finite state space, acyclic LTSs are terminating. -/
 theorem Acyclic.toTerminating [Finite State] (h : lts.Acyclic) : lts.Terminating :=
   h.toBounded.toTerminating
 
-/-- An LTS is acyclic exactly when it has no nonempty multistep cycle. -/
-theorem acyclic_iff_no_nonempty_mTr :
-    lts.Acyclic ↔ ¬ ∃ s μs, lts.MTr s μs s ∧ 0 < μs.length := by
-  constructor
-  · rintro h ⟨s, μs, hmtr, hlength⟩
-    exact h.acyclic.irrefl s (hmtr.toTransGen lts (List.ne_nil_of_length_pos hlength))
-  · intro h
-    refine { acyclic := ⟨fun s hcycle => ?_⟩ }
-    obtain ⟨μs, hne, hmtr⟩ := (transGen_toRelation_iff lts).mp hcycle
-    exact h ⟨s, μs, hmtr, List.length_pos_of_ne_nil hne⟩
-
-/-- Finite LTSs are bounded. -/
-instance finiteLTS_bounded [Finite State] [lts.FiniteLTS] : lts.Bounded :=
-  (inferInstance : lts.Acyclic).toBounded
-
 /-- A state 'may terminate' if it can reach a terminated state. The definition of `Terminated`
 is a parameter. -/
 def MayTerminate (s : State) : Prop := ∃ s', Terminated s' ∧ lts.CanReach s s'
diff --git a/CslibTests/LTS.lean b/CslibTests/LTS.lean
index ad6f5718c..34f3c3db9 100644
--- a/CslibTests/LTS.lean
+++ b/CslibTests/LTS.lean
@@ -6,10 +6,8 @@ Authors: Fabrizio Montesi
 
 import Cslib.Foundations.Semantics.LTS.Divergence
 import Cslib.Foundations.Semantics.LTS.Bisimulation
-import Cslib.Foundations.Semantics.LTS.Termination
 import Mathlib.Algebra.Group.Even
 import Mathlib.Algebra.Ring.Parity
-import Mathlib.Order.WellFounded
 import Cslib.Foundations.Semantics.LTS.Notation
 
 namespace CslibTests
@@ -85,65 +83,6 @@ example : natDivLTS.Divergent n := by
     constructor
   · simp [natInfiniteExecution]
 
--- The three execution properties are distinct on infinite-state LTSs.
-
-def countdownLTS : LTS ℕ Unit where
-  Tr n _ m := n = m + 1
-
-instance : countdownLTS.Terminating where
-  terminating := by
-    apply Subrelation.wf _ Nat.lt_wfRel.wf
-    rintro s2 s1 ⟨μ, h⟩
-    change s2 < s1
-    simp only [countdownLTS] at h
-    omega
-
-example : countdownLTS.Acyclic := inferInstance
-example : Relation.Acyclic countdownLTS.toRelation := inferInstance
-
-private theorem countdownLTS_mTr (n : ℕ) :
-    countdownLTS.MTr n (List.replicate n ()) 0 := by
-  induction n with
-  | zero => exact .refl
-  | succ n ih =>
-      rw [List.replicate_succ]
-      exact .stepL (by simp [countdownLTS]) ih
-
-theorem countdownLTS_not_bounded : ¬ countdownLTS.Bounded := by
-  rintro ⟨bound, hbound⟩
-  have := hbound bound (List.replicate bound ()) 0 (countdownLTS_mTr bound)
-  simp at this
-
-def successorLTS : LTS ℕ Unit where
-  Tr n _ m := m = n + 1
-
-private theorem successorLTS_transGen_lt {n m : ℕ}
-    (h : Relation.TransGen successorLTS.toRelation n m) : n < m := by
-  apply Relation.transGen_minimal (r' := (· < ·)) at h
-  · exact h
-  · rintro n m ⟨μ, htr⟩
-    simp only [successorLTS] at htr
-    omega
-
-instance : successorLTS.Acyclic where
-  acyclic := ⟨fun n h => (Nat.lt_irrefl n) (successorLTS_transGen_lt h)⟩
-
-theorem successorLTS_not_terminating : ¬ successorLTS.Terminating := by
-  intro h
-  have hterminating := h.terminating
-  change WellFounded (fun a b => successorLTS.toRelation b a) at hterminating
-  rw [wellFounded_iff_isEmpty_descending_chain] at hterminating
-  exact hterminating.false ⟨fun n => n, by
-    intro n
-    exact ⟨(), by simp [successorLTS]⟩⟩
-
-def selfLoopLTS : LTS Unit Unit where
-  Tr _ _ _ := True
-
-theorem selfLoopLTS_not_acyclic : ¬ selfLoopLTS.Acyclic := by
-  intro h
-  exact h.acyclic.irrefl () (.single ⟨(), trivial⟩)
-
 -- Examples on decidable LTSs
 def natTrF (n : ℕ) (μ : ℕ) (m : ℕ) : Bool :=
   match n, μ, m with

From 75e9578b30c2e57d0abc717f4992aa8d71fd570a Mon Sep 17 00:00:00 2001
From: Samuel Schlesinger <sgschlesinger@gmail.com>
Date: Sun, 2 Aug 2026 09:00:49 -0400
Subject: [PATCH 5/5] refactor(LTS): rename toRelation to UnlabelledTr

Distinguishes the label-erasing relation from Tr.toRelation and
MTr.toRelation, which fix a label. Also renames the characterization
theorems reflTransGen_toRelation_iff and transGen_toRelation_iff to
match.
---
 Cslib/Foundations/Semantics/LTS/Basic.lean           |  6 +++---
 .../Semantics/LTS/ExampleTermination.lean            |  4 ++--
 Cslib/Foundations/Semantics/LTS/Execution.lean       |  4 ++--
 Cslib/Foundations/Semantics/LTS/Relation.lean        | 12 ++++++------
 Cslib/Foundations/Semantics/LTS/Termination.lean     |  6 +++---
 5 files changed, 16 insertions(+), 16 deletions(-)

diff --git a/Cslib/Foundations/Semantics/LTS/Basic.lean b/Cslib/Foundations/Semantics/LTS/Basic.lean
index 2c536f8bc..ba2932cee 100644
--- a/Cslib/Foundations/Semantics/LTS/Basic.lean
+++ b/Cslib/Foundations/Semantics/LTS/Basic.lean
@@ -68,7 +68,7 @@ structure LTS (State : Type u) (Label : Type v) where
 namespace LTS
 
 /-- The unlabelled transition relation underlying an LTS. -/
-def toRelation (lts : LTS State Label) : State → State → Prop :=
+def UnlabelledTr (lts : LTS State Label) : State → State → Prop :=
   fun s1 s2 => ∃ μ, lts.Tr s1 μ s2
 
 section MultiStep
@@ -375,12 +375,12 @@ class Bounded (lts : LTS State Label) where
 /-- An LTS is terminating if its underlying unlabelled transition relation is terminating,
 equivalently if it admits no infinite execution. -/
 class Terminating (lts : LTS State Label) where
-  terminating : Relation.Terminating lts.toRelation
+  terminating : Relation.Terminating lts.UnlabelledTr
 
 /-- An LTS is acyclic if its underlying unlabelled transition relation contains no nonempty
 cycle. -/
 class Acyclic (lts : LTS State Label) where
-  [acyclic : Relation.Acyclic lts.toRelation]
+  [acyclic : Relation.Acyclic lts.UnlabelledTr]
 
 attribute [instance] Acyclic.acyclic
 
diff --git a/Cslib/Foundations/Semantics/LTS/ExampleTermination.lean b/Cslib/Foundations/Semantics/LTS/ExampleTermination.lean
index a381a1122..a8010801a 100644
--- a/Cslib/Foundations/Semantics/LTS/ExampleTermination.lean
+++ b/Cslib/Foundations/Semantics/LTS/ExampleTermination.lean
@@ -32,7 +32,7 @@ instance countdownLTS_terminating : countdownLTS.Terminating where
     exact Nat.lt_succ_self s2
 
 example : countdownLTS.Acyclic := inferInstance
-example : Relation.Acyclic countdownLTS.toRelation := inferInstance
+example : Relation.Acyclic countdownLTS.UnlabelledTr := inferInstance
 
 private theorem countdownLTS_mTr (n : ℕ) :
     countdownLTS.MTr n (List.replicate n ()) 0 := by
@@ -51,7 +51,7 @@ def successorLTS : LTS ℕ Unit where
   Tr n _ m := m = n + 1
 
 private theorem successorLTS_transGen_lt {n m : ℕ}
-    (h : Relation.TransGen successorLTS.toRelation n m) : n < m := by
+    (h : Relation.TransGen successorLTS.UnlabelledTr n m) : n < m := by
   apply Relation.transGen_minimal (r' := (· < ·)) at h
   · exact h
   · rintro n m ⟨μ, htr⟩
diff --git a/Cslib/Foundations/Semantics/LTS/Execution.lean b/Cslib/Foundations/Semantics/LTS/Execution.lean
index d8b6a98bc..37dc1089b 100644
--- a/Cslib/Foundations/Semantics/LTS/Execution.lean
+++ b/Cslib/Foundations/Semantics/LTS/Execution.lean
@@ -86,8 +86,8 @@ theorem Execution.to_mTr (hexec : lts.Execution s1 μs s2 ss) :
 
 /-- The states visited by an execution form a chain in the underlying unlabelled relation. -/
 theorem Execution.isChain (hexec : lts.Execution s1 μs s2 ss) :
-    ss.IsChain lts.toRelation := by
-  grind [Execution, List.isChain_iff_getElem, toRelation]
+    ss.IsChain lts.UnlabelledTr := by
+  grind [Execution, List.isChain_iff_getElem, UnlabelledTr]
 
 open scoped Execution
 /-- Correspondence of multistep transitions and executions. -/
diff --git a/Cslib/Foundations/Semantics/LTS/Relation.lean b/Cslib/Foundations/Semantics/LTS/Relation.lean
index 57da4faa6..3253fa3eb 100644
--- a/Cslib/Foundations/Semantics/LTS/Relation.lean
+++ b/Cslib/Foundations/Semantics/LTS/Relation.lean
@@ -39,7 +39,7 @@ variable (lts : LTS State Label)
 /-- A multistep transition induces a reflexive-transitive path in the underlying unlabelled
 transition relation. -/
 theorem MTr.toReflTransGen (h : lts.MTr s1 μs s2) :
-    Relation.ReflTransGen lts.toRelation s1 s2 := by
+    Relation.ReflTransGen lts.UnlabelledTr s1 s2 := by
   induction h with
   | refl => exact .refl
   | stepL htr _ ih => exact ih.head ⟨_, htr⟩
@@ -47,15 +47,15 @@ theorem MTr.toReflTransGen (h : lts.MTr s1 μs s2) :
 /-- A nonempty multistep transition induces a nonempty path in the underlying unlabelled
 transition relation. -/
 theorem MTr.toTransGen (h : lts.MTr s1 μs s2) (hne : μs ≠ []) :
-    Relation.TransGen lts.toRelation s1 s2 := by
+    Relation.TransGen lts.UnlabelledTr s1 s2 := by
   cases h with
   | refl => contradiction
   | stepL htr hmtr => exact Relation.TransGen.head' ⟨_, htr⟩ (hmtr.toReflTransGen lts)
 
 /-- The reflexive-transitive closure of the underlying unlabelled transition relation is exactly
 reachability in the LTS. -/
-theorem reflTransGen_toRelation_iff :
-    Relation.ReflTransGen lts.toRelation s1 s2 ↔ lts.CanReach s1 s2 := by
+theorem reflTransGen_unlabelledTr_iff :
+    Relation.ReflTransGen lts.UnlabelledTr s1 s2 ↔ lts.CanReach s1 s2 := by
   constructor
   · intro h
     induction h with
@@ -69,8 +69,8 @@ theorem reflTransGen_toRelation_iff :
 
 /-- The transitive closure of the underlying unlabelled transition relation is exactly the
 nonempty multistep transitions of the LTS. -/
-theorem transGen_toRelation_iff :
-    Relation.TransGen lts.toRelation s1 s2 ↔
+theorem transGen_unlabelledTr_iff :
+    Relation.TransGen lts.UnlabelledTr s1 s2 ↔
       ∃ μs, μs ≠ [] ∧ lts.MTr s1 μs s2 := by
   constructor
   · intro h
diff --git a/Cslib/Foundations/Semantics/LTS/Termination.lean b/Cslib/Foundations/Semantics/LTS/Termination.lean
index 6b8c2f14b..9f3e4184c 100644
--- a/Cslib/Foundations/Semantics/LTS/Termination.lean
+++ b/Cslib/Foundations/Semantics/LTS/Termination.lean
@@ -32,7 +32,7 @@ theorem Bounded.toTerminating (h : lts.Bounded) : lts.Terminating := by
   rw [Relation.Terminating.iff_isEmpty_chain]
   constructor
   rintro ⟨f, hf⟩
-  change ∀ n, lts.toRelation (f n) (f (n + 1)) at hf
+  change ∀ n, lts.UnlabelledTr (f n) (f (n + 1)) at hf
   obtain ⟨bound, hbound⟩ := h.bounded
   have hpaths : ∀ n, ∃ μs, μs.length = n ∧ lts.MTr (f 0) μs (f n) := by
     intro n
@@ -67,9 +67,9 @@ theorem Acyclic.toBoundedUpTo [Finite State] (h : lts.Acyclic) :
   rw [Nat.card_eq_fintype_card]
   intro s1 μs s2 hmtr
   obtain ⟨states, hexec⟩ := Execution.of_mTr hmtr
-  have hchain : states.IsChain (Relation.TransGen lts.toRelation) :=
+  have hchain : states.IsChain (Relation.TransGen lts.UnlabelledTr) :=
     hexec.isChain.imp_of_mem_imp fun _ _ _ _ htr => .single htr
-  letI : Std.Irrefl (Relation.TransGen lts.toRelation) := h.acyclic
+  letI : Std.Irrefl (Relation.TransGen lts.UnlabelledTr) := h.acyclic
   have hcard := hchain.pairwise.nodup.length_le_card
   grind [Execution]