diff --git a/Cslib.lean b/Cslib.lean
index 8c6984eb..cb410fda 100644
--- a/Cslib.lean
+++ b/Cslib.lean
@@ -6,6 +6,7 @@ public import Cslib.Computability.Automata.Acceptors.Acceptor
 public import Cslib.Computability.Automata.Acceptors.OmegaAcceptor
 public import Cslib.Computability.Automata.DA.Basic
 public import Cslib.Computability.Automata.DA.Buchi
+public import Cslib.Computability.Automata.DA.Congr
 public import Cslib.Computability.Automata.DA.Prod
 public import Cslib.Computability.Automata.DA.ToNA
 public import Cslib.Computability.Automata.EpsilonNA.Basic
@@ -20,6 +21,7 @@ public import Cslib.Computability.Automata.NA.Prod
 public import Cslib.Computability.Automata.NA.Sum
 public import Cslib.Computability.Automata.NA.ToDA
 public import Cslib.Computability.Automata.NA.Total
+public import Cslib.Computability.Languages.Congruences.RightCongruence
 public import Cslib.Computability.Languages.ExampleEventuallyZero
 public import Cslib.Computability.Languages.Language
 public import Cslib.Computability.Languages.OmegaLanguage
diff --git a/Cslib/Computability/Automata/DA/Congr.lean b/Cslib/Computability/Automata/DA/Congr.lean
new file mode 100644
index 00000000..dcaaf7f5
--- /dev/null
+++ b/Cslib/Computability/Automata/DA/Congr.lean
@@ -0,0 +1,68 @@
+/-
+Copyright (c) 2026 Ching-Tsun Chou. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Ching-Tsun Chou
+-/
+
+module
+
+public import Cslib.Computability.Automata.DA.Basic
+public import Cslib.Computability.Languages.Congruences.RightCongruence
+
+@[expose] public section
+
+/-! # Deterministic automaton corresponding to a right congruence. -/
+
+namespace Cslib
+
+open scoped FLTS RightCongruence
+
+variable {Symbol : Type*}
+
+/-- Every right congruence gives rise to a DA whose states are the equivalence classes of
+the right congruence, whose start state is the empty word, and whose transition functiuon
+is concatenation on the right of the input symbol. Note that the transition function is
+well-defined only because `c` is a right congruence. -/
+@[scoped grind =]
+def RightCongruence.toDA (c : RightCongruence Symbol) : Automata.DA c.QuotType Symbol where
+  tr s x := Quotient.lift (fun u ↦ ⟦ u ++ [x] ⟧) (by
+    intro u v h_eq
+    apply Quotient.sound
+    exact right_congr h_eq [x]
+  ) s
+  start := ⟦ [] ⟧
+
+namespace Automata.DA
+
+variable [c : RightCongruence Symbol]
+
+/-- After consuming a finite word `xs`, `c.toDA` reaches the state `⟦ xs ⟧` which is
+the equivalence class of `xs`. -/
+@[simp, scoped grind =]
+theorem congr_mtr_eq {xs : List Symbol} :
+    c.toDA.mtr c.toDA.start xs = ⟦ xs ⟧ := by
+  generalize h_rev : xs.reverse = ys
+  induction ys generalizing xs
+  case nil => grind [List.reverse_eq_nil_iff]
+  case cons y ys h_ind =>
+    obtain ⟨rfl⟩ := List.reverse_eq_cons_iff.mp h_rev
+    specialize h_ind (xs := ys.reverse) (by grind)
+    grind [Quotient.lift_mk]
+
+namespace FinAcc
+
+open Acceptor
+
+/-- The language of `c.toDA` with a single accepting state `s` is exactly
+the equivalence class corresponding to `s`. -/
+@[simp]
+theorem congr_language_eq {s : c.QuotType} :
+    language (FinAcc.mk c.toDA {s}) = c.eqvCls s := by
+  ext xs
+  grind
+
+end FinAcc
+
+end Automata.DA
+
+end Cslib
diff --git a/Cslib/Computability/Languages/Congruences/RightCongruence.lean b/Cslib/Computability/Languages/Congruences/RightCongruence.lean
new file mode 100644
index 00000000..981aa5d0
--- /dev/null
+++ b/Cslib/Computability/Languages/Congruences/RightCongruence.lean
@@ -0,0 +1,51 @@
+/-
+Copyright (c) 2026 Ching-Tsun Chou. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Ching-Tsun Chou
+-/
+
+module
+
+public import Cslib.Init
+public import Mathlib.Computability.Language
+
+@[expose] public section
+
+/-!
+# Right Congruence
+
+This file contains basic definitions about right congruences on finite sequences.
+
+NOTE: Left congruences and two-sided congruences can be similarly defined.
+But they are left to future work because they are not needed for now.
+-/
+
+namespace Cslib
+
+/-- A right congruence is an equivalence relation on finite sequences (represented by lists)
+that is preserved by concatenation on the right.  The equivalence relation is represented
+by a setoid to to enable ready access to the quotient construction. -/
+class RightCongruence (α : Type*) extends eq : Setoid (List α) where
+  /-- If `u` an `v` are congruent, then `u ++ w` and `v ++ w` are also congruent for any `w`. -/
+  right_congr {u v} (huv : u ≈ v) (w : List α) : u ++ w ≈ v ++ w
+
+/-- The `≃` notation is supported for right congruences. -/
+instance {α : Type*} [RightCongruence α] : HasEquiv (List α) :=
+  ⟨RightCongruence.eq⟩
+
+namespace RightCongruence
+
+variable {α : Type*}
+
+/-- The quotient type of a RightCongruence relation. -/
+@[scoped grind =]
+def QuotType (c : RightCongruence α) := Quotient c.eq
+
+/-- The equivalence class (as a language) corresponding to an element of the quotient type. -/
+@[scoped grind =]
+def eqvCls [c : RightCongruence α] (s : c.QuotType) : Language α :=
+  (Quotient.mk c.eq) ⁻¹' {s}
+
+end RightCongruence
+
+end Cslib
diff --git a/Cslib/Computability/Languages/RegularLanguage.lean b/Cslib/Computability/Languages/RegularLanguage.lean
index c35951bc..0aa05469 100644
--- a/Cslib/Computability/Languages/RegularLanguage.lean
+++ b/Cslib/Computability/Languages/RegularLanguage.lean
@@ -6,6 +6,7 @@ Authors: Ching-Tsun Chou
 
 module
 
+public import Cslib.Computability.Automata.DA.Congr
 public import Cslib.Computability.Automata.DA.Prod
 public import Cslib.Computability.Automata.DA.ToNA
 public import Cslib.Computability.Automata.NA.Concat
@@ -159,4 +160,12 @@ theorem IsRegular.kstar [Inhabited Symbol] {l : Language Symbol}
     obtain ⟨State, h_fin, nfa, rfl⟩ := h
     use Unit ⊕ (State ⊕ Unit), inferInstance, ⟨finLoop nfa, {inl ()}⟩, loop_language_eq h_l
 
+/-- If a right congruence is of finite index, then each of its equivalence classes is regular. -/
+@[simp]
+theorem IsRegular.congr_fin_index {Symbol : Type} [c : RightCongruence Symbol] [Finite c.QuotType]
+    (s : c.QuotType) : (c.eqvCls s).IsRegular := by
+  rw [IsRegular.iff_dfa]
+  use c.QuotType, inferInstance, ⟨c.toDA, {s}⟩
+  exact DA.FinAcc.congr_language_eq
+
 end Cslib.Language
diff --git a/Cslib/Foundations/Semantics/FLTS/Basic.lean b/Cslib/Foundations/Semantics/FLTS/Basic.lean
index c06cb59f..17f54aa1 100644
--- a/Cslib/Foundations/Semantics/FLTS/Basic.lean
+++ b/Cslib/Foundations/Semantics/FLTS/Basic.lean
@@ -45,9 +45,14 @@ from the left (instead of the right), in order to match the way lists are constr
 @[scoped grind =]
 def mtr (flts : FLTS State Label) (s : State) (μs : List Label) := μs.foldl flts.tr s
 
-@[scoped grind =]
+@[simp, scoped grind =]
 theorem mtr_nil_eq {flts : FLTS State Label} {s : State} : flts.mtr s [] = s := rfl
 
+@[simp, scoped grind =]
+theorem mtr_concat_eq {flts : FLTS State Label} {s : State} {μs : List Label} {μ : Label} :
+    flts.mtr s (μs ++ [μ]) = flts.tr (flts.mtr s μs) μ := by
+  grind
+
 end FLTS
 
 end Cslib