From 7b42cc06dd9a9db2aa340b40f06af19d9b5c1907 Mon Sep 17 00:00:00 2001
From: Ching-Tsun Chou <chingtsun.chou@gmail.com>
Date: Sun, 9 Nov 2025 15:21:53 -0800
Subject: [PATCH 1/5] feat: prove basic properties of deterministic Buchi
 automata

---
 Cslib.lean                                    |  1 +
 Cslib/Computability/Automata/DA.lean          | 58 +++++++++++++++----
 Cslib/Computability/Automata/DABuchi.lean     | 31 ++++++++++
 Cslib/Computability/Automata/DAToNA.lean      | 35 ++++++++++-
 Cslib/Computability/Automata/NA.lean          | 30 ++++++++--
 .../Languages/OmegaRegularLanguage.lean       | 35 ++++++++---
 6 files changed, 162 insertions(+), 28 deletions(-)
 create mode 100644 Cslib/Computability/Automata/DABuchi.lean

diff --git a/Cslib.lean b/Cslib.lean
index 9cec8a39..dbfef1be 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
diff --git a/Cslib/Computability/Automata/DA.lean b/Cslib/Computability/Automata/DA.lean
index 441ab370..5f251e71 100644
--- a/Cslib/Computability/Automata/DA.lean
+++ b/Cslib/Computability/Automata/DA.lean
@@ -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)
-
-/-- Infinite run. -/
-@[scoped grind =]
-def run (da : DA State Symbol) (xs : ωSequence Symbol) : ωSequence State := da.run' xs
+theorem mem_language {a : FinAcc State Symbol} {xs : List Symbol} :
+    xs ∈ language a ↔ a.mtr a.start xs ∈ a.accept :=
+  Iff.rfl
 
-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..27f95c5c
--- /dev/null
+++ b/Cslib/Computability/Automata/DABuchi.lean
@@ -0,0 +1,31 @@
+/-
+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
+import Cslib.Computability.Automata.NA
+
+/-! # 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 ; constructor <;>
+  { intro h ; apply Frequently.mono h ; 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..6b3f7b74 100644
--- a/Cslib/Computability/Automata/NA.lean
+++ b/Cslib/Computability/Automata/NA.lean
@@ -40,6 +40,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 +61,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 +78,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 +99,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/OmegaRegularLanguage.lean b/Cslib/Computability/Languages/OmegaRegularLanguage.lean
index 58493c3f..205b6abf 100644
--- a/Cslib/Computability/Languages/OmegaRegularLanguage.lean
+++ b/Cslib/Computability/Languages/OmegaRegularLanguage.lean
@@ -6,6 +6,9 @@ Authors: Ching-Tsun Chou
 
 import Cslib.Computability.Automata.DA
 import Cslib.Computability.Automata.NA
+import Cslib.Computability.Automata.DAToNA
+import Cslib.Computability.Automata.DABuchi
+import Cslib.Computability.Languages.RegularLanguage
 import Mathlib.Tactic
 
 /-!
@@ -14,7 +17,7 @@ import Mathlib.Tactic
 This file defines ω-regular languages and proves some properties of them.
 -/
 
-open Set Function
+open Set Function Cslib.Automata.ωAcceptor
 open scoped Computability
 open Cslib.Automata
 
@@ -22,18 +25,32 @@ 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 :
+  ∃ 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 := by
+  use State, inferInstance, da.toNABuchi
+  simp
+
+/-- 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
+  rw [← DA.buchi_eq_finAcc_omegaLim]
+  apply IsRegular.of_da_buchi
+
+/-- There is an ω-regular language that is not accepted by any deterministic Buchi automaton. -/
+proof_wanted IsRegular.not_da_buchi :
   ∃ p : ωLanguage Symbol, p.IsRegular ∧
-    ¬ ∃ State : Type, ∃ _ : Finite State, ∃ da : DA.Buchi State Symbol, ωAcceptor.language da = p
+    ¬ ∃ State : Type, ∃ _ : Finite State, ∃ da : DA.Buchi State Symbol, language da = p
 
 /-- 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

From e03f03ab24159a3ea83e677ea75962d65dbcd066 Mon Sep 17 00:00:00 2001
From: Ching-Tsun Chou <chingtsun.chou@gmail.com>
Date: Tue, 11 Nov 2025 12:19:11 -0800
Subject: [PATCH 2/5] feat: prove the existence of an omega-regular language
 not accepted by any deterministic Buchi automaton

---
 Cslib.lean                                    |   2 +
 Cslib/Computability/Automata/DA.lean          |   4 +-
 Cslib/Computability/Automata/DABuchi.lean     |   1 -
 Cslib/Computability/Automata/NA.lean          |   3 +-
 .../Languages/OmegaLanguage.lean              |   9 ++
 .../Languages/OmegaLanguageExamples.lean      | 133 ++++++++++++++++++
 .../Languages/OmegaRegularLanguage.lean       |  22 ++-
 .../Foundations/Data/OmegaSequence/Defs.lean  |   8 --
 .../Data/OmegaSequence/InfOcc.lean            |  44 ++++++
 .../Foundations/Data/OmegaSequence/Init.lean  |   4 +
 10 files changed, 210 insertions(+), 20 deletions(-)
 create mode 100644 Cslib/Computability/Languages/OmegaLanguageExamples.lean
 create mode 100644 Cslib/Foundations/Data/OmegaSequence/InfOcc.lean

diff --git a/Cslib.lean b/Cslib.lean
index dbfef1be..3aac2f24 100644
--- a/Cslib.lean
+++ b/Cslib.lean
@@ -10,6 +10,7 @@ import Cslib.Computability.Automata.OmegaAcceptor
 import Cslib.Computability.Automata.Prod
 import Cslib.Computability.Languages.Language
 import Cslib.Computability.Languages.OmegaLanguage
+import Cslib.Computability.Languages.OmegaLanguageExamples
 import Cslib.Computability.Languages.OmegaRegularLanguage
 import Cslib.Computability.Languages.RegularLanguage
 import Cslib.Foundations.Control.Monad.Free
@@ -20,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 5f251e71..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
 
diff --git a/Cslib/Computability/Automata/DABuchi.lean b/Cslib/Computability/Automata/DABuchi.lean
index 27f95c5c..8ca57198 100644
--- a/Cslib/Computability/Automata/DABuchi.lean
+++ b/Cslib/Computability/Automata/DABuchi.lean
@@ -5,7 +5,6 @@ Authors: Ching-Tsun Chou
 -/
 
 import Cslib.Computability.Automata.DA
-import Cslib.Computability.Automata.NA
 
 /-! # Deterministic Buchi automata.
 -/
diff --git a/Cslib/Computability/Automata/NA.lean b/Cslib/Computability/Automata/NA.lean
index 6b3f7b74..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
 
diff --git a/Cslib/Computability/Languages/OmegaLanguage.lean b/Cslib/Computability/Languages/OmegaLanguage.lean
index dc646fd7..ea460760 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 xs ; simp
+
 @[simp, scoped grind =]
 theorem map_id (p : ωLanguage α) : map id p = p :=
   by simp [map]
diff --git a/Cslib/Computability/Languages/OmegaLanguageExamples.lean b/Cslib/Computability/Languages/OmegaLanguageExamples.lean
new file mode 100644
index 00000000..01648af7
--- /dev/null
+++ b/Cslib/Computability/Languages/OmegaLanguageExamples.lean
@@ -0,0 +1,133 @@
+/-
+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
+import Cslib.Computability.Automata.NA
+import Cslib.Foundations.Data.OmegaSequence.InfOcc
+import Mathlib.Tactic
+
+/-!
+# ω-Regular languages
+
+This file defines ω-regular languages and proves some properties of them.
+-/
+
+open Set Function Filter Cslib.ωSequence Cslib.Automata ωAcceptor
+open scoped Computability
+
+namespace Cslib.ωLanguage.Example
+
+section EventuallyZero
+
+/-- 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. -/
+theorem eventually_zero_accepted_by_na_buchi :
+    ∃ a : NA.Buchi (Fin 2) (Fin 2), language a = eventually_zero := by
+  let a : NA.Buchi (Fin 2) (Fin 2) := {
+    -- 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} }
+  use a ; ext xs ; 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
+    induction k
+    case zero =>
+      have := h_run.2 m
+      grind
+    case succ k h_ind =>
+      have := h_run.2 (m + k)
+      have := h_run.2 (m + k + 1)
+      grind
+  · 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, ?_, ?_⟩
+    · simp [a, ss, NA.Run]
+      grind
+    · apply Eventually.frequently
+      apply eventually_atTop.mpr
+      use (m + 1) ; intro k _
+      simp [a, ss, show m < k by omega]
+
+private lemma extend_by_zero (u : List (Fin 2)) :
+    u ++ω const 0 ∈ eventually_zero := by
+  apply eventually_atTop.mpr
+  use u.length
+  intro k h_k
+  rw [get_append_right' h_k]
+  simp
+
+private lemma extend_by_one (u : List (Fin 2)) :
+    ∃ v, 1 ∈ v ∧ u ++ v ++ω const 0 ∈ eventually_zero := by
+  refine ⟨[1], ?_, ?_⟩
+  · simp
+  · apply 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
+  obtain ⟨m, h_m, h_uv⟩ := frequently_atTop.mp h_pfx (u ++ v).length
+  use (v ++ω ωSequence.const 0).extract 0 (m - u.length)
+  rw [extract_append_zero_right (show v.length ≤ m - u.length by grind)]
+  constructor
+  · simp_all
+  · rw [extract_append_zero_right h_m] at h_uv
+    grind
+
+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
+  refine ⟨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
+      rw [extract_eq_take, ← flatten_take h_pos]
+      suffices _ : ls.take (n + 1) = List.ofFn (fun k : Fin (n + 1) ↦ oneSegs h k) by grind
+      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
+  simp only [← extract_flatten h_pos k, List.mem_iff_getElem, length_extract] at h_k
+  grind
+
+end EventuallyZero
+
+end Cslib.ωLanguage.Example
diff --git a/Cslib/Computability/Languages/OmegaRegularLanguage.lean b/Cslib/Computability/Languages/OmegaRegularLanguage.lean
index 205b6abf..bdd5f07e 100644
--- a/Cslib/Computability/Languages/OmegaRegularLanguage.lean
+++ b/Cslib/Computability/Languages/OmegaRegularLanguage.lean
@@ -9,6 +9,7 @@ import Cslib.Computability.Automata.NA
 import Cslib.Computability.Automata.DAToNA
 import Cslib.Computability.Automata.DABuchi
 import Cslib.Computability.Languages.RegularLanguage
+import Cslib.Computability.Languages.OmegaLanguageExamples
 import Mathlib.Tactic
 
 /-!
@@ -17,9 +18,8 @@ import Mathlib.Tactic
 This file defines ω-regular languages and proves some properties of them.
 -/
 
-open Set Function Cslib.Automata.ωAcceptor
+open Set Function Filter Cslib.ωSequence Cslib.Automata ωAcceptor
 open scoped Computability
-open Cslib.Automata
 
 namespace Cslib.ωLanguage
 
@@ -36,6 +36,19 @@ theorem IsRegular.of_da_buchi {State : Type} [Finite State] (da : DA.Buchi State
   use State, inferInstance, da.toNABuchi
   simp
 
+/-- 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, ?_, ?_⟩
+  · obtain ⟨a, _⟩ := Example.eventually_zero_accepted_by_na_buchi
+    use Fin 2, inferInstance, a
+  · rintro ⟨State, ⟨da, acc⟩, h⟩
+    simp [DA.buchi_eq_finAcc_omegaLim] at h
+    have := Example.eventually_zero_not_omegaLim
+    grind
+
 /-- The ω-limit of a regular language is ω-regular. -/
 theorem IsRegular.regular_omegaLim {l : Language Symbol}
     (h : l.IsRegular) : (l↗ω).IsRegular := by
@@ -43,11 +56,6 @@ theorem IsRegular.regular_omegaLim {l : Language Symbol}
   rw [← DA.buchi_eq_finAcc_omegaLim]
   apply IsRegular.of_da_buchi
 
-/-- There is an ω-regular language that is not accepted by any deterministic Buchi automaton. -/
-proof_wanted IsRegular.not_da_buchi :
-  ∃ p : ωLanguage Symbol, p.IsRegular ∧
-    ¬ ∃ State : Type, ∃ _ : Finite State, ∃ da : DA.Buchi State Symbol, language da = p
-
 /-- McNaughton's Theorem. -/
 proof_wanted IsRegular.iff_da_muller {p : ωLanguage Symbol} :
     p.IsRegular ↔
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..cfd7ee77
--- /dev/null
+++ b/Cslib/Foundations/Data/OmegaSequence/InfOcc.lean
@@ -0,0 +1,44 @@
+/-
+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
+import Mathlib.Order.Filter.AtTopBot.Defs
+import Mathlib.Tactic
+
+/-!
+# 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
+      rintro k ⟨m, rfl⟩
+      simp_all only [mem_setOf_eq]
+    apply Infinite.mono h_range
+    exact infinite_range_of_injective h_mono.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

From 8e1512c406820bd12425bb495e9030c23a6708b3 Mon Sep 17 00:00:00 2001
From: Ching-Tsun Chou <chingtsun.chou@gmail.com>
Date: Sun, 16 Nov 2025 15:04:57 -0800
Subject: [PATCH 3/5] Incorporate Chris Henson's comments

---
 Cslib/Computability/Automata/DABuchi.lean     |  4 +-
 .../Languages/OmegaLanguage.lean              |  2 +-
 .../Languages/OmegaLanguageExamples.lean      | 63 +++++++------------
 .../Languages/OmegaRegularLanguage.lean       | 23 +++----
 .../Data/OmegaSequence/InfOcc.lean            |  9 +--
 5 files changed, 36 insertions(+), 65 deletions(-)

diff --git a/Cslib/Computability/Automata/DABuchi.lean b/Cslib/Computability/Automata/DABuchi.lean
index 8ca57198..7d01c720 100644
--- a/Cslib/Computability/Automata/DABuchi.lean
+++ b/Cslib/Computability/Automata/DABuchi.lean
@@ -24,7 +24,7 @@ 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 ; constructor <;>
-  { intro h ; apply Frequently.mono h ; simp }
+  ext xs
+  simp
 
 end Cslib.Automata.DA
diff --git a/Cslib/Computability/Languages/OmegaLanguage.lean b/Cslib/Computability/Languages/OmegaLanguage.lean
index ea460760..65c19a96 100644
--- a/Cslib/Computability/Languages/OmegaLanguage.lean
+++ b/Cslib/Computability/Languages/OmegaLanguage.lean
@@ -384,7 +384,7 @@ theorem kstar_hmul_omegaPow_eq_omegaPow [Inhabited α] (l : Language α) : l∗
 
 @[simp]
 theorem omegaLim_zero : (0 : Language α)↗ω = ⊥ := by
-  ext xs ; simp
+  ext; simp
 
 @[simp, scoped grind =]
 theorem map_id (p : ωLanguage α) : map id p = p :=
diff --git a/Cslib/Computability/Languages/OmegaLanguageExamples.lean b/Cslib/Computability/Languages/OmegaLanguageExamples.lean
index 01648af7..6966fd41 100644
--- a/Cslib/Computability/Languages/OmegaLanguageExamples.lean
+++ b/Cslib/Computability/Languages/OmegaLanguageExamples.lean
@@ -4,10 +4,7 @@ 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 Cslib.Foundations.Data.OmegaSequence.InfOcc
-import Mathlib.Tactic
 
 /-!
 # ω-Regular languages
@@ -28,64 +25,51 @@ 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 :
-    ∃ a : NA.Buchi (Fin 2) (Fin 2), language a = eventually_zero := by
-  let a : NA.Buchi (Fin 2) (Fin 2) := {
-    -- 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} }
-  use a ; ext xs ; constructor
+    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
-    induction k
-    case zero =>
-      have := h_run.2 m
-      grind
-    case succ k h_ind =>
-      have := h_run.2 (m + k)
-      have := h_run.2 (m + k + 1)
-      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, ?_, ?_⟩
-    · simp [a, ss, NA.Run]
-      grind
+    · grind [NA.Run]
     · apply Eventually.frequently
       apply eventually_atTop.mpr
-      use (m + 1) ; intro k _
-      simp [a, ss, show m < k by omega]
+      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
-  intro k h_k
-  rw [get_append_right' h_k]
-  simp
+  grind [get_append_right']
 
 private lemma extend_by_one (u : List (Fin 2)) :
     ∃ v, 1 ∈ v ∧ u ++ v ++ω const 0 ∈ eventually_zero := by
-  refine ⟨[1], ?_, ?_⟩
-  · simp
-  · apply extend_by_zero
+  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
-  obtain ⟨m, h_m, h_uv⟩ := frequently_atTop.mp h_pfx (u ++ v).length
-  use (v ++ω ωSequence.const 0).extract 0 (m - u.length)
-  rw [extract_append_zero_right (show v.length ≤ m - u.length by grind)]
-  constructor
-  · simp_all
-  · rw [extract_append_zero_right h_m] at h_uv
-    grind
+  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
@@ -97,7 +81,7 @@ private lemma oneSegs_lemma {l : Language (Fin 2)} (h : l↗ω = eventually_zero
     unfold oneSegs
     exact Classical.choose_spec <| extend_by_hyp h (List.ofFn (fun k : Fin n ↦ oneSegs h k)).flatten
   obtain ⟨h1, h2⟩ := this
-  refine ⟨h1, ?_⟩
+  use h1
   rw [List.ofFn_succ_last]
   simpa
 
@@ -115,8 +99,8 @@ theorem eventually_zero_not_omegaLim :
       have := cumLen_strictMono h_pos (show j + 1 < k + 1 by omega)
       grind
     · intro n
-      rw [extract_eq_take, ← flatten_take h_pos]
-      suffices _ : ls.take (n + 1) = List.ofFn (fun k : Fin (n + 1) ↦ oneSegs h k) by grind
+      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
@@ -125,8 +109,7 @@ theorem eventually_zero_not_omegaLim :
     grind
   obtain ⟨n, h_n, k, rfl⟩ := frequently_atTop.mp h_inf m
   have h_k : 1 ∈ ls k := by grind
-  simp only [← extract_flatten h_pos k, List.mem_iff_getElem, length_extract] at h_k
-  grind
+  grind [List.mem_iff_getElem, = _ extract_flatten]
 
 end EventuallyZero
 
diff --git a/Cslib/Computability/Languages/OmegaRegularLanguage.lean b/Cslib/Computability/Languages/OmegaRegularLanguage.lean
index bdd5f07e..bb198ea2 100644
--- a/Cslib/Computability/Languages/OmegaRegularLanguage.lean
+++ b/Cslib/Computability/Languages/OmegaRegularLanguage.lean
@@ -4,13 +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 Cslib.Computability.Automata.DAToNA
 import Cslib.Computability.Automata.DABuchi
-import Cslib.Computability.Languages.RegularLanguage
 import Cslib.Computability.Languages.OmegaLanguageExamples
-import Mathlib.Tactic
+import Cslib.Computability.Languages.RegularLanguage
 
 /-!
 # ω-Regular languages
@@ -32,9 +28,8 @@ def IsRegular (p : ωLanguage Symbol) :=
 
 /-- 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 := by
-  use State, inferInstance, da.toNABuchi
-  simp
+    (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. -/
@@ -42,19 +37,17 @@ 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, ?_, ?_⟩
-  · obtain ⟨a, _⟩ := Example.eventually_zero_accepted_by_na_buchi
-    use Fin 2, inferInstance, a
-  · rintro ⟨State, ⟨da, acc⟩, h⟩
-    simp [DA.buchi_eq_finAcc_omegaLim] at h
+  · 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
+    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
-  rw [← DA.buchi_eq_finAcc_omegaLim]
-  apply IsRegular.of_da_buchi
+  grind [IsRegular.of_da_buchi, =_ DA.buchi_eq_finAcc_omegaLim]
 
 /-- McNaughton's Theorem. -/
 proof_wanted IsRegular.iff_da_muller {p : ωLanguage Symbol} :
diff --git a/Cslib/Foundations/Data/OmegaSequence/InfOcc.lean b/Cslib/Foundations/Data/OmegaSequence/InfOcc.lean
index cfd7ee77..c75e16d8 100644
--- a/Cslib/Foundations/Data/OmegaSequence/InfOcc.lean
+++ b/Cslib/Foundations/Data/OmegaSequence/InfOcc.lean
@@ -5,8 +5,6 @@ Authors: Ching-Tsun Chou
 -/
 
 import Cslib.Foundations.Data.OmegaSequence.Defs
-import Mathlib.Order.Filter.AtTopBot.Defs
-import Mathlib.Tactic
 
 /-!
 # Infinite occurrences
@@ -33,11 +31,8 @@ theorem frequently_iff_strictMono {p : ℕ → Prop} :
     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
-      rintro k ⟨m, rfl⟩
-      simp_all only [mem_setOf_eq]
-    apply Infinite.mono h_range
-    exact infinite_range_of_injective h_mono.injective
+    have h_range : range f ⊆ {n | p n} := by grind
+    grind [Infinite.mono, infinite_range_of_injective, StrictMono.injective]
 
 end ωSequence
 

From e54885fdca1e344ec6d79e18970a44651df54d42 Mon Sep 17 00:00:00 2001
From: Ching-Tsun Chou <chingtsun.chou@gmail.com>
Date: Sun, 16 Nov 2025 15:13:19 -0800
Subject: [PATCH 4/5] Rename OmegaLanguageExamples.lean to
 ExampleEventuallyZero.lean

---
 Cslib.lean                                                    | 2 +-
 ...{OmegaLanguageExamples.lean => ExampleEventuallyZero.lean} | 4 ----
 Cslib/Computability/Languages/OmegaRegularLanguage.lean       | 2 +-
 3 files changed, 2 insertions(+), 6 deletions(-)
 rename Cslib/Computability/Languages/{OmegaLanguageExamples.lean => ExampleEventuallyZero.lean} (98%)

diff --git a/Cslib.lean b/Cslib.lean
index 3aac2f24..eb001240 100644
--- a/Cslib.lean
+++ b/Cslib.lean
@@ -8,9 +8,9 @@ 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.OmegaLanguageExamples
 import Cslib.Computability.Languages.OmegaRegularLanguage
 import Cslib.Computability.Languages.RegularLanguage
 import Cslib.Foundations.Control.Monad.Free
diff --git a/Cslib/Computability/Languages/OmegaLanguageExamples.lean b/Cslib/Computability/Languages/ExampleEventuallyZero.lean
similarity index 98%
rename from Cslib/Computability/Languages/OmegaLanguageExamples.lean
rename to Cslib/Computability/Languages/ExampleEventuallyZero.lean
index 6966fd41..201536a4 100644
--- a/Cslib/Computability/Languages/OmegaLanguageExamples.lean
+++ b/Cslib/Computability/Languages/ExampleEventuallyZero.lean
@@ -17,8 +17,6 @@ open scoped Computability
 
 namespace Cslib.ωLanguage.Example
 
-section EventuallyZero
-
 /-- A sequence `xs` is in `eventually_zero` iff `xs k = 0` for all large `k`. -/
 @[scoped grind =]
 def eventually_zero : ωLanguage (Fin 2) :=
@@ -111,6 +109,4 @@ theorem eventually_zero_not_omegaLim :
   have h_k : 1 ∈ ls k := by grind
   grind [List.mem_iff_getElem, = _ extract_flatten]
 
-end EventuallyZero
-
 end Cslib.ωLanguage.Example
diff --git a/Cslib/Computability/Languages/OmegaRegularLanguage.lean b/Cslib/Computability/Languages/OmegaRegularLanguage.lean
index bb198ea2..2d43bed9 100644
--- a/Cslib/Computability/Languages/OmegaRegularLanguage.lean
+++ b/Cslib/Computability/Languages/OmegaRegularLanguage.lean
@@ -5,7 +5,7 @@ Authors: Ching-Tsun Chou
 -/
 
 import Cslib.Computability.Automata.DABuchi
-import Cslib.Computability.Languages.OmegaLanguageExamples
+import Cslib.Computability.Languages.ExampleEventuallyZero
 import Cslib.Computability.Languages.RegularLanguage
 
 /-!

From 53edf0aa4c2c09b3616b553a1dbf75c661311d6b Mon Sep 17 00:00:00 2001
From: Ching-Tsun Chou <chingtsun.chou@gmail.com>
Date: Sun, 16 Nov 2025 22:30:14 -0800
Subject: [PATCH 5/5] Add a reference to the source of
 ExampleEventuallyZero.lean

---
 .../Computability/Languages/ExampleEventuallyZero.lean |  7 +++++--
 docs/docs/references.bib                               | 10 ++++++++++
 2 files changed, 15 insertions(+), 2 deletions(-)

diff --git a/Cslib/Computability/Languages/ExampleEventuallyZero.lean b/Cslib/Computability/Languages/ExampleEventuallyZero.lean
index 201536a4..74da00ed 100644
--- a/Cslib/Computability/Languages/ExampleEventuallyZero.lean
+++ b/Cslib/Computability/Languages/ExampleEventuallyZero.lean
@@ -7,9 +7,12 @@ Authors: Ching-Tsun Chou
 import Cslib.Computability.Automata.NA
 
 /-!
-# ω-Regular languages
+# An ω-regular language that is not accepted by any deterministic Buchi automaton
 
-This file defines ω-regular languages and proves some properties of them.
+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
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}
+}