diff --git a/Cslib.lean b/Cslib.lean
index 9cec8a39..eb001240 100644
--- a/Cslib.lean
+++ b/Cslib.lean
@@ -1,5 +1,6 @@
 import Cslib.Computability.Automata.Acceptor
 import Cslib.Computability.Automata.DA
+import Cslib.Computability.Automata.DABuchi
 import Cslib.Computability.Automata.DAToNA
 import Cslib.Computability.Automata.EpsilonNA
 import Cslib.Computability.Automata.EpsilonNAToNA
@@ -7,6 +8,7 @@ import Cslib.Computability.Automata.NA
 import Cslib.Computability.Automata.NAToDA
 import Cslib.Computability.Automata.OmegaAcceptor
 import Cslib.Computability.Automata.Prod
+import Cslib.Computability.Languages.ExampleEventuallyZero
 import Cslib.Computability.Languages.Language
 import Cslib.Computability.Languages.OmegaLanguage
 import Cslib.Computability.Languages.OmegaRegularLanguage
@@ -19,6 +21,7 @@ import Cslib.Foundations.Data.HasFresh
 import Cslib.Foundations.Data.Nat.Segment
 import Cslib.Foundations.Data.OmegaSequence.Defs
 import Cslib.Foundations.Data.OmegaSequence.Flatten
+import Cslib.Foundations.Data.OmegaSequence.InfOcc
 import Cslib.Foundations.Data.OmegaSequence.Init
 import Cslib.Foundations.Data.Relation
 import Cslib.Foundations.Lint.Basic
diff --git a/Cslib/Computability/Automata/DA.lean b/Cslib/Computability/Automata/DA.lean
index 441ab370..f5b0cfcc 100644
--- a/Cslib/Computability/Automata/DA.lean
+++ b/Cslib/Computability/Automata/DA.lean
@@ -4,10 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Fabrizio Montesi, Ching-Tsun Chou
 -/
 
-import Cslib.Foundations.Semantics.LTS.FLTS
 import Cslib.Computability.Automata.Acceptor
 import Cslib.Computability.Automata.OmegaAcceptor
-import Cslib.Computability.Languages.OmegaLanguage
+import Cslib.Foundations.Data.OmegaSequence.InfOcc
+import Cslib.Foundations.Semantics.LTS.FLTS
 
 /-! # Deterministic Automata
 
@@ -24,6 +24,9 @@ finiteness assumptions), deterministic Buchi automata, and deterministic Muller
   *Introduction to Automata Theory, Languages, and Computation*][Hopcroft2006]
 -/
 
+open List Filter Cslib.ωSequence
+open scoped Cslib.FLTS
+
 namespace Cslib.Automata
 
 structure DA (State Symbol : Type*) extends FLTS State Symbol where
@@ -34,6 +37,33 @@ namespace DA
 
 variable {State : Type _} {Symbol : Type _}
 
+/-- Helper function for defining `run` below. -/
+@[scoped grind =]
+def run' (da : DA State Symbol) (xs : ωSequence Symbol) : ℕ → State
+  | 0 => da.start
+  | n + 1 => da.tr (run' da xs n) (xs n)
+
+/-- Infinite run. -/
+@[scoped grind =]
+def run (da : DA State Symbol) (xs : ωSequence Symbol) : ωSequence State := da.run' xs
+
+@[simp, scoped grind =]
+theorem run_zero {da : DA State Symbol} {xs : ωSequence Symbol} :
+    da.run xs 0 = da.start :=
+  rfl
+
+@[simp, scoped grind =]
+theorem run_succ {da : DA State Symbol} {xs : ωSequence Symbol} {n : ℕ} :
+    da.run xs (n + 1) = da.tr (da.run xs n) (xs n) := by
+  rfl
+
+@[simp, scoped grind =]
+theorem mtr_extract_eq_run {da : DA State Symbol} {xs : ωSequence Symbol} {n : ℕ} :
+    da.mtr da.start (xs.extract 0 n) = da.run xs n := by
+  induction n
+  case zero => rfl
+  case succ n h_ind => grind [extract_succ_right]
+
 /-- A deterministic automaton that accepts finite strings (lists of symbols). -/
 structure FinAcc (State Symbol : Type*) extends DA State Symbol where
   /-- The accept states. -/
@@ -49,19 +79,13 @@ This is the standard string recognition performed by DFAs in the literature. -/
 instance : Acceptor (DA.FinAcc State Symbol) Symbol where
   Accepts (a : DA.FinAcc State Symbol) (xs : List Symbol) := a.mtr a.start xs ∈ a.accept
 
-end FinAcc
-
-/-- Helper function for defining `run` below. -/
+open Acceptor in
 @[simp, scoped grind =]
-def run' (da : DA State Symbol) (xs : ωSequence Symbol) : ℕ → State
-  | 0 => da.start
-  | n + 1 => da.tr (run' da xs n) (xs n)
+theorem mem_language {a : FinAcc State Symbol} {xs : List Symbol} :
+    xs ∈ language a ↔ a.mtr a.start xs ∈ a.accept :=
+  Iff.rfl
 
-/-- Infinite run. -/
-@[scoped grind =]
-def run (da : DA State Symbol) (xs : ωSequence Symbol) : ωSequence State := da.run' xs
-
-open List Filter
+end FinAcc
 
 /-- Deterministic Buchi automaton. -/
 structure Buchi (State Symbol : Type*) extends DA State Symbol where
@@ -74,6 +98,12 @@ namespace Buchi
 instance : ωAcceptor (Buchi State Symbol) Symbol where
   Accepts (a : Buchi State Symbol) (xs : ωSequence Symbol) := ∃ᶠ k in atTop, a.run xs k ∈ a.accept
 
+open ωAcceptor in
+@[simp, scoped grind =]
+theorem mem_language {a : Buchi State Symbol} {xs : ωSequence Symbol} :
+    xs ∈ language a ↔ ∃ᶠ k in atTop, a.run xs k ∈ a.accept :=
+  Iff.rfl
+
 end Buchi
 
 /-- Deterministic Muller automaton. -/
@@ -87,6 +117,12 @@ namespace Muller
 instance : ωAcceptor (Muller State Symbol) Symbol where
   Accepts (a : Muller State Symbol) (xs : ωSequence Symbol) := (a.run xs).infOcc ∈ a.accept
 
+open ωAcceptor in
+@[simp, scoped grind =]
+theorem mem_language {a : Muller State Symbol} {xs : ωSequence Symbol} :
+    xs ∈ language a ↔ (a.run xs).infOcc ∈ a.accept :=
+  Iff.rfl
+
 end Muller
 
 end DA
diff --git a/Cslib/Computability/Automata/DABuchi.lean b/Cslib/Computability/Automata/DABuchi.lean
new file mode 100644
index 00000000..7d01c720
--- /dev/null
+++ b/Cslib/Computability/Automata/DABuchi.lean
@@ -0,0 +1,30 @@
+/-
+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.DA
+
+/-! # Deterministic Buchi automata.
+-/
+
+open Filter
+
+namespace Cslib.Automata.DA
+
+open scoped FinAcc Buchi
+
+variable {State : Type _} {Symbol : Type _}
+
+open Acceptor ωAcceptor in
+/-- The ω-language accepted by a deterministic Buchi automaton is the ω-limit
+of the language accepted by the same automaton.
+-/
+@[scoped grind =]
+theorem buchi_eq_finAcc_omegaLim {da : DA State Symbol} {acc : Set State} :
+    language (Buchi.mk da acc) = (language (FinAcc.mk da acc))↗ω := by
+  ext xs
+  simp
+
+end Cslib.Automata.DA
diff --git a/Cslib/Computability/Automata/DAToNA.lean b/Cslib/Computability/Automata/DAToNA.lean
index 128f5f37..566ac264 100644
--- a/Cslib/Computability/Automata/DAToNA.lean
+++ b/Cslib/Computability/Automata/DAToNA.lean
@@ -26,6 +26,16 @@ def toNA (a : DA State Symbol) : NA State Symbol :=
 instance : Coe (DA State Symbol) (NA State Symbol) where
   coe := toNA
 
+open scoped FLTS NA in
+@[simp, scoped grind =]
+theorem toNA_run {a : DA State Symbol} {xs : ωSequence Symbol} {ss : ωSequence State} :
+    a.toNA.Run xs ss ↔ a.run xs = ss := by
+  constructor
+  · rintro _
+    ext n
+    induction n <;> grind
+  · grind
+
 namespace FinAcc
 
 /-- `DA.FinAcc` is a special case of `NA.FinAcc`. -/
@@ -35,8 +45,8 @@ def toNAFinAcc (a : DA.FinAcc State Symbol) : NA.FinAcc State Symbol :=
 
 open Acceptor in
 open scoped FLTS NA.FinAcc in
-/-- The `NA` constructed from a `DA` has the same language. -/
-@[scoped grind _=_]
+/-- The `NA.FinAcc` constructed from a `DA.FinAcc` has the same language. -/
+@[simp, scoped grind _=_]
 theorem toNAFinAcc_language_eq {a : DA.FinAcc State Symbol} :
     language a.toNAFinAcc = language a := by
   ext xs
@@ -48,6 +58,27 @@ theorem toNAFinAcc_language_eq {a : DA.FinAcc State Symbol} :
 
 end FinAcc
 
+namespace Buchi
+
+/-- `DA.Buchi` is a special case of `NA.Buchi`. -/
+@[scoped grind =]
+def toNABuchi (a : DA.Buchi State Symbol) : NA.Buchi State Symbol :=
+  { a.toNA with accept := a.accept }
+
+open ωAcceptor in
+open scoped NA.Buchi in
+/-- The `NA.Buchi` constructed from a `DA.Buchi` has the same ω-language. -/
+@[simp, scoped grind _=_]
+theorem toNABuchi_language_eq {a : DA.Buchi State Symbol} :
+    language a.toNABuchi = language a := by
+  ext xs ; constructor
+  · grind
+  · intro _
+    use (a.run xs)
+    grind
+
+end Buchi
+
 end NA
 
 end Cslib.Automata.DA
diff --git a/Cslib/Computability/Automata/NA.lean b/Cslib/Computability/Automata/NA.lean
index 6c6fbfa5..e528a1e0 100644
--- a/Cslib/Computability/Automata/NA.lean
+++ b/Cslib/Computability/Automata/NA.lean
@@ -4,9 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Fabrizio Montesi, Ching-Tsun Chou
 -/
 
-import Cslib.Computability.Languages.OmegaLanguage
+import Cslib.Foundations.Data.OmegaSequence.InfOcc
 import Cslib.Foundations.Semantics.LTS.Basic
-import Cslib.Foundations.Semantics.LTS.FLTS
 import Cslib.Computability.Automata.Acceptor
 import Cslib.Computability.Automata.OmegaAcceptor
 
@@ -40,6 +39,11 @@ namespace NA
 
 variable {State : Type _} {Symbol : Type _}
 
+/-- Infinite run. -/
+@[scoped grind =]
+def Run (na : NA State Symbol) (xs : ωSequence Symbol) (ss : ωSequence State) :=
+  ss 0 ∈ na.start ∧ ∀ n, na.Tr (ss n) (xs n) (ss (n + 1))
+
 /-- A nondeterministic automaton that accepts finite strings (lists of symbols). -/
 structure FinAcc (State Symbol : Type*) extends NA State Symbol where
   /-- The accept states. -/
@@ -56,12 +60,13 @@ instance : Acceptor (FinAcc State Symbol) Symbol where
   Accepts (a : FinAcc State Symbol) (xs : List Symbol) :=
     ∃ s ∈ a.start, ∃ s' ∈ a.accept, a.MTr s xs s'
 
-end FinAcc
+open Acceptor in
+@[simp, scoped grind =]
+theorem mem_language {a : FinAcc State Symbol} {xs : List Symbol} :
+    xs ∈ language a ↔ ∃ s ∈ a.start, ∃ s' ∈ a.accept, a.MTr s xs s' :=
+  Iff.rfl
 
-/-- Infinite run. -/
-@[scoped grind =]
-def Run (na : NA State Symbol) (xs : ωSequence Symbol) (ss : ωSequence State) :=
-  ss 0 ∈ na.start ∧ ∀ n, na.Tr (ss n) (xs n) (ss (n + 1))
+end FinAcc
 
 /-- Nondeterministic Buchi automaton. -/
 structure Buchi (State Symbol : Type*) extends NA State Symbol where
@@ -72,7 +77,13 @@ namespace Buchi
 @[scoped grind =]
 instance : ωAcceptor (Buchi State Symbol) Symbol where
   Accepts (a : Buchi State Symbol) (xs : ωSequence Symbol) :=
-    ∃ ss, ∃ᶠ k in atTop, a.Run xs ss ∧ ss k ∈ a.accept
+    ∃ ss, a.Run xs ss ∧ ∃ᶠ k in atTop, ss k ∈ a.accept
+
+open ωAcceptor in
+@[simp, scoped grind =]
+theorem mem_language {a : Buchi State Symbol} {xs : ωSequence Symbol} :
+    xs ∈ language a ↔ ∃ ss, a.Run xs ss ∧ ∃ᶠ k in atTop, ss k ∈ a.accept :=
+  Iff.rfl
 
 end Buchi
 
@@ -87,6 +98,12 @@ instance : ωAcceptor (Muller State Symbol) Symbol where
   Accepts (a : Muller State Symbol) (xs : ωSequence Symbol) :=
     ∃ ss, a.Run xs ss ∧ ss.infOcc ∈ a.accept
 
+open ωAcceptor in
+@[simp, scoped grind =]
+theorem mem_language {a : Muller State Symbol} {xs : ωSequence Symbol} :
+    xs ∈ language a ↔ ∃ ss, a.Run xs ss ∧ ss.infOcc ∈ a.accept :=
+  Iff.rfl
+
 end Muller
 
 end NA
diff --git a/Cslib/Computability/Languages/ExampleEventuallyZero.lean b/Cslib/Computability/Languages/ExampleEventuallyZero.lean
new file mode 100644
index 00000000..74da00ed
--- /dev/null
+++ b/Cslib/Computability/Languages/ExampleEventuallyZero.lean
@@ -0,0 +1,115 @@
+/-
+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
+
+/-!
+# An ω-regular language that is not accepted by any deterministic Buchi automaton
+
+This example is adapted from Example 4.2 of [Thomas1990].
+
+## References
+* [W. Thomas, "Automata on infinite objects"][Thomas1990]
+-/
+
+open Set Function Filter Cslib.ωSequence Cslib.Automata ωAcceptor
+open scoped Computability
+
+namespace Cslib.ωLanguage.Example
+
+/-- A sequence `xs` is in `eventually_zero` iff `xs k = 0` for all large `k`. -/
+@[scoped grind =]
+def eventually_zero : ωLanguage (Fin 2) :=
+  { xs : ωSequence (Fin 2) | ∀ᶠ k in atTop, xs k = 0 }
+
+/-- `eventually_zero` is accepted by a 2-state nondeterministic Buchi automaton. -/
+@[scoped grind =]
+def eventually_zero_na : NA.Buchi (Fin 2) (Fin 2) where
+  -- Once state 1 is reached, only symbol 0 is accepted and the next state is still 1
+  Tr s x s' := s = 1 → x = 0 ∧ s' = 1
+  start := {0}
+  accept := {1}
+
+theorem eventually_zero_accepted_by_na_buchi :
+    language eventually_zero_na = eventually_zero := by
+  ext xs; unfold eventually_zero_na; constructor
+  · rintro ⟨ss, h_run, h_acc⟩
+    obtain ⟨m, h_m⟩ := Frequently.exists h_acc
+    apply eventually_atTop.mpr
+    use m ; intro n h_n
+    obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le h_n
+    suffices h1 : xs (m + k) = 0 ∧ ss (m + k) = 1 by grind
+    have := h_run.2 m
+    induction k <;> grind [NA.Run]
+  · intro h
+    obtain ⟨m, h_m⟩ := eventually_atTop.mp h
+    let ss : ωSequence (Fin 2) := fun k ↦ if k ≤ m then (0 : Fin 2) else 1
+    refine ⟨ss, ?_, ?_⟩
+    · grind [NA.Run]
+    · apply Eventually.frequently
+      apply eventually_atTop.mpr
+      use (m + 1)
+      grind
+
+private lemma extend_by_zero (u : List (Fin 2)) :
+    u ++ω const 0 ∈ eventually_zero := by
+  apply eventually_atTop.mpr
+  use u.length
+  grind [get_append_right']
+
+private lemma extend_by_one (u : List (Fin 2)) :
+    ∃ v, 1 ∈ v ∧ u ++ v ++ω const 0 ∈ eventually_zero := by
+  use [1]
+  grind [extend_by_zero]
+
+private lemma extend_by_hyp {l : Language (Fin 2)} (h : l↗ω = eventually_zero)
+    (u : List (Fin 2)) : ∃ v, 1 ∈ v ∧ u ++ v ∈ l := by
+  obtain ⟨v, _, h_pfx⟩ := extend_by_one u
+  rw [← h] at h_pfx
+  have := frequently_atTop.mp h_pfx (u ++ v).length
+  grind [extract_append_zero_right]
+
+private noncomputable def oneSegs {l : Language (Fin 2)} (h : l↗ω = eventually_zero) (n : ℕ) :=
+  Classical.choose <| extend_by_hyp h (List.ofFn (fun k : Fin n ↦ oneSegs h k)).flatten
+
+private lemma oneSegs_lemma {l : Language (Fin 2)} (h : l↗ω = eventually_zero) (n : ℕ) :
+    1 ∈ oneSegs h n ∧ (List.ofFn (fun k : Fin (n + 1) ↦ oneSegs h k)).flatten ∈ l := by
+  let P u v := 1 ∈ v ∧ u ++ v ∈ l
+  have : P ((List.ofFn (fun k : Fin n ↦ oneSegs h k)).flatten) (oneSegs h n) := by
+    unfold oneSegs
+    exact Classical.choose_spec <| extend_by_hyp h (List.ofFn (fun k : Fin n ↦ oneSegs h k)).flatten
+  obtain ⟨h1, h2⟩ := this
+  use h1
+  rw [List.ofFn_succ_last]
+  simpa
+
+theorem eventually_zero_not_omegaLim :
+    ¬ ∃ l : Language (Fin 2), l↗ω = eventually_zero := by
+  rintro ⟨l, h⟩
+  let ls := ωSequence.mk (oneSegs h)
+  have h_segs := oneSegs_lemma h
+  have h_pos : ∀ k, (ls k).length > 0 := by grind
+  have h_ev : ls.flatten ∈ eventually_zero := by
+    rw [← h, mem_omegaLim, frequently_iff_strictMono]
+    use (fun k ↦ ls.cumLen (k + 1))
+    constructor
+    · intro j k h_jk
+      have := cumLen_strictMono h_pos (show j + 1 < k + 1 by omega)
+      grind
+    · intro n
+      suffices _ : ls.take (n + 1) = List.ofFn (fun k : Fin (n + 1) ↦ oneSegs h k) by
+        grind [extract_eq_take, ← flatten_take]
+      simp [← extract_eq_take, extract_eq_ofFn, ls]
+  obtain ⟨m, _⟩ := eventually_atTop.mp h_ev
+  have h_inf : ∃ᶠ n in atTop, n ∈ range ls.cumLen := by
+    apply frequently_iff_strictMono.mpr
+    have := cumLen_strictMono h_pos
+    grind
+  obtain ⟨n, h_n, k, rfl⟩ := frequently_atTop.mp h_inf m
+  have h_k : 1 ∈ ls k := by grind
+  grind [List.mem_iff_getElem, = _ extract_flatten]
+
+end Cslib.ωLanguage.Example
diff --git a/Cslib/Computability/Languages/OmegaLanguage.lean b/Cslib/Computability/Languages/OmegaLanguage.lean
index dc646fd7..65c19a96 100644
--- a/Cslib/Computability/Languages/OmegaLanguage.lean
+++ b/Cslib/Computability/Languages/OmegaLanguage.lean
@@ -210,6 +210,11 @@ theorem flatten_mem_omegaPow [Inhabited α] {xs : ωSequence (List α)}
     (h_xs : ∀ k, xs k ∈ l - 1) : xs.flatten ∈ l^ω :=
   ⟨xs, rfl, h_xs⟩
 
+@[simp, scoped grind =]
+theorem mem_omegaLim :
+    s ∈ l↗ω ↔ ∃ᶠ m in atTop, s.extract 0 m ∈ l :=
+  Iff.rfl
+
 theorem mul_hmul : (l * m) * p = l * (m * p) :=
   image2_assoc append_append_ωSequence
 
@@ -377,6 +382,10 @@ theorem kstar_hmul_omegaPow_eq_omegaPow [Inhabited α] (l : Language α) : l∗
     _ = (l∗)^ω := by rw [hmul_omegaPow_eq_omegaPow]
     _ = _ := by simp
 
+@[simp]
+theorem omegaLim_zero : (0 : Language α)↗ω = ⊥ := by
+  ext; simp
+
 @[simp, scoped grind =]
 theorem map_id (p : ωLanguage α) : map id p = p :=
   by simp [map]
diff --git a/Cslib/Computability/Languages/OmegaRegularLanguage.lean b/Cslib/Computability/Languages/OmegaRegularLanguage.lean
index 58493c3f..2d43bed9 100644
--- a/Cslib/Computability/Languages/OmegaRegularLanguage.lean
+++ b/Cslib/Computability/Languages/OmegaRegularLanguage.lean
@@ -4,9 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Ching-Tsun Chou
 -/
 
-import Cslib.Computability.Automata.DA
-import Cslib.Computability.Automata.NA
-import Mathlib.Tactic
+import Cslib.Computability.Automata.DABuchi
+import Cslib.Computability.Languages.ExampleEventuallyZero
+import Cslib.Computability.Languages.RegularLanguage
 
 /-!
 # ω-Regular languages
@@ -14,26 +14,44 @@ import Mathlib.Tactic
 This file defines ω-regular languages and proves some properties of them.
 -/
 
-open Set Function
+open Set Function Filter Cslib.ωSequence Cslib.Automata ωAcceptor
 open scoped Computability
-open Cslib.Automata
 
 namespace Cslib.ωLanguage
 
 variable {Symbol : Type*}
 
-/-- An ω-regular language is one that is accepted by a finite-state Buchi automaton. -/
+/-- An ω-language is ω-regular iff it is accepted by a
+finite-state nondeterministic Buchi automaton. -/
 def IsRegular (p : ωLanguage Symbol) :=
-  ∃ State : Type, ∃ _ : Finite State, ∃ na : NA.Buchi State Symbol, ωAcceptor.language na = p
-
-/-- There is an ω-regular language which is not accepted by any deterministic Buchi automaton. -/
-proof_wanted IsRegular.not_det_buchi :
-  ∃ p : ωLanguage Symbol, p.IsRegular ∧
-    ¬ ∃ State : Type, ∃ _ : Finite State, ∃ da : DA.Buchi State Symbol, ωAcceptor.language da = p
+  ∃ State : Type, ∃ _ : Finite State, ∃ na : NA.Buchi State Symbol, language na = p
+
+/-- The ω-language accepted by a finite-state deterministic Buchi automaton is ω-regular. -/
+theorem IsRegular.of_da_buchi {State : Type} [Finite State] (da : DA.Buchi State Symbol) :
+    (language da).IsRegular :=
+  ⟨State, inferInstance, da.toNABuchi, DA.Buchi.toNABuchi_language_eq⟩
+
+/-- There is an ω-regular language that is not accepted by any deterministic Buchi automaton,
+where the automaton is not even required to be finite-state. -/
+theorem IsRegular.not_da_buchi :
+  ∃ Symbol : Type, ∃ p : ωLanguage Symbol, p.IsRegular ∧
+    ¬ ∃ State : Type, ∃ da : DA.Buchi State Symbol, language da = p := by
+  refine ⟨Fin 2, Example.eventually_zero, ?_, ?_⟩
+  · use Fin 2, inferInstance, Example.eventually_zero_na,
+      Example.eventually_zero_accepted_by_na_buchi
+  · rintro ⟨State, ⟨da, acc⟩, _⟩
+    have := Example.eventually_zero_not_omegaLim
+    grind [DA.buchi_eq_finAcc_omegaLim]
+
+/-- The ω-limit of a regular language is ω-regular. -/
+theorem IsRegular.regular_omegaLim {l : Language Symbol}
+    (h : l.IsRegular) : (l↗ω).IsRegular := by
+  obtain ⟨State, _, ⟨da, acc⟩, rfl⟩ := Language.IsRegular.iff_cslib_dfa.mp h
+  grind [IsRegular.of_da_buchi, =_ DA.buchi_eq_finAcc_omegaLim]
 
 /-- McNaughton's Theorem. -/
-proof_wanted IsRegular.iff_muller_lang {p : ωLanguage Symbol} :
+proof_wanted IsRegular.iff_da_muller {p : ωLanguage Symbol} :
     p.IsRegular ↔
-    ∃ State : Type, ∃ _ : Finite State, ∃ da : DA.Muller State Symbol, ωAcceptor.language da = p
+    ∃ State : Type, ∃ _ : Finite State, ∃ da : DA.Muller State Symbol, language da = p
 
 end Cslib.ωLanguage
diff --git a/Cslib/Foundations/Data/OmegaSequence/Defs.lean b/Cslib/Foundations/Data/OmegaSequence/Defs.lean
index 7cc81730..9ac642d2 100644
--- a/Cslib/Foundations/Data/OmegaSequence/Defs.lean
+++ b/Cslib/Foundations/Data/OmegaSequence/Defs.lean
@@ -4,10 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Ching-Tsun Chou, Fabrizio Montesi
 -/
 import Cslib.Init
-import Mathlib.Data.Nat.Notation
 import Mathlib.Data.FunLike.Basic
 import Mathlib.Logic.Function.Iterate
-import Mathlib.Order.Filter.AtTopBot.Defs
 
 /-!
 # Definition of `ωSequence` and functions on infinite sequences
@@ -24,8 +22,6 @@ Most code below is adapted from Mathlib.Data.Stream.Defs.
 
 namespace Cslib
 
-open Filter
-
 universe u v w
 variable {α : Type u} {β : Type v} {δ : Type w}
 
@@ -88,10 +84,6 @@ def zip (f : α → β → δ) (s₁ : ωSequence α) (s₂ : ωSequence β) : 
 /-- Iterates of a function as an ω-sequence. -/
 def iterate (f : α → α) (a : α) : ωSequence α := fun n => f^[n] a
 
-/-- The set of elements that appear infinitely often in an ω-sequence. -/
-def infOcc (xs : ωSequence α) : Set α :=
-  { x | ∃ᶠ k in atTop, xs k = x }
-
 end ωSequence
 
 end Cslib
diff --git a/Cslib/Foundations/Data/OmegaSequence/InfOcc.lean b/Cslib/Foundations/Data/OmegaSequence/InfOcc.lean
new file mode 100644
index 00000000..c75e16d8
--- /dev/null
+++ b/Cslib/Foundations/Data/OmegaSequence/InfOcc.lean
@@ -0,0 +1,39 @@
+/-
+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.Foundations.Data.OmegaSequence.Defs
+
+/-!
+# Infinite occurrences
+-/
+
+namespace Cslib
+
+open Function Set Filter
+
+namespace ωSequence
+
+universe u v w
+variable {α : Type u} {β : Type v} {δ : Type w}
+
+/-- The set of elements that appear infinitely often in an ω-sequence. -/
+def infOcc (xs : ωSequence α) : Set α :=
+  { x | ∃ᶠ k in atTop, xs k = x }
+
+/-- An alternative characterization of "infinitely often". -/
+theorem frequently_iff_strictMono {p : ℕ → Prop} :
+    (∃ᶠ n in atTop, p n) ↔ ∃ f : ℕ → ℕ, StrictMono f ∧ ∀ m, p (f m) := by
+  constructor
+  · intro h
+    exact extraction_of_frequently_atTop h
+  · rintro ⟨f, h_mono, h_p⟩
+    rw [Nat.frequently_atTop_iff_infinite]
+    have h_range : range f ⊆ {n | p n} := by grind
+    grind [Infinite.mono, infinite_range_of_injective, StrictMono.injective]
+
+end ωSequence
+
+end Cslib
diff --git a/Cslib/Foundations/Data/OmegaSequence/Init.lean b/Cslib/Foundations/Data/OmegaSequence/Init.lean
index 5ec3e327..8c221ac3 100644
--- a/Cslib/Foundations/Data/OmegaSequence/Init.lean
+++ b/Cslib/Foundations/Data/OmegaSequence/Init.lean
@@ -40,6 +40,10 @@ alias cons_head_tail := ωSequence.eta
 protected theorem ext {s₁ s₂ : ωSequence α} : (∀ n, s₁ n = s₂ n) → s₁ = s₂ := by
   apply DFunLike.ext
 
+@[simp, scoped grind =]
+theorem get_fun (f : ℕ → α) (n : ℕ) : ωSequence.mk f n = f n :=
+  rfl
+
 @[simp, scoped grind =]
 theorem get_zero_cons (a : α) (s : ωSequence α) : (a ::ω s) 0 = a :=
   rfl
diff --git a/docs/docs/references.bib b/docs/docs/references.bib
index 31b2d5f1..e18c0342 100644
--- a/docs/docs/references.bib
+++ b/docs/docs/references.bib
@@ -157,3 +157,13 @@ @Book{            Sangiorgi2011
   date          = {2011},
   doi           = {10.1017/CBO9780511777110}
 }
+
+@incollection{ Thomas1990,
+  author       = {Wolfgang Thomas},
+  editor       = {Jan van Leeuwen},
+  title        = {Automata on Infinite Objects},
+  booktitle    = {Handbook of Theoretical Computer Science, Volume {B:} Formal Models and Semantics},
+  pages        = {133--191},
+  publisher    = {Elsevier and {MIT} Press},
+  year         = {1990}
+}