diff --git a/Cslib.lean b/Cslib.lean
index 68c57219..7eb2e73f 100644
--- a/Cslib.lean
+++ b/Cslib.lean
@@ -17,6 +17,7 @@ import Cslib.Computability.Automata.NA.Loop
 import Cslib.Computability.Automata.NA.Prod
 import Cslib.Computability.Automata.NA.Sum
 import Cslib.Computability.Automata.NA.ToDA
+import Cslib.Computability.Automata.NA.Total
 import Cslib.Computability.Languages.ExampleEventuallyZero
 import Cslib.Computability.Languages.Language
 import Cslib.Computability.Languages.OmegaLanguage
diff --git a/Cslib/Computability/Automata/NA/Concat.lean b/Cslib/Computability/Automata/NA/Concat.lean
index 3a1b29d6..e677a81d 100644
--- a/Cslib/Computability/Automata/NA/Concat.lean
+++ b/Cslib/Computability/Automata/NA/Concat.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Ching-Tsun Chou
 -/
 
-import Cslib.Computability.Automata.NA.Basic
+import Cslib.Computability.Automata.NA.Total
 import Cslib.Foundations.Data.OmegaSequence.Temporal
 
 /-! # Concatenation of nondeterministic automata. -/
@@ -74,17 +74,18 @@ lemma concat_run_right {xs : ωSequence Symbol} {ss : ωSequence (State1 ⊕ Sta
 
 /-- A run of `concat na1 na2` containing at least one `na2` state is the concatenation of
 an accepting finite run of `na1` followed by a run of `na2`. -/
-theorem concat_run_proj {xs : ωSequence Symbol} {ss : ωSequence (State1 ⊕ State2)}
-    (hc : (concat na1 na2).Run xs ss) (hr : ∃ k, (ss k).isRight) :
-    ∃ n, xs.take n ∈ language na1 ∧ ∃ ss2, na2.Run (xs.drop n) ss2 ∧ ss.drop n = ss2.map inr := by
-  let n := Nat.find hr
-  have hl (k) (h_k : k < n) := not_isRight.mp <| Nat.find_min hr h_k
-  refine ⟨n, ?_, ?_⟩
+theorem concat_run_proj {xs : ωSequence Symbol} {ss : ωSequence (State1 ⊕ State2)} {k : ℕ}
+    (hc : (concat na1 na2).Run xs ss) (hr : (ss k).isRight) :
+    ∃ n, n ≤ k ∧ xs.take n ∈ language na1 ∧
+    ∃ ss2, na2.Run (xs.drop n) ss2 ∧ ss.drop n = ss2.map inr := by
+  have hr' : ∃ k, (ss k).isRight := by grind
+  let n := Nat.find hr'
+  have hl (k) (h_k : k < n) := not_isRight.mp <| Nat.find_min hr' h_k
+  refine ⟨n, by grind, ?_, ?_⟩
   · by_cases h_n : n = 0
     · grind [concat_start_right]
     · grind [concat_run_left_right]
-  · have hr : (ss n).isRight := Nat.find_spec hr
-    grind [concat_run_right hc n hl hr]
+  · exact concat_run_right hc n hl (Nat.find_spec hr')
 
 /-- Given an accepting finite run of `na1` and a run of `na2`, there exists a run of
 `concat na1 na2` that is the concatenation of the two runs. -/
@@ -117,8 +118,8 @@ theorem concat_language_eq {acc2 : Set State2} :
   ext xs
   constructor
   · rintro ⟨ss, h_run, h_acc⟩
-    have h_ex2 : ∃ k, (ss k).isRight := by grind [Frequently.exists h_acc]
-    obtain ⟨n, h_acc1, ss2, h_run2, h_map2⟩ := concat_run_proj h_run h_ex2
+    obtain ⟨k, h_k⟩ : ∃ k, (ss k).isRight := by grind [Frequently.exists h_acc]
+    obtain ⟨n, _, h_acc1, ss2, h_run2, h_map2⟩ := concat_run_proj h_run h_k
     use xs.take n, h_acc1, xs.drop n, ?_, by simp
     use ss2, h_run2
     grind [(drop_frequently_iff_frequently n).mpr h_acc]
@@ -130,4 +131,49 @@ theorem concat_language_eq {acc2 : Set State2} :
 
 end Buchi
 
+namespace FinAcc
+
+/-- `finConcat na1 na2` is the concatenation of the "totalized" versions of `na1` and `na2`. -/
+def finConcat (na1 : FinAcc State1 Symbol) (na2 : FinAcc State2 Symbol)
+  : NA ((State1 ⊕ Unit) ⊕ (State2 ⊕ Unit)) Symbol :=
+  concat ⟨na1.totalize, inl '' na1.accept⟩ na2.totalize
+
+variable {na1 : FinAcc State1 Symbol} {na2 : FinAcc State2 Symbol}
+
+/-- `finConcat na1 na2` is total. -/
+def finConcat_total : (finConcat na1 na2).Total where
+  next s x := match s with
+    | inl s1 => inl (inr ())
+    | inr s2 => inr (inr ())
+  total s x := by grind [finConcat, concat, NA.totalize, LTS.totalize]
+
+/-- `finConcat na1 na2` accepts the concatenation of the languages of `na1` and `na2`. -/
+theorem finConcat_language_eq [Inhabited Symbol] :
+    language (FinAcc.mk (finConcat na1 na2) (inr '' (inl '' na2.accept))) =
+    language na1 * language na2 := by
+  ext xl
+  constructor
+  · rintro ⟨s, _, t, h_acc, h_mtr⟩
+    obtain ⟨xs, ss, h_ωtr, rfl, rfl⟩ := LTS.Total.mTr_ωTr finConcat_total h_mtr
+    have hc : (finConcat na1 na2).Run (xl ++ω xs) ss := by grind [Run]
+    have hr : (ss xl.length).isRight := by grind
+    obtain ⟨n, _⟩ := concat_run_proj hc hr
+    refine ⟨xl.take n, ?_, xl.drop n, ?_, ?_⟩
+    · grind [totalize_language_eq, take_append_of_le_length]
+    · have : ss xl.length = (ss.drop n) (xl.length - n) := by grind
+      grind [drop_append_of_le_length, take_append_of_le_length, totalize_run_mtr]
+    · exact xl.take_append_drop n
+  · rintro ⟨xl1, h_xl1, xl2, h_xl2, rfl⟩
+    rw [← totalize_language_eq] at h_xl1
+    obtain ⟨_, h_s2, _, _, h_mtr2⟩ := h_xl2
+    obtain ⟨_, _, h_run2, _, _⟩ := totalize_mtr_run h_s2 h_mtr2
+    obtain ⟨ss, ⟨_, h_ωtr⟩, _⟩ := concat_run_exists h_xl1 h_run2
+    grind [
+      finConcat, List.length_append, take_append_of_le_length,
+      extract_eq_drop_take, =_ append_append_ωSequence, get_drop xl2.length xl1.length ss,
+      LTS.ωTr_mTr h_ωtr (zero_le (xl1.length + xl2.length))
+    ]
+
+end FinAcc
+
 end Cslib.Automata.NA
diff --git a/Cslib/Computability/Automata/NA/Loop.lean b/Cslib/Computability/Automata/NA/Loop.lean
index dc24fb30..a6c08907 100644
--- a/Cslib/Computability/Automata/NA/Loop.lean
+++ b/Cslib/Computability/Automata/NA/Loop.lean
@@ -4,14 +4,14 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Ching-Tsun Chou
 -/
 
-import Cslib.Computability.Automata.NA.Basic
+import Cslib.Computability.Automata.NA.Total
 import Cslib.Foundations.Data.OmegaSequence.Temporal
 
 /-! # Loop construction on nondeterministic automata. -/
 
 namespace Cslib.Automata.NA
 
-open Nat List Sum ωSequence Acceptor Language
+open Nat Set Sum ωSequence Acceptor Language
 open scoped Run LTS
 
 variable {Symbol State : Type*}
@@ -77,16 +77,17 @@ lemma loop_run_from_left {xs : ωSequence Symbol} {ss : ωSequence (Unit ⊕ Sta
 
 /-- A run of `na.loop` containing at least one non-initial `()` state is the concatenation
 of a nonempty finite run of `na` followed by a run of `na.loop`. -/
-theorem loop_run_one_iter {xs : ωSequence Symbol} {ss : ωSequence (Unit ⊕ State)}
-    (h : na.loop.Run xs ss) (h1 : ∃ k, 0 < k ∧ (ss k).isLeft) :
-    ∃ n, xs.take n ∈ language na - 1 ∧ na.loop.Run (xs.drop n) (ss.drop n) := by
-  let n := Nat.find h1
-  have : 0 < n ∧ (ss n).isLeft := Nat.find_spec h1
-  have : ∀ k, 0 < k → k < n → (ss k).isRight := by grind [Nat.find_min h1]
-  refine ⟨n, ⟨?_, ?_⟩, ?_⟩
+theorem loop_run_one_iter {xs : ωSequence Symbol} {ss : ωSequence (Unit ⊕ State)} {k : ℕ}
+    (h : na.loop.Run xs ss) (h1 : 0 < k ∧ (ss k).isLeft) :
+    ∃ n, n ≤ k ∧ xs.take n ∈ language na - 1 ∧ na.loop.Run (xs.drop n) (ss.drop n) := by
+  have h1' : ∃ k, 0 < k ∧ (ss k).isLeft := by grind
+  let n := Nat.find h1'
+  have : 0 < n ∧ (ss n).isLeft := Nat.find_spec h1'
+  have : ∀ k, 0 < k → k < n → (ss k).isRight := by grind [Nat.find_min h1']
+  refine ⟨n, by grind, ⟨?_, ?_⟩, ?_⟩
   · grind [loop_run_left_right_left]
   · have neq : (ωSequence.take n xs).length ≠ 0 := by grind
-    exact neq.imp (congrArg length)
+    exact neq.imp (congrArg List.length)
   · grind [loop_run_from_left]
 
 /-- For any finite word in `language na`, there is a corresponding finite run of `na.loop`. -/
@@ -102,6 +103,15 @@ theorem loop_fin_run_exists {xl : List Symbol} (h : xl ∈ language na) :
   · use [inl ()] ++ (sl.extract 1 xl.length).map inr ++ [inl ()]
     grind [FinAcc.loop]
 
+/-- For any finite word in `language na`, there is a corresponding multistep transition
+of `na.loop`. -/
+theorem loop_fin_run_mtr {xl : List Symbol} (h : xl ∈ language na) :
+    na.loop.MTr (inl ()) xl (inl ()) := by
+  obtain ⟨sl, _, _, _, h_run⟩ := loop_fin_run_exists h
+  suffices ∀ k, ∀ _ : k ≤ xl.length, na.loop.MTr (inl ()) (xl.take k) sl[k] by grind
+  intro k
+  induction k <;> grind [LTS.MTr.stepR, List.take_add_one]
+
 /-- For any infinite sequence `xls` of nonempty finite words from `language na`,
 there is an infinite run of `na.loop` corresponding to `xls.flatten` in which
 the state `()` marks the boundaries between the finite words in `xls`. -/
@@ -114,7 +124,7 @@ theorem loop_run_exists [Inhabited Symbol] {xls : ωSequence (List Symbol)}
   choose sls h_sls using fun k ↦ loop_fin_run_exists <| (h k).left
   let segs := ωSequence.mk fun k ↦ (sls k).take (xls k).length
   have h_len : xls.cumLen = segs.cumLen := by ext k; induction k <;> grind
-  have h_pos (k : ℕ) : (segs k).length > 0 := by grind [eq_nil_iff_length_eq_zero]
+  have h_pos (k : ℕ) : (segs k).length > 0 := by grind [List.eq_nil_iff_length_eq_zero]
   have h_mono := cumLen_strictMono h_pos
   have h_zero := cumLen_zero (ls := segs)
   have h_seg0 (k : ℕ) : (segs k)[0]! = inl () := by grind
@@ -144,7 +154,7 @@ theorem loop_language_eq [Inhabited Symbol] :
   apply le_antisymm
   · apply omegaPow_coind
     rintro xs ⟨ss, h_run, h_acc⟩
-    have h1 : ∃ k > 0, (ss k).isLeft := by grind [FinAcc.loop, frequently_atTop'.mp h_acc 0]
+    obtain ⟨k, h1⟩ : ∃ k > 0, (ss k).isLeft := by grind [FinAcc.loop, frequently_atTop'.mp h_acc 0]
     obtain ⟨n, _⟩ := loop_run_one_iter h_run h1
     refine ⟨xs.take n, by grind, xs.drop n, ?_, by simp⟩
     refine ⟨ss.drop n, by grind, ?_⟩
@@ -156,8 +166,66 @@ theorem loop_language_eq [Inhabited Symbol] :
     use ss, h_run
     apply frequently_iff_strictMono.mpr
     use xls.cumLen, ?_, by grind
-    grind [cumLen_strictMono, eq_nil_iff_length_eq_zero]
+    grind [cumLen_strictMono, List.eq_nil_iff_length_eq_zero]
 
 end Buchi
 
+namespace FinAcc
+
+open scoped Computability
+
+/-- `finLoop na` is the loop construction applied to the "totalized" version of `na`. -/
+def finLoop (na : FinAcc State Symbol) : NA (Unit ⊕ (State ⊕ Unit)) Symbol :=
+  FinAcc.loop ⟨na.totalize, inl '' na.accept⟩
+
+/-- `finLoop na` is total, assuming that `na` has at least one start state. -/
+def finLoop_total (h : ∃ s0, s0 ∈ na.start) : na.finLoop.Total where
+  next s x := inr (inr ())
+  total s x := by
+    cases s
+    case inl _ => simpa [finLoop, loop, NA.totalize, LTS.totalize]
+    case inr _ => grind [finLoop, loop, NA.totalize, LTS.totalize]
+
+/-- `finLoop na` accepts the Kleene star of the language of `na`, assuming that
+the latter is nonempty. -/
+theorem loop_language_eq [Inhabited Symbol] (h : ¬ language na = 0) :
+    language (FinAcc.mk na.finLoop {inl ()}) = (language na)∗ := by
+  rw [Language.kstar_iff_mul_add]
+  ext xl; constructor
+  · rintro ⟨s, _, t, h_acc, h_mtr⟩
+    by_cases h_xl : xl = []
+    · grind [mem_add, mem_one]
+    · have h0 : ∃ s0, s0 ∈ na.start := by
+        obtain ⟨_, s0, _, _⟩ := nonempty_iff_ne_empty.mpr h
+        use s0
+      obtain ⟨xs, ss, h_ωtr, rfl, rfl⟩ := LTS.Total.mTr_ωTr (finLoop_total h0) h_mtr
+      have h_run : na.finLoop.Run (xl ++ω xs) ss := by grind [Run]
+      have h1 : 0 < xl.length ∧ (ss xl.length).isLeft := by
+        simp only [mem_singleton_iff] at h_acc
+        grind  [List.eq_nil_iff_length_eq_zero]
+      obtain ⟨n, h_n, _, _, h_ωtr'⟩ := loop_run_one_iter h_run h1
+      left; refine ⟨xl.take n, ?_, xl.drop n, ?_, ?_⟩
+      · grind [totalize_language_eq, take_append_of_le_length]
+      · refine ⟨ss n, by grind, ss xl.length, by grind, ?_⟩
+        have := LTS.ωTr_mTr h_ωtr' (show 0 ≤ xl.length - n by grind)
+        have : n + (xl.length - n) = xl.length := by grind
+        have : ((xl ++ω xs).drop n).extract 0 (xl.length - n) = xl.drop n := by
+          grind [extract_eq_take, drop_append_of_le_length, take_append_of_le_length,
+            List.take_drop, List.take_length, List.length_drop]
+        grind [finLoop]
+      · exact xl.take_append_drop n
+  · rintro (h | h)
+    · obtain ⟨xl1, ⟨h_xl1, _⟩, xl2, h_xl2, rfl⟩ := h
+      rw [← totalize_language_eq] at h_xl1
+      have := loop_fin_run_mtr h_xl1
+      obtain ⟨s1, _, s2, _, _⟩ := h_xl2
+      obtain ⟨rfl⟩ : s1 = inl () := by grind [finLoop, loop]
+      obtain ⟨rfl⟩ : s2 = inl () := by grind [finLoop, loop]
+      refine ⟨inl (), by assumption, inl (), by assumption, ?_⟩
+      apply LTS.MTr.comp <;> assumption
+    · obtain ⟨rfl⟩ := (Language.mem_one xl).mp h
+      refine ⟨inl (), ?_, inl (), ?_, ?_⟩ <;> grind [finLoop, loop]
+
+end FinAcc
+
 end Cslib.Automata.NA
diff --git a/Cslib/Computability/Automata/NA/Total.lean b/Cslib/Computability/Automata/NA/Total.lean
new file mode 100644
index 00000000..95e90f60
--- /dev/null
+++ b/Cslib/Computability/Automata/NA/Total.lean
@@ -0,0 +1,57 @@
+/-
+Copyright (c) 2025 Ching-Tsun Chou. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Ching-Tsun Chou
+-/
+
+import Cslib.Computability.Automata.NA.Basic
+
+/-! # Making a nondeterministic automaton total.
+-/
+
+namespace Cslib.Automata.NA
+
+open Sum ωSequence Acceptor
+
+variable {Symbol State : Type*}
+
+/-- `NA.totalize` makes the original NA total by replacing its LTS with `LTS.totalize`
+and its starting states with their lifted non-sink versions. -/
+def totalize (na : NA State Symbol) : NA (State ⊕ Unit) Symbol where
+  toLTS := na.toLTS.totalize
+  start := inl '' na.start
+
+variable {na : NA State Symbol}
+
+/-- In an infinite execution of `NA.totalize`, as long as the NA stays in a non-sink state,
+the execution so far corresponds to a finite execution of the original NA. -/
+theorem totalize_run_mtr {xs : ωSequence Symbol} {ss : ωSequence (State ⊕ Unit)} {n : ℕ}
+    (h : na.totalize.Run xs ss) (hl : (ss n).isLeft) :
+    ∃ s t, na.MTr s (xs.take n) t ∧ s ∈ na.start ∧ ss 0 = inl s ∧ ss n = inl t := by
+  obtain ⟨s, _, eq₁⟩ := h.start
+  obtain ⟨t, eq₂⟩ := isLeft_iff.mp hl
+  use s, t
+  refine ⟨?_, by grind⟩
+  -- TODO: `grind` does not use congruence relations with `na.totalize.MTr`
+  rw [← LTS.totalize.mtr_left_iff, ← extract_eq_take, eq₁, ← eq₂]
+  exact LTS.ωTr_mTr h.trans (by grind)
+
+/-- Any finite execution of the original NA can be extended to an infinite execution of
+`NA.totalize`, provided that the alphabet is inbabited. -/
+theorem totalize_mtr_run [Inhabited Symbol] {xl : List Symbol} {s t : State}
+    (hs : s ∈ na.start) (hm : na.MTr s xl t) :
+    ∃ xs ss, na.totalize.Run (xl ++ω xs) ss ∧ ss 0 = inl s ∧ ss xl.length = inl t := by
+  grind [totalize, Run, (LTS.totalize.total na.toLTS).mTr_ωTr, =_ LTS.totalize.mtr_left_iff]
+
+namespace FinAcc
+
+/-- `NA.totalize` and the original NA accept the same language of finite words,
+as long as the accepting states are also lifted in the obvious way. -/
+theorem totalize_language_eq {na : FinAcc State Symbol} :
+    language (FinAcc.mk na.totalize (inl '' na.accept)) = language na := by
+  ext xl
+  simp [totalize]
+
+end FinAcc
+
+end Cslib.Automata.NA
diff --git a/Cslib/Computability/Languages/Language.lean b/Cslib/Computability/Languages/Language.lean
index 569171ed..4ccf4e4f 100644
--- a/Cslib/Computability/Languages/Language.lean
+++ b/Cslib/Computability/Languages/Language.lean
@@ -82,4 +82,14 @@ theorem kstar_sub_one : l∗ - 1 = (l - 1) * l∗ := by
       exact ⟨y, h_y, z, h_z, rfl⟩
     · grind [one_def, append_eq_nil_iff]
 
+@[scoped grind =]
+theorem sub_one_kstar : (l - 1)∗ = l∗ := by
+  ext x
+  grind [mem_kstar, mem_kstar_iff_exists_nonempty]
+
+@[scoped grind .]
+theorem kstar_iff_mul_add : m = l∗ ↔ m = (l - 1) * m + 1 := by
+  rw [self_eq_mul_add_iff, mul_one, sub_one_kstar]
+  grind
+
 end Language
diff --git a/Cslib/Computability/Languages/RegularLanguage.lean b/Cslib/Computability/Languages/RegularLanguage.lean
index c7d01175..beaa7c4e 100644
--- a/Cslib/Computability/Languages/RegularLanguage.lean
+++ b/Cslib/Computability/Languages/RegularLanguage.lean
@@ -6,8 +6,11 @@ Authors: Ching-Tsun Chou
 
 import Cslib.Computability.Automata.DA.Prod
 import Cslib.Computability.Automata.DA.ToNA
+import Cslib.Computability.Automata.NA.Concat
+import Cslib.Computability.Automata.NA.Loop
 import Cslib.Computability.Automata.NA.ToDA
 import Mathlib.Computability.DFA
+import Mathlib.Data.Finite.Sum
 import Mathlib.Data.Set.Card
 import Mathlib.Tactic.Common
 
@@ -49,12 +52,14 @@ theorem IsRegular.iff_nfa {l : Language Symbol} :
     use Set State, inferInstance, na.toDAFinAcc
     grind
 
+/-- The complementation of a regular language is regular. -/
 theorem IsRegular.compl {l : Language Symbol} (h : l.IsRegular) : (lᶜ).IsRegular := by
   rw [IsRegular.iff_dfa] at h ⊢
   obtain ⟨State, _, ⟨da, acc⟩, rfl⟩ := h
   use State, inferInstance, ⟨da, accᶜ⟩
   grind
 
+/-- The empty language is regular. -/
 @[simp]
 theorem IsRegular.zero : (0 : Language Symbol).IsRegular := by
   rw [IsRegular.iff_dfa]
@@ -62,6 +67,7 @@ theorem IsRegular.zero : (0 : Language Symbol).IsRegular := by
   use Unit, inferInstance, ⟨DA.mk flts (), ∅⟩
   grind
 
+/-- The language containing only the empty word is regular. -/
 @[simp]
 theorem IsRegular.one : (1 : Language Symbol).IsRegular := by
   rw [IsRegular.iff_dfa]
@@ -73,11 +79,13 @@ theorem IsRegular.one : (1 : Language Symbol).IsRegular := by
     grind
   · grind [Language.mem_one]
 
+/-- The language of all finite words is regular. -/
 @[simp]
 theorem IsRegular.top : (⊤ : Language Symbol).IsRegular := by
   have : (⊥ᶜ : Language Symbol).IsRegular := IsRegular.compl <| IsRegular.zero
   rwa [← compl_bot]
 
+/-- The intersection of two regular languages is regular. -/
 @[simp]
 theorem IsRegular.inf {l1 l2 : Language Symbol}
     (h1 : l1.IsRegular) (h2 : l2.IsRegular) : (l1 ⊓ l2).IsRegular := by
@@ -87,6 +95,7 @@ theorem IsRegular.inf {l1 l2 : Language Symbol}
   use State1 × State2, inferInstance, ⟨da1.prod da2, fst ⁻¹' acc1 ∩ snd ⁻¹' acc2⟩
   ext; grind [Language.mem_inf]
 
+/-- The union of two regular languages is regular. -/
 @[simp]
 theorem IsRegular.add {l1 l2 : Language Symbol}
     (h1 : l1.IsRegular) (h2 : l2.IsRegular) : (l1 + l2).IsRegular := by
@@ -96,6 +105,7 @@ theorem IsRegular.add {l1 l2 : Language Symbol}
   use State1 × State2, inferInstance, ⟨da1.prod da2, fst ⁻¹' acc1 ∪ snd ⁻¹' acc2⟩
   ext; grind [Language.mem_add]
 
+/-- The intersection of any finite number of regular languages is regular. -/
 @[simp]
 theorem IsRegular.iInf {I : Type*} [Finite I] {s : Set I} {l : I → Language Symbol}
     (h : ∀ i ∈ s, (l i).IsRegular) : (⨅ i ∈ s, l i).IsRegular := by
@@ -107,6 +117,7 @@ theorem IsRegular.iInf {I : Type*} [Finite I] {s : Set I} {l : I → Language Sy
     rw [iInf_insert]
     grind [IsRegular.inf]
 
+/-- The union of any finite number of regular languages is regular. -/
 @[simp]
 theorem IsRegular.iSup {I : Type*} [Finite I] {s : Set I} {l : I → Language Symbol}
     (h : ∀ i ∈ s, (l i).IsRegular) : (⨆ i ∈ s, l i).IsRegular := by
@@ -121,4 +132,28 @@ theorem IsRegular.iSup {I : Type*} [Finite I] {s : Set I} {l : I → Language Sy
     rw [iSup_insert]
     apply IsRegular.add <;> grind
 
+open NA.FinAcc Sum in
+/-- The concatenation of two regular languages is regular. -/
+@[simp]
+theorem IsRegular.mul [Inhabited Symbol] {l1 l2 : Language Symbol}
+    (h1 : l1.IsRegular) (h2 : l2.IsRegular) : (l1 * l2).IsRegular := by
+  rw [IsRegular.iff_nfa] at h1 h2 ⊢
+  obtain ⟨State1, h_fin1, nfa1, rfl⟩ := h1
+  obtain ⟨State2, h_fin1, nfa2, rfl⟩ := h2
+  use (State1 ⊕ Unit) ⊕ (State2 ⊕ Unit), inferInstance,
+    ⟨finConcat nfa1 nfa2, inr '' (inl '' nfa2.accept)⟩
+  exact finConcat_language_eq
+
+open NA.FinAcc Sum in
+/-- The Kleene star of a regular language is regular. -/
+@[simp]
+theorem IsRegular.kstar [Inhabited Symbol] {l : Language Symbol}
+    (h : l.IsRegular) : (l∗).IsRegular := by
+  by_cases h_l : l = 0
+  · simp [h_l]
+  · rw [IsRegular.iff_nfa] at h ⊢
+    obtain ⟨State, h_fin, nfa, rfl⟩ := h
+    use Unit ⊕ (State ⊕ Unit), inferInstance, ⟨finLoop nfa, {inl ()}⟩
+    grind [loop_language_eq]
+
 end Cslib.Language
diff --git a/Cslib/Foundations/Semantics/LTS/Basic.lean b/Cslib/Foundations/Semantics/LTS/Basic.lean
index e29c98c8..b5628bcc 100644
--- a/Cslib/Foundations/Semantics/LTS/Basic.lean
+++ b/Cslib/Foundations/Semantics/LTS/Basic.lean
@@ -239,7 +239,7 @@ variable {lts : LTS State Label}
 
 open scoped ωSequence in
 /-- Any finite execution extracted from an infinite execution is valid. -/
-theorem LTS.ωTr_mTr {n m : ℕ} {hnm : n ≤ m} (h : lts.ωTr ss μs) :
+theorem LTS.ωTr_mTr (h : lts.ωTr ss μs) {n m : ℕ} (hnm : n ≤ m) :
     lts.MTr (ss n) (μs.extract n m) (ss m) := by
   by_cases heq : n = m
   case pos => grind
@@ -250,16 +250,119 @@ theorem LTS.ωTr_mTr {n m : ℕ} {hnm : n ≤ m} (h : lts.ωTr ss μs) :
       have : lts.MTr (ss n) (μs.extract n m) (ss m) := ωTr_mTr (hnm := by grind) h
       grind [MTr.comp]
 
-open scoped ωSequence
+open ωSequence
 
 /-- Prepends an infinite execution with a transition. -/
-theorem LTS.ωTr.cons (hmtr : lts.Tr s1 μ s2) (hωtr : lts.ωTr ss μs) (hm : ss 0 = s2) :
-    lts.ωTr (s1 ::ω ss) (μ ::ω μs) := by
+theorem LTS.ωTr.cons (htr : lts.Tr s μ t) (hωtr : lts.ωTr ss μs) (hm : ss 0 = t) :
+    lts.ωTr (s ::ω ss) (μ ::ω μs) := by
   intro i
   induction i <;> grind
 
+/-- Prepends an infinite execution with a finite execution. -/
+theorem LTS.ωTr.append (hmtr : lts.MTr s μl t) (hωtr : lts.ωTr ss μs)
+    (hm : ss 0 = t) : ∃ ss', lts.ωTr ss' (μl ++ω μs) ∧ ss' 0 = s ∧ ss' μl.length = t := by
+  obtain ⟨sl, _, _, _, _⟩ := LTS.MTr.exists_states hmtr
+  refine ⟨sl ++ω ss.drop 1, ?_, by grind [get_append_left], by grind [get_append_left]⟩
+  intro n
+  by_cases n < μl.length
+  · grind [get_append_left]
+  · by_cases n = μl.length
+    · grind [get_append_left]
+    · grind [get_append_right', hωtr (n - μl.length - 1)]
+
 end ωMultiStep
 
+section Total
+
+/-! ## Total LTS
+
+A LTS is total iff every state has a transition for every label.
+-/
+
+open Sum ωSequence
+
+variable {State Label : Type*} {lts : LTS State Label}
+
+/-- `LTS.Total` provides a witness that the LTS is total. -/
+structure LTS.Total (lts : LTS State Label) where
+  /-- `next` provides a next state for any given starting state and label. -/
+  next : State → Label → State
+  /-- A proof that the state provided by `next` indeed forms a legal transition. -/
+  total s μ : lts.Tr s μ (next s μ)
+
+/-- `LTS.makeωTr` builds an infinite execution of a total LTS from any starting state and
+any infinite sequence of labels. -/
+def LTS.makeωTr (lts : LTS State Label) (h : lts.Total)
+    (s : State) (μs : ωSequence Label) : ℕ → State
+  | 0 => s
+  | n + 1 => h.next (lts.makeωTr h s μs n) (μs n)
+
+/-- If a LTS is total, then there exists an infinite execution from any starting state and
+over any infinite sequence of labels. -/
+theorem LTS.Total.ωTr_exists (h : lts.Total) (s : State) (μs : ωSequence Label) :
+    ∃ ss, lts.ωTr ss μs ∧ ss 0 = s := by
+  use lts.makeωTr h s μs
+  grind [LTS.makeωTr, h.total]
+
+/-- If a LTS is total, then any finite execution can be extended to an infinite execution,
+provided that the label type is inbabited. -/
+theorem LTS.Total.mTr_ωTr [Inhabited Label] (ht : lts.Total) {μl : List Label} {s t : State}
+    (hm : lts.MTr s μl t) : ∃ μs ss, lts.ωTr ss (μl ++ω μs) ∧ ss 0 = s ∧ ss μl.length = t := by
+  let μs : ωSequence Label := .const default
+  obtain ⟨ss', ho, h0⟩ := LTS.Total.ωTr_exists ht t μs
+  refine ⟨μs, LTS.ωTr.append hm ho h0⟩
+
+/-- `LTS.totalize` constructs a total LTS from any given LTS by adding a sink state. -/
+def LTS.totalize (lts : LTS State Label) : LTS (State ⊕ Unit) Label where
+  Tr s' μ t' := match s', t' with
+    | inl s, inl t => lts.Tr s μ t
+    | _, inr () => True
+    | inr (), inl _ => False
+
+/-- The LTS constructed by `LTS.totalize` is indeed total. -/
+def LTS.totalize.total (lts : LTS State Label) : lts.totalize.Total where
+  next _ _ := inr ()
+  total _ _ := by simp [LTS.totalize]
+
+/-- In `LTS.totalize`, there is no finite execution from the sink state to any non-sink state. -/
+theorem LTS.totalize.not_right_left {μs : List Label} {t : State} :
+    ¬ lts.totalize.MTr (inr ()) μs (inl t) := by
+  intro h
+  generalize h_s : (inr () : State ⊕ Unit) = s'
+  generalize h_t : (inl t : State ⊕ Unit) = t'
+  rw [h_s, h_t] at h
+  induction h <;> grind [LTS.totalize]
+
+/-- In `LTS.totalize`, the transitions between non-sink states correspond exactly to
+the transitions in the original LTS. -/
+@[simp]
+theorem LTS.totalize.tr_left_iff {μ : Label} {s t : State} :
+    lts.totalize.Tr (inl s) μ (inl t) ↔ lts.Tr s μ t := by
+  simp [LTS.totalize]
+
+/-- In `LTS.totalize`, the multistep transitions between non-sink states correspond exactly to
+the multistep transitions in the original LTS. -/
+@[simp]
+theorem LTS.totalize.mtr_left_iff {μs : List Label} {s t : State} :
+    lts.totalize.MTr (inl s) μs (inl t) ↔ lts.MTr s μs t := by
+  constructor <;> intro h
+  · generalize h_s : (inl s : State ⊕ Unit) = s'
+    generalize h_t : (inl t : State ⊕ Unit) = t'
+    rw [h_s, h_t] at h
+    induction h generalizing s
+    case refl _ => grind [LTS.MTr]
+    case stepL t1' μ t2' μs t3' h_tr h_mtr h_ind =>
+      obtain ⟨rfl⟩ := h_s
+      cases t2'
+      case inl t2 => grind [LTS.MTr, totalize.tr_left_iff.mp h_tr]
+      case inr t2 => grind [totalize.not_right_left]
+  · induction h
+    case refl _ => grind [LTS.MTr]
+    case stepL t1 μ t2 μs t3 h_tr h_mtr h_ind =>
+      grind [LTS.MTr, totalize.tr_left_iff.mpr h_tr]
+
+end Total
+
 section Termination
 /-! ## Definitions about termination -/