From 6a5a473faa2f1ff3c0a5f6daf29c8d5fda72d3f6 Mon Sep 17 00:00:00 2001
From: "Cuijpers, Pieter" <p.j.l.cuijpers@tue.nl>
Date: Fri, 17 Oct 2025 15:40:04 +0200
Subject: [PATCH 01/21] Considering the transitively closed \tau relation

---
 Cslib/Foundations/Semantics/LTS/Basic.lean    | 161 +++++++++++-------
 .../Semantics/LTS/Bisimulation.lean           |   4 +
 2 files changed, 108 insertions(+), 57 deletions(-)

diff --git a/Cslib/Foundations/Semantics/LTS/Basic.lean b/Cslib/Foundations/Semantics/LTS/Basic.lean
index 2176a77d..f4151c97 100644
--- a/Cslib/Foundations/Semantics/LTS/Basic.lean
+++ b/Cslib/Foundations/Semantics/LTS/Basic.lean
@@ -77,7 +77,7 @@ inductive LTS.MTr (lts : LTS State Label) : State → List Label → State → P
   | refl {s : State} : lts.MTr s [] s
   | stepL {s1 : State} {μ : Label} {s2 : State} {μs : List Label} {s3 : State} :
     lts.Tr s1 μ s2 → lts.MTr s2 μs s3 →
-    lts.MTr s1 (μ :: μs) s3
+   lts.MTr s1 (μ :: μs) s3
 
 /-- Any transition is also a multi-step transition. -/
 @[grind]
@@ -416,10 +416,14 @@ section Weak
 class HasTau (Label : Type v) where
   τ : Label
 
+/-- Saturated τ-transition relation. -/
+def LTS.τTr [HasTau Label] (lts : LTS State Label) : State → State → Prop :=
+  Relation.ReflTransGen (fun s1 s2 => lts.Tr s1 HasTau.τ s2)
+
 /-- Saturated transition relation. -/
 inductive LTS.STr [HasTau Label] (lts : LTS State Label) : State → Label → State → Prop where
 | refl : lts.STr s HasTau.τ s
-| tr : lts.STr s1 HasTau.τ s2 → lts.Tr s2 μ s3 → lts.STr s3 HasTau.τ s4 → lts.STr s1 μ s4
+| tr : lts.τTr s1 s2 → lts.Tr s2 μ s3 → lts.τTr s3 s4 → lts.STr s1 μ s4
 
 /-- The `LTS` obtained by saturating the transition relation in `lts`. -/
 @[grind =]
@@ -430,21 +434,37 @@ def LTS.saturate [HasTau Label] (lts : LTS State Label) : LTS State Label where
 @[grind]
 theorem LTS.STr.single [HasTau Label] (lts : LTS State Label) : lts.Tr s μ s' → lts.STr s μ s' := by
   intro h
-  apply LTS.STr.tr LTS.STr.refl h LTS.STr.refl
+  apply LTS.STr.tr Relation.ReflTransGen.refl h Relation.ReflTransGen.refl
+
+/-- STr transitions labeled by HasTau.τ are exactly the τTr transitions. -/
+@[grind]
+theorem LTS.STr_τTr [HasTau Label] (lts : LTS State Label) :
+  lts.STr s HasTau.τ s' ↔ lts.τTr s s' := by
+  apply Iff.intro <;> intro h
+  case mp =>
+    cases h
+    case refl => exact Relation.ReflTransGen.refl
+    case tr _ _ h1 h2 h3 =>
+      exact (Relation.ReflTransGen.trans h1 (Relation.ReflTransGen.head h2 h3))
+  case mpr =>
+    cases h
+    case refl => exact LTS.STr.refl
+    case tail _ h1 h2 => exact LTS.STr.tr h1 h2 Relation.ReflTransGen.refl
+
+/- Do we really need STrN?
 
 /-- As `LTS.str`, but counts the number of `τ`-transitions. This is convenient as induction
 metric. -/
-@[grind]
 inductive LTS.STrN [HasTau Label] (lts : LTS State Label) :
   ℕ → State → Label → State → Prop where
   | refl : lts.STrN 0 s HasTau.τ s
   | tr :
-    lts.STrN n s1 HasTau.τ s2 →
+    lts.τTrN n s1 s2 →
     lts.Tr s2 μ s3 →
-    lts.STrN m s3 HasTau.τ s4 →
+    lts.τTrN m s3 s4 →
     lts.STrN (n + m + 1) s1 μ s4
 
-/-- `LTS.str` and `LTS.strN` are equivalent. -/
+/-- `LTS.sTr` and `LTS.sTrN` are equivalent. -/
 @[grind]
 theorem LTS.sTr_sTrN [HasTau Label] (lts : LTS State Label) :
   lts.STr s1 μ s2 ↔ ∃ n, lts.STrN n s1 μ s2 := by
@@ -454,9 +474,9 @@ theorem LTS.sTr_sTrN [HasTau Label] (lts : LTS State Label) :
     case refl =>
       exists 0
       exact LTS.STrN.refl
-    case tr s1 sb μ sb' s2 hstr1 htr hstr2 ih1 ih2 =>
-      obtain ⟨n1, ih1⟩ := ih1
-      obtain ⟨n2, ih2⟩ := ih2
+    case tr _ _ hτ1 htr hτ2 =>
+      obtain ⟨n1, ih1⟩ := lts.τTr_imp_τTrN hτ1
+      obtain ⟨n2, ih2⟩ := lts.τTr_imp_τTrN hτ2
       exists (n1 + n2 + 1)
       apply LTS.STrN.tr ih1 htr ih2
   case mpr =>
@@ -464,32 +484,40 @@ theorem LTS.sTr_sTrN [HasTau Label] (lts : LTS State Label) :
     induction h
     case refl =>
       constructor
-    case tr n s1 sb μ sb' m s2 hstr1 htr hstr2 ih1 ih2 =>
-      apply LTS.STr.tr ih1 htr ih2
+    case tr m s1 s2 μ s3 k s4 hτ1 htr hτ2 =>
+      apply LTS.STr.tr (lts.τTrN_imp_τTr hτ1) htr (lts.τTrN_imp_τTr hτ2)
 
-/-- Saturated transitions labelled by τ can be composed (weighted version). -/
+/-- STrN transitions labeled by HasTau.τ are exactly the τTrN transitions. -/
 @[grind]
+theorem LTS.STrN_τTrN [HasTau Label] (lts : LTS State Label) :
+  lts.STrN n s HasTau.τ s' ↔ lts.τTrN n s s' := by
+  constructor <;> intro h
+  case mp =>
+    cases h
+    case refl => exact LTS.τTrN.refl
+    case tr n' _ _ m' h1 h2 h3 =>
+      have h4 := LTS.τTrN.tr h1 h2
+      have h5 := LTS.τTrN.append lts h4 h3
+      grind
+  case mpr =>
+    cases h
+    case refl => exact LTS.STrN.refl
+    case tr n' s'' h1 h2 => exact LTS.STrN.tr h1 h2 LTS.τTrN.refl
+
+@[grind]
+theorem LTS.τTr_imp_STrN_τ [HasTau Label] (lts : LTS State Label) :
+  lts.τTr s s' → ∃ n, lts.STrN n s HasTau.τ s' := by
+  intro h
+  obtain ⟨n, h⟩ := lts.τTr_imp_τTrN h
+  exists n
+  grind
+
+/-- Saturated transitions labelled by τ can be composed (weighted version). -/
 theorem LTS.STrN.trans_τ
   [HasTau Label] (lts : LTS State Label)
   (h1 : lts.STrN n s1 HasTau.τ s2) (h2 : lts.STrN m s2 HasTau.τ s3) :
-  lts.STrN (n + m) s1 HasTau.τ s3 := by
-  cases h1
-  case refl => grind
-  case tr n1 sb sb' n2 hstr1 htr hstr2 =>
-    have ih := LTS.STrN.trans_τ lts hstr2 h2
-    have conc := LTS.STrN.tr hstr1 htr ih
-    grind
+  lts.STrN (n + m) s1 HasTau.τ s3 := by grind
 
-/-- Saturated transitions labelled by τ can be composed. -/
-@[grind]
-theorem LTS.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
-  obtain ⟨n, h1N⟩ := (LTS.sTr_sTrN lts).1 h1
-  obtain ⟨m, h2N⟩ := (LTS.sTr_sTrN lts).1 h2
-  have concN := LTS.STrN.trans_τ lts h1N h2N
-  apply (LTS.sTr_sTrN lts).2 ⟨n + m, concN⟩
 
 /-- Saturated transitions can be appended with τ-transitions (weighted version). -/
 @[grind]
@@ -498,13 +526,13 @@ theorem LTS.STrN.append
   (h1 : lts.STrN n1 s1 μ s2)
   (h2 : lts.STrN n2 s2 HasTau.τ s3) :
   lts.STrN (n1 + n2) s1 μ s3 := by
+  rw [STrN_τTrN lts] at h2
   cases h1
   case refl => grind
-  case tr n11 sb sb' n12 hstr1 htr hstr2 =>
-    have hsuffix := LTS.STrN.trans_τ lts hstr2 h2
-    have n_eq : n11 + (n12 + n2) + 1 = (n11 + n12 + 1 + n2) := by omega
-    rw [← n_eq]
-    apply LTS.STrN.tr hstr1 htr hsuffix
+  case tr _ _ _ _ h3 h4 h5 =>
+    have h6 := LTS.τTrN.append lts h5 h2
+    have h7 := LTS.STrN.tr h3 h4 h6
+    grind
 
 /-- Saturated transitions can be composed (weighted version). -/
 @[grind]
@@ -514,13 +542,13 @@ theorem LTS.STrN.comp
   (h2 : lts.STrN n2 s2 μ s3)
   (h3 : lts.STrN n3 s3 HasTau.τ s4) :
   lts.STrN (n1 + n2 + n3) s1 μ s4 := by
+  rw [STrN_τTrN lts] at h1 h3
   cases h2
-  case refl =>
-    apply LTS.STrN.trans_τ lts h1 h3
-  case tr n21 sb sb' n22 hstr1 htr hstr2 =>
-    have hprefix_τ := LTS.STrN.trans_τ lts h1 hstr1
-    have hprefix := LTS.STrN.tr hprefix_τ htr hstr2
-    have conc := LTS.STrN.append lts hprefix h3
+  case refl => grind
+  case tr _ _ _ _ h4 h5 h6 =>
+    have h7 := LTS.τTrN.append lts h1 h4
+    have h8 := LTS.τTrN.append lts h6 h3
+    have h9 := LTS.STrN.tr h7 h5 h8
     grind
 
 /-- Saturated transitions can be composed. -/
@@ -531,16 +559,35 @@ theorem LTS.STr.comp
   (h2 : lts.STr s2 μ s3)
   (h3 : lts.STr s3 HasTau.τ s4) :
   lts.STr s1 μ s4 := by
-  obtain ⟨n1, h1N⟩ := (LTS.sTr_sTrN lts).1 h1
-  obtain ⟨n2, h2N⟩ := (LTS.sTr_sTrN lts).1 h2
-  obtain ⟨n3, h3N⟩ := (LTS.sTr_sTrN lts).1 h3
-  have concN := LTS.STrN.comp lts h1N h2N h3N
-  apply (LTS.sTr_sTrN lts).2 ⟨n1 + n2 + n3, concN⟩
+  rw [LTS.STr_τTr _] at h1 h3
+  cases h2
+  case refl =>
+    rw [LTS.STr_τTr _]
+    apply Relation.ReflTransGen.trans h1 h3
+  case tr _ _ hτ1 htr hτ2 =>
+    exact LTS.STr.tr (Relation.ReflTransGen.trans h1 hτ1) htr (Relation.ReflTransGen.trans hτ2 h3)
 
 @[grind _=_]
 lemma LTS.saturate_tr_sTr [HasTau Label] (lts : LTS State Label) :
   lts.saturate.Tr s HasTau.τ = lts.STr s HasTau.τ := by simp [LTS.saturate]
 
+/-- In a saturated LTS, the transition and saturated transition relations are the same. -/
+@[grind _=_]
+theorem LTS.saturate_τTr_τTr [hHasTau : HasTau Label] (lts : LTS State Label)
+  : lts.saturate.τTr s = lts.τTr s := by
+  ext s''
+  apply Iff.intro <;> intro h
+  case mp =>
+    induction h
+    case refl => constructor
+    case tail _ _ _ h2 h3 => exact Relation.ReflTransGen.trans h3 ((LTS.STr_τTr _).mp h2)
+  case mpr =>
+    cases h
+    case refl => constructor
+    case tail s' h2 h3 =>
+      have h4 := LTS.STr.tr h2 h3 Relation.ReflTransGen.refl
+      exact Relation.ReflTransGen.single h4
+
 /-- In a saturated LTS, the transition and saturated transition relations are the same. -/
 @[grind _=_]
 theorem LTS.saturate_sTr_tr [hHasTau : HasTau Label] (lts : LTS State Label)
@@ -548,20 +595,20 @@ theorem LTS.saturate_sTr_tr [hHasTau : HasTau Label] (lts : LTS State Label)
   ext s'
   apply Iff.intro <;> intro h
   case mp =>
-    induction h
+    cases h
     case refl => constructor
-    case tr s1 sb μ sb' s2 hstr1 htr hstr2 ih1 ih2 =>
-      rw [hμ] at htr
-      apply LTS.STr.single at htr
-      rw [← LTS.saturate_tr_sTr] at htr
-      grind [LTS.STr.tr]
+    case tr hstr1 htr hstr2 =>
+      apply LTS.STr.single
+      exact LTS.STr.tr hstr1 htr hstr2
   case mpr =>
-    induction h
+    cases h
     case refl => constructor
-    case tr s1 sb μ sb' s2 hstr1 htr hstr2 ih1 ih2 =>
-      simp only [LTS.saturate] at ih1 htr ih2
-      simp only [LTS.saturate]
-      grind
+    case tr hstr1 htr hstr2 =>
+      rw [LTS.saturate_τTr_τTr lts] at hstr1 hstr2
+      rw [←LTS.STr_τTr lts] at hstr1 hstr2
+      exact LTS.STr.comp lts hstr1 htr hstr2
+
+-/
 
 /-- In a saturated LTS, every state is in its τ-image. -/
 @[grind]
diff --git a/Cslib/Foundations/Semantics/LTS/Bisimulation.lean b/Cslib/Foundations/Semantics/LTS/Bisimulation.lean
index bcf40bae..c82f03db 100644
--- a/Cslib/Foundations/Semantics/LTS/Bisimulation.lean
+++ b/Cslib/Foundations/Semantics/LTS/Bisimulation.lean
@@ -809,6 +809,7 @@ theorem SWBisimulation.follow_internal_fst_n
     cases hstrN
     rename_i n1 sb sb' n2 hstrN1 htr hstrN2
     let hswb_m := hswb
+    rw [←LTS.STrN_τTrN] at hstrN1 hstrN2
     have ih1 := SWBisimulation.follow_internal_fst_n hswb hr hstrN1
     obtain ⟨sb2, hstrs2, hrsb⟩ := ih1
     have h := (hswb hrsb HasTau.τ).1 sb' htr
@@ -836,6 +837,7 @@ theorem SWBisimulation.follow_internal_snd_n
     cases hstrN
     rename_i n1 sb sb' n2 hstrN1 htr hstrN2
     let hswb_m := hswb
+    rw [←LTS.STrN_τTrN] at hstrN1 hstrN2
     have ih1 := SWBisimulation.follow_internal_snd_n hswb hr hstrN1
     obtain ⟨sb1, hstrs1, hrsb⟩ := ih1
     have h := (hswb hrsb HasTau.τ).2 sb' htr
@@ -897,6 +899,7 @@ theorem LTS.isWeakBisimulation_iff_isSWBisimulation
         constructor; constructor
         exact hr
       case tr sb sb' hstr1 htr hstr2 =>
+        rw [←LTS.STr_τTr] at hstr1 hstr2
         obtain ⟨sb2, hstr2b, hrb⟩ := SWBisimulation.follow_internal_fst h hr hstr1
         obtain ⟨sb2', hstr2b', hrb'⟩ := (h hrb μ).1 _ htr
         obtain ⟨s2', hstr2', hrb2⟩ := SWBisimulation.follow_internal_fst h hrb' hstr2
@@ -912,6 +915,7 @@ theorem LTS.isWeakBisimulation_iff_isSWBisimulation
         constructor; constructor
         exact hr
       case tr sb sb' hstr1 htr hstr2 =>
+        rw [←LTS.STr_τTr] at hstr1 hstr2
         obtain ⟨sb1, hstr1b, hrb⟩ := SWBisimulation.follow_internal_snd h hr hstr1
         obtain ⟨sb2', hstr1b', hrb'⟩ := (h hrb μ).2 _ htr
         obtain ⟨s1', hstr1', hrb2⟩ := SWBisimulation.follow_internal_snd h hrb' hstr2

From cd91c3518d14bbf0e9e4635c33f9cf5d8374b0db Mon Sep 17 00:00:00 2001
From: "Cuijpers, Pieter" <p.j.l.cuijpers@tue.nl>
Date: Fri, 17 Oct 2025 17:47:34 +0200
Subject: [PATCH 02/21] Completed introduction of tauTr, entire library builds
 correctly now. Removed some of the STrN theorems, as I think most of them are
 no longer necessary. Bisimulation theorems now complete using grind.

---
 Cslib/Foundations/Semantics/LTS/Basic.lean    | 306 ++++++++----------
 .../Semantics/LTS/Bisimulation.lean           |  10 +-
 2 files changed, 134 insertions(+), 182 deletions(-)

diff --git a/Cslib/Foundations/Semantics/LTS/Basic.lean b/Cslib/Foundations/Semantics/LTS/Basic.lean
index f4151c97..2f25455f 100644
--- a/Cslib/Foundations/Semantics/LTS/Basic.lean
+++ b/Cslib/Foundations/Semantics/LTS/Basic.lean
@@ -145,6 +145,74 @@ def LTS.generatedBy (s : State) : LTS {s' : State // lts.CanReach s s'} Label wh
 
 end MultiStep
 
+section Relation
+
+/-- Returns the relation that relates all states `s1` and `s2` via a fixed transition label `μ`. -/
+def LTS.Tr.toRelation (lts : LTS State Label) (μ : Label) : State → State → Prop :=
+  fun s1 s2 => lts.Tr s1 μ s2
+
+/-- Returns the relation that relates all states `s1` and `s2` via a fixed list of transition
+labels `μs`. -/
+def LTS.MTr.toRelation (lts : LTS State Label) (μs : List Label) : State → State → Prop :=
+  fun s1 s2 => lts.MTr s1 μs s2
+
+/-- Any homogeneous relation can be seen as an LTS where all transitions have the same label. -/
+def Relation.toLTS [DecidableEq Label] (r : State → State → Prop) (μ : Label) :
+  LTS State Label where
+  Tr := fun s1 μ' s2 => if μ' = μ then r s1 s2 else False
+
+end Relation
+
+section Trans
+
+/-! ## Support for the calc tactic -/
+
+/-- Transitions can be chained. -/
+instance (lts : LTS State Label) :
+  Trans
+    (LTS.Tr.toRelation lts μ1)
+    (LTS.Tr.toRelation lts μ2)
+    (LTS.MTr.toRelation lts [μ1, μ2]) where
+  trans := by
+    intro s1 s2 s3 htr1 htr2
+    apply LTS.MTr.single at htr1
+    apply LTS.MTr.single at htr2
+    apply LTS.MTr.comp lts htr1 htr2
+
+/-- Transitions can be chained with multi-step transitions. -/
+instance (lts : LTS State Label) :
+  Trans
+    (LTS.Tr.toRelation lts μ)
+    (LTS.MTr.toRelation lts μs)
+    (LTS.MTr.toRelation lts (μ :: μs)) where
+  trans := by
+    intro s1 s2 s3 htr1 hmtr2
+    apply LTS.MTr.single at htr1
+    apply LTS.MTr.comp lts htr1 hmtr2
+
+/-- Multi-step transitions can be chained with transitions. -/
+instance (lts : LTS State Label) :
+  Trans
+    (LTS.MTr.toRelation lts μs)
+    (LTS.Tr.toRelation lts μ)
+    (LTS.MTr.toRelation lts (μs ++ [μ])) where
+  trans := by
+    intro s1 s2 s3 hmtr1 htr2
+    apply LTS.MTr.single at htr2
+    apply LTS.MTr.comp lts hmtr1 htr2
+
+/-- Multi-step transitions can be chained. -/
+instance (lts : LTS State Label) :
+  Trans
+    (LTS.MTr.toRelation lts μs1)
+    (LTS.MTr.toRelation lts μs2)
+    (LTS.MTr.toRelation lts (μs1 ++ μs2)) where
+  trans := by
+    intro s1 s2 s3 hmtr1 hmtr2
+    apply LTS.MTr.comp lts hmtr1 hmtr2
+
+end Trans
+
 section Termination
 /-! ## Definitions about termination -/
 
@@ -418,7 +486,7 @@ class HasTau (Label : Type v) where
 
 /-- Saturated τ-transition relation. -/
 def LTS.τTr [HasTau Label] (lts : LTS State Label) : State → State → Prop :=
-  Relation.ReflTransGen (fun s1 s2 => lts.Tr s1 HasTau.τ s2)
+  Relation.ReflTransGen (Tr.toRelation lts HasTau.τ)
 
 /-- Saturated transition relation. -/
 inductive LTS.STr [HasTau Label] (lts : LTS State Label) : State → Label → State → Prop where
@@ -434,7 +502,7 @@ def LTS.saturate [HasTau Label] (lts : LTS State Label) : LTS State Label where
 @[grind]
 theorem LTS.STr.single [HasTau Label] (lts : LTS State Label) : lts.Tr s μ s' → lts.STr s μ s' := by
   intro h
-  apply LTS.STr.tr Relation.ReflTransGen.refl h Relation.ReflTransGen.refl
+  apply LTS.STr.tr .refl h .refl
 
 /-- STr transitions labeled by HasTau.τ are exactly the τTr transitions. -/
 @[grind]
@@ -443,113 +511,13 @@ theorem LTS.STr_τTr [HasTau Label] (lts : LTS State Label) :
   apply Iff.intro <;> intro h
   case mp =>
     cases h
-    case refl => exact Relation.ReflTransGen.refl
+    case refl => exact .refl
     case tr _ _ h1 h2 h3 =>
-      exact (Relation.ReflTransGen.trans h1 (Relation.ReflTransGen.head h2 h3))
+      exact (.trans h1 (.head h2 h3))
   case mpr =>
     cases h
     case refl => exact LTS.STr.refl
-    case tail _ h1 h2 => exact LTS.STr.tr h1 h2 Relation.ReflTransGen.refl
-
-/- Do we really need STrN?
-
-/-- As `LTS.str`, but counts the number of `τ`-transitions. This is convenient as induction
-metric. -/
-inductive LTS.STrN [HasTau Label] (lts : LTS State Label) :
-  ℕ → State → Label → State → Prop where
-  | refl : lts.STrN 0 s HasTau.τ s
-  | tr :
-    lts.τTrN n s1 s2 →
-    lts.Tr s2 μ s3 →
-    lts.τTrN m s3 s4 →
-    lts.STrN (n + m + 1) s1 μ s4
-
-/-- `LTS.sTr` and `LTS.sTrN` are equivalent. -/
-@[grind]
-theorem LTS.sTr_sTrN [HasTau Label] (lts : LTS State Label) :
-  lts.STr s1 μ s2 ↔ ∃ n, lts.STrN n s1 μ s2 := by
-  apply Iff.intro <;> intro h
-  case mp =>
-    induction h
-    case refl =>
-      exists 0
-      exact LTS.STrN.refl
-    case tr _ _ hτ1 htr hτ2 =>
-      obtain ⟨n1, ih1⟩ := lts.τTr_imp_τTrN hτ1
-      obtain ⟨n2, ih2⟩ := lts.τTr_imp_τTrN hτ2
-      exists (n1 + n2 + 1)
-      apply LTS.STrN.tr ih1 htr ih2
-  case mpr =>
-    obtain ⟨n, h⟩ := h
-    induction h
-    case refl =>
-      constructor
-    case tr m s1 s2 μ s3 k s4 hτ1 htr hτ2 =>
-      apply LTS.STr.tr (lts.τTrN_imp_τTr hτ1) htr (lts.τTrN_imp_τTr hτ2)
-
-/-- STrN transitions labeled by HasTau.τ are exactly the τTrN transitions. -/
-@[grind]
-theorem LTS.STrN_τTrN [HasTau Label] (lts : LTS State Label) :
-  lts.STrN n s HasTau.τ s' ↔ lts.τTrN n s s' := by
-  constructor <;> intro h
-  case mp =>
-    cases h
-    case refl => exact LTS.τTrN.refl
-    case tr n' _ _ m' h1 h2 h3 =>
-      have h4 := LTS.τTrN.tr h1 h2
-      have h5 := LTS.τTrN.append lts h4 h3
-      grind
-  case mpr =>
-    cases h
-    case refl => exact LTS.STrN.refl
-    case tr n' s'' h1 h2 => exact LTS.STrN.tr h1 h2 LTS.τTrN.refl
-
-@[grind]
-theorem LTS.τTr_imp_STrN_τ [HasTau Label] (lts : LTS State Label) :
-  lts.τTr s s' → ∃ n, lts.STrN n s HasTau.τ s' := by
-  intro h
-  obtain ⟨n, h⟩ := lts.τTr_imp_τTrN h
-  exists n
-  grind
-
-/-- Saturated transitions labelled by τ can be composed (weighted version). -/
-theorem LTS.STrN.trans_τ
-  [HasTau Label] (lts : LTS State Label)
-  (h1 : lts.STrN n s1 HasTau.τ s2) (h2 : lts.STrN m s2 HasTau.τ s3) :
-  lts.STrN (n + m) s1 HasTau.τ s3 := by grind
-
-
-/-- Saturated transitions can be appended with τ-transitions (weighted version). -/
-@[grind]
-theorem LTS.STrN.append
-  [HasTau Label] (lts : LTS State Label)
-  (h1 : lts.STrN n1 s1 μ s2)
-  (h2 : lts.STrN n2 s2 HasTau.τ s3) :
-  lts.STrN (n1 + n2) s1 μ s3 := by
-  rw [STrN_τTrN lts] at h2
-  cases h1
-  case refl => grind
-  case tr _ _ _ _ h3 h4 h5 =>
-    have h6 := LTS.τTrN.append lts h5 h2
-    have h7 := LTS.STrN.tr h3 h4 h6
-    grind
-
-/-- Saturated transitions can be composed (weighted version). -/
-@[grind]
-theorem LTS.STrN.comp
-  [HasTau Label] (lts : LTS State Label)
-  (h1 : lts.STrN n1 s1 HasTau.τ s2)
-  (h2 : lts.STrN n2 s2 μ s3)
-  (h3 : lts.STrN n3 s3 HasTau.τ s4) :
-  lts.STrN (n1 + n2 + n3) s1 μ s4 := by
-  rw [STrN_τTrN lts] at h1 h3
-  cases h2
-  case refl => grind
-  case tr _ _ _ _ h4 h5 h6 =>
-    have h7 := LTS.τTrN.append lts h1 h4
-    have h8 := LTS.τTrN.append lts h6 h3
-    have h9 := LTS.STrN.tr h7 h5 h8
-    grind
+    case tail _ h1 h2 => exact LTS.STr.tr h1 h2 .refl
 
 /-- Saturated transitions can be composed. -/
 @[grind]
@@ -608,8 +576,6 @@ theorem LTS.saturate_sTr_tr [hHasTau : HasTau Label] (lts : LTS State Label)
       rw [←LTS.STr_τTr lts] at hstr1 hstr2
       exact LTS.STr.comp lts hstr1 htr hstr2
 
--/
-
 /-- In a saturated LTS, every state is in its τ-image. -/
 @[grind]
 theorem LTS.mem_saturate_image_τ [HasTau Label] (lts : LTS State Label) :
@@ -621,6 +587,65 @@ by performing only `τ`-transitions. -/
 def LTS.τClosure [HasTau Label] (lts : LTS State Label) (S : Set State) : Set State :=
   lts.saturate.setImage S HasTau.τ
 
+/-- As `LTS.str`, but counts the number of `τ`-transitions. This is convenient as induction
+metric. -/
+@[grind]
+inductive LTS.STrN [HasTau Label] (lts : LTS State Label) :
+  ℕ → State → Label → State → Prop where
+  | refl : lts.STrN 0 s HasTau.τ s
+  | tr :
+    lts.STrN n s1 HasTau.τ s2 →
+    lts.Tr s2 μ s3 →
+    lts.STrN m s3 HasTau.τ s4 →
+    lts.STrN (n + m + 1) s1 μ s4
+
+@[grind]
+theorem LTS.τTr_imp_sTrN [HasTau Label] (lts : LTS State Label) :
+  lts.τTr s1 s2 → ∃ n, lts.STrN n s1 HasTau.τ s2 := by
+  intro h
+  induction h
+  case refl =>
+    exists 0
+    apply LTS.STrN.refl
+  case tail _ _ _ htr ih =>
+    obtain ⟨n, hn⟩ := ih
+    exists (n + 1)
+    apply LTS.STrN.tr hn htr LTS.STrN.refl
+
+@[grind]
+theorem LTS.sTrN_imp_τTr [HasTau Label] (lts : LTS State Label) :
+  lts.STrN n s1 HasTau.τ s2 → lts.τTr s1 s2 := by
+  intro h
+  cases h
+  case refl => exact Relation.ReflTransGen.refl
+  case tr m _ _ k hτ1 htr hτ2 =>
+    have hτ1' := LTS.sTrN_imp_τTr lts hτ1
+    have hτ3' := LTS.sTrN_imp_τTr lts hτ2
+    exact Relation.ReflTransGen.trans hτ1' (Relation.ReflTransGen.head htr hτ3')
+
+/-- `LTS.str` and `LTS.strN` are equivalent. -/
+@[grind]
+theorem LTS.sTr_sTrN [HasTau Label] (lts : LTS State Label) :
+  lts.STr s1 μ s2 ↔ ∃ n, lts.STrN n s1 μ s2 := by
+  apply Iff.intro <;> intro h
+  case mp =>
+    induction h
+    case refl =>
+      exists 0
+      apply LTS.STrN.refl
+    case tr _ _ hτ1 htr hτ2 =>
+      obtain ⟨n, hn⟩ := LTS.τTr_imp_sTrN lts hτ1
+      obtain ⟨m, hm⟩ := LTS.τTr_imp_sTrN lts hτ2
+      exists (n + m + 1)
+      apply LTS.STrN.tr hn htr hm
+  case mpr =>
+    obtain ⟨n, hn⟩ := h
+    induction hn
+    case refl =>
+      exact LTS.STr.refl
+    case tr _ _ _ _ _ _ h2 _ h1 h3 =>
+      exact LTS.STr.comp lts h1 (LTS.STr.single lts h2) h3
+
 end Weak
 
 /-! ## Divergence -/
@@ -654,73 +679,6 @@ def LTS.DivergenceFree [HasTau Label] (lts : LTS State Label) : Prop :=
 
 end Divergence
 
-section Relation
-
-/-- Returns the relation that relates all states `s1` and `s2` via a fixed transition label `μ`. -/
-def LTS.Tr.toRelation (lts : LTS State Label) (μ : Label) : State → State → Prop :=
-  fun s1 s2 => lts.Tr s1 μ s2
-
-/-- Returns the relation that relates all states `s1` and `s2` via a fixed list of transition
-labels `μs`. -/
-def LTS.MTr.toRelation (lts : LTS State Label) (μs : List Label) : State → State → Prop :=
-  fun s1 s2 => lts.MTr s1 μs s2
-
-/-- Any homogeneous relation can be seen as an LTS where all transitions have the same label. -/
-def Relation.toLTS [DecidableEq Label] (r : State → State → Prop) (μ : Label) :
-  LTS State Label where
-  Tr := fun s1 μ' s2 => if μ' = μ then r s1 s2 else False
-
-end Relation
-
-section Trans
-
-/-! ## Support for the calc tactic -/
-
-/-- Transitions can be chained. -/
-instance (lts : LTS State Label) :
-  Trans
-    (LTS.Tr.toRelation lts μ1)
-    (LTS.Tr.toRelation lts μ2)
-    (LTS.MTr.toRelation lts [μ1, μ2]) where
-  trans := by
-    intro s1 s2 s3 htr1 htr2
-    apply LTS.MTr.single at htr1
-    apply LTS.MTr.single at htr2
-    apply LTS.MTr.comp lts htr1 htr2
-
-/-- Transitions can be chained with multi-step transitions. -/
-instance (lts : LTS State Label) :
-  Trans
-    (LTS.Tr.toRelation lts μ)
-    (LTS.MTr.toRelation lts μs)
-    (LTS.MTr.toRelation lts (μ :: μs)) where
-  trans := by
-    intro s1 s2 s3 htr1 hmtr2
-    apply LTS.MTr.single at htr1
-    apply LTS.MTr.comp lts htr1 hmtr2
-
-/-- Multi-step transitions can be chained with transitions. -/
-instance (lts : LTS State Label) :
-  Trans
-    (LTS.MTr.toRelation lts μs)
-    (LTS.Tr.toRelation lts μ)
-    (LTS.MTr.toRelation lts (μs ++ [μ])) where
-  trans := by
-    intro s1 s2 s3 hmtr1 htr2
-    apply LTS.MTr.single at htr2
-    apply LTS.MTr.comp lts hmtr1 htr2
-
-/-- Multi-step transitions can be chained. -/
-instance (lts : LTS State Label) :
-  Trans
-    (LTS.MTr.toRelation lts μs1)
-    (LTS.MTr.toRelation lts μs2)
-    (LTS.MTr.toRelation lts (μs1 ++ μs2)) where
-  trans := by
-    intro s1 s2 s3 hmtr1 hmtr2
-    apply LTS.MTr.comp lts hmtr1 hmtr2
-
-end Trans
 
 open Lean Elab Meta Command Term
 
diff --git a/Cslib/Foundations/Semantics/LTS/Bisimulation.lean b/Cslib/Foundations/Semantics/LTS/Bisimulation.lean
index c82f03db..0b09b456 100644
--- a/Cslib/Foundations/Semantics/LTS/Bisimulation.lean
+++ b/Cslib/Foundations/Semantics/LTS/Bisimulation.lean
@@ -809,7 +809,6 @@ theorem SWBisimulation.follow_internal_fst_n
     cases hstrN
     rename_i n1 sb sb' n2 hstrN1 htr hstrN2
     let hswb_m := hswb
-    rw [←LTS.STrN_τTrN] at hstrN1 hstrN2
     have ih1 := SWBisimulation.follow_internal_fst_n hswb hr hstrN1
     obtain ⟨sb2, hstrs2, hrsb⟩ := ih1
     have h := (hswb hrsb HasTau.τ).1 sb' htr
@@ -817,9 +816,7 @@ theorem SWBisimulation.follow_internal_fst_n
     have ih2 := SWBisimulation.follow_internal_fst_n hswb hrsb2 hstrN2
     obtain ⟨s2', hstrs2', hrs2⟩ := ih2
     exists s2'
-    constructor
-    · apply LTS.STr.trans_τ lts (LTS.STr.trans_τ lts hstrs2 hstrsb2) hstrs2'
-    · exact hrs2
+    grind
 
 /-- Utility theorem for 'following' internal transitions using an `SWBisimulation`
 (second component, weighted version). -/
@@ -837,7 +834,6 @@ theorem SWBisimulation.follow_internal_snd_n
     cases hstrN
     rename_i n1 sb sb' n2 hstrN1 htr hstrN2
     let hswb_m := hswb
-    rw [←LTS.STrN_τTrN] at hstrN1 hstrN2
     have ih1 := SWBisimulation.follow_internal_snd_n hswb hr hstrN1
     obtain ⟨sb1, hstrs1, hrsb⟩ := ih1
     have h := (hswb hrsb HasTau.τ).2 sb' htr
@@ -845,9 +841,7 @@ theorem SWBisimulation.follow_internal_snd_n
     have ih2 := SWBisimulation.follow_internal_snd_n  hswb hrsb2 hstrN2
     obtain ⟨s2', hstrs2', hrs2⟩ := ih2
     exists s2'
-    constructor
-    · apply LTS.STr.trans_τ lts (LTS.STr.trans_τ lts hstrs1 hstrsb2) hstrs2'
-    · exact hrs2
+    grind
 
 /-- Utility theorem for 'following' internal transitions using an `SWBisimulation`
 (first component). -/

From 2092148e16f818d1b078277b0fd3a0dac77d3553 Mon Sep 17 00:00:00 2001
From: "Cuijpers, Pieter" <p.j.l.cuijpers@tue.nl>
Date: Fri, 17 Oct 2025 17:51:40 +0200
Subject: [PATCH 03/21] Perhaps keep those STrN theorems after all?

---
 Cslib/Foundations/Semantics/LTS/Basic.lean | 31 ++++++++++++++++++++++
 1 file changed, 31 insertions(+)

diff --git a/Cslib/Foundations/Semantics/LTS/Basic.lean b/Cslib/Foundations/Semantics/LTS/Basic.lean
index 2f25455f..ee85d97f 100644
--- a/Cslib/Foundations/Semantics/LTS/Basic.lean
+++ b/Cslib/Foundations/Semantics/LTS/Basic.lean
@@ -623,6 +623,11 @@ theorem LTS.sTrN_imp_τTr [HasTau Label] (lts : LTS State Label) :
     have hτ3' := LTS.sTrN_imp_τTr lts hτ2
     exact Relation.ReflTransGen.trans hτ1' (Relation.ReflTransGen.head htr hτ3')
 
+@[grind]
+theorem LTS.τTr_sTrN [HasTau Label] (lts : LTS State Label) :
+  lts.τTr s1 s2 ↔ ∃ n, lts.STrN n s1 HasTau.τ s2 := by
+  grind
+
 /-- `LTS.str` and `LTS.strN` are equivalent. -/
 @[grind]
 theorem LTS.sTr_sTrN [HasTau Label] (lts : LTS State Label) :
@@ -646,6 +651,32 @@ theorem LTS.sTr_sTrN [HasTau Label] (lts : LTS State Label) :
     case tr _ _ _ _ _ _ h2 _ h1 h3 =>
       exact LTS.STr.comp lts h1 (LTS.STr.single lts h2) h3
 
+/-- Saturated transitions labelled by τ can be composed (weighted version). -/
+theorem LTS.STrN.trans_τ
+    [HasTau Label] (lts : LTS State Label)
+    (h1 : lts.STrN n s1 HasTau.τ s2) (h2 : lts.STrN m s2 HasTau.τ s3) :
+    lts.STrN (n + m) s1 HasTau.τ s3 := by
+  sorry
+
+/-- Saturated transitions can be appended with τ-transitions (weighted version). -/
+@[grind]
+theorem LTS.STrN.append
+    [HasTau Label] (lts : LTS State Label)
+    (h1 : lts.STrN n1 s1 μ s2)
+    (h2 : lts.STrN n2 s2 HasTau.τ s3) :
+    lts.STrN (n1 + n2) s1 μ s3 := by
+  sorry
+
+/-- Saturated transitions can be composed (weighted version). -/
+@[grind]
+theorem LTS.STrN.comp
+    [HasTau Label] (lts : LTS State Label)
+    (h1 : lts.STrN n1 s1 HasTau.τ s2)
+    (h2 : lts.STrN n2 s2 μ s3)
+    (h3 : lts.STrN n3 s3 HasTau.τ s4) :
+    lts.STrN (n1 + n2 + n3) s1 μ s4 := by
+  sorry
+
 end Weak
 
 /-! ## Divergence -/

From 43f9e97c337d69a273ac4b2b295818df55c34145 Mon Sep 17 00:00:00 2001
From: "Cuijpers, Pieter" <p.j.l.cuijpers@tue.nl>
Date: Mon, 15 Dec 2025 10:42:19 +0100
Subject: [PATCH 04/21] removed redundant code that accidentally stayed after
 merge

---
 Cslib/Foundations/Semantics/LTS/Basic.lean | 52 ----------------------
 1 file changed, 52 deletions(-)

diff --git a/Cslib/Foundations/Semantics/LTS/Basic.lean b/Cslib/Foundations/Semantics/LTS/Basic.lean
index 1c5e22e0..40687dcb 100644
--- a/Cslib/Foundations/Semantics/LTS/Basic.lean
+++ b/Cslib/Foundations/Semantics/LTS/Basic.lean
@@ -497,10 +497,6 @@ theorem LTS.STr.comp
   case tr _ _ hτ1 htr hτ2 =>
     exact LTS.STr.tr (Relation.ReflTransGen.trans h1 hτ1) htr (Relation.ReflTransGen.trans hτ2 h3)
 
-@[grind _=_]
-lemma LTS.saturate_tr_sTr [HasTau Label] (lts : LTS State Label) :
-  lts.saturate.Tr s HasTau.τ = lts.STr s HasTau.τ := by simp [LTS.saturate]
-
 /-- In a saturated LTS, the transition and saturated transition relations are the same. -/
 @[grind _=_]
 theorem LTS.saturate_τTr_τTr [hHasTau : HasTau Label] (lts : LTS State Label)
@@ -663,54 +659,6 @@ theorem LTS.STrN.comp
     have conc := LTS.STrN.append lts hprefix h3
     grind
 
-/-- Saturated transitions can be composed. -/
-@[scoped grind <=]
-theorem LTS.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) :
-  lts.STr s1 μ s4 := by
-  obtain ⟨n1, h1N⟩ := (LTS.sTr_sTrN lts).1 h1
-  obtain ⟨n2, h2N⟩ := (LTS.sTr_sTrN lts).1 h2
-  obtain ⟨n3, h3N⟩ := (LTS.sTr_sTrN lts).1 h3
-  have concN := LTS.STrN.comp lts h1N h2N h3N
-  apply (LTS.sTr_sTrN lts).2 ⟨n1 + n2 + n3, concN⟩
-
-open scoped LTS.STr in
-/-- In a saturated LTS, the transition and saturated transition relations are the same. -/
-@[scoped grind _=_]
-theorem LTS.saturate_sTr_tr [hHasTau : HasTau Label] (lts : LTS State Label)
-  (hμ : μ = hHasTau.τ) : lts.saturate.Tr s μ = lts.saturate.STr s μ := by
-  ext s'
-  apply Iff.intro <;> intro h
-  case mp =>
-    induction h
-    case refl => constructor
-    case tr s1 sb μ sb' s2 hstr1 htr hstr2 ih1 ih2 =>
-      rw [hμ] at htr
-      apply LTS.STr.single at htr
-      rw [← LTS.saturate_tr_sTr] at htr
-      grind [LTS.STr.tr]
-  case mpr =>
-    induction h
-    case refl => constructor
-    case tr s1 sb μ sb' s2 hstr1 htr hstr2 ih1 ih2 =>
-      simp only [LTS.saturate] at ih1 htr ih2
-      simp only [LTS.saturate]
-      grind
-
-/-- In a saturated LTS, every state is in its τ-image. -/
-@[scoped grind .]
-theorem LTS.mem_saturate_image_τ [HasTau Label] (lts : LTS State Label) :
-  s ∈ lts.saturate.image s HasTau.τ := LTS.STr.refl
-
-/-- The `τ`-closure of a set of states `S` is the set of states reachable by any state in `S`
-by performing only `τ`-transitions. -/
-@[scoped grind =]
-def LTS.τClosure [HasTau Label] (lts : LTS State Label) (S : Set State) : Set State :=
-  lts.saturate.setImage S HasTau.τ
-
 end Weak
 
 /-! ## Divergence -/

From 8edd9ad4de18ceee86fbb0faa28553e492ffdd8c Mon Sep 17 00:00:00 2001
From: "Cuijpers, Pieter" <p.j.l.cuijpers@tue.nl>
Date: Mon, 15 Dec 2025 11:17:53 +0100
Subject: [PATCH 05/21] Proved STrN.append

---
 Cslib/Foundations/Semantics/LTS/Basic.lean | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/Cslib/Foundations/Semantics/LTS/Basic.lean b/Cslib/Foundations/Semantics/LTS/Basic.lean
index 40687dcb..cf5d86fc 100644
--- a/Cslib/Foundations/Semantics/LTS/Basic.lean
+++ b/Cslib/Foundations/Semantics/LTS/Basic.lean
@@ -640,7 +640,11 @@ theorem LTS.STrN.append
     (h1 : lts.STrN n1 s1 μ s2)
     (h2 : lts.STrN n2 s2 HasTau.τ s3) :
     lts.STrN (n1 + n2) s1 μ s3 := by
-  sorry
+  induction h1
+  case refl => grind
+  case tr hstr1 htr hstr2 ih1 ih2  =>
+    have conc := LTS.STrN.tr hstr1 htr (ih2 h2)
+    grind
 
 /-- Saturated transitions can be composed (weighted version). -/
 @[scoped grind <=]

From 76de0ff86820523a0d8aa73715b988ce775eb167 Mon Sep 17 00:00:00 2001
From: "Cuijpers, Pieter" <p.j.l.cuijpers@tue.nl>
Date: Mon, 15 Dec 2025 11:46:06 +0100
Subject: [PATCH 06/21] Renamed \tauTr to \tauSTr

---
 Cslib/Foundations/Semantics/LTS/Basic.lean | 18 +++++++++---------
 1 file changed, 9 insertions(+), 9 deletions(-)

diff --git a/Cslib/Foundations/Semantics/LTS/Basic.lean b/Cslib/Foundations/Semantics/LTS/Basic.lean
index cf5d86fc..88dad4be 100644
--- a/Cslib/Foundations/Semantics/LTS/Basic.lean
+++ b/Cslib/Foundations/Semantics/LTS/Basic.lean
@@ -442,13 +442,13 @@ class HasTau (Label : Type v) where
   τ : Label
 
 /-- Saturated τ-transition relation. -/
-def LTS.τTr [HasTau Label] (lts : LTS State Label) : State → State → Prop :=
+def LTS.τSTr [HasTau Label] (lts : LTS State Label) : State → State → Prop :=
   Relation.ReflTransGen (Tr.toRelation lts HasTau.τ)
 
 /-- Saturated transition relation. -/
 inductive LTS.STr [HasTau Label] (lts : LTS State Label) : State → Label → State → Prop where
 | refl : lts.STr s HasTau.τ s
-| tr : lts.τTr s1 s2 → lts.Tr s2 μ s3 → lts.τTr s3 s4 → lts.STr s1 μ s4
+| 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 =]
@@ -469,7 +469,7 @@ theorem LTS.STr.single [HasTau Label] (lts : LTS State Label) :
 /-- STr transitions labeled by HasTau.τ are exactly the τTr transitions. -/
 @[grind]
 theorem LTS.STr_τTr [HasTau Label] (lts : LTS State Label) :
-  lts.STr s HasTau.τ s' ↔ lts.τTr s s' := by
+  lts.STr s HasTau.τ s' ↔ lts.τSTr s s' := by
   apply Iff.intro <;> intro h
   case mp =>
     cases h
@@ -500,7 +500,7 @@ theorem LTS.STr.comp
 /-- In a saturated LTS, the transition and saturated transition relations are the same. -/
 @[grind _=_]
 theorem LTS.saturate_τTr_τTr [hHasTau : HasTau Label] (lts : LTS State Label)
-  : lts.saturate.τTr s = lts.τTr s := by
+  : lts.saturate.τSTr s = lts.τSTr s := by
   ext s''
   apply Iff.intro <;> intro h
   case mp =>
@@ -559,7 +559,7 @@ inductive LTS.STrN [HasTau Label] (lts : LTS State Label) :
 
 @[grind]
 theorem LTS.τTr_imp_sTrN [HasTau Label] (lts : LTS State Label) :
-  lts.τTr s1 s2 → ∃ n, lts.STrN n s1 HasTau.τ s2 := by
+  lts.τSTr s1 s2 → ∃ n, lts.STrN n s1 HasTau.τ s2 := by
   intro h
   induction h
   case refl =>
@@ -572,7 +572,7 @@ theorem LTS.τTr_imp_sTrN [HasTau Label] (lts : LTS State Label) :
 
 @[grind]
 theorem LTS.sTrN_imp_τTr [HasTau Label] (lts : LTS State Label) :
-  lts.STrN n s1 HasTau.τ s2 → lts.τTr s1 s2 := by
+  lts.STrN n s1 HasTau.τ s2 → lts.τSTr s1 s2 := by
   intro h
   cases h
   case refl => exact Relation.ReflTransGen.refl
@@ -582,11 +582,11 @@ theorem LTS.sTrN_imp_τTr [HasTau Label] (lts : LTS State Label) :
     exact Relation.ReflTransGen.trans hτ1' (Relation.ReflTransGen.head htr hτ3')
 
 @[grind]
-theorem LTS.τTr_sTrN [HasTau Label] (lts : LTS State Label) :
-  lts.τTr s1 s2 ↔ ∃ n, lts.STrN n s1 HasTau.τ s2 := by
+theorem LTS.τSTr_sTrN [HasTau Label] (lts : LTS State Label) :
+  lts.τSTr s1 s2 ↔ ∃ n, lts.STrN n s1 HasTau.τ s2 := by
   grind
 
-/-- `LTS.str` and `LTS.strN` are equivalent. -/
+/-- `LTS.sTr` and `LTS.sTrN` are equivalent. -/
 @[scoped grind =]
 theorem LTS.sTr_sTrN [HasTau Label] (lts : LTS State Label) :
   lts.STr s1 μ s2 ↔ ∃ n, lts.STrN n s1 μ s2 := by

From ea3b8a77baeb0144947be68cdfb3b4183221be58 Mon Sep 17 00:00:00 2001
From: "Cuijpers, Pieter" <p.j.l.cuijpers@tue.nl>
Date: Mon, 5 Jan 2026 14:41:00 +0100
Subject: [PATCH 07/21] Updated naming

---
 Cslib/Foundations/Semantics/LTS/Basic.lean | 54 +++++++++++-----------
 1 file changed, 27 insertions(+), 27 deletions(-)

diff --git a/Cslib/Foundations/Semantics/LTS/Basic.lean b/Cslib/Foundations/Semantics/LTS/Basic.lean
index be1ae944..edc7c88e 100644
--- a/Cslib/Foundations/Semantics/LTS/Basic.lean
+++ b/Cslib/Foundations/Semantics/LTS/Basic.lean
@@ -502,7 +502,7 @@ def LTS.saturate [HasTau Label] (lts : LTS State Label) : LTS State Label where
   Tr := lts.STr
 
 @[scoped grind _=_]
-theorem LTS.saturate_tr_sTr [HasTau Label] {lts : LTS State Label} :
+theorem LTS.saturate_tr_STr [HasTau Label] {lts : LTS State Label} :
   lts.saturate.Tr = lts.STr := by rfl
 
 /-- Any transition is also a saturated transition. -/
@@ -512,9 +512,9 @@ theorem LTS.STr.single [HasTau Label] (lts : LTS State Label) :
   intro h
   apply LTS.STr.tr .refl h .refl
 
-/-- STr transitions labeled by HasTau.τ are exactly the τTr transitions. -/
-@[grind]
-theorem LTS.STr_τTr [HasTau Label] (lts : LTS State Label) :
+/-- STr transitions labeled by HasTau.τ are exactly the τSTr transitions. -/
+@[grind _=_]
+theorem LTS.STr_τSTr [HasTau Label] (lts : LTS State Label) :
   lts.STr s HasTau.τ s' ↔ lts.τSTr s s' := by
   apply Iff.intro <;> intro h
   case mp =>
@@ -528,31 +528,31 @@ theorem LTS.STr_τTr [HasTau Label] (lts : LTS State Label) :
     case tail _ h1 h2 => exact LTS.STr.tr h1 h2 .refl
 
 /-- Saturated transitions can be composed. -/
-@[grind]
+@[grind →]
 theorem LTS.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) :
   lts.STr s1 μ s4 := by
-  rw [LTS.STr_τTr _] at h1 h3
+  rw [LTS.STr_τSTr _] at h1 h3
   cases h2
   case refl =>
-    rw [LTS.STr_τTr _]
+    rw [LTS.STr_τSTr _]
     apply Relation.ReflTransGen.trans h1 h3
   case tr _ _ hτ1 htr hτ2 =>
     exact LTS.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. -/
 @[grind _=_]
-theorem LTS.saturate_τTr_τTr [hHasTau : HasTau Label] (lts : LTS State Label)
+theorem LTS.saturate_τSTr_τSTr [hHasTau : HasTau Label] (lts : LTS State Label)
   : lts.saturate.τSTr s = lts.τSTr s := by
   ext s''
   apply Iff.intro <;> intro h
   case mp =>
     induction h
     case refl => constructor
-    case tail _ _ _ h2 h3 => exact Relation.ReflTransGen.trans h3 ((LTS.STr_τTr _).mp h2)
+    case tail _ _ _ h2 h3 => exact Relation.ReflTransGen.trans h3 ((LTS.STr_τSTr _).mp h2)
   case mpr =>
     cases h
     case refl => constructor
@@ -562,7 +562,7 @@ theorem LTS.saturate_τTr_τTr [hHasTau : HasTau Label] (lts : LTS State Label)
 
 /-- In a saturated LTS, the transition and saturated transition relations are the same. -/
 @[grind _=_]
-theorem LTS.saturate_sTr_tr [hHasTau : HasTau Label] (lts : LTS State Label)
+theorem LTS.saturate_Tr_saturate_STr [hHasTau : HasTau Label] (lts : LTS State Label)
   (hμ : μ = hHasTau.τ) : lts.saturate.Tr s μ = lts.saturate.STr s μ := by
   ext s'
   apply Iff.intro <;> intro h
@@ -576,12 +576,12 @@ theorem LTS.saturate_sTr_tr [hHasTau : HasTau Label] (lts : LTS State Label)
     cases h
     case refl => constructor
     case tr hstr1 htr hstr2 =>
-      rw [LTS.saturate_τTr_τTr lts] at hstr1 hstr2
-      rw [←LTS.STr_τTr lts] at hstr1 hstr2
+      rw [LTS.saturate_τSTr_τSTr lts] at hstr1 hstr2
+      rw [←LTS.STr_τSTr lts] at hstr1 hstr2
       exact LTS.STr.comp lts hstr1 htr hstr2
 
 /-- In a saturated LTS, every state is in its τ-image. -/
-@[grind]
+@[grind .]
 theorem LTS.mem_saturate_image_τ [HasTau Label] (lts : LTS State Label) :
   s ∈ lts.saturate.image s HasTau.τ := LTS.STr.refl
 
@@ -603,8 +603,8 @@ inductive LTS.STrN [HasTau Label] (lts : LTS State Label) :
     lts.STrN m s3 HasTau.τ s4 →
     lts.STrN (n + m + 1) s1 μ s4
 
-@[grind]
-theorem LTS.τTr_imp_sTrN [HasTau Label] (lts : LTS State Label) :
+@[grind .]
+theorem LTS.τSTr_imp_STrN [HasTau Label] (lts : LTS State Label) :
   lts.τSTr s1 s2 → ∃ n, lts.STrN n s1 HasTau.τ s2 := by
   intro h
   induction h
@@ -616,25 +616,25 @@ theorem LTS.τTr_imp_sTrN [HasTau Label] (lts : LTS State Label) :
     exists (n + 1)
     apply LTS.STrN.tr hn htr LTS.STrN.refl
 
-@[grind]
-theorem LTS.sTrN_imp_τTr [HasTau Label] (lts : LTS State Label) :
+@[grind .]
+theorem LTS.sTrN_imp_τSTr [HasTau Label] (lts : LTS State Label) :
   lts.STrN n s1 HasTau.τ s2 → lts.τSTr s1 s2 := by
   intro h
   cases h
   case refl => exact Relation.ReflTransGen.refl
   case tr m _ _ k hτ1 htr hτ2 =>
-    have hτ1' := LTS.sTrN_imp_τTr lts hτ1
-    have hτ3' := LTS.sTrN_imp_τTr lts hτ2
+    have hτ1' := LTS.sTrN_imp_τSTr lts hτ1
+    have hτ3' := LTS.sTrN_imp_τSTr lts hτ2
     exact Relation.ReflTransGen.trans hτ1' (Relation.ReflTransGen.head htr hτ3')
 
-@[grind]
-theorem LTS.τSTr_sTrN [HasTau Label] (lts : LTS State Label) :
+@[grind .]
+theorem LTS.τSTr_STrN [HasTau Label] (lts : LTS State Label) :
   lts.τSTr s1 s2 ↔ ∃ n, lts.STrN n s1 HasTau.τ s2 := by
   grind
 
 /-- `LTS.sTr` and `LTS.sTrN` are equivalent. -/
 @[scoped grind =]
-theorem LTS.sTr_sTrN [HasTau Label] (lts : LTS State Label) :
+theorem LTS.STr_STrN [HasTau Label] (lts : LTS State Label) :
   lts.STr s1 μ s2 ↔ ∃ n, lts.STrN n s1 μ s2 := by
   apply Iff.intro <;> intro h
   case mp =>
@@ -643,8 +643,8 @@ theorem LTS.sTr_sTrN [HasTau Label] (lts : LTS State Label) :
       exists 0
       apply LTS.STrN.refl
     case tr _ _ hτ1 htr hτ2 =>
-      obtain ⟨n, hn⟩ := LTS.τTr_imp_sTrN lts hτ1
-      obtain ⟨m, hm⟩ := LTS.τTr_imp_sTrN lts hτ2
+      obtain ⟨n, hn⟩ := LTS.τSTr_imp_STrN lts hτ1
+      obtain ⟨m, hm⟩ := LTS.τSTr_imp_STrN lts hτ2
       exists (n + m + 1)
       apply LTS.STrN.tr hn htr hm
   case mpr =>
@@ -674,10 +674,10 @@ theorem LTS.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
-  obtain ⟨n, h1N⟩ := (LTS.sTr_sTrN lts).1 h1
-  obtain ⟨m, h2N⟩ := (LTS.sTr_sTrN lts).1 h2
+  obtain ⟨n, h1N⟩ := (LTS.STr_STrN lts).1 h1
+  obtain ⟨m, h2N⟩ := (LTS.STr_STrN lts).1 h2
   have concN := LTS.STrN.trans_τ lts h1N h2N
-  apply (LTS.sTr_sTrN lts).2 ⟨n + m, concN⟩
+  apply (LTS.STr_STrN lts).2 ⟨n + m, concN⟩
 
 /-- Saturated transitions can be appended with τ-transitions (weighted version). -/
 @[scoped grind <=]

From f85abc22e5c509d898e797b55d304c49c742c27e Mon Sep 17 00:00:00 2001
From: "Cuijpers, Pieter" <p.j.l.cuijpers@tue.nl>
Date: Mon, 5 Jan 2026 15:01:02 +0100
Subject: [PATCH 08/21] Staying closer to original

---
 Cslib/Foundations/Semantics/LTS/Basic.lean | 32 +++++++++++-----------
 1 file changed, 16 insertions(+), 16 deletions(-)

diff --git a/Cslib/Foundations/Semantics/LTS/Basic.lean b/Cslib/Foundations/Semantics/LTS/Basic.lean
index edc7c88e..17ce3e24 100644
--- a/Cslib/Foundations/Semantics/LTS/Basic.lean
+++ b/Cslib/Foundations/Semantics/LTS/Basic.lean
@@ -87,7 +87,7 @@ inductive LTS.MTr (lts : LTS State Label) : State → List Label → State → P
   | refl {s : State} : lts.MTr s [] s
   | stepL {s1 : State} {μ : Label} {s2 : State} {μs : List Label} {s3 : State} :
     lts.Tr s1 μ s2 → lts.MTr s2 μs s3 →
-   lts.MTr s1 (μ :: μs) s3
+    lts.MTr s1 (μ :: μs) s3
 
 /-- Any transition is also a multistep transition. -/
 @[scoped grind →]
@@ -502,7 +502,7 @@ def LTS.saturate [HasTau Label] (lts : LTS State Label) : LTS State Label where
   Tr := lts.STr
 
 @[scoped grind _=_]
-theorem LTS.saturate_tr_STr [HasTau Label] {lts : LTS State Label} :
+theorem LTS.saturate_tr_sTr [HasTau Label] {lts : LTS State Label} :
   lts.saturate.Tr = lts.STr := by rfl
 
 /-- Any transition is also a saturated transition. -/
@@ -514,7 +514,7 @@ theorem LTS.STr.single [HasTau Label] (lts : LTS State Label) :
 
 /-- STr transitions labeled by HasTau.τ are exactly the τSTr transitions. -/
 @[grind _=_]
-theorem LTS.STr_τSTr [HasTau Label] (lts : LTS State Label) :
+theorem LTS.sTr_eq_τSTr [HasTau Label] (lts : LTS State Label) :
   lts.STr s HasTau.τ s' ↔ lts.τSTr s s' := by
   apply Iff.intro <;> intro h
   case mp =>
@@ -535,10 +535,10 @@ theorem LTS.STr.comp
   (h2 : lts.STr s2 μ s3)
   (h3 : lts.STr s3 HasTau.τ s4) :
   lts.STr s1 μ s4 := by
-  rw [LTS.STr_τSTr _] at h1 h3
+  rw [LTS.sTr_eq_τSTr _] at h1 h3
   cases h2
   case refl =>
-    rw [LTS.STr_τSTr _]
+    rw [LTS.sTr_eq_τSTr _]
     apply Relation.ReflTransGen.trans h1 h3
   case tr _ _ hτ1 htr hτ2 =>
     exact LTS.STr.tr (Relation.ReflTransGen.trans h1 hτ1) htr (Relation.ReflTransGen.trans hτ2 h3)
@@ -552,7 +552,7 @@ theorem LTS.saturate_τSTr_τSTr [hHasTau : HasTau Label] (lts : LTS State Label
   case mp =>
     induction h
     case refl => constructor
-    case tail _ _ _ h2 h3 => exact Relation.ReflTransGen.trans h3 ((LTS.STr_τSTr _).mp h2)
+    case tail _ _ _ h2 h3 => exact Relation.ReflTransGen.trans h3 ((LTS.sTr_eq_τSTr _).mp h2)
   case mpr =>
     cases h
     case refl => constructor
@@ -562,7 +562,7 @@ theorem LTS.saturate_τSTr_τSTr [hHasTau : HasTau Label] (lts : LTS State Label
 
 /-- In a saturated LTS, the transition and saturated transition relations are the same. -/
 @[grind _=_]
-theorem LTS.saturate_Tr_saturate_STr [hHasTau : HasTau Label] (lts : LTS State Label)
+theorem LTS.saturate_tr_saturate_sTr [hHasTau : HasTau Label] (lts : LTS State Label)
   (hμ : μ = hHasTau.τ) : lts.saturate.Tr s μ = lts.saturate.STr s μ := by
   ext s'
   apply Iff.intro <;> intro h
@@ -577,7 +577,7 @@ theorem LTS.saturate_Tr_saturate_STr [hHasTau : HasTau Label] (lts : LTS State L
     case refl => constructor
     case tr hstr1 htr hstr2 =>
       rw [LTS.saturate_τSTr_τSTr lts] at hstr1 hstr2
-      rw [←LTS.STr_τSTr lts] at hstr1 hstr2
+      rw [←LTS.sTr_eq_τSTr lts] at hstr1 hstr2
       exact LTS.STr.comp lts hstr1 htr hstr2
 
 /-- In a saturated LTS, every state is in its τ-image. -/
@@ -604,7 +604,7 @@ inductive LTS.STrN [HasTau Label] (lts : LTS State Label) :
     lts.STrN (n + m + 1) s1 μ s4
 
 @[grind .]
-theorem LTS.τSTr_imp_STrN [HasTau Label] (lts : LTS State Label) :
+theorem LTS.τSTr_imp_sTrN [HasTau Label] (lts : LTS State Label) :
   lts.τSTr s1 s2 → ∃ n, lts.STrN n s1 HasTau.τ s2 := by
   intro h
   induction h
@@ -628,13 +628,13 @@ theorem LTS.sTrN_imp_τSTr [HasTau Label] (lts : LTS State Label) :
     exact Relation.ReflTransGen.trans hτ1' (Relation.ReflTransGen.head htr hτ3')
 
 @[grind .]
-theorem LTS.τSTr_STrN [HasTau Label] (lts : LTS State Label) :
+theorem LTS.τSTr_eq_sTrN [HasTau Label] (lts : LTS State Label) :
   lts.τSTr s1 s2 ↔ ∃ n, lts.STrN n s1 HasTau.τ s2 := by
   grind
 
 /-- `LTS.sTr` and `LTS.sTrN` are equivalent. -/
 @[scoped grind =]
-theorem LTS.STr_STrN [HasTau Label] (lts : LTS State Label) :
+theorem LTS.sTr_eq_sTrN [HasTau Label] (lts : LTS State Label) :
   lts.STr s1 μ s2 ↔ ∃ n, lts.STrN n s1 μ s2 := by
   apply Iff.intro <;> intro h
   case mp =>
@@ -643,8 +643,8 @@ theorem LTS.STr_STrN [HasTau Label] (lts : LTS State Label) :
       exists 0
       apply LTS.STrN.refl
     case tr _ _ hτ1 htr hτ2 =>
-      obtain ⟨n, hn⟩ := LTS.τSTr_imp_STrN lts hτ1
-      obtain ⟨m, hm⟩ := LTS.τSTr_imp_STrN lts hτ2
+      obtain ⟨n, hn⟩ := LTS.τSTr_imp_sTrN lts hτ1
+      obtain ⟨m, hm⟩ := LTS.τSTr_imp_sTrN lts hτ2
       exists (n + m + 1)
       apply LTS.STrN.tr hn htr hm
   case mpr =>
@@ -674,10 +674,10 @@ theorem LTS.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
-  obtain ⟨n, h1N⟩ := (LTS.STr_STrN lts).1 h1
-  obtain ⟨m, h2N⟩ := (LTS.STr_STrN lts).1 h2
+  obtain ⟨n, h1N⟩ := (LTS.sTr_eq_sTrN lts).1 h1
+  obtain ⟨m, h2N⟩ := (LTS.sTr_eq_sTrN lts).1 h2
   have concN := LTS.STrN.trans_τ lts h1N h2N
-  apply (LTS.STr_STrN lts).2 ⟨n + m, concN⟩
+  apply (LTS.sTr_eq_sTrN lts).2 ⟨n + m, concN⟩
 
 /-- Saturated transitions can be appended with τ-transitions (weighted version). -/
 @[scoped grind <=]

From ca153219dd5c6ee0906b728f0ecfaa6f068b659b Mon Sep 17 00:00:00 2001
From: "Cuijpers, Pieter" <p.j.l.cuijpers@tue.nl>
Date: Mon, 5 Jan 2026 15:04:32 +0100
Subject: [PATCH 09/21] Minor edits, changing back to old namings

---
 Cslib/Foundations/Semantics/LTS/Basic.lean | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/Cslib/Foundations/Semantics/LTS/Basic.lean b/Cslib/Foundations/Semantics/LTS/Basic.lean
index 17ce3e24..a3fe1bb5 100644
--- a/Cslib/Foundations/Semantics/LTS/Basic.lean
+++ b/Cslib/Foundations/Semantics/LTS/Basic.lean
@@ -628,13 +628,13 @@ theorem LTS.sTrN_imp_τSTr [HasTau Label] (lts : LTS State Label) :
     exact Relation.ReflTransGen.trans hτ1' (Relation.ReflTransGen.head htr hτ3')
 
 @[grind .]
-theorem LTS.τSTr_eq_sTrN [HasTau Label] (lts : LTS State Label) :
+theorem LTS.τSTr_sTrN [HasTau Label] (lts : LTS State Label) :
   lts.τSTr s1 s2 ↔ ∃ n, lts.STrN n s1 HasTau.τ s2 := by
   grind
 
-/-- `LTS.sTr` and `LTS.sTrN` are equivalent. -/
+/-- `LTS.str` and `LTS.strN` are equivalent. -/
 @[scoped grind =]
-theorem LTS.sTr_eq_sTrN [HasTau Label] (lts : LTS State Label) :
+theorem LTS.sTr_sTrN [HasTau Label] (lts : LTS State Label) :
   lts.STr s1 μ s2 ↔ ∃ n, lts.STrN n s1 μ s2 := by
   apply Iff.intro <;> intro h
   case mp =>
@@ -674,10 +674,10 @@ theorem LTS.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
-  obtain ⟨n, h1N⟩ := (LTS.sTr_eq_sTrN lts).1 h1
-  obtain ⟨m, h2N⟩ := (LTS.sTr_eq_sTrN lts).1 h2
+  obtain ⟨n, h1N⟩ := (LTS.sTr_sTrN lts).1 h1
+  obtain ⟨m, h2N⟩ := (LTS.sTr_sTrN lts).1 h2
   have concN := LTS.STrN.trans_τ lts h1N h2N
-  apply (LTS.sTr_eq_sTrN lts).2 ⟨n + m, concN⟩
+  apply (LTS.sTr_sTrN lts).2 ⟨n + m, concN⟩
 
 /-- Saturated transitions can be appended with τ-transitions (weighted version). -/
 @[scoped grind <=]

From dcceb8ffa529fa7c0453a7f5087c14a678040a5b Mon Sep 17 00:00:00 2001
From: "Cuijpers, Pieter" <p.j.l.cuijpers@tue.nl>
Date: Mon, 5 Jan 2026 15:08:23 +0100
Subject: [PATCH 10/21] Final reverts to original. Now PR only contains
 essential changes.

---
 Cslib/Foundations/Semantics/LTS/Basic.lean | 9 ++++-----
 1 file changed, 4 insertions(+), 5 deletions(-)

diff --git a/Cslib/Foundations/Semantics/LTS/Basic.lean b/Cslib/Foundations/Semantics/LTS/Basic.lean
index a3fe1bb5..52250938 100644
--- a/Cslib/Foundations/Semantics/LTS/Basic.lean
+++ b/Cslib/Foundations/Semantics/LTS/Basic.lean
@@ -682,10 +682,10 @@ theorem LTS.STr.trans_τ
 /-- Saturated transitions can be appended with τ-transitions (weighted version). -/
 @[scoped grind <=]
 theorem LTS.STrN.append
-    [HasTau Label] (lts : LTS State Label)
-    (h1 : lts.STrN n1 s1 μ s2)
-    (h2 : lts.STrN n2 s2 HasTau.τ s3) :
-    lts.STrN (n1 + n2) s1 μ s3 := by
+  [HasTau Label] (lts : LTS State Label)
+  (h1 : lts.STrN n1 s1 μ s2)
+  (h2 : lts.STrN n2 s2 HasTau.τ s3) :
+  lts.STrN (n1 + n2) s1 μ s3 := by
   induction h1
   case refl => grind
   case tr hstr1 htr hstr2 ih1 ih2  =>
@@ -739,7 +739,6 @@ class LTS.DivergenceFree [HasTau Label] (lts : LTS State Label) where
 
 end Divergence
 
-
 open Lean Elab Meta Command Term
 
 /-- A command to create an `LTS` from a labelled transition `α → β → α → Prop`, robust to use of

From eeb8bfc5e2536659f994d1a58a8eed31001cca88 Mon Sep 17 00:00:00 2001
From: "Cuijpers, Pieter" <p.j.l.cuijpers@tue.nl>
Date: Mon, 5 Jan 2026 15:34:47 +0100
Subject: [PATCH 11/21] Moving definition STrN up

---
 Cslib/Foundations/Semantics/LTS/Basic.lean | 76 ++++------------------
 1 file changed, 13 insertions(+), 63 deletions(-)

diff --git a/Cslib/Foundations/Semantics/LTS/Basic.lean b/Cslib/Foundations/Semantics/LTS/Basic.lean
index 52250938..2708d993 100644
--- a/Cslib/Foundations/Semantics/LTS/Basic.lean
+++ b/Cslib/Foundations/Semantics/LTS/Basic.lean
@@ -496,6 +496,18 @@ inductive LTS.STr [HasTau Label] (lts : LTS State Label) : State → Label → S
 | refl : lts.STr s HasTau.τ s
 | tr : lts.τSTr s1 s2 → lts.Tr s2 μ s3 → lts.τSTr s3 s4 → lts.STr s1 μ s4
 
+/-- As `LTS.str`, but counts the number of `τ`-transitions. This is convenient as induction
+metric. -/
+@[scoped grind]
+inductive LTS.STrN [HasTau Label] (lts : LTS State Label) :
+  ℕ → State → Label → State → Prop where
+  | refl : lts.STrN 0 s HasTau.τ s
+  | tr :
+    lts.STrN n s1 HasTau.τ s2 →
+    lts.Tr s2 μ s3 →
+    lts.STrN m s3 HasTau.τ s4 →
+    lts.STrN (n + m + 1) s1 μ s4
+
 /-- The `LTS` obtained by saturating the transition relation in `lts`. -/
 @[scoped grind =]
 def LTS.saturate [HasTau Label] (lts : LTS State Label) : LTS State Label where
@@ -512,6 +524,7 @@ theorem LTS.STr.single [HasTau Label] (lts : LTS State Label) :
   intro h
   apply LTS.STr.tr .refl h .refl
 
+
 /-- STr transitions labeled by HasTau.τ are exactly the τSTr transitions. -/
 @[grind _=_]
 theorem LTS.sTr_eq_τSTr [HasTau Label] (lts : LTS State Label) :
@@ -591,69 +604,6 @@ by performing only `τ`-transitions. -/
 def LTS.τClosure [HasTau Label] (lts : LTS State Label) (S : Set State) : Set State :=
   lts.saturate.setImage S HasTau.τ
 
-/-- As `LTS.str`, but counts the number of `τ`-transitions. This is convenient as induction
-metric. -/
-@[scoped grind]
-inductive LTS.STrN [HasTau Label] (lts : LTS State Label) :
-  ℕ → State → Label → State → Prop where
-  | refl : lts.STrN 0 s HasTau.τ s
-  | tr :
-    lts.STrN n s1 HasTau.τ s2 →
-    lts.Tr s2 μ s3 →
-    lts.STrN m s3 HasTau.τ s4 →
-    lts.STrN (n + m + 1) s1 μ s4
-
-@[grind .]
-theorem LTS.τSTr_imp_sTrN [HasTau Label] (lts : LTS State Label) :
-  lts.τSTr s1 s2 → ∃ n, lts.STrN n s1 HasTau.τ s2 := by
-  intro h
-  induction h
-  case refl =>
-    exists 0
-    apply LTS.STrN.refl
-  case tail _ _ _ htr ih =>
-    obtain ⟨n, hn⟩ := ih
-    exists (n + 1)
-    apply LTS.STrN.tr hn htr LTS.STrN.refl
-
-@[grind .]
-theorem LTS.sTrN_imp_τSTr [HasTau Label] (lts : LTS State Label) :
-  lts.STrN n s1 HasTau.τ s2 → lts.τSTr s1 s2 := by
-  intro h
-  cases h
-  case refl => exact Relation.ReflTransGen.refl
-  case tr m _ _ k hτ1 htr hτ2 =>
-    have hτ1' := LTS.sTrN_imp_τSTr lts hτ1
-    have hτ3' := LTS.sTrN_imp_τSTr lts hτ2
-    exact Relation.ReflTransGen.trans hτ1' (Relation.ReflTransGen.head htr hτ3')
-
-@[grind .]
-theorem LTS.τSTr_sTrN [HasTau Label] (lts : LTS State Label) :
-  lts.τSTr s1 s2 ↔ ∃ n, lts.STrN n s1 HasTau.τ s2 := by
-  grind
-
-/-- `LTS.str` and `LTS.strN` are equivalent. -/
-@[scoped grind =]
-theorem LTS.sTr_sTrN [HasTau Label] (lts : LTS State Label) :
-  lts.STr s1 μ s2 ↔ ∃ n, lts.STrN n s1 μ s2 := by
-  apply Iff.intro <;> intro h
-  case mp =>
-    induction h
-    case refl =>
-      exists 0
-      apply LTS.STrN.refl
-    case tr _ _ hτ1 htr hτ2 =>
-      obtain ⟨n, hn⟩ := LTS.τSTr_imp_sTrN lts hτ1
-      obtain ⟨m, hm⟩ := LTS.τSTr_imp_sTrN lts hτ2
-      exists (n + m + 1)
-      apply LTS.STrN.tr hn htr hm
-  case mpr =>
-    obtain ⟨n, hn⟩ := h
-    induction hn
-    case refl =>
-      exact LTS.STr.refl
-    case tr _ _ _ _ _ _ h2 _ h1 h3 =>
-      exact LTS.STr.comp lts h1 (LTS.STr.single lts h2) h3
 
 /-- Saturated transitions labelled by τ can be composed (weighted version). -/
 @[scoped grind →]

From b091047d59197cad4549f0f3565117a3e04e7d54 Mon Sep 17 00:00:00 2001
From: "Cuijpers, Pieter" <p.j.l.cuijpers@tue.nl>
Date: Mon, 5 Jan 2026 15:38:42 +0100
Subject: [PATCH 12/21] One more move

---
 Cslib/Foundations/Semantics/LTS/Basic.lean | 23 +++++++++++-----------
 1 file changed, 11 insertions(+), 12 deletions(-)

diff --git a/Cslib/Foundations/Semantics/LTS/Basic.lean b/Cslib/Foundations/Semantics/LTS/Basic.lean
index 2708d993..627e74c4 100644
--- a/Cslib/Foundations/Semantics/LTS/Basic.lean
+++ b/Cslib/Foundations/Semantics/LTS/Basic.lean
@@ -496,18 +496,6 @@ inductive LTS.STr [HasTau Label] (lts : LTS State Label) : State → Label → S
 | refl : lts.STr s HasTau.τ s
 | tr : lts.τSTr s1 s2 → lts.Tr s2 μ s3 → lts.τSTr s3 s4 → lts.STr s1 μ s4
 
-/-- As `LTS.str`, but counts the number of `τ`-transitions. This is convenient as induction
-metric. -/
-@[scoped grind]
-inductive LTS.STrN [HasTau Label] (lts : LTS State Label) :
-  ℕ → State → Label → State → Prop where
-  | refl : lts.STrN 0 s HasTau.τ s
-  | tr :
-    lts.STrN n s1 HasTau.τ s2 →
-    lts.Tr s2 μ s3 →
-    lts.STrN m s3 HasTau.τ s4 →
-    lts.STrN (n + m + 1) s1 μ s4
-
 /-- The `LTS` obtained by saturating the transition relation in `lts`. -/
 @[scoped grind =]
 def LTS.saturate [HasTau Label] (lts : LTS State Label) : LTS State Label where
@@ -524,6 +512,17 @@ theorem LTS.STr.single [HasTau Label] (lts : LTS State Label) :
   intro h
   apply LTS.STr.tr .refl h .refl
 
+/-- As `LTS.str`, but counts the number of `τ`-transitions. This is convenient as induction
+metric. -/
+@[scoped grind]
+inductive LTS.STrN [HasTau Label] (lts : LTS State Label) :
+  ℕ → State → Label → State → Prop where
+  | refl : lts.STrN 0 s HasTau.τ s
+  | tr :
+    lts.STrN n s1 HasTau.τ s2 →
+    lts.Tr s2 μ s3 →
+    lts.STrN m s3 HasTau.τ s4 →
+    lts.STrN (n + m + 1) s1 μ s4
 
 /-- STr transitions labeled by HasTau.τ are exactly the τSTr transitions. -/
 @[grind _=_]

From 87ce4910dd45d14c0dfde870388d688e1255aeb9 Mon Sep 17 00:00:00 2001
From: "Cuijpers, Pieter" <p.j.l.cuijpers@tue.nl>
Date: Mon, 5 Jan 2026 15:43:33 +0100
Subject: [PATCH 13/21] Move some more

---
 Cslib/Foundations/Semantics/LTS/Basic.lean | 51 ++++++++++++++++++++++
 1 file changed, 51 insertions(+)

diff --git a/Cslib/Foundations/Semantics/LTS/Basic.lean b/Cslib/Foundations/Semantics/LTS/Basic.lean
index 627e74c4..dabcdb3b 100644
--- a/Cslib/Foundations/Semantics/LTS/Basic.lean
+++ b/Cslib/Foundations/Semantics/LTS/Basic.lean
@@ -603,6 +603,57 @@ by performing only `τ`-transitions. -/
 def LTS.τClosure [HasTau Label] (lts : LTS State Label) (S : Set State) : Set State :=
   lts.saturate.setImage S HasTau.τ
 
+@[grind .]
+theorem LTS.τSTr_imp_sTrN [HasTau Label] (lts : LTS State Label) :
+  lts.τSTr s1 s2 → ∃ n, lts.STrN n s1 HasTau.τ s2 := by
+  intro h
+  induction h
+  case refl =>
+    exists 0
+    apply LTS.STrN.refl
+  case tail _ _ _ htr ih =>
+    obtain ⟨n, hn⟩ := ih
+    exists (n + 1)
+    apply LTS.STrN.tr hn htr LTS.STrN.refl
+
+@[grind .]
+theorem LTS.sTrN_imp_τSTr [HasTau Label] (lts : LTS State Label) :
+  lts.STrN n s1 HasTau.τ s2 → lts.τSTr s1 s2 := by
+  intro h
+  cases h
+  case refl => exact Relation.ReflTransGen.refl
+  case tr m _ _ k hτ1 htr hτ2 =>
+    have hτ1' := LTS.sTrN_imp_τSTr lts hτ1
+    have hτ3' := LTS.sTrN_imp_τSTr lts hτ2
+    exact Relation.ReflTransGen.trans hτ1' (Relation.ReflTransGen.head htr hτ3')
+
+@[grind .]
+theorem LTS.τSTr_sTrN [HasTau Label] (lts : LTS State Label) :
+  lts.τSTr s1 s2 ↔ ∃ n, lts.STrN n s1 HasTau.τ s2 := by
+  grind
+
+/-- `LTS.str` and `LTS.strN` are equivalent. -/
+@[scoped grind =]
+theorem LTS.sTr_sTrN [HasTau Label] (lts : LTS State Label) :
+  lts.STr s1 μ s2 ↔ ∃ n, lts.STrN n s1 μ s2 := by
+  apply Iff.intro <;> intro h
+  case mp =>
+    induction h
+    case refl =>
+      exists 0
+      apply LTS.STrN.refl
+    case tr _ _ hτ1 htr hτ2 =>
+      obtain ⟨n, hn⟩ := LTS.τSTr_imp_sTrN lts hτ1
+      obtain ⟨m, hm⟩ := LTS.τSTr_imp_sTrN lts hτ2
+      exists (n + m + 1)
+      apply LTS.STrN.tr hn htr hm
+  case mpr =>
+    obtain ⟨n, hn⟩ := h
+    induction hn
+    case refl =>
+      exact LTS.STr.refl
+    case tr _ _ _ _ _ _ h2 _ h1 h3 =>
+      exact LTS.STr.comp lts h1 (LTS.STr.single lts h2) h3
 
 /-- Saturated transitions labelled by τ can be composed (weighted version). -/
 @[scoped grind →]

From 03b9c262a5055bb9c70ff06344cad453198bc936 Mon Sep 17 00:00:00 2001
From: "Cuijpers, Pieter" <p.j.l.cuijpers@tue.nl>
Date: Mon, 5 Jan 2026 15:47:08 +0100
Subject: [PATCH 14/21] Some more moves

---
 Cslib/Foundations/Semantics/LTS/Basic.lean | 139 +++++++++++----------
 1 file changed, 71 insertions(+), 68 deletions(-)

diff --git a/Cslib/Foundations/Semantics/LTS/Basic.lean b/Cslib/Foundations/Semantics/LTS/Basic.lean
index dabcdb3b..9412e738 100644
--- a/Cslib/Foundations/Semantics/LTS/Basic.lean
+++ b/Cslib/Foundations/Semantics/LTS/Basic.lean
@@ -539,22 +539,6 @@ theorem LTS.sTr_eq_τSTr [HasTau Label] (lts : LTS State Label) :
     case refl => exact LTS.STr.refl
     case tail _ h1 h2 => exact LTS.STr.tr h1 h2 .refl
 
-/-- Saturated transitions can be composed. -/
-@[grind →]
-theorem LTS.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) :
-  lts.STr s1 μ s4 := by
-  rw [LTS.sTr_eq_τSTr _] at h1 h3
-  cases h2
-  case refl =>
-    rw [LTS.sTr_eq_τSTr _]
-    apply Relation.ReflTransGen.trans h1 h3
-  case tr _ _ hτ1 htr hτ2 =>
-    exact LTS.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. -/
 @[grind _=_]
 theorem LTS.saturate_τSTr_τSTr [hHasTau : HasTau Label] (lts : LTS State Label)
@@ -572,25 +556,6 @@ theorem LTS.saturate_τSTr_τSTr [hHasTau : HasTau Label] (lts : LTS State Label
       have h4 := LTS.STr.tr h2 h3 Relation.ReflTransGen.refl
       exact Relation.ReflTransGen.single h4
 
-/-- In a saturated LTS, the transition and saturated transition relations are the same. -/
-@[grind _=_]
-theorem LTS.saturate_tr_saturate_sTr [hHasTau : HasTau Label] (lts : LTS State Label)
-  (hμ : μ = hHasTau.τ) : lts.saturate.Tr s μ = lts.saturate.STr s μ := by
-  ext s'
-  apply Iff.intro <;> intro h
-  case mp =>
-    cases h
-    case refl => constructor
-    case tr hstr1 htr hstr2 =>
-      apply LTS.STr.single
-      exact LTS.STr.tr hstr1 htr hstr2
-  case mpr =>
-    cases h
-    case refl => constructor
-    case tr hstr1 htr hstr2 =>
-      rw [LTS.saturate_τSTr_τSTr lts] at hstr1 hstr2
-      rw [←LTS.sTr_eq_τSTr lts] at hstr1 hstr2
-      exact LTS.STr.comp lts hstr1 htr hstr2
 
 /-- In a saturated LTS, every state is in its τ-image. -/
 @[grind .]
@@ -632,28 +597,6 @@ theorem LTS.τSTr_sTrN [HasTau Label] (lts : LTS State Label) :
   lts.τSTr s1 s2 ↔ ∃ n, lts.STrN n s1 HasTau.τ s2 := by
   grind
 
-/-- `LTS.str` and `LTS.strN` are equivalent. -/
-@[scoped grind =]
-theorem LTS.sTr_sTrN [HasTau Label] (lts : LTS State Label) :
-  lts.STr s1 μ s2 ↔ ∃ n, lts.STrN n s1 μ s2 := by
-  apply Iff.intro <;> intro h
-  case mp =>
-    induction h
-    case refl =>
-      exists 0
-      apply LTS.STrN.refl
-    case tr _ _ hτ1 htr hτ2 =>
-      obtain ⟨n, hn⟩ := LTS.τSTr_imp_sTrN lts hτ1
-      obtain ⟨m, hm⟩ := LTS.τSTr_imp_sTrN lts hτ2
-      exists (n + m + 1)
-      apply LTS.STrN.tr hn htr hm
-  case mpr =>
-    obtain ⟨n, hn⟩ := h
-    induction hn
-    case refl =>
-      exact LTS.STr.refl
-    case tr _ _ _ _ _ _ h2 _ h1 h3 =>
-      exact LTS.STr.comp lts h1 (LTS.STr.single lts h2) h3
 
 /-- Saturated transitions labelled by τ can be composed (weighted version). -/
 @[scoped grind →]
@@ -668,17 +611,6 @@ theorem LTS.STrN.trans_τ
     have conc := LTS.STrN.tr hstr1 htr ih
     grind
 
-/-- Saturated transitions labelled by τ can be composed. -/
-@[scoped grind →]
-theorem LTS.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
-  obtain ⟨n, h1N⟩ := (LTS.sTr_sTrN lts).1 h1
-  obtain ⟨m, h2N⟩ := (LTS.sTr_sTrN lts).1 h2
-  have concN := LTS.STrN.trans_τ lts h1N h2N
-  apply (LTS.sTr_sTrN lts).2 ⟨n + m, concN⟩
-
 /-- Saturated transitions can be appended with τ-transitions (weighted version). -/
 @[scoped grind <=]
 theorem LTS.STrN.append
@@ -709,6 +641,77 @@ theorem LTS.STrN.comp
     have conc := LTS.STrN.append lts hprefix h3
     grind
 
+/-- Saturated transitions can be composed. -/
+@[grind →]
+theorem LTS.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) :
+  lts.STr s1 μ s4 := by
+  rw [LTS.sTr_eq_τSTr _] at h1 h3
+  cases h2
+  case refl =>
+    rw [LTS.sTr_eq_τSTr _]
+    apply Relation.ReflTransGen.trans h1 h3
+  case tr _ _ hτ1 htr hτ2 =>
+    exact LTS.STr.tr (Relation.ReflTransGen.trans h1 hτ1) htr (Relation.ReflTransGen.trans hτ2 h3)
+
+/-- `LTS.str` and `LTS.strN` are equivalent. -/
+@[scoped grind =]
+theorem LTS.sTr_sTrN [HasTau Label] (lts : LTS State Label) :
+  lts.STr s1 μ s2 ↔ ∃ n, lts.STrN n s1 μ s2 := by
+  apply Iff.intro <;> intro h
+  case mp =>
+    induction h
+    case refl =>
+      exists 0
+      apply LTS.STrN.refl
+    case tr _ _ hτ1 htr hτ2 =>
+      obtain ⟨n, hn⟩ := LTS.τSTr_imp_sTrN lts hτ1
+      obtain ⟨m, hm⟩ := LTS.τSTr_imp_sTrN lts hτ2
+      exists (n + m + 1)
+      apply LTS.STrN.tr hn htr hm
+  case mpr =>
+    obtain ⟨n, hn⟩ := h
+    induction hn
+    case refl =>
+      exact LTS.STr.refl
+    case tr _ _ _ _ _ _ h2 _ h1 h3 =>
+      exact LTS.STr.comp lts h1 (LTS.STr.single lts h2) h3
+
+/-- Saturated transitions labelled by τ can be composed. -/
+@[scoped grind →]
+theorem LTS.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
+  obtain ⟨n, h1N⟩ := (LTS.sTr_sTrN lts).1 h1
+  obtain ⟨m, h2N⟩ := (LTS.sTr_sTrN lts).1 h2
+  have concN := LTS.STrN.trans_τ lts h1N h2N
+  apply (LTS.sTr_sTrN lts).2 ⟨n + m, concN⟩
+
+/-- In a saturated LTS, the transition and saturated transition relations are the same. -/
+@[grind _=_]
+theorem LTS.saturate_tr_saturate_sTr [hHasTau : HasTau Label] (lts : LTS State Label)
+  (hμ : μ = hHasTau.τ) : lts.saturate.Tr s μ = lts.saturate.STr s μ := by
+  ext s'
+  apply Iff.intro <;> intro h
+  case mp =>
+    cases h
+    case refl => constructor
+    case tr hstr1 htr hstr2 =>
+      apply LTS.STr.single
+      exact LTS.STr.tr hstr1 htr hstr2
+  case mpr =>
+    cases h
+    case refl => constructor
+    case tr hstr1 htr hstr2 =>
+      rw [LTS.saturate_τSTr_τSTr lts] at hstr1 hstr2
+      rw [←LTS.sTr_eq_τSTr lts] at hstr1 hstr2
+      exact LTS.STr.comp lts hstr1 htr hstr2
+
+
 end Weak
 
 /-! ## Divergence -/

From b25960824fa057a3ec49dbac9b1b59d18b57376a Mon Sep 17 00:00:00 2001
From: "Cuijpers, Pieter" <p.j.l.cuijpers@tue.nl>
Date: Mon, 5 Jan 2026 15:53:20 +0100
Subject: [PATCH 15/21] Revert "Final reverts to original. Now PR only contains
 essential changes."

This reverts commit dcceb8ffa529fa7c0453a7f5087c14a678040a5b.
---
 Cslib/Foundations/Semantics/LTS/Basic.lean | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

diff --git a/Cslib/Foundations/Semantics/LTS/Basic.lean b/Cslib/Foundations/Semantics/LTS/Basic.lean
index 9412e738..4422160c 100644
--- a/Cslib/Foundations/Semantics/LTS/Basic.lean
+++ b/Cslib/Foundations/Semantics/LTS/Basic.lean
@@ -614,10 +614,10 @@ theorem LTS.STrN.trans_τ
 /-- Saturated transitions can be appended with τ-transitions (weighted version). -/
 @[scoped grind <=]
 theorem LTS.STrN.append
-  [HasTau Label] (lts : LTS State Label)
-  (h1 : lts.STrN n1 s1 μ s2)
-  (h2 : lts.STrN n2 s2 HasTau.τ s3) :
-  lts.STrN (n1 + n2) s1 μ s3 := by
+    [HasTau Label] (lts : LTS State Label)
+    (h1 : lts.STrN n1 s1 μ s2)
+    (h2 : lts.STrN n2 s2 HasTau.τ s3) :
+    lts.STrN (n1 + n2) s1 μ s3 := by
   induction h1
   case refl => grind
   case tr hstr1 htr hstr2 ih1 ih2  =>
@@ -742,6 +742,7 @@ class LTS.DivergenceFree [HasTau Label] (lts : LTS State Label) where
 
 end Divergence
 
+
 open Lean Elab Meta Command Term
 
 /-- A command to create an `LTS` from a labelled transition `α → β → α → Prop`, robust to use of

From b4ed3c80fa0a422d47eeb1de92b02f5b4eb4247e Mon Sep 17 00:00:00 2001
From: "Cuijpers, Pieter" <p.j.l.cuijpers@tue.nl>
Date: Mon, 5 Jan 2026 16:14:32 +0100
Subject: [PATCH 16/21] naming convention: _eq_ left out

---
 Cslib/Foundations/Semantics/LTS/Basic.lean | 24 +++++++++++-----------
 1 file changed, 12 insertions(+), 12 deletions(-)

diff --git a/Cslib/Foundations/Semantics/LTS/Basic.lean b/Cslib/Foundations/Semantics/LTS/Basic.lean
index 4422160c..7a979a7e 100644
--- a/Cslib/Foundations/Semantics/LTS/Basic.lean
+++ b/Cslib/Foundations/Semantics/LTS/Basic.lean
@@ -525,8 +525,8 @@ inductive LTS.STrN [HasTau Label] (lts : LTS State Label) :
     lts.STrN (n + m + 1) s1 μ s4
 
 /-- STr transitions labeled by HasTau.τ are exactly the τSTr transitions. -/
-@[grind _=_]
-theorem LTS.sTr_eq_τSTr [HasTau Label] (lts : LTS State Label) :
+@[scoped grind _=_]
+theorem LTS.sTr_τSTr [HasTau Label] (lts : LTS State Label) :
   lts.STr s HasTau.τ s' ↔ lts.τSTr s s' := by
   apply Iff.intro <;> intro h
   case mp =>
@@ -540,7 +540,7 @@ theorem LTS.sTr_eq_τSTr [HasTau Label] (lts : LTS State Label) :
     case tail _ h1 h2 => exact LTS.STr.tr h1 h2 .refl
 
 /-- In a saturated LTS, the transition and saturated transition relations are the same. -/
-@[grind _=_]
+@[scoped grind _=_]
 theorem LTS.saturate_τSTr_τSTr [hHasTau : HasTau Label] (lts : LTS State Label)
   : lts.saturate.τSTr s = lts.τSTr s := by
   ext s''
@@ -548,7 +548,7 @@ theorem LTS.saturate_τSTr_τSTr [hHasTau : HasTau Label] (lts : LTS State Label
   case mp =>
     induction h
     case refl => constructor
-    case tail _ _ _ h2 h3 => exact Relation.ReflTransGen.trans h3 ((LTS.sTr_eq_τSTr _).mp h2)
+    case tail _ _ _ h2 h3 => exact Relation.ReflTransGen.trans h3 ((LTS.sTr_τSTr _).mp h2)
   case mpr =>
     cases h
     case refl => constructor
@@ -558,17 +558,17 @@ theorem LTS.saturate_τSTr_τSTr [hHasTau : HasTau Label] (lts : LTS State Label
 
 
 /-- In a saturated LTS, every state is in its τ-image. -/
-@[grind .]
+@[scoped grind .]
 theorem LTS.mem_saturate_image_τ [HasTau Label] (lts : LTS State Label) :
   s ∈ lts.saturate.image s HasTau.τ := LTS.STr.refl
 
 /-- The `τ`-closure of a set of states `S` is the set of states reachable by any state in `S`
 by performing only `τ`-transitions. -/
-@[grind =]
+@[scoped grind =]
 def LTS.τClosure [HasTau Label] (lts : LTS State Label) (S : Set State) : Set State :=
   lts.saturate.setImage S HasTau.τ
 
-@[grind .]
+@[scoped grind .]
 theorem LTS.τSTr_imp_sTrN [HasTau Label] (lts : LTS State Label) :
   lts.τSTr s1 s2 → ∃ n, lts.STrN n s1 HasTau.τ s2 := by
   intro h
@@ -581,7 +581,7 @@ theorem LTS.τSTr_imp_sTrN [HasTau Label] (lts : LTS State Label) :
     exists (n + 1)
     apply LTS.STrN.tr hn htr LTS.STrN.refl
 
-@[grind .]
+@[scoped grind .]
 theorem LTS.sTrN_imp_τSTr [HasTau Label] (lts : LTS State Label) :
   lts.STrN n s1 HasTau.τ s2 → lts.τSTr s1 s2 := by
   intro h
@@ -592,7 +592,7 @@ theorem LTS.sTrN_imp_τSTr [HasTau Label] (lts : LTS State Label) :
     have hτ3' := LTS.sTrN_imp_τSTr lts hτ2
     exact Relation.ReflTransGen.trans hτ1' (Relation.ReflTransGen.head htr hτ3')
 
-@[grind .]
+@[scoped grind .]
 theorem LTS.τSTr_sTrN [HasTau Label] (lts : LTS State Label) :
   lts.τSTr s1 s2 ↔ ∃ n, lts.STrN n s1 HasTau.τ s2 := by
   grind
@@ -649,10 +649,10 @@ theorem LTS.STr.comp
   (h2 : lts.STr s2 μ s3)
   (h3 : lts.STr s3 HasTau.τ s4) :
   lts.STr s1 μ s4 := by
-  rw [LTS.sTr_eq_τSTr _] at h1 h3
+  rw [LTS.sTr_τSTr _] at h1 h3
   cases h2
   case refl =>
-    rw [LTS.sTr_eq_τSTr _]
+    rw [LTS.sTr_τSTr _]
     apply Relation.ReflTransGen.trans h1 h3
   case tr _ _ hτ1 htr hτ2 =>
     exact LTS.STr.tr (Relation.ReflTransGen.trans h1 hτ1) htr (Relation.ReflTransGen.trans hτ2 h3)
@@ -708,7 +708,7 @@ theorem LTS.saturate_tr_saturate_sTr [hHasTau : HasTau Label] (lts : LTS State L
     case refl => constructor
     case tr hstr1 htr hstr2 =>
       rw [LTS.saturate_τSTr_τSTr lts] at hstr1 hstr2
-      rw [←LTS.sTr_eq_τSTr lts] at hstr1 hstr2
+      rw [←LTS.sTr_τSTr lts] at hstr1 hstr2
       exact LTS.STr.comp lts hstr1 htr hstr2
 
 

From 48188337e0bb144304fea24d6e89a24ce91922c9 Mon Sep 17 00:00:00 2001
From: "Cuijpers, Pieter" <p.j.l.cuijpers@tue.nl>
Date: Mon, 5 Jan 2026 16:22:59 +0100
Subject: [PATCH 17/21] Guesses regarding grind

---
 Cslib/Foundations/Semantics/LTS/Basic.lean | 12 +++++-------
 1 file changed, 5 insertions(+), 7 deletions(-)

diff --git a/Cslib/Foundations/Semantics/LTS/Basic.lean b/Cslib/Foundations/Semantics/LTS/Basic.lean
index 7a979a7e..6bc7d73c 100644
--- a/Cslib/Foundations/Semantics/LTS/Basic.lean
+++ b/Cslib/Foundations/Semantics/LTS/Basic.lean
@@ -497,7 +497,7 @@ inductive LTS.STr [HasTau Label] (lts : LTS State Label) : State → Label → 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 =]
+@[scoped grind]
 def LTS.saturate [HasTau Label] (lts : LTS State Label) : LTS State Label where
   Tr := lts.STr
 
@@ -556,7 +556,6 @@ theorem LTS.saturate_τSTr_τSTr [hHasTau : HasTau Label] (lts : LTS State Label
       have h4 := LTS.STr.tr h2 h3 Relation.ReflTransGen.refl
       exact Relation.ReflTransGen.single h4
 
-
 /-- In a saturated LTS, every state is in its τ-image. -/
 @[scoped grind .]
 theorem LTS.mem_saturate_image_τ [HasTau Label] (lts : LTS State Label) :
@@ -564,7 +563,7 @@ theorem LTS.mem_saturate_image_τ [HasTau Label] (lts : LTS State Label) :
 
 /-- The `τ`-closure of a set of states `S` is the set of states reachable by any state in `S`
 by performing only `τ`-transitions. -/
-@[scoped grind =]
+@[scoped grind]
 def LTS.τClosure [HasTau Label] (lts : LTS State Label) (S : Set State) : Set State :=
   lts.saturate.setImage S HasTau.τ
 
@@ -599,7 +598,7 @@ theorem LTS.τSTr_sTrN [HasTau Label] (lts : LTS State Label) :
 
 
 /-- Saturated transitions labelled by τ can be composed (weighted version). -/
-@[scoped grind →]
+@[scoped grind <=]
 theorem LTS.STrN.trans_τ
   [HasTau Label] (lts : LTS State Label)
   (h1 : lts.STrN n s1 HasTau.τ s2) (h2 : lts.STrN m s2 HasTau.τ s3) :
@@ -642,7 +641,7 @@ theorem LTS.STrN.comp
     grind
 
 /-- Saturated transitions can be composed. -/
-@[grind →]
+@[scoped grind <=]
 theorem LTS.STr.comp
   [HasTau Label] (lts : LTS State Label)
   (h1 : lts.STr s1 HasTau.τ s2)
@@ -681,7 +680,7 @@ theorem LTS.sTr_sTrN [HasTau Label] (lts : LTS State Label) :
       exact LTS.STr.comp lts h1 (LTS.STr.single lts h2) h3
 
 /-- Saturated transitions labelled by τ can be composed. -/
-@[scoped grind →]
+@[scoped grind <=]
 theorem LTS.STr.trans_τ
   [HasTau Label] (lts : LTS State Label)
   (h1 : lts.STr s1 HasTau.τ s2) (h2 : lts.STr s2 HasTau.τ s3) :
@@ -711,7 +710,6 @@ theorem LTS.saturate_tr_saturate_sTr [hHasTau : HasTau Label] (lts : LTS State L
       rw [←LTS.sTr_τSTr lts] at hstr1 hstr2
       exact LTS.STr.comp lts hstr1 htr hstr2
 
-
 end Weak
 
 /-! ## Divergence -/

From 091bdc4a84ae3307ccee9c8c24c1eae36147dc55 Mon Sep 17 00:00:00 2001
From: "Cuijpers, Pieter" <p.j.l.cuijpers@tue.nl>
Date: Mon, 5 Jan 2026 16:33:48 +0100
Subject: [PATCH 18/21] Fixed Weak Bisimulation proofs (open LTS.STr due to
 scoped grind, and updated renamings)

---
 Cslib/Foundations/Semantics/LTS/Basic.lean    | 30 +++++++++----------
 .../Semantics/LTS/Bisimulation.lean           |  6 ++--
 2 files changed, 19 insertions(+), 17 deletions(-)

diff --git a/Cslib/Foundations/Semantics/LTS/Basic.lean b/Cslib/Foundations/Semantics/LTS/Basic.lean
index 6bc7d73c..40abb55e 100644
--- a/Cslib/Foundations/Semantics/LTS/Basic.lean
+++ b/Cslib/Foundations/Semantics/LTS/Basic.lean
@@ -501,12 +501,12 @@ inductive LTS.STr [HasTau Label] (lts : LTS State Label) : State → Label → S
 def LTS.saturate [HasTau Label] (lts : LTS State Label) : LTS State Label where
   Tr := lts.STr
 
-@[scoped grind _=_]
+@[scoped grind]
 theorem LTS.saturate_tr_sTr [HasTau Label] {lts : LTS State Label} :
   lts.saturate.Tr = lts.STr := by rfl
 
 /-- Any transition is also a saturated transition. -/
-@[scoped grind →]
+@[scoped grind]
 theorem LTS.STr.single [HasTau Label] (lts : LTS State Label) :
     lts.Tr s μ s' → lts.STr s μ s' := by
   intro h
@@ -525,7 +525,7 @@ inductive LTS.STrN [HasTau Label] (lts : LTS State Label) :
     lts.STrN (n + m + 1) s1 μ s4
 
 /-- STr transitions labeled by HasTau.τ are exactly the τSTr transitions. -/
-@[scoped grind _=_]
+@[scoped grind]
 theorem LTS.sTr_τSTr [HasTau Label] (lts : LTS State Label) :
   lts.STr s HasTau.τ s' ↔ lts.τSTr s s' := by
   apply Iff.intro <;> intro h
@@ -540,7 +540,7 @@ theorem LTS.sTr_τSTr [HasTau Label] (lts : LTS State Label) :
     case tail _ h1 h2 => exact LTS.STr.tr h1 h2 .refl
 
 /-- In a saturated LTS, the transition and saturated transition relations are the same. -/
-@[scoped grind _=_]
+@[scoped grind]
 theorem LTS.saturate_τSTr_τSTr [hHasTau : HasTau Label] (lts : LTS State Label)
   : lts.saturate.τSTr s = lts.τSTr s := by
   ext s''
@@ -557,7 +557,7 @@ theorem LTS.saturate_τSTr_τSTr [hHasTau : HasTau Label] (lts : LTS State Label
       exact Relation.ReflTransGen.single h4
 
 /-- In a saturated LTS, every state is in its τ-image. -/
-@[scoped grind .]
+@[scoped grind]
 theorem LTS.mem_saturate_image_τ [HasTau Label] (lts : LTS State Label) :
   s ∈ lts.saturate.image s HasTau.τ := LTS.STr.refl
 
@@ -567,7 +567,7 @@ by performing only `τ`-transitions. -/
 def LTS.τClosure [HasTau Label] (lts : LTS State Label) (S : Set State) : Set State :=
   lts.saturate.setImage S HasTau.τ
 
-@[scoped grind .]
+@[scoped grind]
 theorem LTS.τSTr_imp_sTrN [HasTau Label] (lts : LTS State Label) :
   lts.τSTr s1 s2 → ∃ n, lts.STrN n s1 HasTau.τ s2 := by
   intro h
@@ -580,7 +580,7 @@ theorem LTS.τSTr_imp_sTrN [HasTau Label] (lts : LTS State Label) :
     exists (n + 1)
     apply LTS.STrN.tr hn htr LTS.STrN.refl
 
-@[scoped grind .]
+@[scoped grind]
 theorem LTS.sTrN_imp_τSTr [HasTau Label] (lts : LTS State Label) :
   lts.STrN n s1 HasTau.τ s2 → lts.τSTr s1 s2 := by
   intro h
@@ -591,14 +591,14 @@ theorem LTS.sTrN_imp_τSTr [HasTau Label] (lts : LTS State Label) :
     have hτ3' := LTS.sTrN_imp_τSTr lts hτ2
     exact Relation.ReflTransGen.trans hτ1' (Relation.ReflTransGen.head htr hτ3')
 
-@[scoped grind .]
+@[scoped grind]
 theorem LTS.τSTr_sTrN [HasTau Label] (lts : LTS State Label) :
   lts.τSTr s1 s2 ↔ ∃ n, lts.STrN n s1 HasTau.τ s2 := by
   grind
 
 
 /-- Saturated transitions labelled by τ can be composed (weighted version). -/
-@[scoped grind <=]
+@[scoped grind]
 theorem LTS.STrN.trans_τ
   [HasTau Label] (lts : LTS State Label)
   (h1 : lts.STrN n s1 HasTau.τ s2) (h2 : lts.STrN m s2 HasTau.τ s3) :
@@ -611,7 +611,7 @@ theorem LTS.STrN.trans_τ
     grind
 
 /-- Saturated transitions can be appended with τ-transitions (weighted version). -/
-@[scoped grind <=]
+@[scoped grind]
 theorem LTS.STrN.append
     [HasTau Label] (lts : LTS State Label)
     (h1 : lts.STrN n1 s1 μ s2)
@@ -624,7 +624,7 @@ theorem LTS.STrN.append
     grind
 
 /-- Saturated transitions can be composed (weighted version). -/
-@[scoped grind <=]
+@[scoped grind]
 theorem LTS.STrN.comp
   [HasTau Label] (lts : LTS State Label)
   (h1 : lts.STrN n1 s1 HasTau.τ s2)
@@ -641,7 +641,7 @@ theorem LTS.STrN.comp
     grind
 
 /-- Saturated transitions can be composed. -/
-@[scoped grind <=]
+@[scoped grind]
 theorem LTS.STr.comp
   [HasTau Label] (lts : LTS State Label)
   (h1 : lts.STr s1 HasTau.τ s2)
@@ -657,7 +657,7 @@ theorem LTS.STr.comp
     exact LTS.STr.tr (Relation.ReflTransGen.trans h1 hτ1) htr (Relation.ReflTransGen.trans hτ2 h3)
 
 /-- `LTS.str` and `LTS.strN` are equivalent. -/
-@[scoped grind =]
+@[scoped grind]
 theorem LTS.sTr_sTrN [HasTau Label] (lts : LTS State Label) :
   lts.STr s1 μ s2 ↔ ∃ n, lts.STrN n s1 μ s2 := by
   apply Iff.intro <;> intro h
@@ -680,7 +680,7 @@ theorem LTS.sTr_sTrN [HasTau Label] (lts : LTS State Label) :
       exact LTS.STr.comp lts h1 (LTS.STr.single lts h2) h3
 
 /-- Saturated transitions labelled by τ can be composed. -/
-@[scoped grind <=]
+@[scoped grind]
 theorem LTS.STr.trans_τ
   [HasTau Label] (lts : LTS State Label)
   (h1 : lts.STr s1 HasTau.τ s2) (h2 : lts.STr s2 HasTau.τ s3) :
@@ -691,7 +691,7 @@ theorem LTS.STr.trans_τ
   apply (LTS.sTr_sTrN lts).2 ⟨n + m, concN⟩
 
 /-- In a saturated LTS, the transition and saturated transition relations are the same. -/
-@[grind _=_]
+@[grind]
 theorem LTS.saturate_tr_saturate_sTr [hHasTau : HasTau Label] (lts : LTS State Label)
   (hμ : μ = hHasTau.τ) : lts.saturate.Tr s μ = lts.saturate.STr s μ := by
   ext s'
diff --git a/Cslib/Foundations/Semantics/LTS/Bisimulation.lean b/Cslib/Foundations/Semantics/LTS/Bisimulation.lean
index 19d95043..28f0b87a 100644
--- a/Cslib/Foundations/Semantics/LTS/Bisimulation.lean
+++ b/Cslib/Foundations/Semantics/LTS/Bisimulation.lean
@@ -756,6 +756,8 @@ end Bisimulation
 
 section WeakBisimulation
 
+open LTS.STr
+
 /-! ## Weak bisimulation and weak bisimilarity -/
 
 /-- A weak bisimulation is similar to a `Bisimulation`, but allows for the related processes to do
@@ -890,7 +892,7 @@ theorem LTS.isWeakBisimulation_iff_isSWBisimulation
         constructor; constructor
         exact hr
       case tr sb sb' hstr1 htr hstr2 =>
-        rw [←LTS.STr_τTr] at hstr1 hstr2
+        rw [←LTS.sTr_τSTr] at hstr1 hstr2
         obtain ⟨sb2, hstr2b, hrb⟩ := SWBisimulation.follow_internal_fst h hr hstr1
         obtain ⟨sb2', hstr2b', hrb'⟩ := (h hrb μ).1 _ htr
         obtain ⟨s2', hstr2', hrb2⟩ := SWBisimulation.follow_internal_fst h hrb' hstr2
@@ -906,7 +908,7 @@ theorem LTS.isWeakBisimulation_iff_isSWBisimulation
         constructor; constructor
         exact hr
       case tr sb sb' hstr1 htr hstr2 =>
-        rw [←LTS.STr_τTr] at hstr1 hstr2
+        rw [←LTS.sTr_τSTr] at hstr1 hstr2
         obtain ⟨sb1, hstr1b, hrb⟩ := SWBisimulation.follow_internal_snd h hr hstr1
         obtain ⟨sb2', hstr1b', hrb'⟩ := (h hrb μ).2 _ htr
         obtain ⟨s1', hstr1', hrb2⟩ := SWBisimulation.follow_internal_snd h hrb' hstr2

From e0a5a54afa5012311952fc9c9584980af6395901 Mon Sep 17 00:00:00 2001
From: "Cuijpers, Pieter" <p.j.l.cuijpers@tue.nl>
Date: Mon, 5 Jan 2026 16:40:29 +0100
Subject: [PATCH 19/21] Better understanding of @[grind] options, I hope.

---
 Cslib/Foundations/Semantics/LTS/Basic.lean | 31 +++++++++++-----------
 1 file changed, 15 insertions(+), 16 deletions(-)

diff --git a/Cslib/Foundations/Semantics/LTS/Basic.lean b/Cslib/Foundations/Semantics/LTS/Basic.lean
index 40abb55e..1c2fb255 100644
--- a/Cslib/Foundations/Semantics/LTS/Basic.lean
+++ b/Cslib/Foundations/Semantics/LTS/Basic.lean
@@ -501,12 +501,12 @@ inductive LTS.STr [HasTau Label] (lts : LTS State Label) : State → Label → S
 def LTS.saturate [HasTau Label] (lts : LTS State Label) : LTS State Label where
   Tr := lts.STr
 
-@[scoped grind]
+@[scoped grind _=_]
 theorem LTS.saturate_tr_sTr [HasTau Label] {lts : LTS State Label} :
   lts.saturate.Tr = lts.STr := by rfl
 
 /-- Any transition is also a saturated transition. -/
-@[scoped grind]
+@[scoped grind .]
 theorem LTS.STr.single [HasTau Label] (lts : LTS State Label) :
     lts.Tr s μ s' → lts.STr s μ s' := by
   intro h
@@ -525,7 +525,7 @@ inductive LTS.STrN [HasTau Label] (lts : LTS State Label) :
     lts.STrN (n + m + 1) s1 μ s4
 
 /-- STr transitions labeled by HasTau.τ are exactly the τSTr transitions. -/
-@[scoped grind]
+@[scoped grind _=_]
 theorem LTS.sTr_τSTr [HasTau Label] (lts : LTS State Label) :
   lts.STr s HasTau.τ s' ↔ lts.τSTr s s' := by
   apply Iff.intro <;> intro h
@@ -540,7 +540,7 @@ theorem LTS.sTr_τSTr [HasTau Label] (lts : LTS State Label) :
     case tail _ h1 h2 => exact LTS.STr.tr h1 h2 .refl
 
 /-- In a saturated LTS, the transition and saturated transition relations are the same. -/
-@[scoped grind]
+@[scoped grind _=_]
 theorem LTS.saturate_τSTr_τSTr [hHasTau : HasTau Label] (lts : LTS State Label)
   : lts.saturate.τSTr s = lts.τSTr s := by
   ext s''
@@ -557,7 +557,7 @@ theorem LTS.saturate_τSTr_τSTr [hHasTau : HasTau Label] (lts : LTS State Label
       exact Relation.ReflTransGen.single h4
 
 /-- In a saturated LTS, every state is in its τ-image. -/
-@[scoped grind]
+@[scoped grind .]
 theorem LTS.mem_saturate_image_τ [HasTau Label] (lts : LTS State Label) :
   s ∈ lts.saturate.image s HasTau.τ := LTS.STr.refl
 
@@ -567,7 +567,7 @@ by performing only `τ`-transitions. -/
 def LTS.τClosure [HasTau Label] (lts : LTS State Label) (S : Set State) : Set State :=
   lts.saturate.setImage S HasTau.τ
 
-@[scoped grind]
+@[scoped grind .]
 theorem LTS.τSTr_imp_sTrN [HasTau Label] (lts : LTS State Label) :
   lts.τSTr s1 s2 → ∃ n, lts.STrN n s1 HasTau.τ s2 := by
   intro h
@@ -580,7 +580,7 @@ theorem LTS.τSTr_imp_sTrN [HasTau Label] (lts : LTS State Label) :
     exists (n + 1)
     apply LTS.STrN.tr hn htr LTS.STrN.refl
 
-@[scoped grind]
+@[scoped grind →]
 theorem LTS.sTrN_imp_τSTr [HasTau Label] (lts : LTS State Label) :
   lts.STrN n s1 HasTau.τ s2 → lts.τSTr s1 s2 := by
   intro h
@@ -591,14 +591,13 @@ theorem LTS.sTrN_imp_τSTr [HasTau Label] (lts : LTS State Label) :
     have hτ3' := LTS.sTrN_imp_τSTr lts hτ2
     exact Relation.ReflTransGen.trans hτ1' (Relation.ReflTransGen.head htr hτ3')
 
-@[scoped grind]
+@[scoped grind =]
 theorem LTS.τSTr_sTrN [HasTau Label] (lts : LTS State Label) :
   lts.τSTr s1 s2 ↔ ∃ n, lts.STrN n s1 HasTau.τ s2 := by
   grind
 
-
 /-- Saturated transitions labelled by τ can be composed (weighted version). -/
-@[scoped grind]
+@[scoped grind .]
 theorem LTS.STrN.trans_τ
   [HasTau Label] (lts : LTS State Label)
   (h1 : lts.STrN n s1 HasTau.τ s2) (h2 : lts.STrN m s2 HasTau.τ s3) :
@@ -611,7 +610,7 @@ theorem LTS.STrN.trans_τ
     grind
 
 /-- Saturated transitions can be appended with τ-transitions (weighted version). -/
-@[scoped grind]
+@[scoped grind .]
 theorem LTS.STrN.append
     [HasTau Label] (lts : LTS State Label)
     (h1 : lts.STrN n1 s1 μ s2)
@@ -624,7 +623,7 @@ theorem LTS.STrN.append
     grind
 
 /-- Saturated transitions can be composed (weighted version). -/
-@[scoped grind]
+@[scoped grind <=]
 theorem LTS.STrN.comp
   [HasTau Label] (lts : LTS State Label)
   (h1 : lts.STrN n1 s1 HasTau.τ s2)
@@ -641,7 +640,7 @@ theorem LTS.STrN.comp
     grind
 
 /-- Saturated transitions can be composed. -/
-@[scoped grind]
+@[scoped grind <=]
 theorem LTS.STr.comp
   [HasTau Label] (lts : LTS State Label)
   (h1 : lts.STr s1 HasTau.τ s2)
@@ -657,7 +656,7 @@ theorem LTS.STr.comp
     exact LTS.STr.tr (Relation.ReflTransGen.trans h1 hτ1) htr (Relation.ReflTransGen.trans hτ2 h3)
 
 /-- `LTS.str` and `LTS.strN` are equivalent. -/
-@[scoped grind]
+@[scoped grind =]
 theorem LTS.sTr_sTrN [HasTau Label] (lts : LTS State Label) :
   lts.STr s1 μ s2 ↔ ∃ n, lts.STrN n s1 μ s2 := by
   apply Iff.intro <;> intro h
@@ -680,7 +679,7 @@ theorem LTS.sTr_sTrN [HasTau Label] (lts : LTS State Label) :
       exact LTS.STr.comp lts h1 (LTS.STr.single lts h2) h3
 
 /-- Saturated transitions labelled by τ can be composed. -/
-@[scoped grind]
+@[scoped grind <=]
 theorem LTS.STr.trans_τ
   [HasTau Label] (lts : LTS State Label)
   (h1 : lts.STr s1 HasTau.τ s2) (h2 : lts.STr s2 HasTau.τ s3) :
@@ -691,7 +690,7 @@ theorem LTS.STr.trans_τ
   apply (LTS.sTr_sTrN lts).2 ⟨n + m, concN⟩
 
 /-- In a saturated LTS, the transition and saturated transition relations are the same. -/
-@[grind]
+@[scoped grind _=_]
 theorem LTS.saturate_tr_saturate_sTr [hHasTau : HasTau Label] (lts : LTS State Label)
   (hμ : μ = hHasTau.τ) : lts.saturate.Tr s μ = lts.saturate.STr s μ := by
   ext s'

From 12de94f7fb6b3a0247d91da85a06cd493fd70fd7 Mon Sep 17 00:00:00 2001
From: "Cuijpers, Pieter" <p.j.l.cuijpers@tue.nl>
Date: Mon, 5 Jan 2026 17:13:26 +0100
Subject: [PATCH 20/21] CI complained about gind in LTS.STrN.trans_\tau, not
 sure why. Trying a different modifier.

---
 Cslib/Foundations/Semantics/LTS/Basic.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Cslib/Foundations/Semantics/LTS/Basic.lean b/Cslib/Foundations/Semantics/LTS/Basic.lean
index 1c2fb255..6eef21e1 100644
--- a/Cslib/Foundations/Semantics/LTS/Basic.lean
+++ b/Cslib/Foundations/Semantics/LTS/Basic.lean
@@ -597,7 +597,7 @@ theorem LTS.τSTr_sTrN [HasTau Label] (lts : LTS State Label) :
   grind
 
 /-- Saturated transitions labelled by τ can be composed (weighted version). -/
-@[scoped grind .]
+@[scoped grind →]
 theorem LTS.STrN.trans_τ
   [HasTau Label] (lts : LTS State Label)
   (h1 : lts.STrN n s1 HasTau.τ s2) (h2 : lts.STrN m s2 HasTau.τ s3) :
@@ -679,7 +679,7 @@ theorem LTS.sTr_sTrN [HasTau Label] (lts : LTS State Label) :
       exact LTS.STr.comp lts h1 (LTS.STr.single lts h2) h3
 
 /-- Saturated transitions labelled by τ can be composed. -/
-@[scoped grind <=]
+@[scoped grind →]
 theorem LTS.STr.trans_τ
   [HasTau Label] (lts : LTS State Label)
   (h1 : lts.STr s1 HasTau.τ s2) (h2 : lts.STr s2 HasTau.τ s3) :

From 462e8d4318d04075dde65f8069f516c491c2a8b0 Mon Sep 17 00:00:00 2001
From: "Cuijpers, Pieter" <p.j.l.cuijpers@tue.nl>
Date: Thu, 8 Jan 2026 11:09:03 +0100
Subject: [PATCH 21/21] Removed STrN as it is no longer needed

---
 Cslib/Foundations/Semantics/LTS/Basic.lean | 114 +--------------------
 1 file changed, 3 insertions(+), 111 deletions(-)

diff --git a/Cslib/Foundations/Semantics/LTS/Basic.lean b/Cslib/Foundations/Semantics/LTS/Basic.lean
index 6eef21e1..d23fafcb 100644
--- a/Cslib/Foundations/Semantics/LTS/Basic.lean
+++ b/Cslib/Foundations/Semantics/LTS/Basic.lean
@@ -512,18 +512,6 @@ theorem LTS.STr.single [HasTau Label] (lts : LTS State Label) :
   intro h
   apply LTS.STr.tr .refl h .refl
 
-/-- As `LTS.str`, but counts the number of `τ`-transitions. This is convenient as induction
-metric. -/
-@[scoped grind]
-inductive LTS.STrN [HasTau Label] (lts : LTS State Label) :
-  ℕ → State → Label → State → Prop where
-  | refl : lts.STrN 0 s HasTau.τ s
-  | tr :
-    lts.STrN n s1 HasTau.τ s2 →
-    lts.Tr s2 μ s3 →
-    lts.STrN m s3 HasTau.τ s4 →
-    lts.STrN (n + m + 1) s1 μ s4
-
 /-- STr transitions labeled by HasTau.τ are exactly the τSTr transitions. -/
 @[scoped grind _=_]
 theorem LTS.sTr_τSTr [HasTau Label] (lts : LTS State Label) :
@@ -567,78 +555,6 @@ by performing only `τ`-transitions. -/
 def LTS.τClosure [HasTau Label] (lts : LTS State Label) (S : Set State) : Set State :=
   lts.saturate.setImage S HasTau.τ
 
-@[scoped grind .]
-theorem LTS.τSTr_imp_sTrN [HasTau Label] (lts : LTS State Label) :
-  lts.τSTr s1 s2 → ∃ n, lts.STrN n s1 HasTau.τ s2 := by
-  intro h
-  induction h
-  case refl =>
-    exists 0
-    apply LTS.STrN.refl
-  case tail _ _ _ htr ih =>
-    obtain ⟨n, hn⟩ := ih
-    exists (n + 1)
-    apply LTS.STrN.tr hn htr LTS.STrN.refl
-
-@[scoped grind →]
-theorem LTS.sTrN_imp_τSTr [HasTau Label] (lts : LTS State Label) :
-  lts.STrN n s1 HasTau.τ s2 → lts.τSTr s1 s2 := by
-  intro h
-  cases h
-  case refl => exact Relation.ReflTransGen.refl
-  case tr m _ _ k hτ1 htr hτ2 =>
-    have hτ1' := LTS.sTrN_imp_τSTr lts hτ1
-    have hτ3' := LTS.sTrN_imp_τSTr lts hτ2
-    exact Relation.ReflTransGen.trans hτ1' (Relation.ReflTransGen.head htr hτ3')
-
-@[scoped grind =]
-theorem LTS.τSTr_sTrN [HasTau Label] (lts : LTS State Label) :
-  lts.τSTr s1 s2 ↔ ∃ n, lts.STrN n s1 HasTau.τ s2 := by
-  grind
-
-/-- Saturated transitions labelled by τ can be composed (weighted version). -/
-@[scoped grind →]
-theorem LTS.STrN.trans_τ
-  [HasTau Label] (lts : LTS State Label)
-  (h1 : lts.STrN n s1 HasTau.τ s2) (h2 : lts.STrN m s2 HasTau.τ s3) :
-  lts.STrN (n + m) s1 HasTau.τ s3 := by
-  cases h1
-  case refl => grind
-  case tr n1 sb sb' n2 hstr1 htr hstr2 =>
-    have ih := LTS.STrN.trans_τ lts hstr2 h2
-    have conc := LTS.STrN.tr hstr1 htr ih
-    grind
-
-/-- Saturated transitions can be appended with τ-transitions (weighted version). -/
-@[scoped grind .]
-theorem LTS.STrN.append
-    [HasTau Label] (lts : LTS State Label)
-    (h1 : lts.STrN n1 s1 μ s2)
-    (h2 : lts.STrN n2 s2 HasTau.τ s3) :
-    lts.STrN (n1 + n2) s1 μ s3 := by
-  induction h1
-  case refl => grind
-  case tr hstr1 htr hstr2 ih1 ih2  =>
-    have conc := LTS.STrN.tr hstr1 htr (ih2 h2)
-    grind
-
-/-- Saturated transitions can be composed (weighted version). -/
-@[scoped grind <=]
-theorem LTS.STrN.comp
-  [HasTau Label] (lts : LTS State Label)
-  (h1 : lts.STrN n1 s1 HasTau.τ s2)
-  (h2 : lts.STrN n2 s2 μ s3)
-  (h3 : lts.STrN n3 s3 HasTau.τ s4) :
-  lts.STrN (n1 + n2 + n3) s1 μ s4 := by
-  cases h2
-  case refl =>
-    apply LTS.STrN.trans_τ lts h1 h3
-  case tr n21 sb sb' n22 hstr1 htr hstr2 =>
-    have hprefix_τ := LTS.STrN.trans_τ lts h1 hstr1
-    have hprefix := LTS.STrN.tr hprefix_τ htr hstr2
-    have conc := LTS.STrN.append lts hprefix h3
-    grind
-
 /-- Saturated transitions can be composed. -/
 @[scoped grind <=]
 theorem LTS.STr.comp
@@ -655,39 +571,15 @@ theorem LTS.STr.comp
   case tr _ _ hτ1 htr hτ2 =>
     exact LTS.STr.tr (Relation.ReflTransGen.trans h1 hτ1) htr (Relation.ReflTransGen.trans hτ2 h3)
 
-/-- `LTS.str` and `LTS.strN` are equivalent. -/
-@[scoped grind =]
-theorem LTS.sTr_sTrN [HasTau Label] (lts : LTS State Label) :
-  lts.STr s1 μ s2 ↔ ∃ n, lts.STrN n s1 μ s2 := by
-  apply Iff.intro <;> intro h
-  case mp =>
-    induction h
-    case refl =>
-      exists 0
-      apply LTS.STrN.refl
-    case tr _ _ hτ1 htr hτ2 =>
-      obtain ⟨n, hn⟩ := LTS.τSTr_imp_sTrN lts hτ1
-      obtain ⟨m, hm⟩ := LTS.τSTr_imp_sTrN lts hτ2
-      exists (n + m + 1)
-      apply LTS.STrN.tr hn htr hm
-  case mpr =>
-    obtain ⟨n, hn⟩ := h
-    induction hn
-    case refl =>
-      exact LTS.STr.refl
-    case tr _ _ _ _ _ _ h2 _ h1 h3 =>
-      exact LTS.STr.comp lts h1 (LTS.STr.single lts h2) h3
-
 /-- Saturated transitions labelled by τ can be composed. -/
 @[scoped grind →]
 theorem LTS.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
-  obtain ⟨n, h1N⟩ := (LTS.sTr_sTrN lts).1 h1
-  obtain ⟨m, h2N⟩ := (LTS.sTr_sTrN lts).1 h2
-  have concN := LTS.STrN.trans_τ lts h1N h2N
-  apply (LTS.sTr_sTrN lts).2 ⟨n + m, concN⟩
+  rw [LTS.sTr_τSTr _] at h1 h2
+  rw [LTS.sTr_τSTr _]
+  apply Relation.ReflTransGen.trans h1 h2
 
 /-- In a saturated LTS, the transition and saturated transition relations are the same. -/
 @[scoped grind _=_]