diff --git a/Cslib.lean b/Cslib.lean
index c50fa2ec..f696325f 100644
--- a/Cslib.lean
+++ b/Cslib.lean
@@ -1,6 +1,6 @@
-import Cslib.Foundations.Semantics.Lts.Basic
-import Cslib.Foundations.Semantics.Lts.Bisimulation
-import Cslib.Foundations.Semantics.Lts.TraceEq
+import Cslib.Foundations.Semantics.LTS.Basic
+import Cslib.Foundations.Semantics.LTS.Bisimulation
+import Cslib.Foundations.Semantics.LTS.TraceEq
 import Cslib.Foundations.Data.Relation
 import Cslib.Languages.CombinatoryLogic.Defs
 import Cslib.Languages.CombinatoryLogic.Basic
diff --git a/Cslib/Computability/Automata/DA.lean b/Cslib/Computability/Automata/DA.lean
new file mode 100644
index 00000000..a9f5a85f
--- /dev/null
+++ b/Cslib/Computability/Automata/DA.lean
@@ -0,0 +1,17 @@
+/-
+Copyright (c) 2025 Fabrizio Montesi. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Fabrizio Montesi
+-/
+
+import Cslib.Computability.Automata.NA
+
+/-! # Deterministic Automaton
+
+A Deterministic Automaton (DA) is an automaton defined by a transition function.
+-/
+structure DA (State : Type _) (Symbol : Type _) where
+  /-- The initial state of the automaton. -/
+  start : State
+  /-- The transition function of the automaton. -/
+  tr : State → Symbol → State
diff --git a/Cslib/Computability/Automata/DFA.lean b/Cslib/Computability/Automata/DFA.lean
new file mode 100644
index 00000000..c6a42f33
--- /dev/null
+++ b/Cslib/Computability/Automata/DFA.lean
@@ -0,0 +1,61 @@
+/-
+Copyright (c) 2025 Fabrizio Montesi. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Fabrizio Montesi
+-/
+
+import Cslib.Computability.Automata.DA
+
+set_option linter.style.longLine false in
+/-! # Deterministic Finite-State Automata
+
+A Deterministic Finite Automaton (DFA) is a finite-state machine that accepts or rejects
+a finite string.
+
+## References
+
+* [J. E. Hopcroft, R. Motwani, J. D. Ullman, *Introduction to Automata Theory, Languages, and Computation*][Hopcroft2006]
+-/
+
+/-- A Deterministic Finite Automaton (DFA) consists of a labelled transition function
+`tr` over finite sets of states and labels (called symbols), a starting state `start` and a finite
+set of accepting states `accept`. -/
+structure DFA (State : Type _) (Symbol : Type _) extends DA State Symbol where
+  /-- The set of accepting states of the automaton. -/
+  accept : Set State
+  /-- The automaton is finite-state. -/
+  finite_state : Finite State
+  /-- The type of symbols (also called 'alphabet') is finite. -/
+  finite_symbol : Finite Symbol
+
+
+namespace DFA
+
+/-- Extended transition function.
+
+Implementation note: compared to [Hopcroft2006], the definition consumes the input list of symbols
+from the left (instead of the right), in order to match the way lists are constructed.
+-/
+@[scoped grind =]
+def mtr (dfa : DFA State Symbol) (s : State) (xs : List Symbol) := xs.foldl dfa.tr s
+
+@[scoped grind =]
+theorem mtr_nil_eq {dfa : DFA State Symbol} : dfa.mtr s [] = s := by rfl
+
+/-- A DFA accepts a string if there is a multi-step accepting derivative with that trace from
+the start state. -/
+@[scoped grind →]
+def Accepts (dfa : DFA State Symbol) (xs : List Symbol) :=
+  dfa.mtr dfa.start xs ∈ dfa.accept
+
+/-- The language of a DFA is the set of strings that it accepts. -/
+@[scoped grind =]
+def language (dfa : DFA State Symbol) : Set (List Symbol) :=
+  { xs | dfa.Accepts xs }
+
+/-- A string is accepted by a DFA iff it is in the language of the DFA. -/
+@[scoped grind _=_]
+theorem accepts_mem_language (dfa : DFA State Symbol) (xs : List Symbol) :
+  dfa.Accepts xs ↔ xs ∈ dfa.language := by rfl
+
+end DFA
diff --git a/Cslib/Computability/Automata/DFAToNFA.lean b/Cslib/Computability/Automata/DFAToNFA.lean
new file mode 100644
index 00000000..ee85b12b
--- /dev/null
+++ b/Cslib/Computability/Automata/DFAToNFA.lean
@@ -0,0 +1,63 @@
+/-
+Copyright (c) 2025 Fabrizio Montesi. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Fabrizio Montesi
+-/
+
+import Cslib.Computability.Automata.DFA
+import Cslib.Computability.Automata.NFA
+
+/-! # Translation of DFA into NFA -/
+
+namespace DFA
+section NFA
+
+/-- `DFA` is a special case of `NFA`. -/
+@[scoped grind =]
+def toNFA (dfa : DFA State Symbol) : NFA State Symbol where
+  start := {dfa.start}
+  accept := dfa.accept
+  Tr := fun s1 μ s2 => dfa.tr s1 μ = s2
+  finite_state := dfa.finite_state
+  finite_symbol := dfa.finite_symbol
+
+@[scoped grind =]
+lemma toNFA_start {dfa : DFA State Symbol} : dfa.toNFA.start = {dfa.start} := rfl
+
+instance : Coe (DFA State Symbol) (NFA State Symbol) where
+  coe := toNFA
+
+/-- `DA.toNA` correctly characterises transitions. -/
+@[scoped grind =]
+theorem toNA_tr {dfa : DFA State Symbol} :
+  dfa.toNFA.Tr s1 μ s2 ↔ dfa.tr s1 μ = s2 := by
+  rfl
+
+/-- The transition system of a DA is deterministic. -/
+@[scoped grind ⇒]
+theorem toNFA_deterministic (dfa : DFA State Symbol) : dfa.toNFA.Deterministic := by
+  grind
+
+/-- The transition system of a DA is image-finite. -/
+@[scoped grind ⇒]
+theorem toNFA_imageFinite (dfa : DFA State Symbol) : dfa.toNFA.ImageFinite :=
+  dfa.toNFA.deterministic_imageFinite dfa.toNFA_deterministic
+
+/-- Characterisation of multistep transitions. -/
+@[scoped grind =]
+theorem toNFA_mtr {dfa : DFA State Symbol} :
+  dfa.toNFA.MTr s1 xs s2 ↔ dfa.mtr s1 xs = s2 := by
+  have : ∀ x, dfa.toNFA.Tr s1 x (dfa.tr s1 x) := by grind
+  constructor <;> intro h
+  case mp => induction h <;> grind
+  case mpr => induction xs generalizing s1 <;> grind
+
+/-- The `NFA` constructed from a `DFA` has the same language. -/
+@[scoped grind =]
+theorem toNFA_language_eq {dfa : DFA State Symbol} :
+  dfa.toNFA.language = dfa.language := by
+  ext xs
+  refine ⟨?_, fun _ => ⟨dfa.start, ?_⟩⟩ <;> open NFA in grind
+
+end NFA
+end DFA
diff --git a/Cslib/Computability/Automata/EpsilonNFA.lean b/Cslib/Computability/Automata/EpsilonNFA.lean
new file mode 100644
index 00000000..0b62a42c
--- /dev/null
+++ b/Cslib/Computability/Automata/EpsilonNFA.lean
@@ -0,0 +1,52 @@
+/-
+Copyright (c) 2025 Fabrizio Montesi. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Fabrizio Montesi
+-/
+
+import Cslib.Computability.Automata.NA
+
+/-! # Nondeterministic automata with ε-transitions. -/
+
+/-- A nondeterministic finite automaton with ε-transitions (`εNFA`) is an `NA` with an `Option`
+symbol type. The special symbol ε is represented by the `Option.none` case.
+
+Internally, ε (`Option.none`) is treated as the `τ` label of the underlying transition system,
+allowing for reusing the definitions and results on saturated transitions of `LTS` to deal with
+ε-closure. -/
+structure εNFA (State : Type _) (Symbol : Type _) extends NA State (Option Symbol) where
+  /-- The set of accepting states of the automaton. -/
+  accept : Set State
+  /-- The automaton is finite-state. -/
+  finite_state : Finite State
+  /-- The type of symbols (also called 'alphabet') is finite. -/
+  finite_symbol : Finite Symbol
+
+@[local grind =]
+private instance : HasTau (Option α) := ⟨.none⟩
+
+/-- The `ε`-closure of a set of states `S` is the set of states reachable by any state in `S`
+by performing only `ε`-transitions. We use `LTS.τClosure` since `ε` (`Option.none`) is an instance
+of `HasTau.τ`. -/
+abbrev εNFA.εClosure (enfa : εNFA State Symbol) (S : Set State) := enfa.τClosure S
+
+namespace εNFA
+
+/-- An εNFA accepts a string if there is a saturated multistep accepting derivative with that trace
+from the start state. -/
+@[scoped grind]
+def Accepts (enfa : εNFA State Symbol) (xs : List Symbol) :=
+  ∃ s ∈ enfa.εClosure enfa.start, ∃ s' ∈ enfa.accept,
+  enfa.saturate.MTr s (xs.map (some ·)) s'
+
+/-- The language of an εDA is the set of strings that it accepts. -/
+@[scoped grind =]
+def language (enfa : εNFA State Symbol) : Set (List Symbol) :=
+  { xs | enfa.Accepts xs }
+
+/-- A string is accepted by an εNFA iff it is in the language of the NA. -/
+@[scoped grind =]
+theorem accepts_mem_language (enfa : εNFA State Symbol) (xs : List Symbol) :
+  enfa.Accepts xs ↔ xs ∈ enfa.language := by rfl
+
+end εNFA
diff --git a/Cslib/Computability/Automata/EpsilonNFAToNFA.lean b/Cslib/Computability/Automata/EpsilonNFAToNFA.lean
new file mode 100644
index 00000000..e705fe58
--- /dev/null
+++ b/Cslib/Computability/Automata/EpsilonNFAToNFA.lean
@@ -0,0 +1,55 @@
+/-
+Copyright (c) 2025 Fabrizio Montesi. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Fabrizio Montesi
+-/
+
+import Cslib.Computability.Automata.EpsilonNFA
+import Cslib.Computability.Automata.NFA
+
+/-! # Translation of εNFA into NFA -/
+
+/-- Converts an `LTS` with Option labels into an `LTS` on the carried label type, by removing all
+ε-transitions. -/
+@[grind]
+private def LTS.noε (lts : LTS State (Option Label)) : LTS State Label where
+  Tr := fun s μ s' => lts.Tr s (some μ) s'
+
+@[local grind]
+private lemma LTS.noε_saturate_tr
+  {lts : LTS State (Option Label)} {h : μ = some μ'} :
+  lts.saturate.Tr s μ s' ↔ lts.saturate.noε.Tr s μ' s' := by
+  simp only [LTS.noε]
+  grind
+
+namespace εNFA
+section NFA
+
+/-- Any εNFA can be converted into an NFA that does not use ε-transitions. -/
+@[scoped grind]
+def toNFA (enfa : εNFA State Symbol) : NFA State Symbol where
+  start := enfa.εClosure enfa.start
+  accept := enfa.accept
+  Tr := enfa.saturate.noε.Tr
+  finite_state := enfa.finite_state
+  finite_symbol := enfa.finite_symbol
+
+@[scoped grind]
+lemma LTS.noε_saturate_mTr
+  {lts : LTS State (Option Label)} :
+  lts.saturate.MTr s (μs.map (some ·)) = lts.saturate.noε.MTr s μs := by
+  ext s'
+  induction μs generalizing s <;> grind [<= LTS.MTr.stepL]
+
+
+/-- Correctness of `toNFA`. -/
+@[scoped grind]
+theorem toNFA_language_eq {enfa : εNFA State Symbol} :
+  enfa.toNFA.language = enfa.language := by
+  ext xs
+  have : ∀ s s', enfa.saturate.MTr s (xs.map (some ·)) s' = enfa.saturate.noε.MTr s xs s' := by
+    simp [LTS.noε_saturate_mTr]
+  open NFA in grind
+
+end NFA
+end εNFA
diff --git a/Cslib/Computability/Automata/NA.lean b/Cslib/Computability/Automata/NA.lean
new file mode 100644
index 00000000..71d5592d
--- /dev/null
+++ b/Cslib/Computability/Automata/NA.lean
@@ -0,0 +1,19 @@
+/-
+Copyright (c) 2025 Fabrizio Montesi. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Fabrizio Montesi
+-/
+
+import Cslib.Foundations.Semantics.LTS.Basic
+
+/-! # Nondeterministic Automaton
+
+A Nondeterministic Automaton (NA) is an automaton with a set of initial states.
+
+This definition extends `LTS` and thus stores the transition system as a relation `Tr` of the form
+`State → Symbol → State → Prop`. Note that you can also instantiate `Tr` by passing an argument of
+type `State → Symbol → Set State`; it gets automatically expanded to the former shape.
+-/
+structure NA (State : Type _) (Symbol : Type _) extends LTS State Symbol where
+  /-- The set of initial states of the automaton. -/
+  start : Set State
diff --git a/Cslib/Computability/Automata/NFA.lean b/Cslib/Computability/Automata/NFA.lean
new file mode 100644
index 00000000..1d3df5ba
--- /dev/null
+++ b/Cslib/Computability/Automata/NFA.lean
@@ -0,0 +1,37 @@
+/-
+Copyright (c) 2025 Fabrizio Montesi. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Fabrizio Montesi
+-/
+
+import Cslib.Computability.Automata.NA
+
+/-- A Nondeterministic Finite Automaton (NFA) is a nondeterministic automaton (NA)
+over finite sets of states and symbols. -/
+structure NFA (State : Type _) (Symbol : Type _) extends NA State Symbol where
+  /-- The set of accepting states of the automaton. -/
+  accept : Set State
+  /-- The automaton is finite-state. -/
+  finite_state : Finite State
+  /-- The type of symbols (also called 'alphabet') is finite. -/
+  finite_symbol : Finite Symbol
+
+namespace NFA
+
+/-- An NFA accepts a string if there is a multi-step accepting derivative with that trace from
+the start state. -/
+@[scoped grind]
+def Accepts (nfa : NFA State Symbol) (xs : List Symbol) :=
+  ∃ s ∈ nfa.start, ∃ s' ∈ nfa.accept, nfa.MTr s xs s'
+
+/-- The language of an NFA is the set of strings that it accepts. -/
+@[scoped grind]
+def language (nfa : NFA State Symbol) : Set (List Symbol) :=
+  { xs | nfa.Accepts xs }
+
+/-- A string is accepted by an NFA iff it is in the language of the NFA. -/
+@[scoped grind]
+theorem accepts_mem_language (nfa : NFA State Symbol) (xs : List Symbol) :
+  nfa.Accepts xs ↔ xs ∈ nfa.language := by rfl
+
+end NFA
diff --git a/Cslib/Computability/Automata/NFAToDFA.lean b/Cslib/Computability/Automata/NFAToDFA.lean
new file mode 100644
index 00000000..6a852474
--- /dev/null
+++ b/Cslib/Computability/Automata/NFAToDFA.lean
@@ -0,0 +1,64 @@
+/-
+Copyright (c) 2025 Fabrizio Montesi. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Fabrizio Montesi
+-/
+
+import Cslib.Computability.Automata.DFA
+import Cslib.Computability.Automata.NFA
+import Mathlib.Data.Fintype.Powerset
+
+/-! # Translation of NFA into DFA (subset construction) -/
+
+namespace NFA
+section SubsetConstruction
+
+/-- Converts an `NFA` into a `DFA` using the subset construction. -/
+@[scoped grind =]
+def toDFA (nfa : NFA State Symbol) : DFA (Set State) Symbol := {
+  start := nfa.start
+  accept := { S | ∃ s ∈ S, s ∈ nfa.accept }
+  tr := nfa.setImage
+  finite_state := by
+    haveI := nfa.finite_state
+    infer_instance
+  finite_symbol := nfa.finite_symbol
+}
+
+/-- Characterisation of transitions in `NFA.toDFA` wrt transitions in the original NA. -/
+@[scoped grind =]
+theorem toDFA_mem_tr {nfa : NFA State Symbol} :
+  s' ∈ nfa.toDFA.tr S x ↔ ∃ s ∈ S, nfa.Tr s x s' := by
+  simp only [NFA.toDFA, LTS.setImage, Set.mem_iUnion, exists_prop]
+  grind
+
+/-- Characterisation of multistep transitions in `NFA.toDFA` wrt multistep transitions in the
+original NA. -/
+@[scoped grind =]
+theorem toDFA_mem_mtr {nfa : NFA State Symbol} :
+  s' ∈ nfa.toDFA.mtr S xs ↔ ∃ s ∈ S, nfa.MTr s xs s' := by
+  simp only [NFA.toDFA, DFA.mtr]
+  /- TODO: Grind does not catch a useful rewrite in the subset construction for automata
+
+    A very similar issue seems to occur in the proof of `NFA.toDFA_language_eq`.
+
+    labels: grind, lts, automata
+  -/
+  rw [← LTS.setImageMultistep_foldl_setImage]
+  grind
+
+/-- Characterisation of multistep transitions in `NFA.toDFA` as image transitions in `LTS`. -/
+@[scoped grind =]
+theorem toDFA_mtr_setImageMultistep {nfa : NFA State Symbol} :
+  nfa.toDFA.mtr = nfa.setImageMultistep := by grind
+
+/-- The `DFA` constructed from an `NFA` has the same language. -/
+@[scoped grind =]
+theorem toDFA_language_eq {nfa : NFA State Symbol} :
+  nfa.toDFA.language = nfa.language := by
+  ext xs
+  rw [← DFA.accepts_mem_language]
+  open DFA in grind
+
+end SubsetConstruction
+end NFA
diff --git a/Cslib/Computability/Dfa/Basic.lean b/Cslib/Computability/Dfa/Basic.lean
deleted file mode 100644
index 052ff92a..00000000
--- a/Cslib/Computability/Dfa/Basic.lean
+++ /dev/null
@@ -1,108 +0,0 @@
-/-
-Copyright (c) 2025 Fabrizio Montesi. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Fabrizio Montesi
--/
-
-import Cslib.Foundations.Semantics.Lts.Basic
-
-set_option linter.style.longLine false in
-/-! # Deterministic Finite-State Automata
-
-A Deterministic Finite Automaton (DFA) is a finite-state machine that accepts or rejects
-a finite string.
-
-## References
-
-* [J. E. Hopcroft, R. Motwani, J. D. Ullman, *Introduction to Automata Theory, Languages, and Computation*][Hopcroft2006]
--/
-
-/-- A Deterministic Finite-State Automaton (DFA) consists of a labelled transition function
-`tr` over finite sets of states and labels (called symbols), a starting state `start` and a finite
-set of accepting states `accept`. -/
-structure Dfa (State : Type _) (Symbol : Type _) where
-  /-- The transition function of the automaton. -/
-  tr : State → Symbol → State
-  /-- Start state. -/
-  start : State
-  /-- Accept states. -/
-  accept : Finset State
-  /-- The automaton is finite-state. -/
-  finite_state : Finite State
-  /-- The type of symbols (also called 'alphabet') is finite. -/
-  finite_symbol : Finite Symbol
-
-namespace Dfa
-
-/-- Extended transition function.
-
-Implementation note: compared to [Hopcroft2006], the definition consumes the input list of symbols
-from the left (instead of the right), in order to follow the way lists are constructed.
--/
-@[grind]
-def mtr (dfa : Dfa State Symbol) (s : State) (xs : List Symbol) :=
-  match xs with
-  | [] => s
-  | x :: xs => dfa.mtr (dfa.tr s x) xs
-
-@[grind]
-theorem mtr_nil_eq {dfa : Dfa State Symbol} : dfa.mtr s [] = s := by rfl
-
-/-- A DFA accepts a trace if there is a multi-step accepting derivative with that trace from
-the start state. -/
-@[grind]
-def Accepts (dfa : Dfa State Symbol) (μs : List Symbol) :=
-  (dfa.mtr dfa.start μs) ∈ dfa.accept
-
-/-- The language of a DFA is the set of traces that it accepts. -/
-@[grind]
-def language (dfa : Dfa State Symbol) : Set (List Symbol) :=
-  { μs | dfa.Accepts μs }
-
-/-- A trace is accepted by a DFA iff it is in the language of the DFA. -/
-@[grind]
-theorem accepts_mem_language (dfa : Dfa State Symbol) (μs : List Symbol) :
-  dfa.Accepts μs ↔ μs ∈ dfa.language := by rfl
-
-section Lts
-
-/-- `Dfa` is a special case of `Lts`. -/
-@[grind]
-def toLts (dfa : Dfa State Symbol) : Lts State Symbol :=
-  Lts.mk (fun s1 μ s2 => dfa.tr s1 μ = s2)
-
-instance : Coe (Dfa State Symbol) (Lts State Symbol) where
-  coe := toLts
-
-/-- `Dfa.toLts` correctly characterises transitions. -/
-@[grind]
-theorem toLts_tr {dfa : Dfa State Symbol} :
-  dfa.toLts.Tr s1 μ s2 ↔ dfa.tr s1 μ = s2 := by
-  rfl
-
-/-- `Dfa.toLts` correctly characterises multistep transitions. -/
-@[grind]
-theorem toLts_mtr {dfa : Dfa State Symbol} :
-  dfa.toLts.MTr s1 xs s2 ↔ dfa.mtr s1 xs = s2 := by
-  constructor <;> intro h
-  case mp =>
-    induction h <;> grind
-  case mpr =>
-    induction xs generalizing s1
-    case nil => grind
-    case cons x xs ih =>
-      apply Lts.MTr.stepL (s2 := dfa.tr s1 x) <;> grind
-
-/-- The LTS induced by a DFA is deterministic. -/
-@[grind]
-theorem toLts_deterministic (dfa : Dfa State Symbol) : dfa.toLts.Deterministic := by
-  grind
-
-/-- The LTS induced by a DFA is finite-state. -/
-@[grind]
-theorem toLts_finiteState (dfa : Dfa State Symbol) : dfa.toLts.FiniteState :=
-  dfa.finite_state
-
-end Lts
-
-end Dfa
diff --git a/Cslib/Foundations/Semantics/Lts/Basic.lean b/Cslib/Foundations/Semantics/LTS/Basic.lean
similarity index 52%
rename from Cslib/Foundations/Semantics/Lts/Basic.lean
rename to Cslib/Foundations/Semantics/LTS/Basic.lean
index b6eaa4d1..2176a77d 100644
--- a/Cslib/Foundations/Semantics/Lts/Basic.lean
+++ b/Cslib/Foundations/Semantics/LTS/Basic.lean
@@ -11,35 +11,36 @@ import Mathlib.Logic.Function.Defs
 import Mathlib.Data.Set.Finite.Basic
 import Mathlib.Data.Stream.Defs
 import Mathlib.Util.Notation3
+import Mathlib.Order.SetNotation
 
 /-!
 # Labelled Transition System (LTS)
 
-A Labelled Transition System (`Lts`) models the observable behaviour of the possible states of a
+A Labelled Transition System (`LTS`) models the observable behaviour of the possible states of a
 system. They are particularly popular in the fields of concurrency theory, logic, and programming
 languages.
 
 ## Main definitions
 
-- `Lts` is a structure for labelled transition systems, consisting of a labelled transition
+- `LTS` is a structure for labelled transition systems, consisting of a labelled transition
 relation `Tr` between states. We follow the style and conventions in [Sangiorgi2011].
 
-- `Lts.MTr` extends the transition relation of any Lts to a multi-step transition relation,
+- `LTS.MTr` extends the transition relation of any LTS to a multi-step transition relation,
 formalising the inference system and admissible rules for such relations in [Montesi2023].
 
-- Definitions for all the common classes of Ltss: image-finite, finitely branching, finite-state,
+- Definitions for all the common classes of LTSs: image-finite, finitely branching, finite-state,
 finite, and deterministic.
 
 ## Main statements
 
-- A series of results on `Lts.MTr` that allow for obtaining and composing multi-step transitions in
+- A series of results on `LTS.MTr` that allow for obtaining and composing multi-step transitions in
 different ways.
 
-- `Lts.deterministic_imageFinite`: every deterministic Lts is also image-finite.
+- `LTS.deterministic_imageFinite`: every deterministic LTS is also image-finite.
 
-- `Lts.finiteState_imageFinite`: every finite-state Lts is also image-finite.
+- `LTS.finiteState_imageFinite`: every finite-state LTS is also image-finite.
 
-- `Lts.finiteState_finitelyBranching`: every finite-state Lts is also finitely-branching, if the
+- `LTS.finiteState_finitelyBranching`: every finite-state LTS is also finitely-branching, if the
 type of labels is finite.
 
 ## References
@@ -51,10 +52,10 @@ type of labels is finite.
 universe u v
 
 /--
-A Labelled Transition System (Lts) consists of a type of states (`State`), a type of transition
+A Labelled Transition System (LTS) consists of a type of states (`State`), a type of transition
 labels (`Label`), and a labelled transition relation (`Tr`).
 -/
-structure Lts (State : Type u) (Label : Type v) where
+structure LTS (State : Type u) (Label : Type v) where
   /-- The transition relation. -/
   Tr : State → Label → State → Prop
 
@@ -62,7 +63,7 @@ section MultiStep
 
 /-! ## Multi-step transitions -/
 
-variable {State : Type u} {Label : Type v} (lts : Lts State Label)
+variable {State : Type u} {Label : Type v} (lts : LTS State Label)
 
 /--
 Definition of a multi-step transition.
@@ -72,7 +73,7 @@ rule. This makes working with lists of labels more convenient, because we follow
 construction. It is also similar to what is done in the `SimpleGraph` library in mathlib.)
 -/
 @[grind]
-inductive Lts.MTr (lts : Lts State Label) : State → List Label → State → Prop where
+inductive LTS.MTr (lts : LTS State Label) : State → List Label → State → Prop where
   | 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 →
@@ -80,41 +81,41 @@ inductive Lts.MTr (lts : Lts State Label) : State → List Label → State → P
 
 /-- Any transition is also a multi-step transition. -/
 @[grind]
-theorem Lts.MTr.single {s1 : State} {μ : Label} {s2 : State} :
+theorem LTS.MTr.single {s1 : State} {μ : Label} {s2 : State} :
   lts.Tr s1 μ s2 → lts.MTr s1 [μ] s2 := by
   intro h
-  apply Lts.MTr.stepL
+  apply LTS.MTr.stepL
   · exact h
-  · apply Lts.MTr.refl
+  · apply LTS.MTr.refl
 
 /-- Any multi-step transition can be extended by adding a transition. -/
 @[grind]
-theorem Lts.MTr.stepR {s1 : State} {μs : List Label} {s2 : State} {μ : Label} {s3 : State} :
+theorem LTS.MTr.stepR {s1 : State} {μs : List Label} {s2 : State} {μ : Label} {s3 : State} :
   lts.MTr s1 μs s2 → lts.Tr s2 μ s3 → lts.MTr s1 (μs ++ [μ]) s3 := by
   intro h1 h2
   induction h1
-  case refl s1' => exact Lts.MTr.single lts h2
+  case refl s1' => exact LTS.MTr.single lts h2
   case stepL s1' μ' s2' μs' s3' h1' h3 ih =>
-    apply Lts.MTr.stepL
+    apply LTS.MTr.stepL
     · exact h1'
     · apply ih h2
 
 /-- Multi-step transitions can be composed. -/
 @[grind]
-theorem Lts.MTr.comp {s1 : State} {μs1 : List Label} {s2 : State} {μs2 : List Label} {s3 : State} :
+theorem LTS.MTr.comp {s1 : State} {μs1 : List Label} {s2 : State} {μs2 : List Label} {s3 : State} :
   lts.MTr s1 μs1 s2 → lts.MTr s2 μs2 s3 →
   lts.MTr s1 (μs1 ++ μs2) s3 := by
   intro h1 h2
   induction h1
   case refl => assumption
   case stepL s1 μ s' μs1' s'' h1' h3 ih  =>
-    apply Lts.MTr.stepL
+    apply LTS.MTr.stepL
     · exact h1'
     · apply ih h2
 
 /-- Any 1-sized multi-step transition implies a transition with the same states and label. -/
 @[grind]
-theorem Lts.MTr.single_invert (s1 : State) (μ : Label) (s2 : State) :
+theorem LTS.MTr.single_invert (s1 : State) (μ : Label) (s2 : State) :
   lts.MTr s1 [μ] s2 → lts.Tr s1 μ s2 := by
   intro h
   cases h
@@ -124,22 +125,22 @@ theorem Lts.MTr.single_invert (s1 : State) (μ : Label) (s2 : State) :
 
 /-- In any zero-steps multi-step transition, the origin and the derivative are the same. -/
 @[grind]
-theorem Lts.MTr.nil_eq (h : lts.MTr s1 [] s2) : s1 = s2 := by
+theorem LTS.MTr.nil_eq (h : lts.MTr s1 [] s2) : s1 = s2 := by
   cases h
   rfl
 
 /-- A state `s1` can reach a state `s2` if there exists a multi-step transition from
 `s1` to `s2`. -/
-def Lts.CanReach (s1 s2 : State) : Prop :=
+def LTS.CanReach (s1 s2 : State) : Prop :=
   ∃ μs, lts.MTr s1 μs s2
 
 /-- Any state can reach itself. -/
-theorem Lts.CanReach.refl (s : State) : lts.CanReach s s := by
+theorem LTS.CanReach.refl (s : State) : lts.CanReach s s := by
   exists []
-  apply Lts.MTr.refl
+  apply LTS.MTr.refl
 
-/-- The Lts generated by a state `s` is the Lts given by all the states reachable from `s`. -/
-def Lts.generatedBy (s : State) : Lts {s' : State // lts.CanReach s s'} Label where
+/-- The LTS generated by a state `s` is the LTS given by all the states reachable from `s`. -/
+def LTS.generatedBy (s : State) : LTS {s' : State // lts.CanReach s s'} Label where
   Tr := fun s1 μ s2 => lts.CanReach s s1 ∧ lts.CanReach s s2 ∧ lts.Tr s1 μ s2
 
 end MultiStep
@@ -147,34 +148,38 @@ end MultiStep
 section Termination
 /-! ## Definitions about termination -/
 
-variable {State} {Label} (lts : Lts State Label) {Terminated : State → Prop}
+variable {State} {Label} (lts : LTS State Label) {Terminated : State → Prop}
 
 /-- A state 'may terminate' if it can reach a terminated state. The definition of `Terminated`
 is a parameter. -/
-def Lts.MayTerminate (s : State) : Prop := ∃ s', Terminated s' ∧ lts.CanReach s s'
+def LTS.MayTerminate (s : State) : Prop := ∃ s', Terminated s' ∧ lts.CanReach s s'
 
 /-- A state 'is stuck' if it is not terminated and cannot go forward. The definition of `Terminated`
 is a parameter. -/
-def Lts.Stuck (s : State) : Prop :=
+def LTS.Stuck (s : State) : Prop :=
   ¬Terminated s ∧ ¬∃ μ s', lts.Tr s μ s'
 
 end Termination
 
 section Union
-/-! ## Definitions for the unions of Ltss
+/-! ## Definitions for the unions of LTSs
 
 Note: there is a nontrivial balance between ergonomics and generality here. These definitions might
 change in the future. -/
 
 variable {State : Type u} {Label : Type v}
 
-/-- The union of two Ltss that have common supertypes for states and labels. -/
-def Lts.unionSubtype
+/-- The union of two LTSs defined on the same types. -/
+def LTS.union (lts1 lts2 : LTS State Label) : LTS State Label where
+  Tr := lts1.Tr ⊔ lts2.Tr
+
+/-- The union of two LTSs that have common supertypes for states and labels. -/
+def LTS.unionSubtype
 {S1 : State → Prop} {L1 : Label → Prop} {S2 : State → Prop} {L2 : Label → Prop}
 [DecidablePred S1] [DecidablePred L1] [DecidablePred S2] [DecidablePred L2]
-(lts1 : Lts (@Subtype State S1) (@Subtype Label L1))
-(lts2 : Lts (@Subtype State S2) (@Subtype Label L2)) :
-  Lts State Label where
+(lts1 : LTS (@Subtype State S1) (@Subtype Label L1))
+(lts2 : LTS (@Subtype State S2) (@Subtype Label L2)) :
+  LTS State Label where
   Tr := fun s μ s' =>
     if h : S1 s ∧ L1 μ ∧ S1 s' then
       lts1.Tr ⟨s, h.1⟩ ⟨μ, h.2.1⟩ ⟨s', h.2.2⟩
@@ -184,14 +189,14 @@ def Lts.unionSubtype
       False
 
 /-- TODO: move this to `Sum`? -/
-def Sum.isLeftP {α} {β} (x : α ⊕ β) : Prop := Sum.isLeft x = true
+def Sum.IsLeftP {α} {β} (x : α ⊕ β) : Prop := Sum.isLeft x = true
 
 /-- TODO: move this to `Sum`? -/
-def Sum.isRightP {α} {β} (x : α ⊕ β) : Prop := Sum.isRight x = true
+def Sum.IsRightP {α} {β} (x : α ⊕ β) : Prop := Sum.isRight x = true
 
-/-- Lifting of an `Lts State Label` to `Lts (State ⊕ State') Label`. -/
-def Lts.inl {State'} (lts : Lts State Label) :
-  Lts (@Subtype (State ⊕ State') Sum.isLeftP) (@Subtype Label (Function.const Label True)) where
+/-- Lifting of an `LTS State Label` to `LTS (State ⊕ State') Label`. -/
+def LTS.inl {State'} (lts : LTS State Label) :
+  LTS (@Subtype (State ⊕ State') Sum.IsLeftP) (@Subtype Label (Function.const Label True)) where
   Tr := fun s μ s' =>
     let ⟨s, _⟩ := s
     let ⟨s', _⟩ := s'
@@ -199,9 +204,9 @@ def Lts.inl {State'} (lts : Lts State Label) :
     | Sum.inl s1, μ, Sum.inl s2 => lts.Tr s1 μ s2
     | _, _, _ => False
 
-/-- Lifting of an `Lts State Label` to `Lts (State' ⊕ State) Label`. -/
-def Lts.inr {State'} (lts : Lts State Label) :
-  Lts (@Subtype (State' ⊕ State) Sum.isRightP) (@Subtype Label (Function.const Label True)) where
+/-- Lifting of an `LTS State Label` to `LTS (State' ⊕ State) Label`. -/
+def LTS.inr {State'} (lts : LTS State Label) :
+  LTS (@Subtype (State' ⊕ State) Sum.IsRightP) (@Subtype Label (Function.const Label True)) where
   Tr := fun s μ s' =>
     let ⟨s, _⟩ := s
     let ⟨s', _⟩ := s'
@@ -209,22 +214,22 @@ def Lts.inr {State'} (lts : Lts State Label) :
     | Sum.inr s1, μ, Sum.inr s2 => lts.Tr s1 μ s2
     | _, _, _ => False
 
-/-- Union of two Ltss with the same `Label` type. The result combines the original respective state
+/-- Union of two LTSs with the same `Label` type. The result combines the original respective state
 types `State1` and `State2` into `(State1 ⊕ State2)`. -/
-def Lts.unionSum {State1} {State2} (lts1 : Lts State1 Label) (lts2 : Lts State2 Label) :
-  Lts (State1 ⊕ State2) Label :=
-  @Lts.unionSubtype
+def LTS.unionSum {State1} {State2} (lts1 : LTS State1 Label) (lts2 : LTS State2 Label) :
+  LTS (State1 ⊕ State2) Label :=
+  @LTS.unionSubtype
     (State1 ⊕ State2) Label
-    Sum.isLeftP
+    Sum.IsLeftP
     (Function.const Label True)
-    Sum.isRightP
+    Sum.IsRightP
     (Function.const Label True)
     (by
       intro s
       cases h : s
       · apply Decidable.isTrue
         trivial
-      · simp only [Sum.isLeftP, Sum.isLeft_inr, Bool.false_eq_true]
+      · simp only [Sum.IsLeftP, Sum.isLeft_inr, Bool.false_eq_true]
         apply Decidable.isFalse
         trivial)
     (by
@@ -234,7 +239,7 @@ def Lts.unionSum {State1} {State2} (lts1 : Lts State1 Label) (lts2 : Lts State2
     (by
       intro s
       cases h : s
-      · simp only [Sum.isRightP, Sum.isRight_inl, Bool.false_eq_true]
+      · simp only [Sum.IsRightP, Sum.isRight_inl, Bool.false_eq_true]
         apply Decidable.isFalse
         trivial
       · apply Decidable.isTrue
@@ -250,30 +255,83 @@ end Union
 
 section Classes
 /-!
-### Classes of Ltss
+### Classes of LTSs
 -/
 
-variable {State : Type u} {Label : Type v} (lts : Lts State Label)
+variable {State : Type u} {Label : Type v} (lts : LTS State Label)
 
 /-- An lts is deterministic if a state cannot reach different states with the same transition
 label. -/
 @[grind]
-def Lts.Deterministic : Prop :=
+def LTS.Deterministic : Prop :=
   ∀ (s1 : State) (μ : Label) (s2 s3 : State),
     lts.Tr s1 μ s2 → lts.Tr s1 μ s3 → s2 = s3
 
 /-- The `μ`-image of a state `s` is the set of all `μ`-derivatives of `s`. -/
 @[grind]
-def Lts.Image (s : State) (μ : Label) : Set State := { s' : State | lts.Tr s μ s' }
+def LTS.image (s : State) (μ : Label) : Set State := { s' : State | lts.Tr s μ s' }
+
+/-- The `μs`-image of a state `s`, where `μs` is a list of labels, is the set of all
+`μs`-derivatives of `s`. -/
+@[grind]
+def LTS.imageMultistep (s : State) (μs : List Label) : Set State := { s' : State | lts.MTr s μs s' }
+
+/-- The `μ`-image of a set of states `S` is the union of all `μ`-images of the states in `S`. -/
+@[grind]
+def LTS.setImage (S : Set State) (μ : Label) : Set State :=
+  ⋃ s ∈ S, lts.image s μ
+
+/-- The `μs`-image of a set of states `S`, where `μs` is a list of labels, is the union of all
+`μs`-images of the states in `S`. -/
+@[grind]
+def LTS.setImageMultistep (S : Set State) (μs : List Label) : Set State :=
+  ⋃ s ∈ S, lts.imageMultistep s μs
+
+/-- Characterisation of `setImage` wrt `Tr`. -/
+@[grind]
+theorem LTS.mem_setImage (lts : LTS State Label) :
+  s' ∈ lts.setImage S μ ↔ ∃ s ∈ S, lts.Tr s μ s' := by
+  simp only [setImage, Set.mem_iUnion, exists_prop]
+  grind
+
+@[grind]
+theorem LTS.tr_setImage (lts : LTS State Label) (hs : s ∈ S) (htr : lts.Tr s μ s') :
+  s' ∈ lts.setImage S μ := by grind
+
+/-- Characterisation of `setImageMultistep` with `MTr`. -/
+@[grind]
+theorem LTS.mem_setImageMultistep (lts : LTS State Label) :
+  s' ∈ lts.setImageMultistep S μs ↔ ∃ s ∈ S, lts.MTr s μs s' := by
+  simp only [setImageMultistep, Set.mem_iUnion, exists_prop]
+  grind
+
+@[grind]
+theorem LTS.mTr_setImage (lts : LTS State Label) (hs : s ∈ S) (htr : lts.MTr s μs s') :
+  s' ∈ lts.setImageMultistep S μs := by grind
+
+/-- The image of the empty set is always the empty set. -/
+@[grind]
+theorem LTS.setImage_empty (lts : LTS State Label) : lts.setImage ∅ μ = ∅ := by grind
+
+@[grind]
+lemma LTS.setImageMultistep_setImage_head (lts : LTS State Label) :
+  lts.setImageMultistep S (μ :: μs) = lts.setImageMultistep (lts.setImage S μ ) μs := by grind
+
+/-- Characterisation of `LTS.setImageMultistep` as `List.foldl` on `LTS.setImage`. -/
+@[grind _=_]
+theorem LTS.setImageMultistep_foldl_setImage (lts : LTS State Label) :
+  lts.setImageMultistep = List.foldl lts.setImage := by
+  ext S μs s'
+  induction μs generalizing S <;> grind
 
 /-- An lts is image-finite if all images of its states are finite. -/
 @[grind]
-def Lts.ImageFinite : Prop :=
-  ∀ s μ, Finite (lts.Image s μ)
+def LTS.ImageFinite : Prop :=
+  ∀ s μ, Finite (lts.image s μ)
 
-/-- In a deterministic Lts, if a state has a `μ`-derivative, then it can have no other
+/-- In a deterministic LTS, if a state has a `μ`-derivative, then it can have no other
 `μ`-derivative. -/
-theorem Lts.deterministic_not_lto (hDet : lts.Deterministic) :
+theorem LTS.deterministic_not_lto (hDet : lts.Deterministic) :
   ∀ s μ s' s'', s' ≠ s'' → lts.Tr s μ s' → ¬lts.Tr s μ s'' := by
   intro s μ s' s'' hneq hltos'
   by_contra hltos''
@@ -281,18 +339,18 @@ theorem Lts.deterministic_not_lto (hDet : lts.Deterministic) :
   simp only [← hDet'] at hneq
   contradiction
 
-/-- In a deterministic Lts, any image is either a singleton or the empty set. -/
-theorem Lts.deterministic_image_char (hDet : lts.Deterministic) :
-  ∀ s μ, (∃ s', lts.Image s μ = { s' }) ∨ (lts.Image s μ = ∅) := by
+/-- In a deterministic LTS, any image is either a singleton or the empty set. -/
+theorem LTS.deterministic_image_char (hDet : lts.Deterministic) :
+  ∀ s μ, (∃ s', lts.image s μ = { s' }) ∨ (lts.image s μ = ∅) := by
   intro s μ
-  by_cases hs' : ∃ s', lts.Tr s μ s' <;> aesop (add simp [Image])
+  by_cases hs' : ∃ s', lts.Tr s μ s' <;> aesop (add simp [image])
 
-/-- Every deterministic Lts is also image-finite. -/
-theorem Lts.deterministic_imageFinite :
+/-- Every deterministic LTS is also image-finite. -/
+theorem LTS.deterministic_imageFinite :
   lts.Deterministic → lts.ImageFinite := by
   simp only [ImageFinite]
   intro h s μ
-  have hDet := Lts.deterministic_image_char lts h s μ
+  have hDet := LTS.deterministic_image_char lts h s μ
   cases hDet
   case inl hDet =>
     obtain ⟨s', hDet'⟩ := hDet
@@ -303,46 +361,51 @@ theorem Lts.deterministic_imageFinite :
     apply Set.finite_empty
 
 /-- A state has an outgoing label `μ` if it has a `μ`-derivative. -/
-def Lts.HasOutLabel (s : State) (μ : Label) : Prop :=
+def LTS.HasOutLabel (s : State) (μ : Label) : Prop :=
   ∃ s', lts.Tr s μ s'
 
 /-- The set of outgoing labels of a state. -/
-def Lts.OutgoingLabels (s : State) := { μ | lts.HasOutLabel s μ }
+def LTS.outgoingLabels (s : State) := { μ | lts.HasOutLabel s μ }
 
-/-- An Lts is finitely branching if it is image-finite and all states have finite sets of
+/-- An LTS is finitely branching if it is image-finite and all states have finite sets of
 outgoing labels. -/
-def Lts.FinitelyBranching : Prop :=
-  lts.ImageFinite ∧ ∀ s, Finite (lts.OutgoingLabels s)
+def LTS.FinitelyBranching : Prop :=
+  lts.ImageFinite ∧ ∀ s, Finite (lts.outgoingLabels s)
 
-/-- An Lts is finite-state if it has a finite `State` type. -/
+/-- An LTS is finite-state if it has a finite `State` type. -/
 @[nolint unusedArguments]
-def Lts.FiniteState (_ : Lts State Label) : Prop := Finite State
+def LTS.FiniteState (_ : LTS State Label) : Prop := Finite State
 
-/-- Every finite-state Lts is also image-finite. -/
-theorem Lts.finiteState_imageFinite (hFinite : lts.FiniteState) :
+/-- Every finite-state LTS is also image-finite. -/
+theorem LTS.finiteState_imageFinite (hFinite : lts.FiniteState) :
   lts.ImageFinite := by
   intro s μ
   apply @Subtype.finite State hFinite
 
-/-- Every Lts with finite types for states and labels is also finitely branching. -/
-theorem Lts.finiteState_finitelyBranching
+/-- Every LTS with finite types for states and labels is also finitely branching. -/
+theorem LTS.finiteState_finitelyBranching
   (hFiniteLabel : Finite Label) (hFiniteState : lts.FiniteState) :
   lts.FinitelyBranching := by
   constructor
   case left =>
-    apply Lts.finiteState_imageFinite lts hFiniteState
+    apply LTS.finiteState_imageFinite lts hFiniteState
   case right =>
     intro s
     apply @Subtype.finite Label hFiniteLabel
 
-/-- An Lts is acyclic if there are no infinite multi-step transitions. -/
-def Lts.Acyclic : Prop :=
+/-- An LTS is acyclic if there are no infinite multi-step transitions. -/
+def LTS.Acyclic : Prop :=
   ∃ n, ∀ s1 μs s2, lts.MTr s1 μs s2 → μs.length < n
 
-/-- An Lts is finite if it is finite-state and acyclic. -/
-def Lts.Finite : Prop :=
+/-- An LTS is finite if it is finite-state and acyclic. -/
+def LTS.Finite : Prop :=
   lts.FiniteState ∧ lts.Acyclic
 
+/-
+/-- An LTS has a complete transition relation if every state has a `μ`-derivative for every `μ`. -/
+def LTS.CompleteTr (lts : LTS State Label) : Prop := ∀ s μ, ∃ s', lts.Tr s μ s'
+-/
+
 end Classes
 
 /-! ## Weak transitions (single- and multi-step) -/
@@ -354,116 +417,162 @@ class HasTau (Label : Type v) where
   τ : Label
 
 /-- Saturated transition relation. -/
-inductive Lts.STr [HasTau Label] (lts : Lts State Label) : State → Label → State → Prop where
+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
 
-/-- The `Lts` obtained by saturating the transition relation in `lts`. -/
-def Lts.saturate [HasTau Label] (lts : Lts State Label) : Lts State Label where
-  Tr := Lts.STr lts
+/-- The `LTS` obtained by saturating the transition relation in `lts`. -/
+@[grind =]
+def LTS.saturate [HasTau Label] (lts : LTS State Label) : LTS State Label where
+  Tr := lts.STr
 
 /-- Any transition is also a saturated transition. -/
-theorem Lts.STr.single [HasTau Label] (lts : Lts State Label) : lts.Tr s μ s' → lts.STr s μ s' := by
+@[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 LTS.STr.refl h LTS.STr.refl
 
-/-- As `Lts.str`, but counts the number of `τ`-transitions. This is convenient as induction
+/-- As `LTS.str`, but counts the number of `τ`-transitions. This is convenient as induction
 metric. -/
-inductive Lts.strN [HasTau Label] (lts : Lts State Label) :
+@[grind]
+inductive LTS.STrN [HasTau Label] (lts : LTS State Label) :
   ℕ → State → Label → State → Prop where
-  | refl : lts.strN 0 s HasTau.τ s
+  | refl : lts.STrN 0 s HasTau.τ s
   | tr :
-    lts.strN n s1 HasTau.τ s2 →
+    lts.STrN n s1 HasTau.τ s2 →
     lts.Tr s2 μ s3 →
-    lts.strN m s3 HasTau.τ s4 →
-    lts.strN (n + m + 1) s1 μ s4
+    lts.STrN m s3 HasTau.τ s4 →
+    lts.STrN (n + m + 1) s1 μ s4
 
-/-- `Lts.str` and `Lts.strN` are equivalent. -/
-theorem Lts.str_strN [HasTau Label] (lts : Lts State Label) :
-  lts.STr s1 μ s2 ↔ ∃ n, lts.strN n s1 μ s2 := by
+/-- `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
+      exact LTS.STrN.refl
     case tr s1 sb μ sb' s2 hstr1 htr hstr2 ih1 ih2 =>
       obtain ⟨n1, ih1⟩ := ih1
       obtain ⟨n2, ih2⟩ := ih2
       exists (n1 + n2 + 1)
-      apply Lts.strN.tr ih1 htr ih2
+      apply LTS.STrN.tr ih1 htr ih2
   case mpr =>
     obtain ⟨n, h⟩ := h
     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
+      apply LTS.STr.tr ih1 htr ih2
 
 /-- 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]
+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
+    have ih := LTS.STrN.trans_τ lts hstr2 h2
+    have conc := LTS.STrN.tr hstr1 htr ih
     grind
 
 /-- Saturated transitions labelled by τ can be composed. -/
-theorem Lts.STr.trans_τ
-  [HasTau Label] (lts : Lts State Label)
+@[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⟩
+  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). -/
-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
+@[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
   cases h1
   case refl => grind
   case tr n11 sb sb' n12 hstr1 htr hstr2 =>
-    have hsuffix := Lts.strN.trans_τ lts hstr2 h2
+    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
+    apply LTS.STrN.tr hstr1 htr hsuffix
 
 /-- Saturated transitions can be composed (weighted version). -/
-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
+@[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
+    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
+    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. -/
-theorem Lts.STr.comp
-  [HasTau Label] (lts : Lts State Label)
+@[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⟩
+  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⟩
+
+@[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_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. -/
+@[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 =]
+def LTS.τClosure [HasTau Label] (lts : LTS State Label) (S : Set State) : Set State :=
+  lts.saturate.setImage S HasTau.τ
 
 end Weak
 
@@ -473,27 +582,27 @@ section Divergence
 
 /-- A divergent execution is a stream of states where each state is the anti-τ-derivative of the
 next. -/
-def Lts.DivergentExecution [HasTau Label] (lts : Lts State Label)
+def LTS.DivergentExecution [HasTau Label] (lts : LTS State Label)
   (stream : Stream' State) : Prop :=
   ∀ n, lts.Tr (stream n) HasTau.τ (stream n.succ)
 
 /-- A state is divergent if there is a divergent execution from it. -/
-def Lts.Divergent [HasTau Label] (lts : Lts State Label) (s : State) : Prop :=
+def LTS.Divergent [HasTau Label] (lts : LTS State Label) (s : State) : Prop :=
   ∃ stream : Stream' State, stream 0 = s ∧ lts.DivergentExecution stream
 
 /-- If a stream is a divergent execution, then any 'suffix' is also a divergent execution. -/
-theorem Lts.divergent_drop
-  [HasTau Label] (lts : Lts State Label) (stream : Stream' State)
+theorem LTS.divergent_drop
+  [HasTau Label] (lts : LTS State Label) (stream : Stream' State)
   (h : lts.DivergentExecution stream) (n : ℕ) :
   lts.DivergentExecution (stream.drop n) := by
-  simp only [Lts.DivergentExecution]
+  simp only [LTS.DivergentExecution]
   intro m
   simp only [Stream'.drop, Stream'.get]
-  simp [Lts.DivergentExecution] at h
+  simp [LTS.DivergentExecution] at h
   grind
 
-/-- An Lts is divergence-free if it has no divergent state. -/
-def Lts.DivergenceFree [HasTau Label] (lts : Lts State Label) : Prop :=
+/-- An LTS is divergence-free if it has no divergent state. -/
+def LTS.DivergenceFree [HasTau Label] (lts : LTS State Label) : Prop :=
   ¬∃ s, lts.Divergent s
 
 end Divergence
@@ -501,17 +610,17 @@ 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 :=
+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 :=
+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
+/-- 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
@@ -521,54 +630,54 @@ section Trans
 /-! ## Support for the calc tactic -/
 
 /-- Transitions can be chained. -/
-instance (lts : Lts State Label) :
+instance (lts : LTS State Label) :
   Trans
-    (Lts.Tr.toRelation lts μ1)
-    (Lts.Tr.toRelation lts μ2)
-    (Lts.MTr.toRelation lts [μ1, μ2]) where
+    (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
+    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) :
+instance (lts : LTS State Label) :
   Trans
-    (Lts.Tr.toRelation lts μ)
-    (Lts.MTr.toRelation lts μs)
-    (Lts.MTr.toRelation lts (μ :: μs)) where
+    (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
+    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) :
+instance (lts : LTS State Label) :
   Trans
-    (Lts.MTr.toRelation lts μs)
-    (Lts.Tr.toRelation lts μ)
-    (Lts.MTr.toRelation lts (μs ++ [μ])) where
+    (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
+    apply LTS.MTr.single at htr2
+    apply LTS.MTr.comp lts hmtr1 htr2
 
 /-- Multi-step transitions can be chained. -/
-instance (lts : Lts State Label) :
+instance (lts : LTS State Label) :
   Trans
-    (Lts.MTr.toRelation lts μs1)
-    (Lts.MTr.toRelation lts μs2)
-    (Lts.MTr.toRelation lts (μs1 ++ μs2)) where
+    (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
+    apply LTS.MTr.comp lts hmtr1 hmtr2
 
 end Trans
 
 open Lean Elab Meta Command Term
 
-/-- A command to create an `Lts` from a labelled transition `α → β → α → Prop`, robust to use of
+/-- A command to create an `LTS` from a labelled transition `α → β → α → Prop`, robust to use of
 `variable `-/
 elab "create_lts" lt:ident name:ident : command => do
   liftTermElabM do
@@ -584,7 +693,7 @@ elab "create_lts" lt:ident name:ident : command => do
         throwError m!"expecting Prop, not{indentExpr ty}"
       let params := ci.levelParams.map .param
       let lt := mkAppN (.const lt params) args[0:args.size-3]
-      let bundle ← mkAppM ``Lts.mk #[lt]
+      let bundle ← mkAppM ``LTS.mk #[lt]
       let value ← mkLambdaFVars args[0:args.size-3] bundle
       let type ← inferType value
       addAndCompile <| .defnDecl {
@@ -599,7 +708,7 @@ elab "create_lts" lt:ident name:ident : command => do
       addDeclarationRangesFromSyntax name.getId name
 
 /--
-  This command adds transition notations for an `Lts`. This should not usually be called directly,
+  This command adds transition notations for an `LTS`. This should not usually be called directly,
   but from the `lts` attribute.
 
   As an example `lts_transition_notation foo "β"` will add the notations "[⬝]⭢β" and "[⬝]↠β"
@@ -612,13 +721,13 @@ syntax "lts_transition_notation" ident (str)? : command
 macro_rules
   | `(lts_transition_notation $lts $sym) =>
     `(
-      notation3 t:39 "["μ"]⭢" $sym:str t':39 => (Lts.Tr.toRelation $lts μ) t t'
-      notation3 t:39 "["μs"]↠" $sym:str t':39 => (Lts.MTr.toRelation $lts μs) t t'
+      notation3 t:39 "["μ"]⭢" $sym:str t':39 => (LTS.Tr.toRelation $lts μ) t t'
+      notation3 t:39 "["μs"]↠" $sym:str t':39 => (LTS.MTr.toRelation $lts μs) t t'
      )
   | `(lts_transition_notation $lts) =>
     `(
-      notation3 t:39 "["μ"]⭢" t':39 => (Lts.Tr.toRelation $lts μ) t t'
-      notation3 t:39 "["μs"]↠" t':39 => (Lts.MTr.toRelation $lts μs) t t'
+      notation3 t:39 "["μ"]⭢" t':39 => (LTS.Tr.toRelation $lts μ) t t'
+      notation3 t:39 "["μs"]↠" t':39 => (LTS.MTr.toRelation $lts μs) t t'
      )
 
 /-- This attribute calls the `lts_transition_notation` command for the annotated declaration. -/
@@ -626,7 +735,7 @@ syntax (name := lts_attr) "lts" ident (ppSpace str)? : attr
 
 initialize Lean.registerBuiltinAttribute {
   name := `lts_attr
-  descr := "Register notation for an Lts"
+  descr := "Register notation for an LTS"
   add := fun decl stx _ => MetaM.run' do
     match stx with
     | `(attr | lts $lts $sym) =>
diff --git a/Cslib/Foundations/Semantics/Lts/Bisimulation.lean b/Cslib/Foundations/Semantics/LTS/Bisimulation.lean
similarity index 86%
rename from Cslib/Foundations/Semantics/Lts/Bisimulation.lean
rename to Cslib/Foundations/Semantics/LTS/Bisimulation.lean
index fd805642..bcf40bae 100644
--- a/Cslib/Foundations/Semantics/Lts/Bisimulation.lean
+++ b/Cslib/Foundations/Semantics/LTS/Bisimulation.lean
@@ -4,21 +4,21 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Fabrizio Montesi
 -/
 
-import Cslib.Foundations.Semantics.Lts.Basic
-import Cslib.Foundations.Semantics.Lts.TraceEq
+import Cslib.Foundations.Semantics.LTS.Basic
+import Cslib.Foundations.Semantics.LTS.TraceEq
 import Cslib.Foundations.Data.Relation
-import Cslib.Foundations.Semantics.Lts.Simulation
+import Cslib.Foundations.Semantics.LTS.Simulation
 import Mathlib.Order.CompleteLattice.Defs
 
 /-! # Bisimulation and Bisimilarity
 
-A bisimulation is a binary relation on the states of an `Lts`, which establishes a tight semantic
+A bisimulation is a binary relation on the states of an `LTS`, which establishes a tight semantic
 correspondence. More specifically, if two states `s1` and `s2` are related by a bisimulation, then
 `s1` can mimic all transitions of `s2` and vice versa. Furthermore, the derivatives reaches through
 these transitions remain related by the bisimulation.
 
-Bisimilarity is the largest bisimulation: given an `Lts`, it relates any two states that are related
-by a bisimulation for that Lts.
+Bisimilarity is the largest bisimulation: given an `LTS`, it relates any two states that are related
+by a bisimulation for that LTS.
 
 Weak bisimulation (resp. bisimilarity) is the relaxed version of bisimulation (resp. bisimilarity)
 whereby internal actions performed by processes can be ignored.
@@ -33,7 +33,7 @@ related by some bisimulation on `lts`.
 - `lts.IsBisimulationUpTo r`: the relation `r` is a bisimulation up to bisimilarity (this is known
 as one of the 'up to' techniques for bisimulation).
 
-- `lts.IsWeakBisimulation r`: the relation `r` on the states of the Lts `lts` is a weak
+- `lts.IsWeakBisimulation r`: the relation `r` on the states of the LTS `lts` is a weak
 bisimulation.
 - `WeakBisimilarity lts` is the binary relation on the states of `lts` that relates any two states
 related by some weak bisimulation on `lts`.
@@ -44,24 +44,24 @@ related by some sw-bisimulation on `lts`.
 
 ## Notations
 
-- `s1 ~[lts] s2`: the states `s1` and `s2` are bisimilar in the Lts `lts`.
-- `s1 ≈[lts] s2`: the states `s1` and `s2` are weakly bisimilar in the Lts `lts`.
-- `s1 ≈sw[lts] s2`: the states `s1` and `s2` are sw bisimilar in the Lts `lts`.
+- `s1 ~[lts] s2`: the states `s1` and `s2` are bisimilar in the LTS `lts`.
+- `s1 ≈[lts] s2`: the states `s1` and `s2` are weakly bisimilar in the LTS `lts`.
+- `s1 ≈sw[lts] s2`: the states `s1` and `s2` are sw bisimilar in the LTS `lts`.
 
 ## Main statements
 
-- `Lts.IsBisimulation.inv`: the inverse of a bisimulation is a bisimulation.
+- `LTS.IsBisimulation.inv`: the inverse of a bisimulation is a bisimulation.
 - `Bisimilarity.eqv`: bisimilarity is an equivalence relation (see `Equivalence`).
 - `Bisimilarity.isBisimulation`: bisimilarity is itself a bisimulation.
 - `Bisimilarity.largest_bisimulation`: bisimilarity is the largest bisimulation.
 - `Bisimilarity.gfp`: the union of bisimilarity and any bisimulation is equal to bisimilarity.
-- `Lts.IsBisimulationUpTo.isBisimulation`: any bisimulation up to bisimilarity is a bisimulation.
-- `Lts.IsBisimulation.traceEq`: any bisimulation that relates two states implies that they are
+- `LTS.IsBisimulationUpTo.isBisimulation`: any bisimulation up to bisimilarity is a bisimulation.
+- `LTS.IsBisimulation.traceEq`: any bisimulation that relates two states implies that they are
 trace equivalent (see `TraceEq`).
-- `Bisimilarity.deterministic_bisim_eq_traceEq`: in a deterministic Lts, bisimilarity and trace
+- `Bisimilarity.deterministic_bisim_eq_traceEq`: in a deterministic LTS, bisimilarity and trace
 equivalence coincide.
 - `WeakBisimilarity.weakBisim_eq_swBisim`: weak bisimilarity and sw-bisimilarity coincide in all
-Ltss.
+LTSs.
 - `WeakBisimilarity.eqv`: weak bisimilarity is an equivalence relation.
 - `SWBisimilarity.eqv`: sw-bisimilarity is an equivalence relation.
 
@@ -71,22 +71,22 @@ universe u v
 
 section Bisimulation
 
-variable {State : Type u} {Label : Type v} {lts : Lts State Label}
+variable {State : Type u} {Label : Type v} {lts : LTS State Label}
 
 /-- A relation is a bisimulation if, whenever it relates two states in an lts,
 the transitions originating from these states mimic each other and the reached
 derivatives are themselves related. -/
 @[grind]
-def Lts.IsBisimulation (lts : Lts State Label) (r : State → State → Prop) : Prop :=
+def LTS.IsBisimulation (lts : LTS State Label) (r : State → State → Prop) : Prop :=
   ∀ ⦃s1 s2⦄, r s1 s2 → ∀ μ, (
     (∀ s1', lts.Tr s1 μ s1' → ∃ s2', lts.Tr s2 μ s2' ∧ r s1' s2')
     ∧
     (∀ s2', lts.Tr s2 μ s2' → ∃ s1', lts.Tr s1 μ s1' ∧ r s1' s2')
   )
 
-/- Semi-bundled version of `Lts.IsBisimulation`. -/
+/- Semi-bundled version of `LTS.IsBisimulation`. -/
 -- @[grind ext]
--- structure Bisimulation (lts : Lts State Label) where
+-- structure Bisimulation (lts : LTS State Label) where
 --   /-- The relation on the states of the lts. -/
 --   rel : State → State → Prop
 --   /-- Proof that the relation is a bisimulation. -/
@@ -97,20 +97,20 @@ def Lts.IsBisimulation (lts : Lts State Label) (r : State → State → Prop) :
 --   coe := fun bisim => bisim.rel
 
 /-- Helper for following a transition by the first state in a pair of a `Bisimulation`. -/
-theorem Lts.IsBisimulation.follow_fst
+theorem LTS.IsBisimulation.follow_fst
   (hb : lts.IsBisimulation r) (hr : r s1 s2) (htr : lts.Tr s1 μ s1') :
   ∃ s2', lts.Tr s2 μ s2' ∧ r s1' s2' :=
   (hb hr μ).1 _ htr
 
 /-- Helper for following a transition by the second state in a pair of a `Bisimulation`. -/
-theorem Lts.IsBisimulation.follow_snd
+theorem LTS.IsBisimulation.follow_snd
   (hb : lts.IsBisimulation r) (hr : r s1 s2) (htr : lts.Tr s2 μ s2') :
   ∃ s1', lts.Tr s1 μ s1' ∧ r s1' s2' :=
   (hb hr μ).2 _ htr
 
 /-- Two states are bisimilar if they are related by some bisimulation. -/
 @[grind]
-def Bisimilarity (lts : Lts State Label) : State → State → Prop :=
+def Bisimilarity (lts : LTS State Label) : State → State → Prop :=
   fun s1 s2 => ∃ r : State → State → Prop, r s1 s2 ∧ lts.IsBisimulation r
 
 /--
@@ -129,7 +129,7 @@ theorem Bisimilarity.refl (s : State) : s ~[lts] s := by
 
 /-- The inverse of a bisimulation is a bisimulation. -/
 @[grind]
-theorem Lts.IsBisimulation.inv (h : lts.IsBisimulation r) :
+theorem LTS.IsBisimulation.inv (h : lts.IsBisimulation r) :
   lts.IsBisimulation (flip r) := by grind [flip]
 
 /-- Bisimilarity is symmetric. -/
@@ -141,7 +141,7 @@ theorem Bisimilarity.symm {s1 s2 : State} (h : s1 ~[lts] s2) : s2 ~[lts] s1 := b
 
 /-- The composition of two bisimulations is a bisimulation. -/
 @[grind]
-theorem Lts.IsBisimulation.comp
+theorem LTS.IsBisimulation.comp
   (h1 : lts.IsBisimulation r1) (h2 : lts.IsBisimulation r2) :
   lts.IsBisimulation (Relation.Comp r1 r2) := by grind [Relation.Comp]
 
@@ -295,7 +295,7 @@ end Order
 states in an lts, the transitions originating from these states mimic each other and the reached
 derivatives are themselves related by `r` up to bisimilarity. -/
 @[grind]
-def Lts.IsBisimulationUpTo (lts : Lts State Label) (r : State → State → Prop) : Prop :=
+def LTS.IsBisimulationUpTo (lts : LTS State Label) (r : State → State → Prop) : Prop :=
   ∀ ⦃s1 s2⦄, r s1 s2 → ∀ μ, (
     (∀ s1', lts.Tr s1 μ s1' → ∃ s2', lts.Tr s2 μ s2' ∧ Relation.UpTo r (Bisimilarity lts) s1' s2')
     ∧
@@ -304,7 +304,7 @@ def Lts.IsBisimulationUpTo (lts : Lts State Label) (r : State → State → Prop
 
 /-- Any bisimulation up to bisimilarity is a bisimulation. -/
 @[grind]
-theorem Lts.IsBisimulationUpTo.isBisimulation (h : lts.IsBisimulationUpTo r) :
+theorem LTS.IsBisimulationUpTo.isBisimulation (h : lts.IsBisimulationUpTo r) :
   lts.IsBisimulation (Relation.UpTo r (Bisimilarity lts)) := by
   intro s1 s2 hr μ
   rcases hr with ⟨s1b, hr1b, s2b, hrb, hr2b⟩
@@ -389,7 +389,7 @@ theorem Bisimulation.bisim_trace
 
 /-- Any bisimulation implies trace equivalence. -/
 @[grind]
-theorem Lts.IsBisimulation.traceEq
+theorem LTS.IsBisimulation.traceEq
   (hb : lts.IsBisimulation r) (hr : r s1 s2) :
   s1 ~tr[lts] s2 := by
   funext μs
@@ -431,10 +431,10 @@ private inductive BisimMotTr : ℕ → Char → ℕ → Prop where
 /-- In general, trace equivalence is not a bisimulation (extra conditions are needed, see for
 example `Bisimulation.deterministic_trace_eq_is_bisim`). -/
 theorem Bisimulation.traceEq_not_bisim :
-  ∃ (State : Type) (Label : Type) (lts : Lts State Label), ¬(lts.IsBisimulation (TraceEq lts)) := by
+  ∃ (State : Type) (Label : Type) (lts : LTS State Label), ¬(lts.IsBisimulation (TraceEq lts)) := by
   exists ℕ
   exists Char
-  let lts := Lts.mk BisimMotTr
+  let lts := LTS.mk BisimMotTr
   exists lts
   intro h
   -- specialize h 1 5
@@ -472,18 +472,18 @@ theorem Bisimulation.traceEq_not_bisim :
           case inl h1 =>
             simp only [h1]
             exists 2
-            apply Lts.MTr.single; constructor
+            apply LTS.MTr.single; constructor
           case inr h1 =>
             cases h1
             case inl h1 =>
               simp only [h1]
               exists 3
-              constructor; apply BisimMotTr.one2two; apply Lts.MTr.single;
+              constructor; apply BisimMotTr.one2two; apply LTS.MTr.single;
                 apply BisimMotTr.two2three
             case inr h1 =>
               cases h1
               exists 4
-              constructor; apply BisimMotTr.one2two; apply Lts.MTr.single;
+              constructor; apply BisimMotTr.one2two; apply LTS.MTr.single;
                 apply BisimMotTr.two2four
     have htraces2 : lts.traces 5 = {[], ['a'], ['a', 'b'], ['a', 'c']} := by
       apply Set.ext_iff.2
@@ -529,18 +529,18 @@ theorem Bisimulation.traceEq_not_bisim :
           case inl h1 =>
             simp only [h1]
             exists 6
-            apply Lts.MTr.single; constructor
+            apply LTS.MTr.single; constructor
           case inr h1 =>
             cases h1
             case inl h1 =>
               simp only [h1]
               exists 7
-              constructor; apply BisimMotTr.five2six; apply Lts.MTr.single;
+              constructor; apply BisimMotTr.five2six; apply LTS.MTr.single;
                 apply BisimMotTr.six2seven
             case inr h1 =>
               cases h1
               exists 9
-              constructor; apply BisimMotTr.five2eight; apply Lts.MTr.single;
+              constructor; apply BisimMotTr.five2eight; apply LTS.MTr.single;
                 apply BisimMotTr.eight2nine
     simp [htraces1, htraces2]
   specialize h htreq
@@ -690,7 +690,7 @@ theorem Bisimulation.traceEq_not_bisim :
 
 /-- In general, bisimilarity and trace equivalence are distinct. -/
 theorem Bisimilarity.bisimilarity_neq_traceEq :
-  ∃ (State : Type) (Label : Type) (lts : Lts State Label), Bisimilarity lts ≠ TraceEq lts := by
+  ∃ (State : Type) (Label : Type) (lts : LTS State Label), Bisimilarity lts ≠ TraceEq lts := by
   obtain ⟨State, Label, lts, h⟩ := Bisimulation.traceEq_not_bisim
   exists State; exists Label; exists lts
   intro heq
@@ -698,11 +698,11 @@ theorem Bisimilarity.bisimilarity_neq_traceEq :
   rw [heq] at hb
   contradiction
 
-/-- In any deterministic Lts, trace equivalence is a bisimulation. -/
+/-- In any deterministic LTS, trace equivalence is a bisimulation. -/
 theorem Bisimulation.deterministic_traceEq_is_bisim
   (hdet : lts.Deterministic) :
   (lts.IsBisimulation (TraceEq lts)) := by
-  simp only [Lts.IsBisimulation]
+  simp only [LTS.IsBisimulation]
   intro s1 s2 hteq μ
   constructor
   case left =>
@@ -719,7 +719,7 @@ theorem Bisimulation.deterministic_traceEq_is_bisim
     case right =>
       apply h.2.symm
 
-/-- In any deterministic Lts, trace equivalence implies bisimilarity. -/
+/-- In any deterministic LTS, trace equivalence implies bisimilarity. -/
 theorem Bisimilarity.deterministic_traceEq_bisim
   (hdet : lts.Deterministic) (h : s1 ~tr[lts] s2) :
   (s1 ~[lts] s2) := by
@@ -730,9 +730,9 @@ theorem Bisimilarity.deterministic_traceEq_bisim
   case right =>
     apply Bisimulation.deterministic_traceEq_is_bisim hdet
 
-/-- In any deterministic Lts, bisimilarity and trace equivalence coincide. -/
+/-- In any deterministic LTS, bisimilarity and trace equivalence coincide. -/
 theorem Bisimilarity.deterministic_bisim_eq_traceEq
-  (lts : Lts State Label) (hdet : lts.Deterministic) :
+  (lts : LTS State Label) (hdet : lts.Deterministic) :
   Bisimilarity lts = TraceEq lts := by
   funext s1 s2
   simp only [eq_iff_iff]
@@ -745,16 +745,16 @@ theorem Bisimilarity.deterministic_bisim_eq_traceEq
 /-! ## Relation to simulation -/
 
 /-- Any bisimulation is also a simulation. -/
-theorem Bisimulation.is_simulation (lts : Lts State Label) (r : State → State → Prop) :
+theorem Bisimulation.is_simulation (lts : LTS State Label) (r : State → State → Prop) :
   lts.IsBisimulation r → Simulation lts r := by
   grind [Simulation]
 
 /-- A relation is a bisimulation iff both it and its inverse are simulations. -/
-theorem Bisimulation.simulation_iff (lts : Lts State Label) (r : State → State → Prop) :
+theorem Bisimulation.simulation_iff (lts : LTS State Label) (r : State → State → Prop) :
   lts.IsBisimulation r ↔ (Simulation lts r ∧ Simulation lts (flip r)) := by
   constructor
   case mp => grind [Simulation, flip]
-  case mpr => aesop (add simp [Lts.IsBisimulation])
+  case mpr => aesop (add simp [LTS.IsBisimulation])
 
 end Bisimulation
 
@@ -763,12 +763,12 @@ section WeakBisimulation
 /-! ## Weak bisimulation and weak bisimilarity -/
 
 /-- A weak bisimulation is similar to a `Bisimulation`, but allows for the related processes to do
-internal work. Technically, this is defined as a `Bisimulation` on the saturation of the Lts. -/
-def Lts.IsWeakBisimulation [HasTau Label] (lts : Lts State Label) (r : State → State → Prop) :=
+internal work. Technically, this is defined as a `Bisimulation` on the saturation of the LTS. -/
+def LTS.IsWeakBisimulation [HasTau Label] (lts : LTS State Label) (r : State → State → Prop) :=
   lts.saturate.IsBisimulation  r
 
 /-- Two states are weakly bisimilar if they are related by some weak bisimulation. -/
-def WeakBisimilarity [HasTau Label] (lts : Lts State Label) : State → State → Prop :=
+def WeakBisimilarity [HasTau Label] (lts : LTS State Label) : State → State → Prop :=
   fun s1 s2 =>
     ∃ r : State → State → Prop, r s1 s2 ∧ lts.IsWeakBisimulation r
 
@@ -778,7 +778,7 @@ notation s:max " ≈[" lts "] " s':max => WeakBisimilarity lts s s'
 /-- An `SWBisimulation` is a more convenient definition of weak bisimulation, because the challenge
 is a single transition. We prove later that this technique is sound, following a strategy inspired
 by [Sangiorgi2011]. -/
-def Lts.IsSWBisimulation [HasTau Label] (lts : Lts State Label) (r : State → State → Prop) : Prop :=
+def LTS.IsSWBisimulation [HasTau Label] (lts : LTS State Label) (r : State → State → Prop) : Prop :=
   ∀ ⦃s1 s2⦄, r s1 s2 → ∀ μ, (
     (∀ s1', lts.Tr s1 μ s1' → ∃ s2', lts.STr s2 μ s2' ∧ r s1' s2')
     ∧
@@ -786,7 +786,7 @@ def Lts.IsSWBisimulation [HasTau Label] (lts : Lts State Label) (r : State → S
   )
 
 /-- Two states are sw-bisimilar if they are related by some sw-bisimulation. -/
-def SWBisimilarity [HasTau Label] (lts : Lts State Label) : State → State → Prop :=
+def SWBisimilarity [HasTau Label] (lts : LTS State Label) : State → State → Prop :=
   fun s1 s2 =>
     ∃ r : State → State → Prop, r s1 s2 ∧ lts.IsSWBisimulation r
 
@@ -796,8 +796,8 @@ notation s:max " ≈sw[" lts "] " s':max => SWBisimilarity lts s s'
 /-- Utility theorem for 'following' internal transitions using an `SWBisimulation`
 (first component, weighted version). -/
 theorem SWBisimulation.follow_internal_fst_n
-  [HasTau Label] {lts : Lts State Label}
-  (hswb : lts.IsSWBisimulation r) (hr : r s1 s2) (hstrN : lts.strN n s1 HasTau.τ s1') :
+  [HasTau Label] {lts : LTS State Label}
+  (hswb : lts.IsSWBisimulation r) (hr : r s1 s2) (hstrN : lts.STrN n s1 HasTau.τ s1') :
   ∃ s2', lts.STr s2 HasTau.τ s2' ∧ r s1' s2' := by
   cases n
   case zero =>
@@ -817,14 +817,14 @@ theorem SWBisimulation.follow_internal_fst_n
     obtain ⟨s2', hstrs2', hrs2⟩ := ih2
     exists s2'
     constructor
-    · apply Lts.STr.trans_τ lts (Lts.STr.trans_τ lts hstrs2 hstrsb2) hstrs2'
+    · apply LTS.STr.trans_τ lts (LTS.STr.trans_τ lts hstrs2 hstrsb2) hstrs2'
     · exact hrs2
 
 /-- Utility theorem for 'following' internal transitions using an `SWBisimulation`
 (second component, weighted version). -/
 theorem SWBisimulation.follow_internal_snd_n
-  [HasTau Label] {lts : Lts State Label}
-  (hswb : lts.IsSWBisimulation r) (hr : r s1 s2) (hstrN : lts.strN n s2 HasTau.τ s2') :
+  [HasTau Label] {lts : LTS State Label}
+  (hswb : lts.IsSWBisimulation r) (hr : r s1 s2) (hstrN : lts.STrN n s2 HasTau.τ s2') :
   ∃ s1', lts.STr s1 HasTau.τ s1' ∧ r s1' s2' := by
   cases n
   case zero =>
@@ -844,31 +844,31 @@ theorem SWBisimulation.follow_internal_snd_n
     obtain ⟨s2', hstrs2', hrs2⟩ := ih2
     exists s2'
     constructor
-    · apply Lts.STr.trans_τ lts (Lts.STr.trans_τ lts hstrs1 hstrsb2) hstrs2'
+    · apply LTS.STr.trans_τ lts (LTS.STr.trans_τ lts hstrs1 hstrsb2) hstrs2'
     · exact hrs2
 
 /-- Utility theorem for 'following' internal transitions using an `SWBisimulation`
 (first component). -/
 theorem SWBisimulation.follow_internal_fst
-  [HasTau Label] {lts : Lts State Label}
+  [HasTau Label] {lts : LTS State Label}
   (hswb : lts.IsSWBisimulation r) (hr : r s1 s2) (hstr : lts.STr s1 HasTau.τ s1') :
   ∃ s2', lts.STr s2 HasTau.τ s2' ∧ r s1' s2' := by
-  obtain ⟨n, hstrN⟩ := (Lts.str_strN lts).1 hstr
+  obtain ⟨n, hstrN⟩ := (LTS.sTr_sTrN lts).1 hstr
   apply SWBisimulation.follow_internal_fst_n hswb hr hstrN
 
 /-- Utility theorem for 'following' internal transitions using an `SWBisimulation`
 (second component). -/
 theorem SWBisimulation.follow_internal_snd
-  [HasTau Label] {lts : Lts State Label}
+  [HasTau Label] {lts : LTS State Label}
   (hswb : lts.IsSWBisimulation r) (hr : r s1 s2) (hstr : lts.STr s2 HasTau.τ s2') :
   ∃ s1', lts.STr s1 HasTau.τ s1' ∧ r s1' s2' := by
-  obtain ⟨n, hstrN⟩ := (Lts.str_strN lts).1 hstr
+  obtain ⟨n, hstrN⟩ := (LTS.sTr_sTrN lts).1 hstr
   apply SWBisimulation.follow_internal_snd_n hswb hr hstrN
 
 /-- We can now prove that any relation is a `WeakBisimulation` iff it is an `SWBisimulation`.
 This formalises lemma 4.2.10 in [Sangiorgi2011]. -/
-theorem Lts.isWeakBisimulation_iff_isSWBisimulation
-  [HasTau Label] {lts : Lts State Label} :
+theorem LTS.isWeakBisimulation_iff_isSWBisimulation
+  [HasTau Label] {lts : LTS State Label} :
   lts.IsWeakBisimulation r ↔ lts.IsSWBisimulation r := by
   apply Iff.intro
   case mp =>
@@ -877,13 +877,13 @@ theorem Lts.isWeakBisimulation_iff_isSWBisimulation
     case left =>
       intro s1' htr
       specialize h hr μ
-      have h' := h.1 s1' (Lts.STr.single lts htr)
+      have h' := h.1 s1' (LTS.STr.single lts htr)
       obtain ⟨s2', htr2, hr2⟩ := h'
       exists s2'
     case right =>
       intro s2' htr
       specialize h hr μ
-      have h' := h.2 s2' (Lts.STr.single lts htr)
+      have h' := h.2 s2' (LTS.STr.single lts htr)
       obtain ⟨s1', htr1, hr1⟩ := h'
       exists s1'
   case mpr =>
@@ -902,7 +902,7 @@ theorem Lts.isWeakBisimulation_iff_isSWBisimulation
         obtain ⟨s2', hstr2', hrb2⟩ := SWBisimulation.follow_internal_fst h hrb' hstr2
         exists s2'
         constructor
-        · exact Lts.STr.comp lts hstr2b hstr2b' hstr2'
+        · exact LTS.STr.comp lts hstr2b hstr2b' hstr2'
         · exact hrb2
     case right =>
       intro s2' hstr
@@ -917,29 +917,29 @@ theorem Lts.isWeakBisimulation_iff_isSWBisimulation
         obtain ⟨s1', hstr1', hrb2⟩ := SWBisimulation.follow_internal_snd h hrb' hstr2
         exists s1'
         constructor
-        · exact Lts.STr.comp lts hstr1b hstr1b' hstr1'
+        · exact LTS.STr.comp lts hstr1b hstr1b' hstr1'
         · exact hrb2
 
 theorem WeakBisimulation.toSwBisimulation
-  [HasTau Label] {lts : Lts State Label} {r : State → State → Prop} (h : lts.IsWeakBisimulation r) :
-    lts.IsSWBisimulation r := Lts.isWeakBisimulation_iff_isSWBisimulation.1 h
+  [HasTau Label] {lts : LTS State Label} {r : State → State → Prop} (h : lts.IsWeakBisimulation r) :
+    lts.IsSWBisimulation r := LTS.isWeakBisimulation_iff_isSWBisimulation.1 h
 
 theorem SWBisimulation.toWeakBisimulation
-  [HasTau Label] {lts : Lts State Label} {r : State → State → Prop} (h : lts.IsSWBisimulation r) :
-    lts.IsWeakBisimulation r := Lts.isWeakBisimulation_iff_isSWBisimulation.2 h
+  [HasTau Label] {lts : LTS State Label} {r : State → State → Prop} (h : lts.IsSWBisimulation r) :
+    lts.IsWeakBisimulation r := LTS.isWeakBisimulation_iff_isSWBisimulation.2 h
 
 /-- If two states are related by an `SWBisimulation`, then they are weakly bisimilar. -/
 theorem WeakBisimilarity.by_swBisimulation [HasTau Label]
-  (lts : Lts State Label) (r : State → State → Prop)
+  (lts : LTS State Label) (r : State → State → Prop)
   (hb : lts.IsSWBisimulation r) (hr : r s1 s2) : s1 ≈[lts] s2 := by
   exists r
   constructor
   · exact hr
-  apply Lts.isWeakBisimulation_iff_isSWBisimulation.2 hb
+  apply LTS.isWeakBisimulation_iff_isSWBisimulation.2 hb
 
-/-- Weak bisimilarity and sw-bisimilarity coincide for all Ltss. -/
+/-- Weak bisimilarity and sw-bisimilarity coincide for all LTSs. -/
 @[grind _=_]
-theorem WeakBisimilarity.weakBisim_eq_swBisim [HasTau Label] (lts : Lts State Label) :
+theorem WeakBisimilarity.weakBisim_eq_swBisim [HasTau Label] (lts : LTS State Label) :
   WeakBisimilarity lts = SWBisimilarity lts := by
   funext s1 s2
   simp only [eq_iff_iff]
@@ -950,21 +950,21 @@ theorem WeakBisimilarity.weakBisim_eq_swBisim [HasTau Label] (lts : Lts State La
     exists r
     constructor
     · exact hr
-    apply Lts.isWeakBisimulation_iff_isSWBisimulation.1 hrh
+    apply LTS.isWeakBisimulation_iff_isSWBisimulation.1 hrh
   case mpr =>
     intro h
     obtain ⟨r, hr, hrh⟩ := h
     exists r
     constructor
     · exact hr
-    apply Lts.isWeakBisimulation_iff_isSWBisimulation.2 hrh
+    apply LTS.isWeakBisimulation_iff_isSWBisimulation.2 hrh
 
 /-- sw-bisimilarity is reflexive. -/
-theorem SWBisimilarity.refl [HasTau Label] (lts : Lts State Label) (s : State) : s ≈sw[lts] s := by
+theorem SWBisimilarity.refl [HasTau Label] (lts : LTS State Label) (s : State) : s ≈sw[lts] s := by
   exists Eq
   constructor
   · rfl
-  simp only [Lts.IsSWBisimulation]
+  simp only [LTS.IsSWBisimulation]
   intro s1 s2 hr μ
   cases hr
   constructor
@@ -972,26 +972,26 @@ theorem SWBisimilarity.refl [HasTau Label] (lts : Lts State Label) (s : State) :
     intro s1' htr
     exists s1'
     constructor
-    · apply Lts.STr.single _ htr
+    · apply LTS.STr.single _ htr
     · constructor
   case right =>
     intro s2' htr
     exists s2'
     constructor
-    · apply Lts.STr.single _ htr
+    · apply LTS.STr.single _ htr
     · constructor
 
 /-- Weak bisimilarity is reflexive. -/
-theorem WeakBisimilarity.refl [HasTau Label] (lts : Lts State Label) (s : State) : s ≈[lts] s := by
+theorem WeakBisimilarity.refl [HasTau Label] (lts : LTS State Label) (s : State) : s ≈[lts] s := by
   rw [WeakBisimilarity.weakBisim_eq_swBisim lts]
   apply SWBisimilarity.refl
 
 /-- The inverse of an sw-bisimulation is an sw-bisimulation. -/
-theorem SWBisimulation.inv [HasTau Label] (lts : Lts State Label)
+theorem SWBisimulation.inv [HasTau Label] (lts : LTS State Label)
   (r : State → State → Prop) (h : lts.IsSWBisimulation r) :
   lts.IsSWBisimulation (flip r) := by
-  simp only [Lts.IsSWBisimulation] at h
-  simp only [Lts.IsSWBisimulation]
+  simp only [LTS.IsSWBisimulation] at h
+  simp only [LTS.IsSWBisimulation]
   intro s1 s2 hrinv μ
   constructor
   case left =>
@@ -1008,7 +1008,7 @@ theorem SWBisimulation.inv [HasTau Label] (lts : Lts State Label)
     exists s1'
 
 /-- The inverse of a weak bisimulation is a weak bisimulation. -/
-theorem WeakBisimulation.inv [HasTau Label] (lts : Lts State Label)
+theorem WeakBisimulation.inv [HasTau Label] (lts : LTS State Label)
   (r : State → State → Prop) (h : lts.IsWeakBisimulation r) :
   lts.IsWeakBisimulation (flip r) := by
   apply WeakBisimulation.toSwBisimulation at h
@@ -1017,7 +1017,7 @@ theorem WeakBisimulation.inv [HasTau Label] (lts : Lts State Label)
   exact h'
 
 /-- sw-bisimilarity is symmetric. -/
-theorem SWBisimilarity.symm [HasTau Label] (lts : Lts State Label) (h : s1 ≈sw[lts] s2) :
+theorem SWBisimilarity.symm [HasTau Label] (lts : LTS State Label) (h : s1 ≈sw[lts] s2) :
     s2 ≈sw[lts] s1 := by
   obtain ⟨r, hr, hrh⟩ := h
   exists (flip r)
@@ -1029,7 +1029,7 @@ theorem SWBisimilarity.symm [HasTau Label] (lts : Lts State Label) (h : s1 ≈sw
     apply SWBisimulation.inv lts r hrh
 
 /-- Weak bisimilarity is symmetric. -/
-theorem WeakBisimilarity.symm [HasTau Label] (lts : Lts State Label) (h : s1 ≈[lts] s2) :
+theorem WeakBisimilarity.symm [HasTau Label] (lts : LTS State Label) (h : s1 ≈[lts] s2) :
     s2 ≈[lts] s1 := by
   rw [WeakBisimilarity.weakBisim_eq_swBisim]
   rw [WeakBisimilarity.weakBisim_eq_swBisim] at h
@@ -1038,26 +1038,26 @@ theorem WeakBisimilarity.symm [HasTau Label] (lts : Lts State Label) (h : s1 ≈
 /-- The composition of two weak bisimulations is a weak bisimulation. -/
 theorem WeakBisimulation.comp
   [HasTau Label]
-  (lts : Lts State Label)
+  (lts : LTS State Label)
   (r1 r2 : State → State → Prop) (h1 : lts.IsWeakBisimulation r1) (h2 : lts.IsWeakBisimulation r2) :
   lts.IsWeakBisimulation (Relation.Comp r1 r2) := by
-  simp_all only [Lts.IsWeakBisimulation]
+  simp_all only [LTS.IsWeakBisimulation]
   exact h1.comp h2
 
 /-- The composition of two sw-bisimulations is an sw-bisimulation. -/
 theorem SWBisimulation.comp
   [HasTau Label]
-  (lts : Lts State Label)
+  (lts : LTS State Label)
   (r1 r2 : State → State → Prop) (h1 : lts.IsSWBisimulation r1) (h2 : lts.IsSWBisimulation r2) :
   lts.IsSWBisimulation (Relation.Comp r1 r2) := by
   apply SWBisimulation.toWeakBisimulation at h1
   apply SWBisimulation.toWeakBisimulation at h2
-  apply Lts.isWeakBisimulation_iff_isSWBisimulation.1
+  apply LTS.isWeakBisimulation_iff_isSWBisimulation.1
   apply WeakBisimulation.comp lts r1 r2 h1 h2
 
 /-- Weak bisimilarity is transitive. -/
 theorem WeakBisimilarity.trans [HasTau Label] {s1 s2 s3 : State}
-    (lts : Lts State Label) (h1 : s1 ≈[lts] s2) (h2 : s2 ≈[lts] s3) : s1 ≈[lts] s3 := by
+    (lts : LTS State Label) (h1 : s1 ≈[lts] s2) (h2 : s2 ≈[lts] s3) : s1 ≈[lts] s3 := by
   obtain ⟨r1, hr1, hr1b⟩ := h1
   obtain ⟨r2, hr2, hr2b⟩ := h2
   exists Relation.Comp r1 r2
@@ -1069,12 +1069,12 @@ theorem WeakBisimilarity.trans [HasTau Label] {s1 s2 s3 : State}
 
 /-- sw-bisimilarity is transitive. -/
 theorem SWBisimilarity.trans [HasTau Label] {s1 s2 s3 : State}
-    (lts : Lts State Label) (h1 : s1 ≈sw[lts] s2) (h2 : s2 ≈sw[lts] s3) : s1 ≈sw[lts] s3 := by
+    (lts : LTS State Label) (h1 : s1 ≈sw[lts] s2) (h2 : s2 ≈sw[lts] s3) : s1 ≈sw[lts] s3 := by
   rw [← (WeakBisimilarity.weakBisim_eq_swBisim lts)] at *
   apply WeakBisimilarity.trans lts h1 h2
 
 /-- Weak bisimilarity is an equivalence relation. -/
-theorem WeakBisimilarity.eqv [HasTau Label] {lts : Lts State Label} :
+theorem WeakBisimilarity.eqv [HasTau Label] {lts : LTS State Label} :
   Equivalence (WeakBisimilarity lts) := {
     refl := WeakBisimilarity.refl lts
     symm := WeakBisimilarity.symm lts
@@ -1082,7 +1082,7 @@ theorem WeakBisimilarity.eqv [HasTau Label] {lts : Lts State Label} :
   }
 
 /-- SW-bisimilarity is an equivalence relation. -/
-theorem SWBisimilarity.eqv [HasTau Label] {lts : Lts State Label} :
+theorem SWBisimilarity.eqv [HasTau Label] {lts : LTS State Label} :
   Equivalence (SWBisimilarity lts) := {
     refl := SWBisimilarity.refl lts
     symm := SWBisimilarity.symm lts
diff --git a/Cslib/Foundations/Semantics/Lts/Simulation.lean b/Cslib/Foundations/Semantics/LTS/Simulation.lean
similarity index 86%
rename from Cslib/Foundations/Semantics/Lts/Simulation.lean
rename to Cslib/Foundations/Semantics/LTS/Simulation.lean
index 9e69c92a..7b6066d4 100644
--- a/Cslib/Foundations/Semantics/Lts/Simulation.lean
+++ b/Cslib/Foundations/Semantics/LTS/Simulation.lean
@@ -4,23 +4,23 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Fabrizio Montesi
 -/
 
-import Cslib.Foundations.Semantics.Lts.Basic
+import Cslib.Foundations.Semantics.LTS.Basic
 import Cslib.Foundations.Data.Relation
 
 /-! # Simulation and Similarity
 
-A simulation is a binary relation on the states of an `Lts`: if two states `s1` and `s2` are
+A simulation is a binary relation on the states of an `LTS`: if two states `s1` and `s2` are
 related by a simulation, then `s2` can mimic all transitions of `s1`. Furthermore, the derivatives
 reaches through these transitions remain related by the simulation.
 
-Similarity is the largest simulation: given an `Lts`, it relates any two states that are related
-by a simulation for that Lts.
+Similarity is the largest simulation: given an `LTS`, it relates any two states that are related
+by a simulation for that LTS.
 
 For an introduction to theory of simulation, we refer to [Sangiorgi2011].
 
 ## Main definitions
 
-- `Simulation lts r`: the relation `r` on the states of the Lts `lts` is a simulation.
+- `Simulation lts r`: the relation `r` on the states of the LTS `lts` is a simulation.
 - `Similarity lts` is the binary relation on the states of `lts` that relates any two states
 related by some simulation on `lts`.
 - `SimulationEquiv lts` is the binary relation on the states of `lts` that relates any two states
@@ -28,8 +28,8 @@ similar to each other.
 
 ## Notations
 
-- `s1 ≤[lts] s2`: the states `s1` and `s2` are similar in the Lts `lts`.
-- `s1 ≤≥[lts] s2`: the states `s1` and `s2` are simulation equivalent in the Lts `lts`.
+- `s1 ≤[lts] s2`: the states `s1` and `s2` are similar in the LTS `lts`.
+- `s1 ≤≥[lts] s2`: the states `s1` and `s2` are simulation equivalent in the LTS `lts`.
 
 ## Main statements
 
@@ -41,16 +41,16 @@ universe u v
 
 section Simulation
 
-variable {State : Type u} {Label : Type v} (lts : Lts State Label)
+variable {State : Type u} {Label : Type v} (lts : LTS State Label)
 
 /-- A relation is a simulation if, whenever it relates two states in an lts,
 any transition originating from the first state is mimicked by a transition from the second state
 and the reached derivatives are themselves related. -/
-def Simulation (lts : Lts State Label) (r : State → State → Prop) : Prop :=
+def Simulation (lts : LTS State Label) (r : State → State → Prop) : Prop :=
   ∀ s1 s2, r s1 s2 → ∀ μ s1', lts.Tr s1 μ s1' → ∃ s2', lts.Tr s2 μ s2' ∧ r s1' s2'
 
 /-- Two states are similar if they are related by some simulation. -/
-def Similarity (lts : Lts State Label) : State → State → Prop :=
+def Similarity (lts : LTS State Label) : State → State → Prop :=
   fun s1 s2 =>
     ∃ r : State → State → Prop, r s1 s2 ∧ Simulation lts r
 
@@ -98,7 +98,7 @@ theorem Similarity.trans (h1 : s1 ≤[lts] s2) (h2 : s2 ≤[lts] s3) : s1 ≤[lt
 
 /-- Simulation equivalence relates all states `s1` and `s2` such that `s1 ≤[lts] s2` and
 `s2 ≤[lts] s1`. -/
-def SimulationEquiv (lts : Lts State Label) : State → State → Prop :=
+def SimulationEquiv (lts : LTS State Label) : State → State → Prop :=
   fun s1 s2 =>
     s1 ≤[lts] s2 ∧ s2 ≤[lts] s1
 
@@ -121,7 +121,7 @@ theorem SimulationEquiv.trans {s1 s2 s3 : State} (h1 : s1 ≤≥[lts] s2) (h2 :
   grind [SimulationEquiv, Similarity.trans]
 
 /-- Simulation equivalence is an equivalence relation. -/
-theorem SimulationEquiv.eqv (lts : Lts State Label) :
+theorem SimulationEquiv.eqv (lts : LTS State Label) :
   Equivalence (SimulationEquiv lts) := {
     refl := SimulationEquiv.refl lts
     symm := SimulationEquiv.symm lts
diff --git a/Cslib/Foundations/Semantics/Lts/TraceEq.lean b/Cslib/Foundations/Semantics/LTS/TraceEq.lean
similarity index 71%
rename from Cslib/Foundations/Semantics/Lts/TraceEq.lean
rename to Cslib/Foundations/Semantics/LTS/TraceEq.lean
index 0ecd49e0..adc8806e 100644
--- a/Cslib/Foundations/Semantics/Lts/TraceEq.lean
+++ b/Cslib/Foundations/Semantics/LTS/TraceEq.lean
@@ -4,17 +4,17 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Fabrizio Montesi
 -/
 
-import Cslib.Foundations.Semantics.Lts.Basic
+import Cslib.Foundations.Semantics.LTS.Basic
 import Mathlib.Data.Set.Finite.Basic
 
 /-!
 # Trace Equivalence
 
-Definitions and results on trace equivalence for `Lts`s.
+Definitions and results on trace equivalence for `LTS`s.
 
 ## Main definitions
 
-- `Lts.traces`: the set of traces of a state.
+- `LTS.traces`: the set of traces of a state.
 - `TraceEq s1 s2`: `s1` and `s2` are trace equivalent, i.e., they have the same sets of traces.
 
 ## Notations
@@ -24,21 +24,21 @@ Definitions and results on trace equivalence for `Lts`s.
 ## Main statements
 
 - `TraceEq.eqv`: trace equivalence is an equivalence relation (see `Equivalence`).
-- `TraceEq.deterministic_sim`: in any deterministic `Lts`, trace equivalence is a simulation.
+- `TraceEq.deterministic_sim`: in any deterministic `LTS`, trace equivalence is a simulation.
 
 -/
 
 universe u v
 
-variable {State : Type u} {Label : Type v} (lts : Lts State Label)
+variable {State : Type u} {Label : Type v} (lts : LTS State Label)
 
 /-- The traces of a state `s` is the set of all lists of labels `μs` such that there is a multi-step
 transition labelled by `μs` originating from `s`. -/
-def Lts.traces (s : State) := { μs : List Label | ∃ s', lts.MTr s μs s' }
+def LTS.traces (s : State) := { μs : List Label | ∃ s', lts.MTr s μs s' }
 
 /-- If there is a multi-step transition from `s` labelled by `μs`, then `μs` is in the traces of
 `s`. -/
-theorem Lts.traces_in (s : State) (μs : List Label) (s' : State) (h : lts.MTr s μs s') :
+theorem LTS.traces_in (s : State) (μs : List Label) (s' : State) (h : lts.MTr s μs s') :
     μs ∈ lts.traces s := by
   exists s'
 
@@ -58,7 +58,7 @@ theorem TraceEq.refl (s : State) : s ~tr[lts] s := by
   simp only [TraceEq]
 
 /-- Trace equivalence is symmetric. -/
-theorem TraceEq.symm (lts : Lts State Label) {s1 s2 : State} (h : s1 ~tr[lts] s2) :
+theorem TraceEq.symm (lts : LTS State Label) {s1 s2 : State} (h : s1 ~tr[lts] s2) :
   s2 ~tr[lts] s1 := by
   simp only [TraceEq] at h
   simp only [TraceEq]
@@ -71,7 +71,7 @@ theorem TraceEq.trans {s1 s2 s3 : State} (h1 : s1 ~tr[lts] s2) (h2 : s2 ~tr[lts]
   rw [h1, h2]
 
 /-- Trace equivalence is an equivalence relation. -/
-theorem TraceEq.eqv (lts : Lts State Label) : Equivalence (TraceEq lts) := {
+theorem TraceEq.eqv (lts : LTS State Label) : Equivalence (TraceEq lts) := {
     refl := TraceEq.refl lts
     symm := TraceEq.symm lts
     trans := TraceEq.trans lts
@@ -81,19 +81,19 @@ theorem TraceEq.eqv (lts : Lts State Label) : Equivalence (TraceEq lts) := {
 instance : Trans (TraceEq lts) (TraceEq lts) (TraceEq lts) where
   trans := TraceEq.trans lts
 
-/-- In a deterministic Lts, trace equivalence is a simulation. -/
+/-- In a deterministic LTS, trace equivalence is a simulation. -/
 theorem TraceEq.deterministic_sim
-  (lts : Lts State Label) (hdet : lts.Deterministic) (s1 s2 : State) (h : s1 ~tr[lts] s2) :
+  (lts : LTS State Label) (hdet : lts.Deterministic) (s1 s2 : State) (h : s1 ~tr[lts] s2) :
   ∀ μ s1', lts.Tr s1 μ s1' → ∃ s2', lts.Tr s2 μ s2' ∧ s1' ~tr[lts] s2' := by
   intro μ s1' htr1
-  have hmtr1 := Lts.MTr.single lts htr1
-  have hin := Lts.traces_in lts s1 [μ] s1' hmtr1
+  have hmtr1 := LTS.MTr.single lts htr1
+  have hin := LTS.traces_in lts s1 [μ] s1' hmtr1
   rw [h] at hin
   obtain ⟨s2', hmtr2⟩ := hin
   exists s2'
   constructor
-  · apply Lts.MTr.single_invert lts _ _ _ hmtr2
-  · simp only [TraceEq, Lts.traces]
+  · apply LTS.MTr.single_invert lts _ _ _ hmtr2
+  · simp only [TraceEq, LTS.traces]
     funext μs'
     simp only [eq_iff_iff]
     simp only [setOf]
@@ -101,28 +101,28 @@ theorem TraceEq.deterministic_sim
     case mp =>
       intro hmtr1'
       obtain ⟨s1'', hmtr1'⟩ := hmtr1'
-      have hmtr1comp := Lts.MTr.comp lts hmtr1 hmtr1'
-      have hin := Lts.traces_in lts s1 ([μ] ++ μs') s1'' hmtr1comp
+      have hmtr1comp := LTS.MTr.comp lts hmtr1 hmtr1'
+      have hin := LTS.traces_in lts s1 ([μ] ++ μs') s1'' hmtr1comp
       rw [h] at hin
       obtain ⟨s', hmtr2'⟩ := hin
       cases hmtr2'
       case stepL s2'' htr2 hmtr2' =>
         exists s'
-        have htr2' := Lts.MTr.single_invert lts _ _ _ hmtr2
+        have htr2' := LTS.MTr.single_invert lts _ _ _ hmtr2
         have hdets2 := hdet s2 μ s2' s2'' htr2' htr2
         rw [hdets2]
         exact hmtr2'
     case mpr =>
       intro hmtr2'
       obtain ⟨s2'', hmtr2'⟩ := hmtr2'
-      have hmtr2comp := Lts.MTr.comp lts hmtr2 hmtr2'
-      have hin := Lts.traces_in lts s2 ([μ] ++ μs') s2'' hmtr2comp
+      have hmtr2comp := LTS.MTr.comp lts hmtr2 hmtr2'
+      have hin := LTS.traces_in lts s2 ([μ] ++ μs') s2'' hmtr2comp
       rw [← h] at hin
       obtain ⟨s', hmtr1'⟩ := hin
       cases hmtr1'
       case stepL s1'' htr1 hmtr1' =>
         exists s'
-        have htr1' := Lts.MTr.single_invert lts _ _ _ hmtr1
+        have htr1' := LTS.MTr.single_invert lts _ _ _ hmtr1
         have hdets1 := hdet s1 μ s1' s1'' htr1' htr1
         rw [hdets1]
         exact hmtr1'
diff --git a/Cslib/Languages/CCS/BehaviouralTheory.lean b/Cslib/Languages/CCS/BehaviouralTheory.lean
index 4c627441..838aa0e8 100644
--- a/Cslib/Languages/CCS/BehaviouralTheory.lean
+++ b/Cslib/Languages/CCS/BehaviouralTheory.lean
@@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Fabrizio Montesi
 -/
 
-import Cslib.Foundations.Semantics.Lts.Basic
-import Cslib.Foundations.Semantics.Lts.Bisimulation
+import Cslib.Foundations.Semantics.LTS.Basic
+import Cslib.Foundations.Semantics.LTS.Bisimulation
 import Cslib.Languages.CCS.Basic
 import Cslib.Languages.CCS.Semantics
 
@@ -61,7 +61,7 @@ theorem bisimilarity_par_comm : (par p q) ~[lts (defs := defs)] (par q p) := by
   case left =>
     constructor
   case right =>
-    simp only [Lts.IsBisimulation]
+    simp only [LTS.IsBisimulation]
     intro s1 s2 hr μ
     cases hr
     case parComm p q =>
@@ -237,7 +237,7 @@ private inductive ChoiceComm : (Process Name Constant) → (Process Name Constan
 theorem bisimilarity_choice_comm : (choice p q) ~[lts (defs := defs)] (choice q p) := by
   exists @ChoiceComm Name Constant defs
   repeat constructor
-  simp only [Lts.IsBisimulation]
+  simp only [LTS.IsBisimulation]
   intro s1 s2 hr μ
   cases hr
   case choiceComm =>
@@ -302,7 +302,7 @@ theorem bisimilarity_congr_pre :
   exists @PreBisim _ _ defs
   constructor
   · constructor; assumption
-  simp only [Lts.IsBisimulation]
+  simp only [LTS.IsBisimulation]
   intro s1 s2 hr μ'
   cases hr
   case pre =>
@@ -355,7 +355,7 @@ theorem bisimilarity_congr_res :
   exists @ResBisim _ _ defs
   constructor
   · constructor; assumption
-  simp only [Lts.IsBisimulation]
+  simp only [LTS.IsBisimulation]
   intro s1 s2 hr μ'
   cases hr
   rename_i p q a h
@@ -390,7 +390,7 @@ theorem bisimilarity_congr_choice :
   exists @ChoiceBisim _ _ defs
   constructor
   · constructor; assumption
-  simp only [Lts.IsBisimulation]
+  simp only [LTS.IsBisimulation]
   intro s1 s2 r μ
   constructor
   case left =>
@@ -458,7 +458,7 @@ theorem bisimilarity_congr_par :
   exists @ParBisim _ _ defs
   constructor
   · constructor; assumption
-  simp only [Lts.IsBisimulation]
+  simp only [LTS.IsBisimulation]
   intro s1 s2 r μ
   constructor
   case left =>
diff --git a/Cslib/Languages/CCS/Semantics.lean b/Cslib/Languages/CCS/Semantics.lean
index 212b1473..65f183f5 100644
--- a/Cslib/Languages/CCS/Semantics.lean
+++ b/Cslib/Languages/CCS/Semantics.lean
@@ -4,14 +4,14 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Fabrizio Montesi
 -/
 
-import Cslib.Foundations.Semantics.Lts.Basic
+import Cslib.Foundations.Semantics.LTS.Basic
 import Cslib.Languages.CCS.Basic
 
 /-! # Semantics of CCS
 
 ## Main definitions
 - `CCS.Tr`: transition relation for CCS.
-- `CCS.lts`: the `Lts` of CCS.
+- `CCS.lts`: the `LTS` of CCS.
 
 -/
 
diff --git a/CslibTests/Bisimulation.lean b/CslibTests/Bisimulation.lean
index 5b2f3818..ed2cb44e 100644
--- a/CslibTests/Bisimulation.lean
+++ b/CslibTests/Bisimulation.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Fabrizio Montesi
 -/
 
-import Cslib.Foundations.Semantics.Lts.Bisimulation
+import Cslib.Foundations.Semantics.LTS.Bisimulation
 
 /- An LTS with two bisimilar states. -/
 private inductive tr1 : ℕ → Char → ℕ → Prop where
@@ -17,7 +17,7 @@ private inductive tr1 : ℕ → Char → ℕ → Prop where
 | six2seven : tr1 6 'b' 7
 | six2eight : tr1 6 'c' 8
 
-def lts1 := Lts.mk tr1
+def lts1 := LTS.mk tr1
 
 private inductive Bisim15 : ℕ → ℕ → Prop where
 | oneFive : Bisim15 1 5
@@ -50,8 +50,8 @@ example : 1 ~[lts1] 5 := by
   --   (add simp Bisimulation)
   --   (add safe constructors Bisim15)
   --   (add safe cases Bisim15)
-  --   (add safe cases [Lts.mtr])
-  --   (add simp Lts.tr)
+  --   (add safe cases [LTS.mtr])
+  --   (add simp LTS.tr)
   --   (add safe constructors tr1)
   --   (add unsafe apply Bisimulation.follow_fst)
   --   (add unsafe apply Bisimulation.follow_snd)
diff --git a/CslibTests/Dfa.lean b/CslibTests/DFA.lean
similarity index 92%
rename from CslibTests/Dfa.lean
rename to CslibTests/DFA.lean
index fd6a3463..705f7441 100644
--- a/CslibTests/Dfa.lean
+++ b/CslibTests/DFA.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Fabrizio Montesi
 -/
 
-import Cslib.Computability.Dfa.Basic
+import Cslib.Computability.Automata.DFA
 
 /-! A simple elevator. -/
 
@@ -39,7 +39,7 @@ def tr (floor : Floor) (dir : Direction) : Floor :=
   | .two, .up => .two
   | .two, .down => .one
 
-def elevator : Dfa Floor Direction := {
+def elevator : DFA Floor Direction := {
   tr := tr
   start := .one
   accept := { Floor.one }
diff --git a/CslibTests/Lts.lean b/CslibTests/LTS.lean
similarity index 84%
rename from CslibTests/Lts.lean
rename to CslibTests/LTS.lean
index 4f292dc2..7f24d5d8 100644
--- a/CslibTests/Lts.lean
+++ b/CslibTests/LTS.lean
@@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Fabrizio Montesi
 -/
 
-import Cslib.Foundations.Semantics.Lts.Basic
-import Cslib.Foundations.Semantics.Lts.Bisimulation
+import Cslib.Foundations.Semantics.LTS.Basic
+import Cslib.Foundations.Semantics.LTS.Bisimulation
 import Mathlib.Algebra.Group.Even
 import Mathlib.Algebra.Ring.Parity
 
@@ -21,7 +21,7 @@ theorem NatTr.dom : NatTr n μ m → (n = 1 ∨ n = 2) ∧ (m = 1 ∨ m = 2) :=
   intro h
   cases h <;> simp
 
-def natLts : Lts ℕ ℕ := ⟨NatTr⟩
+def natLTS : LTS ℕ ℕ := ⟨NatTr⟩
 
 inductive NatBisim : ℕ → ℕ → Prop where
 | one_one : NatBisim 1 1
@@ -29,7 +29,7 @@ inductive NatBisim : ℕ → ℕ → Prop where
 | two_one : NatBisim 2 1
 | two_two : NatBisim 2 2
 
-example : 1 ~[natLts] 2 := by
+example : 1 ~[natLTS] 2 := by
   exists NatBisim
   constructor
   · constructor
@@ -50,32 +50,32 @@ instance : HasTau TLabel := {
 inductive NatDivergentTr : ℕ → TLabel → ℕ → Prop where
 | step : NatDivergentTr n τ n.succ
 
-def natDivLts : Lts ℕ TLabel := ⟨NatDivergentTr⟩
+def natDivLTS : LTS ℕ TLabel := ⟨NatDivergentTr⟩
 
 def natInfiniteExecution : Stream' ℕ := fun n => n
 
 theorem natInfiniteExecution.infiniteExecution : 
-    natDivLts.DivergentExecution natInfiniteExecution := by
+    natDivLTS.DivergentExecution natInfiniteExecution := by
   intro n
   constructor
 
-example : natDivLts.Divergent 0 := by
+example : natDivLTS.Divergent 0 := by
   exists natInfiniteExecution
   constructor; constructor
   exact natInfiniteExecution.infiniteExecution
 
-example : natDivLts.Divergent 3 := by
+example : natDivLTS.Divergent 3 := by
   exists natInfiniteExecution.drop 3
   constructor
   · constructor
   · intro; constructor
 
-example : natDivLts.Divergent n := by
+example : natDivLTS.Divergent n := by
   exists natInfiniteExecution.drop n
   simp only [Stream'.drop, zero_add]
   constructor
   · constructor
-  · apply Lts.divergent_drop
+  · apply LTS.divergent_drop
     exact natInfiniteExecution.infiniteExecution
 
 -- check that notation works
@@ -104,7 +104,7 @@ end foo
 #guard_msgs in
 #check foo.bar
 
-/-- info: foo.namespaced_lts : Lts ℕ ℕ -/
+/-- info: foo.namespaced_lts : LTS ℕ ℕ -/
 #guard_msgs in
 #check foo.namespaced_lts