From 603e7be80d429e46afa7798d1a2c7d5988c80d41 Mon Sep 17 00:00:00 2001
From: crei <crei.github@gmail.com>
Date: Wed, 9 Sep 2026 17:43:30 +0200
Subject: [PATCH 01/13] Two-way automata accept only regular languages.

---
 Cslib.lean                                    |   1 +
 .../Automata/TwoWayNA/Basic.lean              |  17 +
 .../Computability/Automata/TwoWayNA/ToNA.lean | 449 ++++++++++++++++++
 3 files changed, 467 insertions(+)
 create mode 100644 Cslib/Computability/Automata/TwoWayNA/ToNA.lean

diff --git a/Cslib.lean b/Cslib.lean
index 11234c94b..55e05fa6b 100644
--- a/Cslib.lean
+++ b/Cslib.lean
@@ -29,6 +29,7 @@ public import Cslib.Computability.Automata.NA.ToDA
 public import Cslib.Computability.Automata.NA.Total
 public import Cslib.Computability.Automata.Transducers.Transducer
 public import Cslib.Computability.Automata.TwoWayNA.Basic
+public import Cslib.Computability.Automata.TwoWayNA.ToNA
 public import Cslib.Computability.Circuit.Basic
 public import Cslib.Computability.Circuit.Homomorphism
 public import Cslib.Computability.Circuit.Program
diff --git a/Cslib/Computability/Automata/TwoWayNA/Basic.lean b/Cslib/Computability/Automata/TwoWayNA/Basic.lean
index 4741a0c3f..6cad890a4 100644
--- a/Cslib/Computability/Automata/TwoWayNA/Basic.lean
+++ b/Cslib/Computability/Automata/TwoWayNA/Basic.lean
@@ -108,6 +108,23 @@ lemma TwoWayNA.toCfgNAFinAcc_input_eq {State Symbol : Type*} (a : TwoWayNA State
   intro c μ c' h_tr rfl
   simp_all [TwoWayNA.toCfgNAFinAcc]
 
+/-- A configuration running on `input` is the one determined by its state and head position. -/
+theorem TwoWayNACfg.eta {input : List Symbol} {c : TwoWayNACfg State Symbol}
+    (h : c.input = input) (h' : (c.pos : ℕ) < input.length + 1) :
+    ({ input := input, pos := ⟨c.pos, h'⟩, state := c.state } : TwoWayNACfg State Symbol) = c := by
+  cases c
+  subst h
+  rfl
+
+/-- A step reads the symbol at the head position, which therefore lies inside the input. -/
+theorem TwoWayNA.getElem_of_tr {a : TwoWayNA State Symbol} {input : List Symbol}
+    {c c' : TwoWayNACfg State Symbol} {x : Symbol} {m : SignType}
+    (htr : (a.toCfgNAFinAcc input).Tr c (x, m) c') (hc : c.input = input) :
+    ∃ h : (c.pos : ℕ) < input.length, input[(c.pos : ℕ)] = x := by
+  obtain ⟨-, hx, -, -⟩ := htr
+  subst hc
+  exact List.getElem?_eq_some_iff.mp hx.symm
+
 @[simp, scoped grind =]
 instance : Acceptor (TwoWayNA State Symbol) Symbol where
   Accepts (a : TwoWayNA State Symbol) (input : List Symbol) :=
diff --git a/Cslib/Computability/Automata/TwoWayNA/ToNA.lean b/Cslib/Computability/Automata/TwoWayNA/ToNA.lean
new file mode 100644
index 000000000..dc8c19054
--- /dev/null
+++ b/Cslib/Computability/Automata/TwoWayNA/ToNA.lean
@@ -0,0 +1,449 @@
+/-
+Copyright (c) 2026 Christian Reitwiessner. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Christian Reitwiessner
+-/
+
+module
+
+public import Cslib.Computability.Automata.NA.Basic
+public import Cslib.Computability.Automata.TwoWayNA.Basic
+public import Cslib.Computability.Languages.RegularLanguage
+public import Cslib.Foundations.Semantics.LTS.Relation
+
+/-! # Two-way automata are not more powerful than one-way automata
+
+Every language recognised by a nondeterministic two-way automaton (`TwoWayNA`) is also recognised by
+a one-way nondeterministic automaton (`NA`). We follow Vardi's proof, which -- unlike
+Shepherdson's classical crossing-sequence argument -- proceeds by characterising *non*-acceptance
+in a way that can be checked by a single left-to-right sweep over the input.
+
+## Vardi's condition of non-acceptance
+
+Fix a `TwoWayNA` `a` and an input word `input` of length `n`. A *rejection certificate* is a family
+of subsets `T i ⊆ State`, one for every head position `i ∈ {0, …, n}`, subject to three
+conditions:
+
+1. `T` contains every initial state at position `0` (`IsRejectionCert.start_mem`);
+2. `T` is an invariant of the transitions of `a`: if the state `c.state` is in `T c.pos` and `a`
+   can step from the configuration `c` to the configuration `c'`, then `c'.state` is in `T c'.pos`
+   (`TwoWayNA.IsStepClosed`, `IsRejectionCert.step_closed`);
+3. no state in `T n`, i.e. at the position just past the end of the input, is accepting
+   (`IsRejectionCert.accept_notMem`).
+
+Intuitively, `T i` over-approximates the set of states in which `a` can be while its head sits at
+position `i`: conditions 1 and 2 make `T` an inductive invariant of the reachable configurations,
+and condition 3 says that this invariant rules out acceptance -- being preserved by every step, it
+holds at the end of every run (`LTS.mtrInv_of_trInv`). Conversely, the reachable states
+(`TwoWayNA.reachable`) themselves form the least such family, so a certificate exists exactly when
+`a` rejects (`TwoWayNA.not_accepts_iff_exists_isRejectionCert`).
+
+## The one-way automaton
+
+The point of the reformulation is locality: `TwoWayNA.isStepClosed_iff_localOK` turns condition 2
+into a condition `TwoWayNA.LocalOK` relating only `T (i - 1)`, `T i` and `T (i + 1)` with the
+symbol at position `i`. A one-way automaton can therefore guess the certificate while scanning
+the input, keeping only the last two subsets in its state. This is `TwoWayNA.toNAComplement`, and
+`TwoWayNA.accepts_toNAComplement_iff` shows that it accepts exactly the complement of the language
+of `a`.
+
+## Regular languages
+
+Conversely, a one-way automaton is the special case of a two-way automaton that always moves its
+head to the right (`NA.FinAcc.toTwoWayNA`). Rejection certificates play no role here: since the
+head advances by exactly one symbol per step, the runs of the two-way automaton correspond directly
+to multistep transitions of the one-way one (`NA.FinAcc.mTr_take_of_canReach` and
+`NA.FinAcc.canReach_of_mTr`). Together with closure of regular languages under complement this
+gives `Cslib.Language.IsRegular.iff_twoWayNA`: a language is regular if and only if
+it is accepted by a two-way automaton with finitely many states.
+
+## Implementation notes
+
+A rejection certificate is indexed by `ℕ` rather than by `Fin (input.length + 1)`, the type of
+`TwoWayNACfg.pos`: positions past the end of the input are simply left unconstrained, which avoids
+casts when the certificate is compared along a run, whose configurations carry their own input.
+
+Where a `List (Set State)` is more convenient is `TwoWayNA.exists_accepting_mTr_iff`, which is
+proved by induction on the input word and prepends a subset to the certificate at each step.
+`TwoWayNA.certOfList` and `TwoWayNA.certToList` translate between the two encodings, the latter
+prefixing `Set.univ` for the missing position to the left of the input, mirroring
+`TwoWayNA.prevSet`.
+
+## References
+
+* [M. Y. Vardi, *A note on the reduction of two-way automata to one-way automata*][Vardi1989]
+-/
+
+@[expose] public section
+
+namespace List
+
+/-- Dropping the head of a list shifts total indexing by one. -/
+@[simp]
+private theorem getI_tail {α : Type*} [Inhabited α] (l : List α) (i : ℕ) :
+    l.tail.getI i = l.getI (i + 1) := by
+  cases l <;> simp
+
+end List
+
+namespace Cslib.Automata
+
+variable {State Symbol : Type*} {a : TwoWayNA State Symbol} {input : List Symbol}
+
+namespace TwoWayNA
+
+/-! ## Vardi's condition of non-acceptance -/
+
+/-- Every step of `a` on `input` out of a state that `T` attaches to the head position lands in a
+state that `T` attaches to the new head position. -/
+def IsStepClosed (a : TwoWayNA State Symbol) (input : List Symbol) (T : ℕ → Set State) : Prop :=
+  ∀ c c', c.input = input → (a.toCfgNAFinAcc input).UnlabelledTr c c' → c.state ∈ T c.pos →
+    c'.state ∈ T c'.pos
+
+/-- A family of subsets of the state set, one for every position of the input head on `input`,
+which contains all initial states, is closed under the transitions of `a`, and contains no
+accepting state at the position just past the end of the input. -/
+structure IsRejectionCert (a : TwoWayNA State Symbol) (input : List Symbol)
+    (T : ℕ → Set State) : Prop where
+  /-- Every initial state occurs at the initial head position. -/
+  start_mem : ∀ s ∈ a.start, s ∈ T 0
+  /-- The family is an invariant of the transitions of `a`. -/
+  step_closed : a.IsStepClosed input T
+  /-- No accepting state occurs past the end of the input. -/
+  accept_notMem : ∀ s ∈ T input.length, s ∉ a.accept
+
+variable {T : ℕ → Set State}
+
+/-- If a rejection certificate for `input` exists, then `a` does not accept `input`. -/
+theorem IsRejectionCert.not_accepts (hT : a.IsRejectionCert input T) :
+    ¬ Acceptor.Accepts a input := by
+  rintro ⟨μs, c, ⟨hstart, hpos, hinput⟩, c', ⟨hacc, hlast⟩, hmtr⟩
+  have hinv : (a.toCfgNAFinAcc input).MTrInv
+      (fun d => d.input = input ∧ d.state ∈ T d.pos) := by
+    apply LTS.mtrInv_of_trInv
+    rintro d μ d' htr ⟨hd_input, hd_mem⟩
+    exact ⟨a.toCfgNAFinAcc_input_eq input d μ d' htr hd_input,
+      hT.step_closed d d' hd_input ⟨μ, htr⟩ hd_mem⟩
+  obtain ⟨hinput', hmem⟩ :=
+    hinv c μs c' hmtr ⟨hinput, by rw [hpos]; simpa using hT.start_mem c.state hstart⟩
+  rw [hlast, Fin.val_last, hinput'] at hmem
+  exact hT.accept_notMem c'.state hmem hacc
+
+/-- The set of states that `a` can be in while its head sits at position `i` of `input`, having
+started in an initial configuration. -/
+def reachable (a : TwoWayNA State Symbol) (input : List Symbol) (i : ℕ) :
+    Set State :=
+  {q | ∃ c, c.IsInitialForInput a input ∧
+      ∃ h : i < input.length + 1,
+      (a.toCfgNAFinAcc input).CanReach c { input := input, pos := ⟨i, h⟩, state := q } }
+
+/-- If `a` does not accept `input`, then its reachable states form a rejection certificate. -/
+theorem isRejectionCert_reachable (h : ¬ Acceptor.Accepts a input) :
+    a.IsRejectionCert input (a.reachable input) where
+  start_mem s hs :=
+    ⟨{ input := input, pos := ⟨0, Nat.succ_pos _⟩, state := s },
+      ⟨hs, Fin.ext (by simp), rfl⟩, Nat.succ_pos _, LTS.CanReach.refl _ _⟩
+  step_closed c c' hc_input htr hmem := by
+    obtain ⟨c₀, hstart, hlt, hreach⟩ := hmem
+    have hc'_input : c'.input = input := by
+      obtain ⟨μ, htr⟩ := htr
+      exact a.toCfgNAFinAcc_input_eq input c μ c' htr hc_input
+    rw [TwoWayNACfg.eta hc_input hlt] at hreach
+    refine ⟨c₀, hstart, by rw [← hc'_input]; exact c'.pos.isLt, ?_⟩
+    rw [TwoWayNACfg.eta hc'_input]
+    exact (LTS.reflTransGen_unlabelledTr_iff _).mp
+      (((LTS.reflTransGen_unlabelledTr_iff _).mpr hreach).tail htr)
+  accept_notMem s hs hacc := by
+    obtain ⟨c₀, hstart, hlt, μs, hmtr⟩ := hs
+    exact h ⟨μs, c₀, hstart, _, ⟨hacc, Fin.ext (by simp)⟩, hmtr⟩
+
+/-- A two-way automaton rejects an input exactly when a rejection certificate for it exists. -/
+theorem not_accepts_iff_exists_isRejectionCert (a : TwoWayNA State Symbol)
+    (input : List Symbol) :
+    ¬ Acceptor.Accepts a input ↔ ∃ T, a.IsRejectionCert input T :=
+  ⟨fun h => ⟨_, isRejectionCert_reachable h⟩, by rintro ⟨_, hT⟩; exact hT.not_accepts⟩
+
+/-! ## Localising the closure condition -/
+
+/-- The subset that `T` attaches to the position to the left of `i`, and everything at position
+`0`, which has no position to its left. -/
+def prevSet (T : ℕ → Set State) : ℕ → Set State
+  | 0 => Set.univ
+  | i + 1 => T i
+
+/-- Every move of `a` out of a state in `C` while reading `x` lands in `P`, in `C` or in `N`,
+according to whether it moves the head to the left, keeps it in place, or moves it to the right. -/
+def LocalOK (a : TwoWayNA State Symbol) (x : Symbol) (P C N : Set State) : Prop :=
+  ∀ q ∈ C, ∀ m q', a.Tr q x m q' →
+    q' ∈ match m with | .neg => P | .zero => C | .pos => N
+
+/-- Closure of `T` under the transitions of `a` is the same as local consistency of `T` at every
+position carrying an input symbol. -/
+theorem isStepClosed_iff_localOK :
+    a.IsStepClosed input T ↔
+      ∀ i : Fin input.length, a.LocalOK input[i] (prevSet T i) (T i) (T (i + 1)) := by
+  constructor
+  · intro hcl i q hq m q' htr
+    have hlt : (i : ℕ) < input.length := i.isLt
+    cases m with
+    | zero =>
+      exact hcl ⟨input, q, ⟨i, by omega⟩⟩ ⟨input, q', ⟨i, by omega⟩⟩ rfl
+        ⟨(input[i], SignType.zero), rfl, by simp, htr, by simp⟩ hq
+    | pos =>
+      exact hcl ⟨input, q, ⟨i, by omega⟩⟩ ⟨input, q', ⟨i + 1, by omega⟩⟩ rfl
+        ⟨(input[i], SignType.pos), rfl, by simp, htr, by simp⟩ hq
+    | neg =>
+      obtain ⟨iv, hiv⟩ := i
+      obtain _ | j := iv
+      · exact Set.mem_univ q'
+      · exact hcl ⟨input, q, ⟨j + 1, by omega⟩⟩ ⟨input, q', ⟨j, by omega⟩⟩ rfl
+          ⟨(input[j + 1], SignType.neg), rfl, by simp, htr, by simp⟩ hq
+  · rintro hloc c c' hc_input ⟨⟨x, m⟩, hstep⟩ hmem
+    obtain ⟨hlt, rfl⟩ := getElem_of_tr hstep hc_input
+    obtain ⟨-, -, htr, hpos⟩ := hstep
+    have hthis := hloc ⟨(c.pos : ℕ), hlt⟩ c.state hmem m c'.state htr
+    cases m with
+    | zero =>
+      rw [show (c'.pos : ℕ) = (c.pos : ℕ) by simp at hpos; omega]
+      exact hthis
+    | pos =>
+      rw [show (c'.pos : ℕ) = (c.pos : ℕ) + 1 by simp at hpos; omega]
+      exact hthis
+    | neg =>
+      simp only [SignType.neg_eq_neg_one, SignType.coe_neg_one] at hpos
+      obtain ⟨j, hj⟩ : ∃ j, (c.pos : ℕ) = j + 1 := ⟨(c.pos : ℕ) - 1, by omega⟩
+      rw [show (c'.pos : ℕ) = j by omega]
+      rw [show ((⟨(c.pos : ℕ), hlt⟩ : Fin input.length) : ℕ) = j + 1 from hj] at hthis
+      exact hthis
+
+/-! ## The one-way automaton for the complement -/
+
+/-- The one-way automaton that guesses a rejection certificate `T` for `a` while scanning the
+input, keeping the pair `(T (i - 1), T i)` in its state after reading `i` symbols. Reading the
+symbol at position `i` guesses `T (i + 1)` and checks local consistency at position `i`. -/
+def toNAComplement (a : TwoWayNA State Symbol) : NA.FinAcc (Set State × Set State) Symbol where
+  Tr PC x PC' := PC'.1 = PC.2 ∧ a.LocalOK x PC.1 PC.2 PC'.2
+  start := {PC | PC.1 = Set.univ ∧ a.start ⊆ PC.2}
+  accept := {PC | ∀ s ∈ PC.2, s ∉ a.accept}
+
+/-- An accepting multistep transition of `a.toNAComplement` out of `(P, C)` over `xs` is the same
+thing as a list of subsets starting with `P` and `C` that is locally consistent at every position
+of `xs` and ends in a subset without accepting states. -/
+theorem exists_accepting_mTr_iff (a : TwoWayNA State Symbol) (xs : List Symbol) (P C : Set State) :
+    (∃ f ∈ a.toNAComplement.accept, a.toNAComplement.MTr (P, C) xs f) ↔
+      ∃ T : List (Set State), T.getI 0 = P ∧ T.getI 1 = C ∧
+        (∀ i, ∀ hi : i < xs.length, a.LocalOK xs[i] (T.getI i) (T.getI (i + 1)) (T.getI (i + 2))) ∧
+        ∀ s ∈ T.getI (xs.length + 1), s ∉ a.accept := by
+  induction xs generalizing P C with
+  | nil =>
+    constructor
+    · rintro ⟨f, hf, hmtr⟩
+      rw [LTS.MTr.nil_iff] at hmtr
+      subst hmtr
+      exact ⟨[P, C], by simp, by simp, by simp, by simpa [toNAComplement] using hf⟩
+    · rintro ⟨T, h0, h1, -, hacc⟩
+      exact ⟨(P, C), by rw [← h1]; simpa [toNAComplement] using hacc, by simp⟩
+  | cons x xs ih =>
+    constructor
+    · rintro ⟨f, hf, hmtr⟩
+      rw [LTS.MTr.cons_iff] at hmtr
+      obtain ⟨⟨m₁, m₂⟩, ⟨rfl, hlocal⟩, hmtr⟩ := hmtr
+      obtain ⟨T, h0, h1, hloc, hacc⟩ := (ih m₁ m₂).mp ⟨f, hf, hmtr⟩
+      have hlocal' : a.LocalOK x P m₁ m₂ := hlocal
+      have hstep : ∀ i, ∀ hi : i < (x :: xs).length,
+          a.LocalOK (x :: xs)[i]
+            ((P :: T).getI i) ((P :: T).getI (i + 1)) ((P :: T).getI (i + 2)) := by
+        intro i hi
+        obtain _ | i := i
+        · simpa [h0, h1] using hlocal'
+        · simpa using hloc i (by simpa using hi)
+      exact ⟨P :: T, by simp, by simpa using h0, hstep, by simpa using hacc⟩
+    · rintro ⟨T, h0, h1, hloc, hacc⟩
+      have hstep : ∀ i, ∀ hi : i < xs.length,
+          a.LocalOK xs[i] (T.tail.getI i) (T.tail.getI (i + 1)) (T.tail.getI (i + 2)) := by
+        intro i hi
+        have h := hloc (i + 1) (by simpa using hi)
+        rw [List.getElem_cons_succ] at h
+        simpa using h
+      obtain ⟨f, hf, hmtr⟩ := (ih C (T.getI 2)).mpr
+        ⟨T.tail, by simpa using h1, by simp, hstep, by simpa using hacc⟩
+      have hlocal : a.LocalOK x P C (T.getI 2) := by
+        have h := hloc 0 (by simp)
+        rw [List.getElem_cons_zero] at h
+        simpa [h0, h1] using h
+      have htr : a.toNAComplement.Tr (P, C) x (C, T.getI 2) := ⟨rfl, hlocal⟩
+      exact ⟨f, hf, LTS.MTr.cons_iff.mpr ⟨(C, T.getI 2), htr, hmtr⟩⟩
+
+/-- The family of subsets carried by a list, which holds the subset for the position to the left
+of `0` in front, so that position `i` is entry `i + 1` of the list. -/
+def certOfList (T : List (Set State)) (i : ℕ) : Set State :=
+  T.getI (i + 1)
+
+/-- The subsets that `T` attaches to the positions of the input head, as a list, prefixed by
+`Set.univ` for the position to the left of `0`. -/
+def certToList (input : List Symbol) (T : ℕ → Set State) : List (Set State) :=
+  Set.univ :: (List.range (input.length + 1)).map T
+
+/-- Entry `i + 1` of `TwoWayNA.certToList` is the subset that `T` attaches to position `i`. -/
+@[simp]
+theorem getI_certToList {T : ℕ → Set State} {i : ℕ} (hi : i < input.length + 1) :
+    (certToList input T).getI (i + 1) = T i := by
+  rw [certToList, List.getI_cons_succ, List.getI_eq_getElem (hn := by simpa using hi)]
+  simp
+
+/-- `a.toNAComplement` accepts exactly the words that `a` rejects. -/
+theorem accepts_toNAComplement_iff (a : TwoWayNA State Symbol) (input : List Symbol) :
+    Acceptor.Accepts a.toNAComplement input ↔ ¬ Acceptor.Accepts a input := by
+  rw [not_accepts_iff_exists_isRejectionCert]
+  constructor
+  · rintro ⟨s, ⟨hs, hstart⟩, f, hf, hmtr⟩
+    obtain ⟨T, h0, h1, hloc, hacc⟩ := (exists_accepting_mTr_iff a input s.1 s.2).mp ⟨f, hf, hmtr⟩
+    have hstep : ∀ i : Fin input.length,
+        a.LocalOK input[i] (prevSet (certOfList T) i) (certOfList T i) (certOfList T (i + 1)) := by
+      intro i
+      obtain ⟨iv, hiv⟩ := i
+      obtain _ | j := iv
+      · simpa [prevSet, certOfList, h0, hs] using hloc 0 hiv
+      · simpa [prevSet, certOfList] using hloc (j + 1) hiv
+    exact ⟨certOfList T,
+      { start_mem := by
+          intro q hq
+          simpa [certOfList, h1] using hstart hq
+        step_closed := isStepClosed_iff_localOK.mpr hstep
+        accept_notMem := by simpa [certOfList] using hacc }⟩
+  · rintro ⟨T, hT⟩
+    have hloc := isStepClosed_iff_localOK.mp hT.step_closed
+    have hstep : ∀ i, ∀ hi : i < input.length, a.LocalOK input[i]
+        ((certToList input T).getI i) ((certToList input T).getI (i + 1))
+          ((certToList input T).getI (i + 2)) := by
+      intro i hi
+      have e0 : (certToList input T).getI i = prevSet T i := by
+        obtain _ | j := i
+        · rfl
+        · exact getI_certToList (by omega)
+      have e1 : (certToList input T).getI (i + 1) = T i := getI_certToList (by omega)
+      have e2 : (certToList input T).getI (i + 2) = T (i + 1) := getI_certToList (by omega)
+      rw [e0, e1, e2]
+      exact hloc ⟨i, hi⟩
+    obtain ⟨f, hf, hmtr⟩ := (exists_accepting_mTr_iff a input Set.univ (T 0)).mpr
+      ⟨certToList input T, rfl, getI_certToList (by omega), hstep,
+        by rw [getI_certToList (by omega)]; exact hT.accept_notMem⟩
+    exact ⟨(Set.univ, T 0), ⟨rfl, hT.start_mem⟩, f, hf, hmtr⟩
+
+/-- `a.toNAComplement` recognises the complement of the language of `a`. -/
+theorem language_toNAComplement (a : TwoWayNA State Symbol) :
+    Acceptor.language a.toNAComplement = (Acceptor.language a)ᶜ := by
+  ext xs
+  simp only [Acceptor.mem_language]
+  exact accepts_toNAComplement_iff a xs
+
+end TwoWayNA
+
+/-! ## One-way automata as two-way automata -/
+
+namespace NA.FinAcc
+
+variable {n : NA.FinAcc State Symbol}
+
+/-- The two-way automaton that performs the transitions of `n`, always moving its head one symbol
+to the right. -/
+def toTwoWayNA (n : NA.FinAcc State Symbol) : TwoWayNA State Symbol where
+  Tr q x m q' := m = SignType.pos ∧ n.Tr q x q'
+  start := n.start
+  accept := n.accept
+
+/-- A run of `n.toTwoWayNA` starting on `input` reads a multistep transition of `n` over the
+prefix of `input` scanned so far. -/
+theorem mTr_take_of_canReach {s : State} {c c' : TwoWayNACfg State Symbol}
+    (hreach : (n.toTwoWayNA.toCfgNAFinAcc input).CanReach c c') (hc : c.input = input)
+    (hmtr : n.MTr s (input.take c.pos) c.state) :
+    c'.input = input ∧ n.MTr s (input.take c'.pos) c'.state := by
+  obtain ⟨μs, hreach⟩ := hreach
+  refine LTS.mtrInv_of_trInv
+    (p := fun d => d.input = input ∧ n.MTr s (input.take d.pos) d.state) ?_ c μs c' hreach
+    ⟨hc, hmtr⟩
+  rintro d ⟨x, m⟩ d' hstep ⟨hd, hmtr⟩
+  obtain ⟨hlt, rfl⟩ := TwoWayNA.getElem_of_tr hstep hd
+  obtain ⟨hinput, -, ⟨rfl, htr⟩, hpos⟩ := hstep
+  refine ⟨by rw [← hinput, hd], ?_⟩
+  rw [show (d'.pos : ℕ) = (d.pos : ℕ) + 1 by simp at hpos; omega,
+    List.take_succ_eq_append_getElem hlt]
+  exact LTS.MTr.stepR _ hmtr htr
+
+/-- A multistep transition of `n` over the part of `input` that starts at position `p` is read by
+a run of `n.toTwoWayNA` taking its head from `p` to the end of the input. -/
+theorem canReach_of_mTr {suf : List Symbol} {s s' : State} {p : ℕ}
+    (hp : p < input.length + 1) (hdrop : input.drop p = suf) (hmtr : n.MTr s suf s') :
+    (n.toTwoWayNA.toCfgNAFinAcc input).CanReach ⟨input, s, ⟨p, hp⟩⟩ ⟨input, s', Fin.last _⟩ := by
+  induction suf generalizing s p with
+  | nil =>
+    rw [LTS.MTr.nil_iff] at hmtr
+    subst hmtr
+    obtain rfl : p = input.length := by grind [List.drop_eq_nil_iff]
+    exact LTS.CanReach.refl _ _
+  | cons x xs ih =>
+    rw [LTS.MTr.cons_iff] at hmtr
+    obtain ⟨t, htr, hmtr⟩ := hmtr
+    have hlt : p < input.length := by
+      by_contra hc
+      grind [List.drop_eq_nil_iff]
+    have hx : input[p]'hlt = x := by
+      have h0 : (input.drop p)[0]? = some x := by rw [hdrop]; simp
+      grind
+    have hdrop' : input.drop (p + 1) = xs := by simp [← List.tail_drop, hdrop]
+    have hstep : (n.toTwoWayNA.toCfgNAFinAcc input).Tr
+        ⟨input, s, ⟨p, hp⟩⟩ (x, SignType.pos) ⟨input, t, ⟨p + 1, by omega⟩⟩ :=
+      ⟨rfl, by rw [← hx]; simp, ⟨rfl, htr⟩, by simp⟩
+    obtain ⟨μs, hmtr'⟩ := ih (by omega) hdrop' hmtr
+    exact ⟨(x, SignType.pos) :: μs, LTS.MTr.cons_iff.mpr ⟨_, hstep, hmtr'⟩⟩
+
+/-- A one-way automaton and its two-way rendering accept the same words. -/
+theorem accepts_toTwoWayNA_iff (n : NA.FinAcc State Symbol) (input : List Symbol) :
+    Acceptor.Accepts n.toTwoWayNA input ↔ Acceptor.Accepts n input := by
+  constructor
+  · rintro ⟨μs, c, ⟨hs, hpos, hinput⟩, c', ⟨hacc, hlast⟩, hmtr⟩
+    have hstart : n.MTr c.state (input.take c.pos) c.state := by
+      rw [hpos]
+      simp
+    obtain ⟨hinput', hmtr⟩ := mTr_take_of_canReach ⟨μs, hmtr⟩ hinput hstart
+    rw [hlast, Fin.val_last, hinput', List.take_length] at hmtr
+    exact ⟨c.state, hs, c'.state, hacc, hmtr⟩
+  · rintro ⟨s, hs, s', hs', hmtr⟩
+    obtain ⟨μs, hmtr⟩ :=
+      canReach_of_mTr (suf := input) (by omega) List.drop_zero hmtr
+    exact ⟨μs, ⟨input, s, ⟨0, by omega⟩⟩, ⟨hs, Fin.ext (by simp), rfl⟩,
+      ⟨input, s', Fin.last _⟩, ⟨hs', rfl⟩, hmtr⟩
+
+/-- A one-way automaton and its two-way rendering recognise the same language. -/
+theorem language_toTwoWayNA (n : NA.FinAcc State Symbol) :
+    Acceptor.language n.toTwoWayNA = Acceptor.language n := by
+  ext xs
+  simp only [Acceptor.mem_language]
+  exact accepts_toTwoWayNA_iff n xs
+
+end NA.FinAcc
+
+end Cslib.Automata
+
+namespace Cslib.Language
+
+open Automata Acceptor
+
+/-- A language is regular if and only if it is accepted by some two-way nondeterministic
+automaton with finitely many states. -/
+theorem IsRegular.iff_twoWayNA {Symbol : Type*} {l : Language Symbol} :
+    l.IsRegular ↔ ∃ State : Type, ∃ _ : Finite State,
+      ∃ a : Automata.TwoWayNA State Symbol, language a = l := by
+  constructor
+  · intro h
+    rw [IsRegular.iff_nfa] at h
+    obtain ⟨State, hfin, na, rfl⟩ := h
+    exact ⟨State, hfin, na.toTwoWayNA, na.language_toTwoWayNA⟩
+  · rintro ⟨State, hfin, a, rfl⟩
+    have := hfin
+    have hc : (language a)ᶜ.IsRegular := by
+      rw [IsRegular.iff_nfa]
+      exact ⟨Set State × Set State, inferInstance, a.toNAComplement, a.language_toNAComplement⟩
+    simpa using hc.compl
+
+end Cslib.Language

From 1abff3179cbbe7f5d6053dc22f0e27b5de639b98 Mon Sep 17 00:00:00 2001
From: crei <crei.github@gmail.com>
Date: Thu, 10 Sep 2026 11:23:59 +0200
Subject: [PATCH 02/13] Use TrInv.

---
 .../Computability/Automata/TwoWayNA/ToNA.lean | 49 ++++++++-----------
 1 file changed, 21 insertions(+), 28 deletions(-)

diff --git a/Cslib/Computability/Automata/TwoWayNA/ToNA.lean b/Cslib/Computability/Automata/TwoWayNA/ToNA.lean
index dc8c19054..e6904ea7b 100644
--- a/Cslib/Computability/Automata/TwoWayNA/ToNA.lean
+++ b/Cslib/Computability/Automata/TwoWayNA/ToNA.lean
@@ -13,10 +13,10 @@ public import Cslib.Foundations.Semantics.LTS.Relation
 
 /-! # Two-way automata are not more powerful than one-way automata
 
-Every language recognised by a nondeterministic two-way automaton (`TwoWayNA`) is also recognised by
+Every language accepted by a nondeterministic two-way automaton (`TwoWayNA`) is also accepted by
 a one-way nondeterministic automaton (`NA`). We follow Vardi's proof, which -- unlike
-Shepherdson's classical crossing-sequence argument -- proceeds by characterising *non*-acceptance
-in a way that can be checked by a single left-to-right sweep over the input.
+Shepherdson's crossing-sequence argument -- proceeds by characterising *non*-acceptance in a way
+that can be checked by a single left-to-right sweep over the input.
 
 ## Vardi's condition of non-acceptance
 
@@ -95,10 +95,10 @@ namespace TwoWayNA
 /-! ## Vardi's condition of non-acceptance -/
 
 /-- Every step of `a` on `input` out of a state that `T` attaches to the head position lands in a
-state that `T` attaches to the new head position. -/
+state that `T` attaches to the new head position. The conjunct on the input restricts the
+invariant to the configurations that run on `input`. -/
 def IsStepClosed (a : TwoWayNA State Symbol) (input : List Symbol) (T : ℕ → Set State) : Prop :=
-  ∀ c c', c.input = input → (a.toCfgNAFinAcc input).UnlabelledTr c c' → c.state ∈ T c.pos →
-    c'.state ∈ T c'.pos
+  (a.toCfgNAFinAcc input).TrInv (fun c => c.input = input ∧ c.state ∈ T c.pos)
 
 /-- A family of subsets of the state set, one for every position of the input head on `input`,
 which contains all initial states, is closed under the transitions of `a`, and contains no
@@ -118,14 +118,8 @@ variable {T : ℕ → Set State}
 theorem IsRejectionCert.not_accepts (hT : a.IsRejectionCert input T) :
     ¬ Acceptor.Accepts a input := by
   rintro ⟨μs, c, ⟨hstart, hpos, hinput⟩, c', ⟨hacc, hlast⟩, hmtr⟩
-  have hinv : (a.toCfgNAFinAcc input).MTrInv
-      (fun d => d.input = input ∧ d.state ∈ T d.pos) := by
-    apply LTS.mtrInv_of_trInv
-    rintro d μ d' htr ⟨hd_input, hd_mem⟩
-    exact ⟨a.toCfgNAFinAcc_input_eq input d μ d' htr hd_input,
-      hT.step_closed d d' hd_input ⟨μ, htr⟩ hd_mem⟩
-  obtain ⟨hinput', hmem⟩ :=
-    hinv c μs c' hmtr ⟨hinput, by rw [hpos]; simpa using hT.start_mem c.state hstart⟩
+  obtain ⟨hinput', hmem⟩ := LTS.mtrInv_of_trInv hT.step_closed c μs c' hmtr
+    ⟨hinput, by rw [hpos]; simpa using hT.start_mem c.state hstart⟩
   rw [hlast, Fin.val_last, hinput'] at hmem
   exact hT.accept_notMem c'.state hmem hacc
 
@@ -143,16 +137,14 @@ theorem isRejectionCert_reachable (h : ¬ Acceptor.Accepts a input) :
   start_mem s hs :=
     ⟨{ input := input, pos := ⟨0, Nat.succ_pos _⟩, state := s },
       ⟨hs, Fin.ext (by simp), rfl⟩, Nat.succ_pos _, LTS.CanReach.refl _ _⟩
-  step_closed c c' hc_input htr hmem := by
-    obtain ⟨c₀, hstart, hlt, hreach⟩ := hmem
-    have hc'_input : c'.input = input := by
-      obtain ⟨μ, htr⟩ := htr
-      exact a.toCfgNAFinAcc_input_eq input c μ c' htr hc_input
+  step_closed c μ c' htr := by
+    rintro ⟨hc_input, c₀, hstart, hlt, hreach⟩
+    have hc'_input : c'.input = input := a.toCfgNAFinAcc_input_eq input c μ c' htr hc_input
     rw [TwoWayNACfg.eta hc_input hlt] at hreach
-    refine ⟨c₀, hstart, by rw [← hc'_input]; exact c'.pos.isLt, ?_⟩
+    refine ⟨hc'_input, c₀, hstart, by rw [← hc'_input]; exact c'.pos.isLt, ?_⟩
     rw [TwoWayNACfg.eta hc'_input]
     exact (LTS.reflTransGen_unlabelledTr_iff _).mp
-      (((LTS.reflTransGen_unlabelledTr_iff _).mpr hreach).tail htr)
+      (((LTS.reflTransGen_unlabelledTr_iff _).mpr hreach).tail ⟨μ, htr⟩)
   accept_notMem s hs hacc := by
     obtain ⟨c₀, hstart, hlt, μs, hmtr⟩ := hs
     exact h ⟨μs, c₀, hstart, _, ⟨hacc, Fin.ext (by simp)⟩, hmtr⟩
@@ -187,18 +179,19 @@ theorem isStepClosed_iff_localOK :
     have hlt : (i : ℕ) < input.length := i.isLt
     cases m with
     | zero =>
-      exact hcl ⟨input, q, ⟨i, by omega⟩⟩ ⟨input, q', ⟨i, by omega⟩⟩ rfl
-        ⟨(input[i], SignType.zero), rfl, by simp, htr, by simp⟩ hq
+      exact (hcl ⟨input, q, ⟨i, by omega⟩⟩ (input[i], SignType.zero)
+        ⟨input, q', ⟨i, by omega⟩⟩ ⟨rfl, by simp, htr, by simp⟩ ⟨rfl, hq⟩).2
     | pos =>
-      exact hcl ⟨input, q, ⟨i, by omega⟩⟩ ⟨input, q', ⟨i + 1, by omega⟩⟩ rfl
-        ⟨(input[i], SignType.pos), rfl, by simp, htr, by simp⟩ hq
+      exact (hcl ⟨input, q, ⟨i, by omega⟩⟩ (input[i], SignType.pos)
+        ⟨input, q', ⟨i + 1, by omega⟩⟩ ⟨rfl, by simp, htr, by simp⟩ ⟨rfl, hq⟩).2
     | neg =>
       obtain ⟨iv, hiv⟩ := i
       obtain _ | j := iv
       · exact Set.mem_univ q'
-      · exact hcl ⟨input, q, ⟨j + 1, by omega⟩⟩ ⟨input, q', ⟨j, by omega⟩⟩ rfl
-          ⟨(input[j + 1], SignType.neg), rfl, by simp, htr, by simp⟩ hq
-  · rintro hloc c c' hc_input ⟨⟨x, m⟩, hstep⟩ hmem
+      · exact (hcl ⟨input, q, ⟨j + 1, by omega⟩⟩ (input[j + 1], SignType.neg)
+          ⟨input, q', ⟨j, by omega⟩⟩ ⟨rfl, by simp, htr, by simp⟩ ⟨rfl, hq⟩).2
+  · rintro hloc c ⟨x, m⟩ c' hstep ⟨hc_input, hmem⟩
+    refine ⟨a.toCfgNAFinAcc_input_eq input c (x, m) c' hstep hc_input, ?_⟩
     obtain ⟨hlt, rfl⟩ := getElem_of_tr hstep hc_input
     obtain ⟨-, -, htr, hpos⟩ := hstep
     have hthis := hloc ⟨(c.pos : ℕ), hlt⟩ c.state hmem m c'.state htr

From ba0bc949a0791eff6cedbdb54f2177b3d87b72f5 Mon Sep 17 00:00:00 2001
From: crei <crei.github@gmail.com>
Date: Thu, 10 Sep 2026 12:15:23 +0200
Subject: [PATCH 03/13] Split into multiple files.

---
 Cslib.lean                                    |   2 +
 .../Automata/TwoWayNA/Basic.lean              |   7 +-
 .../Computability/Automata/TwoWayNA/OfNA.lean | 105 ++++++++++
 .../Automata/TwoWayNA/Regular.lean            |  40 ++++
 .../Computability/Automata/TwoWayNA/ToNA.lean | 182 ++++--------------
 5 files changed, 186 insertions(+), 150 deletions(-)
 create mode 100644 Cslib/Computability/Automata/TwoWayNA/OfNA.lean
 create mode 100644 Cslib/Computability/Automata/TwoWayNA/Regular.lean

diff --git a/Cslib.lean b/Cslib.lean
index 55e05fa6b..3b06f1c9c 100644
--- a/Cslib.lean
+++ b/Cslib.lean
@@ -29,6 +29,8 @@ public import Cslib.Computability.Automata.NA.ToDA
 public import Cslib.Computability.Automata.NA.Total
 public import Cslib.Computability.Automata.Transducers.Transducer
 public import Cslib.Computability.Automata.TwoWayNA.Basic
+public import Cslib.Computability.Automata.TwoWayNA.OfNA
+public import Cslib.Computability.Automata.TwoWayNA.Regular
 public import Cslib.Computability.Automata.TwoWayNA.ToNA
 public import Cslib.Computability.Circuit.Basic
 public import Cslib.Computability.Circuit.Homomorphism
diff --git a/Cslib/Computability/Automata/TwoWayNA/Basic.lean b/Cslib/Computability/Automata/TwoWayNA/Basic.lean
index 6cad890a4..78d491818 100644
--- a/Cslib/Computability/Automata/TwoWayNA/Basic.lean
+++ b/Cslib/Computability/Automata/TwoWayNA/Basic.lean
@@ -27,7 +27,12 @@ ends in an accepting state with the head just past the end of the input.
 
 * `TwoWayNA`, the automaton itself
 * `TwoWayNACfg`, a configuration of a `TwoWayNA`: Its input plus a state and the head position.
-* `TwoWayNA.Step`, The single-step relation between configurations.
+* `TwoWayNA.toCfgNAFinAcc`, the finite acceptor on configurations whose runs on a fixed input are
+  the runs of the two-way automaton on that input. It also provides the `Acceptor` instance.
+
+The comparison with finite acceptors is in `Cslib.Computability.Automata.TwoWayNA.ToNA`,
+`Cslib.Computability.Automata.TwoWayNA.OfNA` and
+`Cslib.Computability.Automata.TwoWayNA.Regular`.
 
 ## Implementation notes
 
diff --git a/Cslib/Computability/Automata/TwoWayNA/OfNA.lean b/Cslib/Computability/Automata/TwoWayNA/OfNA.lean
new file mode 100644
index 000000000..7051b0f14
--- /dev/null
+++ b/Cslib/Computability/Automata/TwoWayNA/OfNA.lean
@@ -0,0 +1,105 @@
+/-
+Copyright (c) 2026 Christian Reitwiessner. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Christian Reitwiessner
+-/
+
+module
+
+public import Cslib.Computability.Automata.TwoWayNA.Basic
+
+/-! # Finite acceptors as two-way automata
+
+A nondeterministic finite acceptor (`NA.FinAcc`) is the special case of a nondeterministic two-way
+automaton (`TwoWayNA`) that moves its head one symbol to the right in every step, `TwoWayNA.ofNA`.
+
+The head of `TwoWayNA.ofNA n` is thus at position `i` exactly when `n` has read the first `i`
+symbols of the input, so the runs of the two-way automaton are in lockstep with the multistep
+transitions of `n` (`TwoWayNA.mTr_take_of_canReach`, `TwoWayNA.canReach_of_mTr`) and the two accept
+the same words (`TwoWayNA.accepts_ofNA_iff`, `TwoWayNA.language_ofNA`).
+-/
+
+@[expose] public section
+
+namespace Cslib.Automata
+
+variable {State Symbol : Type*} {input : List Symbol}
+
+namespace TwoWayNA
+
+variable {n : NA.FinAcc State Symbol}
+
+/-- The two-way automaton that performs the transitions of the nondeterministic finite acceptor
+`n`, always moving its head one symbol to the right. -/
+def ofNA (n : NA.FinAcc State Symbol) : TwoWayNA State Symbol where
+  Tr q x m q' := m = SignType.pos ∧ n.Tr q x q'
+  start := n.start
+  accept := n.accept
+
+/-- A run of `ofNA n` starting on `input` reads a multistep transition of `n` over the prefix of
+`input` scanned so far. -/
+theorem mTr_take_of_canReach {s : State} {c c' : TwoWayNACfg State Symbol}
+    (hreach : ((ofNA n).toCfgNAFinAcc input).CanReach c c') (hc : c.input = input)
+    (hmtr : n.MTr s (input.take c.pos) c.state) :
+    c'.input = input ∧ n.MTr s (input.take c'.pos) c'.state := by
+  obtain ⟨μs, hreach⟩ := hreach
+  refine LTS.mtrInv_of_trInv
+    (p := fun d => d.input = input ∧ n.MTr s (input.take d.pos) d.state) ?_ c μs c' hreach
+    ⟨hc, hmtr⟩
+  rintro d ⟨x, m⟩ d' hstep ⟨hd, hmtr⟩
+  obtain ⟨hlt, rfl⟩ := getElem_of_tr hstep hd
+  obtain ⟨hinput, -, ⟨rfl, htr⟩, hpos⟩ := hstep
+  refine ⟨hinput ▸ hd, ?_⟩
+  rw [show (d'.pos : ℕ) = (d.pos : ℕ) + 1 by simp at hpos; omega]
+  rw [List.take_succ_eq_append_getElem hlt]
+  exact LTS.MTr.stepR _ hmtr htr
+
+/-- A multistep transition of `n` over the part of `input` that starts at position `p` is read by a
+run of `ofNA n` taking its head from `p` to the end of the input. -/
+theorem canReach_of_mTr {suf : List Symbol} {s s' : State} {p : ℕ}
+    (hp : p < input.length + 1) (hdrop : input.drop p = suf) (hmtr : n.MTr s suf s') :
+    ((ofNA n).toCfgNAFinAcc input).CanReach ⟨input, s, ⟨p, hp⟩⟩ ⟨input, s', Fin.last _⟩ := by
+  induction suf generalizing s p with
+  | nil =>
+    rw [LTS.MTr.nil_iff] at hmtr
+    subst hmtr
+    obtain rfl : p = input.length := by grind [List.drop_eq_nil_iff]
+    exact LTS.CanReach.refl _ _
+  | cons x xs ih =>
+    rw [LTS.MTr.cons_iff] at hmtr
+    obtain ⟨t, htr, hmtr⟩ := hmtr
+    have hlt : p < input.length := by grind [List.drop_eq_nil_iff]
+    have hx : input[p]'hlt = x := by
+      have h0 : (input.drop p)[0]? = some x := by simp [hdrop]
+      grind
+    have hdrop' : input.drop (p + 1) = xs := by simp [← List.tail_drop, hdrop]
+    have hstep : ((ofNA n).toCfgNAFinAcc input).Tr
+        ⟨input, s, ⟨p, hp⟩⟩ (x, SignType.pos) ⟨input, t, ⟨p + 1, by omega⟩⟩ :=
+      ⟨rfl, by simp [← hx], ⟨rfl, htr⟩, by simp⟩
+    obtain ⟨μs, hmtr'⟩ := ih (by omega) hdrop' hmtr
+    exact ⟨(x, SignType.pos) :: μs, LTS.MTr.cons_iff.mpr ⟨_, hstep, hmtr'⟩⟩
+
+/-- A nondeterministic finite acceptor and its two-way rendering accept the same words. -/
+theorem accepts_ofNA_iff (a : NA.FinAcc State Symbol) (input : List Symbol) :
+    Acceptor.Accepts (ofNA a) input ↔ Acceptor.Accepts a input := by
+  constructor
+  · rintro ⟨μs, c, ⟨hs, hpos, hinput⟩, c', ⟨hacc, hlast⟩, hmtr⟩
+    have hstart : a.MTr c.state (input.take c.pos) c.state := by simp [hpos]
+    obtain ⟨hinput', hmtr⟩ := mTr_take_of_canReach ⟨μs, hmtr⟩ hinput hstart
+    rw [hlast, Fin.val_last, hinput', List.take_length] at hmtr
+    exact ⟨c.state, hs, c'.state, hacc, hmtr⟩
+  · rintro ⟨s, hs, s', hs', hmtr⟩
+    obtain ⟨μs, hmtr⟩ :=
+      canReach_of_mTr (suf := input) (by omega) List.drop_zero hmtr
+    exact ⟨μs, ⟨input, s, ⟨0, by omega⟩⟩, ⟨hs, Fin.ext (by simp), rfl⟩,
+      ⟨input, s', Fin.last _⟩, ⟨hs', rfl⟩, hmtr⟩
+
+/-- A nondeterministic finite acceptor and its two-way rendering recognise the same language. -/
+theorem language_ofNA (a : NA.FinAcc State Symbol) :
+    Acceptor.language (ofNA a) = Acceptor.language a := by
+  ext xs
+  simpa [Acceptor.mem_language] using accepts_ofNA_iff a xs
+
+end TwoWayNA
+
+end Cslib.Automata
diff --git a/Cslib/Computability/Automata/TwoWayNA/Regular.lean b/Cslib/Computability/Automata/TwoWayNA/Regular.lean
new file mode 100644
index 000000000..f235c2178
--- /dev/null
+++ b/Cslib/Computability/Automata/TwoWayNA/Regular.lean
@@ -0,0 +1,40 @@
+/-
+Copyright (c) 2026 Christian Reitwiessner. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Christian Reitwiessner
+-/
+
+module
+
+public import Cslib.Computability.Automata.TwoWayNA.OfNA
+public import Cslib.Computability.Automata.TwoWayNA.ToNA
+public import Cslib.Computability.Languages.RegularLanguage
+
+/-! # Two-way automata recognise exactly the regular languages
+
+This is the combination of the results of `TwoWayNA.ofNA` and `TwoWayNA.toNAComplement`
+plus the fact that regular languages are closed under complementation.
+-/
+
+namespace Cslib.Language
+
+open Automata Acceptor
+
+/-- A language is regular if and only if it is accepted by some two-way nondeterministic
+automaton with finitely many states. -/
+public theorem IsRegular.iff_twoWayNA {Symbol : Type*} {l : Language Symbol} :
+    l.IsRegular ↔ ∃ State : Type, ∃ _ : Finite State,
+      ∃ a : Automata.TwoWayNA State Symbol, language a = l := by
+  constructor
+  · intro h
+    rw [IsRegular.iff_nfa] at h
+    obtain ⟨State, hfin, na, rfl⟩ := h
+    exact ⟨State, hfin, TwoWayNA.ofNA na, TwoWayNA.language_ofNA na⟩
+  · rintro ⟨State, hfin, a, rfl⟩
+    have := hfin
+    have hc : (language a)ᶜ.IsRegular := by
+      rw [IsRegular.iff_nfa]
+      exact ⟨Set State × Set State, inferInstance, a.toNAComplement, a.language_toNAComplement⟩
+    simpa using hc.compl
+
+end Cslib.Language
diff --git a/Cslib/Computability/Automata/TwoWayNA/ToNA.lean b/Cslib/Computability/Automata/TwoWayNA/ToNA.lean
index e6904ea7b..eb65afbb9 100644
--- a/Cslib/Computability/Automata/TwoWayNA/ToNA.lean
+++ b/Cslib/Computability/Automata/TwoWayNA/ToNA.lean
@@ -8,15 +8,18 @@ module
 
 public import Cslib.Computability.Automata.NA.Basic
 public import Cslib.Computability.Automata.TwoWayNA.Basic
-public import Cslib.Computability.Languages.RegularLanguage
 public import Cslib.Foundations.Semantics.LTS.Relation
 
-/-! # Two-way automata are not more powerful than one-way automata
+/-! # A finite acceptor for the complement of the language of a two-way automaton
 
-Every language accepted by a nondeterministic two-way automaton (`TwoWayNA`) is also accepted by
-a one-way nondeterministic automaton (`NA`). We follow Vardi's proof, which -- unlike
-Shepherdson's crossing-sequence argument -- proceeds by characterising *non*-acceptance in a way
-that can be checked by a single left-to-right sweep over the input.
+For every nondeterministic two-way automaton (`TwoWayNA`) `a`, this file constructs a
+nondeterministic finite acceptor (`NA.FinAcc`) that accepts exactly the words rejected by `a`
+(`TwoWayNA.toNAComplement`, `TwoWayNA.language_toNAComplement`). We follow Vardi's proof, which --
+unlike Shepherdson's crossing-sequence argument -- characterises non-acceptance in a way that can
+be checked by a single left-to-right sweep over the input.
+
+This result is the main ingredient in proving equivalence of two-way and one-way automata, which
+can be found in `Cslib.Computability.Automata.TwoWayNA.Regular`.
 
 ## Vardi's condition of non-acceptance
 
@@ -38,24 +41,13 @@ holds at the end of every run (`LTS.mtrInv_of_trInv`). Conversely, the reachable
 (`TwoWayNA.reachable`) themselves form the least such family, so a certificate exists exactly when
 `a` rejects (`TwoWayNA.not_accepts_iff_exists_isRejectionCert`).
 
-## The one-way automaton
+## The finite acceptor for the complement
 
 The point of the reformulation is locality: `TwoWayNA.isStepClosed_iff_localOK` turns condition 2
 into a condition `TwoWayNA.LocalOK` relating only `T (i - 1)`, `T i` and `T (i + 1)` with the
-symbol at position `i`. A one-way automaton can therefore guess the certificate while scanning
-the input, keeping only the last two subsets in its state. This is `TwoWayNA.toNAComplement`, and
-`TwoWayNA.accepts_toNAComplement_iff` shows that it accepts exactly the complement of the language
-of `a`.
-
-## Regular languages
-
-Conversely, a one-way automaton is the special case of a two-way automaton that always moves its
-head to the right (`NA.FinAcc.toTwoWayNA`). Rejection certificates play no role here: since the
-head advances by exactly one symbol per step, the runs of the two-way automaton correspond directly
-to multistep transitions of the one-way one (`NA.FinAcc.mTr_take_of_canReach` and
-`NA.FinAcc.canReach_of_mTr`). Together with closure of regular languages under complement this
-gives `Cslib.Language.IsRegular.iff_twoWayNA`: a language is regular if and only if
-it is accepted by a two-way automaton with finitely many states.
+symbol at position `i`. A finite acceptor can therefore guess the certificate while scanning the
+input, keeping only the last two subsets in its state. This is `TwoWayNA.toNAComplement`, and
+`TwoWayNA.accepts_toNAComplement_iff` shows that it accepts exactly the words rejected by `a`.
 
 ## Implementation notes
 
@@ -119,7 +111,7 @@ theorem IsRejectionCert.not_accepts (hT : a.IsRejectionCert input T) :
     ¬ Acceptor.Accepts a input := by
   rintro ⟨μs, c, ⟨hstart, hpos, hinput⟩, c', ⟨hacc, hlast⟩, hmtr⟩
   obtain ⟨hinput', hmem⟩ := LTS.mtrInv_of_trInv hT.step_closed c μs c' hmtr
-    ⟨hinput, by rw [hpos]; simpa using hT.start_mem c.state hstart⟩
+    ⟨hinput, by simpa [hpos] using hT.start_mem c.state hstart⟩
   rw [hlast, Fin.val_last, hinput'] at hmem
   exact hT.accept_notMem c'.state hmem hacc
 
@@ -141,7 +133,7 @@ theorem isRejectionCert_reachable (h : ¬ Acceptor.Accepts a input) :
     rintro ⟨hc_input, c₀, hstart, hlt, hreach⟩
     have hc'_input : c'.input = input := a.toCfgNAFinAcc_input_eq input c μ c' htr hc_input
     rw [TwoWayNACfg.eta hc_input hlt] at hreach
-    refine ⟨hc'_input, c₀, hstart, by rw [← hc'_input]; exact c'.pos.isLt, ?_⟩
+    refine ⟨hc'_input, c₀, hstart, hc'_input ▸ c'.pos.isLt, ?_⟩
     rw [TwoWayNACfg.eta hc'_input]
     exact (LTS.reflTransGen_unlabelledTr_iff _).mp
       (((LTS.reflTransGen_unlabelledTr_iff _).mpr hreach).tail ⟨μ, htr⟩)
@@ -197,23 +189,23 @@ theorem isStepClosed_iff_localOK :
     have hthis := hloc ⟨(c.pos : ℕ), hlt⟩ c.state hmem m c'.state htr
     cases m with
     | zero =>
-      rw [show (c'.pos : ℕ) = (c.pos : ℕ) by simp at hpos; omega]
-      exact hthis
+      have hpos' : (c'.pos : ℕ) = (c.pos : ℕ) := by simp at hpos; omega
+      rwa [hpos']
     | pos =>
-      rw [show (c'.pos : ℕ) = (c.pos : ℕ) + 1 by simp at hpos; omega]
-      exact hthis
+      have hpos' : (c'.pos : ℕ) = (c.pos : ℕ) + 1 := by simp at hpos; omega
+      rwa [hpos']
     | neg =>
       simp only [SignType.neg_eq_neg_one, SignType.coe_neg_one] at hpos
       obtain ⟨j, hj⟩ : ∃ j, (c.pos : ℕ) = j + 1 := ⟨(c.pos : ℕ) - 1, by omega⟩
-      rw [show (c'.pos : ℕ) = j by omega]
-      rw [show ((⟨(c.pos : ℕ), hlt⟩ : Fin input.length) : ℕ) = j + 1 from hj] at hthis
-      exact hthis
+      have hpos' : (c'.pos : ℕ) = j := by omega
+      rw [hpos']
+      rwa [show ((⟨(c.pos : ℕ), hlt⟩ : Fin input.length) : ℕ) = j + 1 from hj] at hthis
 
-/-! ## The one-way automaton for the complement -/
+/-! ## The finite acceptor for the complement -/
 
-/-- The one-way automaton that guesses a rejection certificate `T` for `a` while scanning the
-input, keeping the pair `(T (i - 1), T i)` in its state after reading `i` symbols. Reading the
-symbol at position `i` guesses `T (i + 1)` and checks local consistency at position `i`. -/
+/-- The nondeterministic finite acceptor that guesses a rejection certificate `T` for `a` while
+scanning the input, keeping the pair `(T (i - 1), T i)` in its state after reading `i` symbols.
+Reading the symbol at position `i` guesses `T (i + 1)` and checks local consistency at `i`. -/
 def toNAComplement (a : TwoWayNA State Symbol) : NA.FinAcc (Set State × Set State) Symbol where
   Tr PC x PC' := PC'.1 = PC.2 ∧ a.LocalOK x PC.1 PC.2 PC'.2
   start := {PC | PC.1 = Set.univ ∧ a.start ⊆ PC.2}
@@ -235,7 +227,7 @@ theorem exists_accepting_mTr_iff (a : TwoWayNA State Symbol) (xs : List Symbol)
       subst hmtr
       exact ⟨[P, C], by simp, by simp, by simp, by simpa [toNAComplement] using hf⟩
     · rintro ⟨T, h0, h1, -, hacc⟩
-      exact ⟨(P, C), by rw [← h1]; simpa [toNAComplement] using hacc, by simp⟩
+      exact ⟨(P, C), by simpa [toNAComplement, ← h1] using hacc, by simp⟩
   | cons x xs ih =>
     constructor
     · rintro ⟨f, hf, hmtr⟩
@@ -248,7 +240,7 @@ theorem exists_accepting_mTr_iff (a : TwoWayNA State Symbol) (xs : List Symbol)
             ((P :: T).getI i) ((P :: T).getI (i + 1)) ((P :: T).getI (i + 2)) := by
         intro i hi
         obtain _ | i := i
-        · simpa [h0, h1] using hlocal'
+        · simpa [h0, h1] using hlocal
         · simpa using hloc i (by simpa using hi)
       exact ⟨P :: T, by simp, by simpa using h0, hstep, by simpa using hacc⟩
     · rintro ⟨T, h0, h1, hloc, hacc⟩
@@ -311,16 +303,15 @@ theorem accepts_toNAComplement_iff (a : TwoWayNA State Symbol) (input : List Sym
           ((certToList input T).getI (i + 2)) := by
       intro i hi
       have e0 : (certToList input T).getI i = prevSet T i := by
-        obtain _ | j := i
-        · rfl
-        · exact getI_certToList (by omega)
+        cases i with
+        | zero => rfl
+        | succ j => exact getI_certToList (by omega)
       have e1 : (certToList input T).getI (i + 1) = T i := getI_certToList (by omega)
       have e2 : (certToList input T).getI (i + 2) = T (i + 1) := getI_certToList (by omega)
-      rw [e0, e1, e2]
-      exact hloc ⟨i, hi⟩
+      simpa [e0, e1, e2] using hloc ⟨i, hi⟩
     obtain ⟨f, hf, hmtr⟩ := (exists_accepting_mTr_iff a input Set.univ (T 0)).mpr
       ⟨certToList input T, rfl, getI_certToList (by omega), hstep,
-        by rw [getI_certToList (by omega)]; exact hT.accept_notMem⟩
+        by simpa using hT.accept_notMem⟩
     exact ⟨(Set.univ, T 0), ⟨rfl, hT.start_mem⟩, f, hf, hmtr⟩
 
 /-- `a.toNAComplement` recognises the complement of the language of `a`. -/
@@ -332,111 +323,4 @@ theorem language_toNAComplement (a : TwoWayNA State Symbol) :
 
 end TwoWayNA
 
-/-! ## One-way automata as two-way automata -/
-
-namespace NA.FinAcc
-
-variable {n : NA.FinAcc State Symbol}
-
-/-- The two-way automaton that performs the transitions of `n`, always moving its head one symbol
-to the right. -/
-def toTwoWayNA (n : NA.FinAcc State Symbol) : TwoWayNA State Symbol where
-  Tr q x m q' := m = SignType.pos ∧ n.Tr q x q'
-  start := n.start
-  accept := n.accept
-
-/-- A run of `n.toTwoWayNA` starting on `input` reads a multistep transition of `n` over the
-prefix of `input` scanned so far. -/
-theorem mTr_take_of_canReach {s : State} {c c' : TwoWayNACfg State Symbol}
-    (hreach : (n.toTwoWayNA.toCfgNAFinAcc input).CanReach c c') (hc : c.input = input)
-    (hmtr : n.MTr s (input.take c.pos) c.state) :
-    c'.input = input ∧ n.MTr s (input.take c'.pos) c'.state := by
-  obtain ⟨μs, hreach⟩ := hreach
-  refine LTS.mtrInv_of_trInv
-    (p := fun d => d.input = input ∧ n.MTr s (input.take d.pos) d.state) ?_ c μs c' hreach
-    ⟨hc, hmtr⟩
-  rintro d ⟨x, m⟩ d' hstep ⟨hd, hmtr⟩
-  obtain ⟨hlt, rfl⟩ := TwoWayNA.getElem_of_tr hstep hd
-  obtain ⟨hinput, -, ⟨rfl, htr⟩, hpos⟩ := hstep
-  refine ⟨by rw [← hinput, hd], ?_⟩
-  rw [show (d'.pos : ℕ) = (d.pos : ℕ) + 1 by simp at hpos; omega,
-    List.take_succ_eq_append_getElem hlt]
-  exact LTS.MTr.stepR _ hmtr htr
-
-/-- A multistep transition of `n` over the part of `input` that starts at position `p` is read by
-a run of `n.toTwoWayNA` taking its head from `p` to the end of the input. -/
-theorem canReach_of_mTr {suf : List Symbol} {s s' : State} {p : ℕ}
-    (hp : p < input.length + 1) (hdrop : input.drop p = suf) (hmtr : n.MTr s suf s') :
-    (n.toTwoWayNA.toCfgNAFinAcc input).CanReach ⟨input, s, ⟨p, hp⟩⟩ ⟨input, s', Fin.last _⟩ := by
-  induction suf generalizing s p with
-  | nil =>
-    rw [LTS.MTr.nil_iff] at hmtr
-    subst hmtr
-    obtain rfl : p = input.length := by grind [List.drop_eq_nil_iff]
-    exact LTS.CanReach.refl _ _
-  | cons x xs ih =>
-    rw [LTS.MTr.cons_iff] at hmtr
-    obtain ⟨t, htr, hmtr⟩ := hmtr
-    have hlt : p < input.length := by
-      by_contra hc
-      grind [List.drop_eq_nil_iff]
-    have hx : input[p]'hlt = x := by
-      have h0 : (input.drop p)[0]? = some x := by rw [hdrop]; simp
-      grind
-    have hdrop' : input.drop (p + 1) = xs := by simp [← List.tail_drop, hdrop]
-    have hstep : (n.toTwoWayNA.toCfgNAFinAcc input).Tr
-        ⟨input, s, ⟨p, hp⟩⟩ (x, SignType.pos) ⟨input, t, ⟨p + 1, by omega⟩⟩ :=
-      ⟨rfl, by rw [← hx]; simp, ⟨rfl, htr⟩, by simp⟩
-    obtain ⟨μs, hmtr'⟩ := ih (by omega) hdrop' hmtr
-    exact ⟨(x, SignType.pos) :: μs, LTS.MTr.cons_iff.mpr ⟨_, hstep, hmtr'⟩⟩
-
-/-- A one-way automaton and its two-way rendering accept the same words. -/
-theorem accepts_toTwoWayNA_iff (n : NA.FinAcc State Symbol) (input : List Symbol) :
-    Acceptor.Accepts n.toTwoWayNA input ↔ Acceptor.Accepts n input := by
-  constructor
-  · rintro ⟨μs, c, ⟨hs, hpos, hinput⟩, c', ⟨hacc, hlast⟩, hmtr⟩
-    have hstart : n.MTr c.state (input.take c.pos) c.state := by
-      rw [hpos]
-      simp
-    obtain ⟨hinput', hmtr⟩ := mTr_take_of_canReach ⟨μs, hmtr⟩ hinput hstart
-    rw [hlast, Fin.val_last, hinput', List.take_length] at hmtr
-    exact ⟨c.state, hs, c'.state, hacc, hmtr⟩
-  · rintro ⟨s, hs, s', hs', hmtr⟩
-    obtain ⟨μs, hmtr⟩ :=
-      canReach_of_mTr (suf := input) (by omega) List.drop_zero hmtr
-    exact ⟨μs, ⟨input, s, ⟨0, by omega⟩⟩, ⟨hs, Fin.ext (by simp), rfl⟩,
-      ⟨input, s', Fin.last _⟩, ⟨hs', rfl⟩, hmtr⟩
-
-/-- A one-way automaton and its two-way rendering recognise the same language. -/
-theorem language_toTwoWayNA (n : NA.FinAcc State Symbol) :
-    Acceptor.language n.toTwoWayNA = Acceptor.language n := by
-  ext xs
-  simp only [Acceptor.mem_language]
-  exact accepts_toTwoWayNA_iff n xs
-
-end NA.FinAcc
-
 end Cslib.Automata
-
-namespace Cslib.Language
-
-open Automata Acceptor
-
-/-- A language is regular if and only if it is accepted by some two-way nondeterministic
-automaton with finitely many states. -/
-theorem IsRegular.iff_twoWayNA {Symbol : Type*} {l : Language Symbol} :
-    l.IsRegular ↔ ∃ State : Type, ∃ _ : Finite State,
-      ∃ a : Automata.TwoWayNA State Symbol, language a = l := by
-  constructor
-  · intro h
-    rw [IsRegular.iff_nfa] at h
-    obtain ⟨State, hfin, na, rfl⟩ := h
-    exact ⟨State, hfin, na.toTwoWayNA, na.language_toTwoWayNA⟩
-  · rintro ⟨State, hfin, a, rfl⟩
-    have := hfin
-    have hc : (language a)ᶜ.IsRegular := by
-      rw [IsRegular.iff_nfa]
-      exact ⟨Set State × Set State, inferInstance, a.toNAComplement, a.language_toNAComplement⟩
-    simpa using hc.compl
-
-end Cslib.Language

From eea48873afc1f94420bea525c00c09d63462a0aa Mon Sep 17 00:00:00 2001
From: crei <crei.github@gmail.com>
Date: Thu, 10 Sep 2026 12:19:52 +0200
Subject: [PATCH 04/13] Remove text in basic.

---
 Cslib/Computability/Automata/TwoWayNA/Basic.lean | 4 ----
 1 file changed, 4 deletions(-)

diff --git a/Cslib/Computability/Automata/TwoWayNA/Basic.lean b/Cslib/Computability/Automata/TwoWayNA/Basic.lean
index 78d491818..d34539e45 100644
--- a/Cslib/Computability/Automata/TwoWayNA/Basic.lean
+++ b/Cslib/Computability/Automata/TwoWayNA/Basic.lean
@@ -30,10 +30,6 @@ ends in an accepting state with the head just past the end of the input.
 * `TwoWayNA.toCfgNAFinAcc`, the finite acceptor on configurations whose runs on a fixed input are
   the runs of the two-way automaton on that input. It also provides the `Acceptor` instance.
 
-The comparison with finite acceptors is in `Cslib.Computability.Automata.TwoWayNA.ToNA`,
-`Cslib.Computability.Automata.TwoWayNA.OfNA` and
-`Cslib.Computability.Automata.TwoWayNA.Regular`.
-
 ## Implementation notes
 
 The definition of `TwoWayNA` is kept close to [Vardi][Vardi1989]'s, because the main point is to

From c035971026d622e414d774c109a239400104ba90 Mon Sep 17 00:00:00 2001
From: crei <crei.github@gmail.com>
Date: Fri, 11 Sep 2026 13:26:29 +0200
Subject: [PATCH 05/13] Rename toCfgNAFinAcc to toCfgNA

---
 Cslib/Computability/Automata/TwoWayNA/Basic.lean | 16 ++++++++--------
 Cslib/Computability/Automata/TwoWayNA/OfNA.lean  |  6 +++---
 Cslib/Computability/Automata/TwoWayNA/ToNA.lean  |  8 ++++----
 3 files changed, 15 insertions(+), 15 deletions(-)

diff --git a/Cslib/Computability/Automata/TwoWayNA/Basic.lean b/Cslib/Computability/Automata/TwoWayNA/Basic.lean
index d34539e45..930fc62cd 100644
--- a/Cslib/Computability/Automata/TwoWayNA/Basic.lean
+++ b/Cslib/Computability/Automata/TwoWayNA/Basic.lean
@@ -27,7 +27,7 @@ ends in an accepting state with the head just past the end of the input.
 
 * `TwoWayNA`, the automaton itself
 * `TwoWayNACfg`, a configuration of a `TwoWayNA`: Its input plus a state and the head position.
-* `TwoWayNA.toCfgNAFinAcc`, the finite acceptor on configurations whose runs on a fixed input are
+* `TwoWayNA.toCfgNA`, the finite acceptor on configurations whose runs on a fixed input are
   the runs of the two-way automaton on that input. It also provides the `Acceptor` instance.
 
 ## Implementation notes
@@ -85,7 +85,7 @@ def TwoWayNACfg.IsAccepting (a : TwoWayNA State Symbol) (c : TwoWayNACfg State S
 
 /-- Returns a nondeterministic finite acceptor on the configurations as states, accepting exactly
 the runs of the two-way automaton on `input` that end in an accepting configuration. -/
-def TwoWayNA.toCfgNAFinAcc {State Symbol : Type*} (a : TwoWayNA State Symbol)
+def TwoWayNA.toCfgNA {State Symbol : Type*} (a : TwoWayNA State Symbol)
     (input : List Symbol) :
     NA.FinAcc (TwoWayNACfg State Symbol) (Symbol × SignType) where
   Tr
@@ -102,12 +102,12 @@ def TwoWayNA.toCfgNAFinAcc {State Symbol : Type*} (a : TwoWayNA State Symbol)
   start := { c | c.IsInitialForInput a input }
   accept := { c | c.IsAccepting a }
 
-/-- Any reachable state of `a.toCfgNAFinAcc input` contains the original input. -/
-lemma TwoWayNA.toCfgNAFinAcc_input_eq {State Symbol : Type*} (a : TwoWayNA State Symbol)
+/-- Any reachable state of `a.toCfgNA input` contains the original input. -/
+lemma TwoWayNA.toCfgNA_input_eq {State Symbol : Type*} (a : TwoWayNA State Symbol)
     (input : List Symbol) :
-    (a.toCfgNAFinAcc input).toLTS.TrInv (fun c => c.input = input) := by
+    (a.toCfgNA input).toLTS.TrInv (fun c => c.input = input) := by
   intro c μ c' h_tr rfl
-  simp_all [TwoWayNA.toCfgNAFinAcc]
+  simp_all [TwoWayNA.toCfgNA]
 
 /-- A configuration running on `input` is the one determined by its state and head position. -/
 theorem TwoWayNACfg.eta {input : List Symbol} {c : TwoWayNACfg State Symbol}
@@ -120,7 +120,7 @@ theorem TwoWayNACfg.eta {input : List Symbol} {c : TwoWayNACfg State Symbol}
 /-- A step reads the symbol at the head position, which therefore lies inside the input. -/
 theorem TwoWayNA.getElem_of_tr {a : TwoWayNA State Symbol} {input : List Symbol}
     {c c' : TwoWayNACfg State Symbol} {x : Symbol} {m : SignType}
-    (htr : (a.toCfgNAFinAcc input).Tr c (x, m) c') (hc : c.input = input) :
+    (htr : (a.toCfgNA input).Tr c (x, m) c') (hc : c.input = input) :
     ∃ h : (c.pos : ℕ) < input.length, input[(c.pos : ℕ)] = x := by
   obtain ⟨-, hx, -, -⟩ := htr
   subst hc
@@ -129,6 +129,6 @@ theorem TwoWayNA.getElem_of_tr {a : TwoWayNA State Symbol} {input : List Symbol}
 @[simp, scoped grind =]
 instance : Acceptor (TwoWayNA State Symbol) Symbol where
   Accepts (a : TwoWayNA State Symbol) (input : List Symbol) :=
-    ∃ μs, Acceptor.Accepts (a.toCfgNAFinAcc input) μs
+    ∃ μs, Acceptor.Accepts (a.toCfgNA input) μs
 
 end Cslib.Automata
diff --git a/Cslib/Computability/Automata/TwoWayNA/OfNA.lean b/Cslib/Computability/Automata/TwoWayNA/OfNA.lean
index 7051b0f14..d33e809b0 100644
--- a/Cslib/Computability/Automata/TwoWayNA/OfNA.lean
+++ b/Cslib/Computability/Automata/TwoWayNA/OfNA.lean
@@ -39,7 +39,7 @@ def ofNA (n : NA.FinAcc State Symbol) : TwoWayNA State Symbol where
 /-- A run of `ofNA n` starting on `input` reads a multistep transition of `n` over the prefix of
 `input` scanned so far. -/
 theorem mTr_take_of_canReach {s : State} {c c' : TwoWayNACfg State Symbol}
-    (hreach : ((ofNA n).toCfgNAFinAcc input).CanReach c c') (hc : c.input = input)
+    (hreach : ((ofNA n).toCfgNA input).CanReach c c') (hc : c.input = input)
     (hmtr : n.MTr s (input.take c.pos) c.state) :
     c'.input = input ∧ n.MTr s (input.take c'.pos) c'.state := by
   obtain ⟨μs, hreach⟩ := hreach
@@ -58,7 +58,7 @@ theorem mTr_take_of_canReach {s : State} {c c' : TwoWayNACfg State Symbol}
 run of `ofNA n` taking its head from `p` to the end of the input. -/
 theorem canReach_of_mTr {suf : List Symbol} {s s' : State} {p : ℕ}
     (hp : p < input.length + 1) (hdrop : input.drop p = suf) (hmtr : n.MTr s suf s') :
-    ((ofNA n).toCfgNAFinAcc input).CanReach ⟨input, s, ⟨p, hp⟩⟩ ⟨input, s', Fin.last _⟩ := by
+    ((ofNA n).toCfgNA input).CanReach ⟨input, s, ⟨p, hp⟩⟩ ⟨input, s', Fin.last _⟩ := by
   induction suf generalizing s p with
   | nil =>
     rw [LTS.MTr.nil_iff] at hmtr
@@ -73,7 +73,7 @@ theorem canReach_of_mTr {suf : List Symbol} {s s' : State} {p : ℕ}
       have h0 : (input.drop p)[0]? = some x := by simp [hdrop]
       grind
     have hdrop' : input.drop (p + 1) = xs := by simp [← List.tail_drop, hdrop]
-    have hstep : ((ofNA n).toCfgNAFinAcc input).Tr
+    have hstep : ((ofNA n).toCfgNA input).Tr
         ⟨input, s, ⟨p, hp⟩⟩ (x, SignType.pos) ⟨input, t, ⟨p + 1, by omega⟩⟩ :=
       ⟨rfl, by simp [← hx], ⟨rfl, htr⟩, by simp⟩
     obtain ⟨μs, hmtr'⟩ := ih (by omega) hdrop' hmtr
diff --git a/Cslib/Computability/Automata/TwoWayNA/ToNA.lean b/Cslib/Computability/Automata/TwoWayNA/ToNA.lean
index eb65afbb9..947629064 100644
--- a/Cslib/Computability/Automata/TwoWayNA/ToNA.lean
+++ b/Cslib/Computability/Automata/TwoWayNA/ToNA.lean
@@ -90,7 +90,7 @@ namespace TwoWayNA
 state that `T` attaches to the new head position. The conjunct on the input restricts the
 invariant to the configurations that run on `input`. -/
 def IsStepClosed (a : TwoWayNA State Symbol) (input : List Symbol) (T : ℕ → Set State) : Prop :=
-  (a.toCfgNAFinAcc input).TrInv (fun c => c.input = input ∧ c.state ∈ T c.pos)
+  (a.toCfgNA input).TrInv (fun c => c.input = input ∧ c.state ∈ T c.pos)
 
 /-- A family of subsets of the state set, one for every position of the input head on `input`,
 which contains all initial states, is closed under the transitions of `a`, and contains no
@@ -121,7 +121,7 @@ def reachable (a : TwoWayNA State Symbol) (input : List Symbol) (i : ℕ) :
     Set State :=
   {q | ∃ c, c.IsInitialForInput a input ∧
       ∃ h : i < input.length + 1,
-      (a.toCfgNAFinAcc input).CanReach c { input := input, pos := ⟨i, h⟩, state := q } }
+      (a.toCfgNA input).CanReach c { input := input, pos := ⟨i, h⟩, state := q } }
 
 /-- If `a` does not accept `input`, then its reachable states form a rejection certificate. -/
 theorem isRejectionCert_reachable (h : ¬ Acceptor.Accepts a input) :
@@ -131,7 +131,7 @@ theorem isRejectionCert_reachable (h : ¬ Acceptor.Accepts a input) :
       ⟨hs, Fin.ext (by simp), rfl⟩, Nat.succ_pos _, LTS.CanReach.refl _ _⟩
   step_closed c μ c' htr := by
     rintro ⟨hc_input, c₀, hstart, hlt, hreach⟩
-    have hc'_input : c'.input = input := a.toCfgNAFinAcc_input_eq input c μ c' htr hc_input
+    have hc'_input : c'.input = input := a.toCfgNA_input_eq input c μ c' htr hc_input
     rw [TwoWayNACfg.eta hc_input hlt] at hreach
     refine ⟨hc'_input, c₀, hstart, hc'_input ▸ c'.pos.isLt, ?_⟩
     rw [TwoWayNACfg.eta hc'_input]
@@ -183,7 +183,7 @@ theorem isStepClosed_iff_localOK :
       · exact (hcl ⟨input, q, ⟨j + 1, by omega⟩⟩ (input[j + 1], SignType.neg)
           ⟨input, q', ⟨j, by omega⟩⟩ ⟨rfl, by simp, htr, by simp⟩ ⟨rfl, hq⟩).2
   · rintro hloc c ⟨x, m⟩ c' hstep ⟨hc_input, hmem⟩
-    refine ⟨a.toCfgNAFinAcc_input_eq input c (x, m) c' hstep hc_input, ?_⟩
+    refine ⟨a.toCfgNA_input_eq input c (x, m) c' hstep hc_input, ?_⟩
     obtain ⟨hlt, rfl⟩ := getElem_of_tr hstep hc_input
     obtain ⟨-, -, htr, hpos⟩ := hstep
     have hthis := hloc ⟨(c.pos : ℕ), hlt⟩ c.state hmem m c'.state htr

From b4c8c1ea713792516ed9dce666115679650a34f9 Mon Sep 17 00:00:00 2001
From: crei <crei.github@gmail.com>
Date: Fri, 11 Sep 2026 13:31:24 +0200
Subject: [PATCH 06/13] Move acceptor instance.

---
 Cslib/Computability/Automata/TwoWayNA/Basic.lean | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/Cslib/Computability/Automata/TwoWayNA/Basic.lean b/Cslib/Computability/Automata/TwoWayNA/Basic.lean
index 930fc62cd..edd70a119 100644
--- a/Cslib/Computability/Automata/TwoWayNA/Basic.lean
+++ b/Cslib/Computability/Automata/TwoWayNA/Basic.lean
@@ -102,10 +102,15 @@ def TwoWayNA.toCfgNA {State Symbol : Type*} (a : TwoWayNA State Symbol)
   start := { c | c.IsInitialForInput a input }
   accept := { c | c.IsAccepting a }
 
+@[simp, scoped grind =]
+instance : Acceptor (TwoWayNA State Symbol) Symbol where
+  Accepts (a : TwoWayNA State Symbol) (input : List Symbol) :=
+    ∃ μs, Acceptor.Accepts (a.toCfgNA input) μs
+
 /-- Any reachable state of `a.toCfgNA input` contains the original input. -/
 lemma TwoWayNA.toCfgNA_input_eq {State Symbol : Type*} (a : TwoWayNA State Symbol)
     (input : List Symbol) :
-    (a.toCfgNA input).toLTS.TrInv (fun c => c.input = input) := by
+    (a.toCfgNA input).TrInv (fun c => c.input = input) := by
   intro c μ c' h_tr rfl
   simp_all [TwoWayNA.toCfgNA]
 
@@ -126,9 +131,4 @@ theorem TwoWayNA.getElem_of_tr {a : TwoWayNA State Symbol} {input : List Symbol}
   subst hc
   exact List.getElem?_eq_some_iff.mp hx.symm
 
-@[simp, scoped grind =]
-instance : Acceptor (TwoWayNA State Symbol) Symbol where
-  Accepts (a : TwoWayNA State Symbol) (input : List Symbol) :=
-    ∃ μs, Acceptor.Accepts (a.toCfgNA input) μs
-
 end Cslib.Automata

From ffdac59fee4c7450e33793eab8f25f85354101c1 Mon Sep 17 00:00:00 2001
From: crei <crei.github@gmail.com>
Date: Fri, 11 Sep 2026 14:30:11 +0200
Subject: [PATCH 07/13] Review comments for OfNA.lean.

---
 .../Computability/Automata/TwoWayNA/OfNA.lean | 113 +++++++++---------
 .../Automata/TwoWayNA/Regular.lean            |   4 +-
 2 files changed, 59 insertions(+), 58 deletions(-)

diff --git a/Cslib/Computability/Automata/TwoWayNA/OfNA.lean b/Cslib/Computability/Automata/TwoWayNA/OfNA.lean
index d33e809b0..5a556b013 100644
--- a/Cslib/Computability/Automata/TwoWayNA/OfNA.lean
+++ b/Cslib/Computability/Automata/TwoWayNA/OfNA.lean
@@ -11,12 +11,13 @@ public import Cslib.Computability.Automata.TwoWayNA.Basic
 /-! # Finite acceptors as two-way automata
 
 A nondeterministic finite acceptor (`NA.FinAcc`) is the special case of a nondeterministic two-way
-automaton (`TwoWayNA`) that moves its head one symbol to the right in every step, `TwoWayNA.ofNA`.
+automaton (`TwoWayNA`) that moves its head one symbol to the right in every step,
+`NA.FinAcc.toTwoWayNA`.
 
-The head of `TwoWayNA.ofNA n` is thus at position `i` exactly when `n` has read the first `i`
+The head of `a.toTwoWayNA` is thus at position `i` exactly when `a` has read the first `i`
 symbols of the input, so the runs of the two-way automaton are in lockstep with the multistep
-transitions of `n` (`TwoWayNA.mTr_take_of_canReach`, `TwoWayNA.canReach_of_mTr`) and the two accept
-the same words (`TwoWayNA.accepts_ofNA_iff`, `TwoWayNA.language_ofNA`).
+transitions of `a` (`TwoWayNA.mTr_take_of_mTr_toCfgNA`, `TwoWayNA.mTr_toCfgNA_of_mTr`) and the two
+accept the same words (`TwoWayNA.accepts_toTwoWayNA_iff`, `TwoWayNA.language_toTwoWayNA`).
 -/
 
 @[expose] public section
@@ -25,80 +26,80 @@ namespace Cslib.Automata
 
 variable {State Symbol : Type*} {input : List Symbol}
 
-namespace TwoWayNA
-
-variable {n : NA.FinAcc State Symbol}
-
 /-- The two-way automaton that performs the transitions of the nondeterministic finite acceptor
 `n`, always moving its head one symbol to the right. -/
-def ofNA (n : NA.FinAcc State Symbol) : TwoWayNA State Symbol where
+def NA.FinAcc.toTwoWayNA (n : NA.FinAcc State Symbol) : TwoWayNA State Symbol where
   Tr q x m q' := m = SignType.pos ∧ n.Tr q x q'
   start := n.start
   accept := n.accept
 
-/-- A run of `ofNA n` starting on `input` reads a multistep transition of `n` over the prefix of
-`input` scanned so far. -/
-theorem mTr_take_of_canReach {s : State} {c c' : TwoWayNACfg State Symbol}
-    (hreach : ((ofNA n).toCfgNA input).CanReach c c') (hc : c.input = input)
-    (hmtr : n.MTr s (input.take c.pos) c.state) :
-    c'.input = input ∧ n.MTr s (input.take c'.pos) c'.state := by
-  obtain ⟨μs, hreach⟩ := hreach
-  refine LTS.mtrInv_of_trInv
-    (p := fun d => d.input = input ∧ n.MTr s (input.take d.pos) d.state) ?_ c μs c' hreach
-    ⟨hc, hmtr⟩
+namespace TwoWayNA
+
+variable {a : NA.FinAcc State Symbol}
+
+/-- A run of `a.toTwoWayNA` that starts in an initial configuration reads a multistep transition
+of `a` over the prefix of `input` that its head has scanned. -/
+theorem mTr_take_of_mTr_toCfgNA {c c' : TwoWayNACfg State Symbol}
+    {μs : List (Symbol × SignType)}
+    (hstart : c ∈ (a.toTwoWayNA.toCfgNA input).start)
+    (hrun : (a.toTwoWayNA.toCfgNA input).MTr c μs c') :
+    a.MTr c.state (input.take c'.pos) c'.state := by
+  obtain ⟨-, hpos, rfl⟩ := hstart
+  refine (LTS.mtrInv_of_trInv
+    (p := fun d => d.input = c.input ∧ a.MTr c.state (c.input.take d.pos) d.state) ?_ c μs c' hrun
+    ⟨rfl, by simp [hpos]⟩).2
   rintro d ⟨x, m⟩ d' hstep ⟨hd, hmtr⟩
-  obtain ⟨hlt, rfl⟩ := getElem_of_tr hstep hd
+  obtain ⟨hlt, rfl⟩ := getElem_of_tr (input := c.input) hstep hd
   obtain ⟨hinput, -, ⟨rfl, htr⟩, hpos⟩ := hstep
+  have hpos' : (d'.pos : ℕ) = (d.pos : ℕ) + 1 := by simp at hpos; omega
   refine ⟨hinput ▸ hd, ?_⟩
-  rw [show (d'.pos : ℕ) = (d.pos : ℕ) + 1 by simp at hpos; omega]
-  rw [List.take_succ_eq_append_getElem hlt]
+  rw [hpos', List.take_succ_eq_append_getElem hlt]
   exact LTS.MTr.stepR _ hmtr htr
 
-/-- A multistep transition of `n` over the part of `input` that starts at position `p` is read by a
-run of `ofNA n` taking its head from `p` to the end of the input. -/
-theorem canReach_of_mTr {suf : List Symbol} {s s' : State} {p : ℕ}
-    (hp : p < input.length + 1) (hdrop : input.drop p = suf) (hmtr : n.MTr s suf s') :
-    ((ofNA n).toCfgNA input).CanReach ⟨input, s, ⟨p, hp⟩⟩ ⟨input, s', Fin.last _⟩ := by
-  induction suf generalizing s p with
-  | nil =>
-    rw [LTS.MTr.nil_iff] at hmtr
-    subst hmtr
-    obtain rfl : p = input.length := by grind [List.drop_eq_nil_iff]
-    exact LTS.CanReach.refl _ _
-  | cons x xs ih =>
-    rw [LTS.MTr.cons_iff] at hmtr
-    obtain ⟨t, htr, hmtr⟩ := hmtr
-    have hlt : p < input.length := by grind [List.drop_eq_nil_iff]
-    have hx : input[p]'hlt = x := by
-      have h0 : (input.drop p)[0]? = some x := by simp [hdrop]
-      grind
-    have hdrop' : input.drop (p + 1) = xs := by simp [← List.tail_drop, hdrop]
-    have hstep : ((ofNA n).toCfgNA input).Tr
-        ⟨input, s, ⟨p, hp⟩⟩ (x, SignType.pos) ⟨input, t, ⟨p + 1, by omega⟩⟩ :=
+/-- A multistep transition of `a` over a prefix of `input` is read by the run of `a.toTwoWayNA`
+that takes its head from the beginning of the input to the end of that prefix, moving one symbol
+to the right in every step. -/
+theorem mTr_toCfgNA_of_mTr {s s' : State} {pre : List Symbol} (hpre : pre <+: input)
+    (hmtr : a.MTr s pre s') :
+    (a.toTwoWayNA.toCfgNA input).MTr ⟨input, s, 0⟩ (pre.map (·, SignType.pos))
+      ⟨input, s', ⟨pre.length, by grind⟩⟩ := by
+  induction pre using List.reverseRecOn generalizing s' with
+  | nil => simp_all
+  | append_singleton pre x ih =>
+    rw [LTS.MTr.append_iff] at hmtr
+    obtain ⟨t, hmtr, htr⟩ := hmtr
+    rw [LTS.MTr.singleton_iff] at htr
+    have hlt : pre.length < input.length := by grind
+    have hx : input[pre.length] = x := by
+      rw [← hpre.getElem (by simp)]
+      simp
+    have hstep : (a.toTwoWayNA.toCfgNA input).Tr
+        ⟨input, t, ⟨pre.length, by omega⟩⟩ (x, SignType.pos)
+        ⟨input, s', ⟨(pre ++ [x]).length, by simpa using hlt⟩⟩ :=
       ⟨rfl, by simp [← hx], ⟨rfl, htr⟩, by simp⟩
-    obtain ⟨μs, hmtr'⟩ := ih (by omega) hdrop' hmtr
-    exact ⟨(x, SignType.pos) :: μs, LTS.MTr.cons_iff.mpr ⟨_, hstep, hmtr'⟩⟩
+    rw [List.map_append]
+    exact LTS.MTr.stepR _ (ih ((List.prefix_append _ _).trans hpre) hmtr) hstep
+
+open Acceptor
 
 /-- A nondeterministic finite acceptor and its two-way rendering accept the same words. -/
-theorem accepts_ofNA_iff (a : NA.FinAcc State Symbol) (input : List Symbol) :
-    Acceptor.Accepts (ofNA a) input ↔ Acceptor.Accepts a input := by
+theorem accepts_toTwoWayNA_iff (a : NA.FinAcc State Symbol) (input : List Symbol) :
+    Accepts a.toTwoWayNA input ↔ Accepts a input := by
   constructor
   · rintro ⟨μs, c, ⟨hs, hpos, hinput⟩, c', ⟨hacc, hlast⟩, hmtr⟩
-    have hstart : a.MTr c.state (input.take c.pos) c.state := by simp [hpos]
-    obtain ⟨hinput', hmtr⟩ := mTr_take_of_canReach ⟨μs, hmtr⟩ hinput hstart
+    subst hinput
+    have hinput' := LTS.mtrInv_of_trInv (toCfgNA_input_eq _ _) c μs c' hmtr rfl
+    have hmtr := mTr_take_of_mTr_toCfgNA ⟨hs, hpos, rfl⟩ hmtr
     rw [hlast, Fin.val_last, hinput', List.take_length] at hmtr
     exact ⟨c.state, hs, c'.state, hacc, hmtr⟩
   · rintro ⟨s, hs, s', hs', hmtr⟩
-    obtain ⟨μs, hmtr⟩ :=
-      canReach_of_mTr (suf := input) (by omega) List.drop_zero hmtr
-    exact ⟨μs, ⟨input, s, ⟨0, by omega⟩⟩, ⟨hs, Fin.ext (by simp), rfl⟩,
-      ⟨input, s', Fin.last _⟩, ⟨hs', rfl⟩, hmtr⟩
+    exact ⟨_, ⟨input, s, 0⟩, ⟨hs, rfl, rfl⟩, ⟨input, s', Fin.last _⟩, ⟨hs', rfl⟩,
+      mTr_toCfgNA_of_mTr (List.prefix_refl _) hmtr⟩
 
 /-- A nondeterministic finite acceptor and its two-way rendering recognise the same language. -/
-theorem language_ofNA (a : NA.FinAcc State Symbol) :
-    Acceptor.language (ofNA a) = Acceptor.language a := by
+theorem language_toTwoWayNA (a : NA.FinAcc State Symbol) : language a.toTwoWayNA = language a := by
   ext xs
-  simpa [Acceptor.mem_language] using accepts_ofNA_iff a xs
+  simpa [Acceptor.mem_language] using accepts_toTwoWayNA_iff a xs
 
 end TwoWayNA
 
diff --git a/Cslib/Computability/Automata/TwoWayNA/Regular.lean b/Cslib/Computability/Automata/TwoWayNA/Regular.lean
index f235c2178..d7e94919c 100644
--- a/Cslib/Computability/Automata/TwoWayNA/Regular.lean
+++ b/Cslib/Computability/Automata/TwoWayNA/Regular.lean
@@ -12,7 +12,7 @@ public import Cslib.Computability.Languages.RegularLanguage
 
 /-! # Two-way automata recognise exactly the regular languages
 
-This is the combination of the results of `TwoWayNA.ofNA` and `TwoWayNA.toNAComplement`
+This is the combination of the results of `NA.FinAcc.toTwoWayNA` and `TwoWayNA.toNAComplement`
 plus the fact that regular languages are closed under complementation.
 -/
 
@@ -29,7 +29,7 @@ public theorem IsRegular.iff_twoWayNA {Symbol : Type*} {l : Language Symbol} :
   · intro h
     rw [IsRegular.iff_nfa] at h
     obtain ⟨State, hfin, na, rfl⟩ := h
-    exact ⟨State, hfin, TwoWayNA.ofNA na, TwoWayNA.language_ofNA na⟩
+    exact ⟨State, hfin, NA.FinAcc.toTwoWayNA na, TwoWayNA.language_toTwoWayNA na⟩
   · rintro ⟨State, hfin, a, rfl⟩
     have := hfin
     have hc : (language a)ᶜ.IsRegular := by

From aac671ab7f545b66da4baa14d110da2027b2f232 Mon Sep 17 00:00:00 2001
From: crei <crei.github@gmail.com>
Date: Fri, 11 Sep 2026 14:38:18 +0200
Subject: [PATCH 08/13] Move regular result to RegularLanguage.lean

---
 Cslib.lean                                    |  1 -
 .../Automata/TwoWayNA/Regular.lean            | 40 -------------------
 .../Languages/RegularLanguage.lean            | 19 +++++++++
 3 files changed, 19 insertions(+), 41 deletions(-)
 delete mode 100644 Cslib/Computability/Automata/TwoWayNA/Regular.lean

diff --git a/Cslib.lean b/Cslib.lean
index 3b06f1c9c..2fa58466d 100644
--- a/Cslib.lean
+++ b/Cslib.lean
@@ -30,7 +30,6 @@ public import Cslib.Computability.Automata.NA.Total
 public import Cslib.Computability.Automata.Transducers.Transducer
 public import Cslib.Computability.Automata.TwoWayNA.Basic
 public import Cslib.Computability.Automata.TwoWayNA.OfNA
-public import Cslib.Computability.Automata.TwoWayNA.Regular
 public import Cslib.Computability.Automata.TwoWayNA.ToNA
 public import Cslib.Computability.Circuit.Basic
 public import Cslib.Computability.Circuit.Homomorphism
diff --git a/Cslib/Computability/Automata/TwoWayNA/Regular.lean b/Cslib/Computability/Automata/TwoWayNA/Regular.lean
deleted file mode 100644
index d7e94919c..000000000
--- a/Cslib/Computability/Automata/TwoWayNA/Regular.lean
+++ /dev/null
@@ -1,40 +0,0 @@
-/-
-Copyright (c) 2026 Christian Reitwiessner. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Christian Reitwiessner
--/
-
-module
-
-public import Cslib.Computability.Automata.TwoWayNA.OfNA
-public import Cslib.Computability.Automata.TwoWayNA.ToNA
-public import Cslib.Computability.Languages.RegularLanguage
-
-/-! # Two-way automata recognise exactly the regular languages
-
-This is the combination of the results of `NA.FinAcc.toTwoWayNA` and `TwoWayNA.toNAComplement`
-plus the fact that regular languages are closed under complementation.
--/
-
-namespace Cslib.Language
-
-open Automata Acceptor
-
-/-- A language is regular if and only if it is accepted by some two-way nondeterministic
-automaton with finitely many states. -/
-public theorem IsRegular.iff_twoWayNA {Symbol : Type*} {l : Language Symbol} :
-    l.IsRegular ↔ ∃ State : Type, ∃ _ : Finite State,
-      ∃ a : Automata.TwoWayNA State Symbol, language a = l := by
-  constructor
-  · intro h
-    rw [IsRegular.iff_nfa] at h
-    obtain ⟨State, hfin, na, rfl⟩ := h
-    exact ⟨State, hfin, NA.FinAcc.toTwoWayNA na, TwoWayNA.language_toTwoWayNA na⟩
-  · rintro ⟨State, hfin, a, rfl⟩
-    have := hfin
-    have hc : (language a)ᶜ.IsRegular := by
-      rw [IsRegular.iff_nfa]
-      exact ⟨Set State × Set State, inferInstance, a.toNAComplement, a.language_toNAComplement⟩
-    simpa using hc.compl
-
-end Cslib.Language
diff --git a/Cslib/Computability/Languages/RegularLanguage.lean b/Cslib/Computability/Languages/RegularLanguage.lean
index ae70a9fee..a99107605 100644
--- a/Cslib/Computability/Languages/RegularLanguage.lean
+++ b/Cslib/Computability/Languages/RegularLanguage.lean
@@ -14,6 +14,8 @@ public import Cslib.Computability.Automata.DA.Prod
 public import Cslib.Computability.Automata.NA.Reverse
 public import Cslib.Computability.Automata.NA.ToDA
 public import Cslib.Computability.Automata.DA.ToNA
+public import Cslib.Computability.Automata.TwoWayNA.OfNA
+public import Cslib.Computability.Automata.TwoWayNA.ToNA
 public import Mathlib.Computability.DFA
 public import Mathlib.Computability.RegularExpressions
 public import Mathlib.Basic.Finite.Sum
@@ -70,6 +72,23 @@ theorem IsRegular.compl {l : Language Symbol} (h : l.IsRegular) : (lᶜ).IsRegul
   simp only [language, Accepts]
   rfl
 
+/-- A language is regular if and only if it is accepted by some two-way nondeterministic
+automaton with finitely many states. -/
+theorem IsRegular.iff_twoWayNA {l : Language Symbol} :
+    l.IsRegular ↔ ∃ State : Type, ∃ _ : Finite State,
+      ∃ a : TwoWayNA State Symbol, language a = l := by
+  constructor
+  · intro h
+    rw [IsRegular.iff_nfa] at h
+    obtain ⟨State, hfin, na, rfl⟩ := h
+    exact ⟨State, hfin, NA.FinAcc.toTwoWayNA na, TwoWayNA.language_toTwoWayNA na⟩
+  · rintro ⟨State, hfin, a, rfl⟩
+    have := hfin
+    have hc : (language a)ᶜ.IsRegular := by
+      rw [IsRegular.iff_nfa]
+      exact ⟨Set State × Set State, inferInstance, a.toNAComplement, a.language_toNAComplement⟩
+    simpa using hc.compl
+
 /-- The empty language is regular. -/
 @[simp]
 theorem IsRegular.zero : (0 : Language Symbol).IsRegular := by

From 5ffdfe315689acb06061f3a88fae99881dd8b40e Mon Sep 17 00:00:00 2001
From: crei <crei.github@gmail.com>
Date: Fri, 11 Sep 2026 14:42:05 +0200
Subject: [PATCH 09/13] Rename ToNA.lean to ComplToNA.lean.

---
 Cslib.lean                                                      | 2 +-
 .../Automata/TwoWayNA/{ToNA.lean => ComplToNA.lean}             | 0
 Cslib/Computability/Languages/RegularLanguage.lean              | 2 +-
 3 files changed, 2 insertions(+), 2 deletions(-)
 rename Cslib/Computability/Automata/TwoWayNA/{ToNA.lean => ComplToNA.lean} (100%)

diff --git a/Cslib.lean b/Cslib.lean
index 2fa58466d..0c4dab5e5 100644
--- a/Cslib.lean
+++ b/Cslib.lean
@@ -29,8 +29,8 @@ public import Cslib.Computability.Automata.NA.ToDA
 public import Cslib.Computability.Automata.NA.Total
 public import Cslib.Computability.Automata.Transducers.Transducer
 public import Cslib.Computability.Automata.TwoWayNA.Basic
+public import Cslib.Computability.Automata.TwoWayNA.ComplToNA
 public import Cslib.Computability.Automata.TwoWayNA.OfNA
-public import Cslib.Computability.Automata.TwoWayNA.ToNA
 public import Cslib.Computability.Circuit.Basic
 public import Cslib.Computability.Circuit.Homomorphism
 public import Cslib.Computability.Circuit.Program
diff --git a/Cslib/Computability/Automata/TwoWayNA/ToNA.lean b/Cslib/Computability/Automata/TwoWayNA/ComplToNA.lean
similarity index 100%
rename from Cslib/Computability/Automata/TwoWayNA/ToNA.lean
rename to Cslib/Computability/Automata/TwoWayNA/ComplToNA.lean
diff --git a/Cslib/Computability/Languages/RegularLanguage.lean b/Cslib/Computability/Languages/RegularLanguage.lean
index a99107605..91d3d5a68 100644
--- a/Cslib/Computability/Languages/RegularLanguage.lean
+++ b/Cslib/Computability/Languages/RegularLanguage.lean
@@ -15,7 +15,7 @@ public import Cslib.Computability.Automata.NA.Reverse
 public import Cslib.Computability.Automata.NA.ToDA
 public import Cslib.Computability.Automata.DA.ToNA
 public import Cslib.Computability.Automata.TwoWayNA.OfNA
-public import Cslib.Computability.Automata.TwoWayNA.ToNA
+public import Cslib.Computability.Automata.TwoWayNA.ComplToNA
 public import Mathlib.Computability.DFA
 public import Mathlib.Computability.RegularExpressions
 public import Mathlib.Basic.Finite.Sum

From 7ed37aa74327c6ba60859486927b641b00fe84a4 Mon Sep 17 00:00:00 2001
From: crei <crei.github@gmail.com>
Date: Fri, 11 Sep 2026 14:45:02 +0200
Subject: [PATCH 10/13] Rename toNAComplement.

---
 .../Automata/TwoWayNA/ComplToNA.lean          | 32 +++++++++----------
 .../Languages/RegularLanguage.lean            |  2 +-
 2 files changed, 17 insertions(+), 17 deletions(-)

diff --git a/Cslib/Computability/Automata/TwoWayNA/ComplToNA.lean b/Cslib/Computability/Automata/TwoWayNA/ComplToNA.lean
index 947629064..42d1fea82 100644
--- a/Cslib/Computability/Automata/TwoWayNA/ComplToNA.lean
+++ b/Cslib/Computability/Automata/TwoWayNA/ComplToNA.lean
@@ -14,7 +14,7 @@ public import Cslib.Foundations.Semantics.LTS.Relation
 
 For every nondeterministic two-way automaton (`TwoWayNA`) `a`, this file constructs a
 nondeterministic finite acceptor (`NA.FinAcc`) that accepts exactly the words rejected by `a`
-(`TwoWayNA.toNAComplement`, `TwoWayNA.language_toNAComplement`). We follow Vardi's proof, which --
+(`TwoWayNA.complToNA`, `TwoWayNA.language_complToNA`). We follow Vardi's proof, which --
 unlike Shepherdson's crossing-sequence argument -- characterises non-acceptance in a way that can
 be checked by a single left-to-right sweep over the input.
 
@@ -46,8 +46,8 @@ holds at the end of every run (`LTS.mtrInv_of_trInv`). Conversely, the reachable
 The point of the reformulation is locality: `TwoWayNA.isStepClosed_iff_localOK` turns condition 2
 into a condition `TwoWayNA.LocalOK` relating only `T (i - 1)`, `T i` and `T (i + 1)` with the
 symbol at position `i`. A finite acceptor can therefore guess the certificate while scanning the
-input, keeping only the last two subsets in its state. This is `TwoWayNA.toNAComplement`, and
-`TwoWayNA.accepts_toNAComplement_iff` shows that it accepts exactly the words rejected by `a`.
+input, keeping only the last two subsets in its state. This is `TwoWayNA.complToNA`, and
+`TwoWayNA.accepts_complToNA_iff` shows that it accepts exactly the words rejected by `a`.
 
 ## Implementation notes
 
@@ -206,16 +206,16 @@ theorem isStepClosed_iff_localOK :
 /-- The nondeterministic finite acceptor that guesses a rejection certificate `T` for `a` while
 scanning the input, keeping the pair `(T (i - 1), T i)` in its state after reading `i` symbols.
 Reading the symbol at position `i` guesses `T (i + 1)` and checks local consistency at `i`. -/
-def toNAComplement (a : TwoWayNA State Symbol) : NA.FinAcc (Set State × Set State) Symbol where
+def complToNA (a : TwoWayNA State Symbol) : NA.FinAcc (Set State × Set State) Symbol where
   Tr PC x PC' := PC'.1 = PC.2 ∧ a.LocalOK x PC.1 PC.2 PC'.2
   start := {PC | PC.1 = Set.univ ∧ a.start ⊆ PC.2}
   accept := {PC | ∀ s ∈ PC.2, s ∉ a.accept}
 
-/-- An accepting multistep transition of `a.toNAComplement` out of `(P, C)` over `xs` is the same
+/-- An accepting multistep transition of `a.complToNA` out of `(P, C)` over `xs` is the same
 thing as a list of subsets starting with `P` and `C` that is locally consistent at every position
 of `xs` and ends in a subset without accepting states. -/
 theorem exists_accepting_mTr_iff (a : TwoWayNA State Symbol) (xs : List Symbol) (P C : Set State) :
-    (∃ f ∈ a.toNAComplement.accept, a.toNAComplement.MTr (P, C) xs f) ↔
+    (∃ f ∈ a.complToNA.accept, a.complToNA.MTr (P, C) xs f) ↔
       ∃ T : List (Set State), T.getI 0 = P ∧ T.getI 1 = C ∧
         (∀ i, ∀ hi : i < xs.length, a.LocalOK xs[i] (T.getI i) (T.getI (i + 1)) (T.getI (i + 2))) ∧
         ∀ s ∈ T.getI (xs.length + 1), s ∉ a.accept := by
@@ -225,9 +225,9 @@ theorem exists_accepting_mTr_iff (a : TwoWayNA State Symbol) (xs : List Symbol)
     · rintro ⟨f, hf, hmtr⟩
       rw [LTS.MTr.nil_iff] at hmtr
       subst hmtr
-      exact ⟨[P, C], by simp, by simp, by simp, by simpa [toNAComplement] using hf⟩
+      exact ⟨[P, C], by simp, by simp, by simp, by simpa [complToNA] using hf⟩
     · rintro ⟨T, h0, h1, -, hacc⟩
-      exact ⟨(P, C), by simpa [toNAComplement, ← h1] using hacc, by simp⟩
+      exact ⟨(P, C), by simpa [complToNA, ← h1] using hacc, by simp⟩
   | cons x xs ih =>
     constructor
     · rintro ⟨f, hf, hmtr⟩
@@ -256,7 +256,7 @@ theorem exists_accepting_mTr_iff (a : TwoWayNA State Symbol) (xs : List Symbol)
         have h := hloc 0 (by simp)
         rw [List.getElem_cons_zero] at h
         simpa [h0, h1] using h
-      have htr : a.toNAComplement.Tr (P, C) x (C, T.getI 2) := ⟨rfl, hlocal⟩
+      have htr : a.complToNA.Tr (P, C) x (C, T.getI 2) := ⟨rfl, hlocal⟩
       exact ⟨f, hf, LTS.MTr.cons_iff.mpr ⟨(C, T.getI 2), htr, hmtr⟩⟩
 
 /-- The family of subsets carried by a list, which holds the subset for the position to the left
@@ -276,9 +276,9 @@ theorem getI_certToList {T : ℕ → Set State} {i : ℕ} (hi : i < input.length
   rw [certToList, List.getI_cons_succ, List.getI_eq_getElem (hn := by simpa using hi)]
   simp
 
-/-- `a.toNAComplement` accepts exactly the words that `a` rejects. -/
-theorem accepts_toNAComplement_iff (a : TwoWayNA State Symbol) (input : List Symbol) :
-    Acceptor.Accepts a.toNAComplement input ↔ ¬ Acceptor.Accepts a input := by
+/-- `a.complToNA` accepts exactly the words that `a` rejects. -/
+theorem accepts_complToNA_iff (a : TwoWayNA State Symbol) (input : List Symbol) :
+    Acceptor.Accepts a.complToNA input ↔ ¬ Acceptor.Accepts a input := by
   rw [not_accepts_iff_exists_isRejectionCert]
   constructor
   · rintro ⟨s, ⟨hs, hstart⟩, f, hf, hmtr⟩
@@ -314,12 +314,12 @@ theorem accepts_toNAComplement_iff (a : TwoWayNA State Symbol) (input : List Sym
         by simpa using hT.accept_notMem⟩
     exact ⟨(Set.univ, T 0), ⟨rfl, hT.start_mem⟩, f, hf, hmtr⟩
 
-/-- `a.toNAComplement` recognises the complement of the language of `a`. -/
-theorem language_toNAComplement (a : TwoWayNA State Symbol) :
-    Acceptor.language a.toNAComplement = (Acceptor.language a)ᶜ := by
+/-- `a.complToNA` recognises the complement of the language of `a`. -/
+theorem language_complToNA (a : TwoWayNA State Symbol) :
+    Acceptor.language a.complToNA = (Acceptor.language a)ᶜ := by
   ext xs
   simp only [Acceptor.mem_language]
-  exact accepts_toNAComplement_iff a xs
+  exact accepts_complToNA_iff a xs
 
 end TwoWayNA
 
diff --git a/Cslib/Computability/Languages/RegularLanguage.lean b/Cslib/Computability/Languages/RegularLanguage.lean
index 91d3d5a68..f14436718 100644
--- a/Cslib/Computability/Languages/RegularLanguage.lean
+++ b/Cslib/Computability/Languages/RegularLanguage.lean
@@ -86,7 +86,7 @@ theorem IsRegular.iff_twoWayNA {l : Language Symbol} :
     have := hfin
     have hc : (language a)ᶜ.IsRegular := by
       rw [IsRegular.iff_nfa]
-      exact ⟨Set State × Set State, inferInstance, a.toNAComplement, a.language_toNAComplement⟩
+      exact ⟨Set State × Set State, inferInstance, a.complToNA, a.language_complToNA⟩
     simpa using hc.compl
 
 /-- The empty language is regular. -/

From 7575be611fbd5328373dedb1ea648fe4de0c6082 Mon Sep 17 00:00:00 2001
From: crei <crei.github@gmail.com>
Date: Fri, 11 Sep 2026 15:40:25 +0200
Subject: [PATCH 11/13] Rename T.

---
 .../Automata/TwoWayNA/ComplToNA.lean          | 173 +++++++++---------
 1 file changed, 88 insertions(+), 85 deletions(-)

diff --git a/Cslib/Computability/Automata/TwoWayNA/ComplToNA.lean b/Cslib/Computability/Automata/TwoWayNA/ComplToNA.lean
index 42d1fea82..0af31eafe 100644
--- a/Cslib/Computability/Automata/TwoWayNA/ComplToNA.lean
+++ b/Cslib/Computability/Automata/TwoWayNA/ComplToNA.lean
@@ -19,23 +19,23 @@ unlike Shepherdson's crossing-sequence argument -- characterises non-acceptance
 be checked by a single left-to-right sweep over the input.
 
 This result is the main ingredient in proving equivalence of two-way and one-way automata, which
-can be found in `Cslib.Computability.Automata.TwoWayNA.Regular`.
+can be found in `Cslib.Computability.Languages.RegularLanguages`.
 
 ## Vardi's condition of non-acceptance
 
 Fix a `TwoWayNA` `a` and an input word `input` of length `n`. A *rejection certificate* is a family
-of subsets `T i ⊆ State`, one for every head position `i ∈ {0, …, n}`, subject to three
+of subsets `cert i ⊆ State`, one for every head position `i ∈ {0, …, n}`, subject to three
 conditions:
 
-1. `T` contains every initial state at position `0` (`IsRejectionCert.start_mem`);
-2. `T` is an invariant of the transitions of `a`: if the state `c.state` is in `T c.pos` and `a`
-   can step from the configuration `c` to the configuration `c'`, then `c'.state` is in `T c'.pos`
-   (`TwoWayNA.IsStepClosed`, `IsRejectionCert.step_closed`);
-3. no state in `T n`, i.e. at the position just past the end of the input, is accepting
+1. `cert` contains every initial state at position `0` (`IsRejectionCert.start_mem`);
+2. `cert` is an invariant of the transitions of `a`: if the state `c.state` is in `cert c.pos` and
+  `a` can step from the configuration `c` to the configuration `c'`, then `c'.state` is in
+  `cert c'.pos` (`TwoWayNA.IsStepClosed`, `IsRejectionCert.step_closed`);
+3. no state in `cert n`, i.e. at the position just past the end of the input, is accepting
    (`IsRejectionCert.accept_notMem`).
 
-Intuitively, `T i` over-approximates the set of states in which `a` can be while its head sits at
-position `i`: conditions 1 and 2 make `T` an inductive invariant of the reachable configurations,
+Intuitively, `cert i` over-approximates the set of states in which `a` can be while its head sits at
+position `i`: conditions 1 and 2 make `cert` an inductive invariant of the reachable configurations,
 and condition 3 says that this invariant rules out acceptance -- being preserved by every step, it
 holds at the end of every run (`LTS.mtrInv_of_trInv`). Conversely, the reachable states
 (`TwoWayNA.reachable`) themselves form the least such family, so a certificate exists exactly when
@@ -44,8 +44,8 @@ holds at the end of every run (`LTS.mtrInv_of_trInv`). Conversely, the reachable
 ## The finite acceptor for the complement
 
 The point of the reformulation is locality: `TwoWayNA.isStepClosed_iff_localOK` turns condition 2
-into a condition `TwoWayNA.LocalOK` relating only `T (i - 1)`, `T i` and `T (i + 1)` with the
-symbol at position `i`. A finite acceptor can therefore guess the certificate while scanning the
+into a condition `TwoWayNA.LocalOK` relating only `cert (i - 1)`, `cert i` and `cert (i + 1)` with
+the symbol at position `i`. A finite acceptor can therefore guess the certificate while scanning the
 input, keeping only the last two subsets in its state. This is `TwoWayNA.complToNA`, and
 `TwoWayNA.accepts_complToNA_iff` shows that it accepts exactly the words rejected by `a`.
 
@@ -86,28 +86,28 @@ namespace TwoWayNA
 
 /-! ## Vardi's condition of non-acceptance -/
 
-/-- Every step of `a` on `input` out of a state that `T` attaches to the head position lands in a
-state that `T` attaches to the new head position. The conjunct on the input restricts the
+/-- Every step of `a` on `input` out of a state that `cert` attaches to the head position lands in a
+state that `cert` attaches to the new head position. The conjunct on the input restricts the
 invariant to the configurations that run on `input`. -/
-def IsStepClosed (a : TwoWayNA State Symbol) (input : List Symbol) (T : ℕ → Set State) : Prop :=
-  (a.toCfgNA input).TrInv (fun c => c.input = input ∧ c.state ∈ T c.pos)
+def IsStepClosed (a : TwoWayNA State Symbol) (input : List Symbol) (cert : ℕ → Set State) : Prop :=
+  (a.toCfgNA input).TrInv (fun c => c.input = input ∧ c.state ∈ cert c.pos)
 
 /-- A family of subsets of the state set, one for every position of the input head on `input`,
 which contains all initial states, is closed under the transitions of `a`, and contains no
 accepting state at the position just past the end of the input. -/
 structure IsRejectionCert (a : TwoWayNA State Symbol) (input : List Symbol)
-    (T : ℕ → Set State) : Prop where
+    (cert : ℕ → Set State) : Prop where
   /-- Every initial state occurs at the initial head position. -/
-  start_mem : ∀ s ∈ a.start, s ∈ T 0
+  start_mem : ∀ s ∈ a.start, s ∈ cert 0
   /-- The family is an invariant of the transitions of `a`. -/
-  step_closed : a.IsStepClosed input T
+  step_closed : a.IsStepClosed input cert
   /-- No accepting state occurs past the end of the input. -/
-  accept_notMem : ∀ s ∈ T input.length, s ∉ a.accept
+  accept_notMem : ∀ s ∈ cert input.length, s ∉ a.accept
 
-variable {T : ℕ → Set State}
+variable {cert : ℕ → Set State}
 
 /-- If a rejection certificate for `input` exists, then `a` does not accept `input`. -/
-theorem IsRejectionCert.not_accepts (hT : a.IsRejectionCert input T) :
+theorem IsRejectionCert.not_accepts (hT : a.IsRejectionCert input cert) :
     ¬ Acceptor.Accepts a input := by
   rintro ⟨μs, c, ⟨hstart, hpos, hinput⟩, c', ⟨hacc, hlast⟩, hmtr⟩
   obtain ⟨hinput', hmem⟩ := LTS.mtrInv_of_trInv hT.step_closed c μs c' hmtr
@@ -149,23 +149,24 @@ theorem not_accepts_iff_exists_isRejectionCert (a : TwoWayNA State Symbol)
 
 /-! ## Localising the closure condition -/
 
-/-- The subset that `T` attaches to the position to the left of `i`, and everything at position
+/-- The subset that `cert` attaches to the position to the left of `i`, and everything at position
 `0`, which has no position to its left. -/
-def prevSet (T : ℕ → Set State) : ℕ → Set State
+def leftSet (cert : ℕ → Set State) : ℕ → Set State
   | 0 => Set.univ
-  | i + 1 => T i
+  | i + 1 => cert i
 
-/-- Every move of `a` out of a state in `C` while reading `x` lands in `P`, in `C` or in `N`,
-according to whether it moves the head to the left, keeps it in place, or moves it to the right. -/
-def LocalOK (a : TwoWayNA State Symbol) (x : Symbol) (P C N : Set State) : Prop :=
-  ∀ q ∈ C, ∀ m q', a.Tr q x m q' →
-    q' ∈ match m with | .neg => P | .zero => C | .pos => N
+/-- Every move of `a` out of a state in `cur` while reading `x` lands in `left`, in `cur` or in
+`right`, according to whether it moves the head to the left, keeps it in place, or moves it to the
+right. -/
+def LocalOK (a : TwoWayNA State Symbol) (x : Symbol) (left cur right : Set State) : Prop :=
+  ∀ q ∈ cur, ∀ m q', a.Tr q x m q' →
+    q' ∈ match m with | .neg => left | .zero => cur | .pos => right
 
-/-- Closure of `T` under the transitions of `a` is the same as local consistency of `T` at every
-position carrying an input symbol. -/
+/-- Closure of `cert` under the transitions of `a` is the same as local consistency of `cert` at
+every position carrying an input symbol. -/
 theorem isStepClosed_iff_localOK :
-    a.IsStepClosed input T ↔
-      ∀ i : Fin input.length, a.LocalOK input[i] (prevSet T i) (T i) (T (i + 1)) := by
+    a.IsStepClosed input cert ↔
+      ∀ i : Fin input.length, a.LocalOK input[i] (leftSet cert i) (cert i) (cert (i + 1)) := by
   constructor
   · intro hcl i q hq m q' htr
     have hlt : (i : ℕ) < input.length := i.isLt
@@ -203,76 +204,78 @@ theorem isStepClosed_iff_localOK :
 
 /-! ## The finite acceptor for the complement -/
 
-/-- The nondeterministic finite acceptor that guesses a rejection certificate `T` for `a` while
-scanning the input, keeping the pair `(T (i - 1), T i)` in its state after reading `i` symbols.
-Reading the symbol at position `i` guesses `T (i + 1)` and checks local consistency at `i`. -/
+/-- The nondeterministic finite acceptor that guesses a rejection certificate `cert` for `a` while
+scanning the input, keeping the pair `(cert (i - 1), cert i)` in its state after reading `i`
+symbols.
+Reading the symbol at position `i` guesses `cert (i + 1)` and checks local consistency at `i`. -/
 def complToNA (a : TwoWayNA State Symbol) : NA.FinAcc (Set State × Set State) Symbol where
   Tr PC x PC' := PC'.1 = PC.2 ∧ a.LocalOK x PC.1 PC.2 PC'.2
   start := {PC | PC.1 = Set.univ ∧ a.start ⊆ PC.2}
   accept := {PC | ∀ s ∈ PC.2, s ∉ a.accept}
 
-/-- An accepting multistep transition of `a.complToNA` out of `(P, C)` over `xs` is the same
-thing as a list of subsets starting with `P` and `C` that is locally consistent at every position
-of `xs` and ends in a subset without accepting states. -/
-theorem exists_accepting_mTr_iff (a : TwoWayNA State Symbol) (xs : List Symbol) (P C : Set State) :
-    (∃ f ∈ a.complToNA.accept, a.complToNA.MTr (P, C) xs f) ↔
-      ∃ T : List (Set State), T.getI 0 = P ∧ T.getI 1 = C ∧
-        (∀ i, ∀ hi : i < xs.length, a.LocalOK xs[i] (T.getI i) (T.getI (i + 1)) (T.getI (i + 2))) ∧
-        ∀ s ∈ T.getI (xs.length + 1), s ∉ a.accept := by
-  induction xs generalizing P C with
+/-- An accepting multistep transition of `a.complToNA` out of `(left, cur)` over `xs` is the same
+thing as a list of subsets starting with `left` and `cur` that is locally consistent at every
+position of `xs` and ends in a subset without accepting states. -/
+theorem exists_accepting_mTr_iff (a : TwoWayNA State Symbol) (xs : List Symbol)
+    (left cur : Set State) :
+    (∃ f ∈ a.complToNA.accept, a.complToNA.MTr (left, cur) xs f) ↔
+      ∃ cert : List (Set State), cert.getI 0 = left ∧ cert.getI 1 = cur ∧
+        (∀ i, ∀ hi : i < xs.length,
+          a.LocalOK xs[i] (cert.getI i) (cert.getI (i + 1)) (cert.getI (i + 2))) ∧
+          ∀ s ∈ cert.getI (xs.length + 1), s ∉ a.accept := by
+  induction xs generalizing left cur with
   | nil =>
     constructor
     · rintro ⟨f, hf, hmtr⟩
       rw [LTS.MTr.nil_iff] at hmtr
       subst hmtr
-      exact ⟨[P, C], by simp, by simp, by simp, by simpa [complToNA] using hf⟩
+      exact ⟨[left, cur], by simp, by simp, by simp, by simpa [complToNA] using hf⟩
     · rintro ⟨T, h0, h1, -, hacc⟩
-      exact ⟨(P, C), by simpa [complToNA, ← h1] using hacc, by simp⟩
+      exact ⟨(left, cur), by simpa [complToNA, ← h1] using hacc, by simp⟩
   | cons x xs ih =>
     constructor
     · rintro ⟨f, hf, hmtr⟩
       rw [LTS.MTr.cons_iff] at hmtr
       obtain ⟨⟨m₁, m₂⟩, ⟨rfl, hlocal⟩, hmtr⟩ := hmtr
-      obtain ⟨T, h0, h1, hloc, hacc⟩ := (ih m₁ m₂).mp ⟨f, hf, hmtr⟩
-      have hlocal' : a.LocalOK x P m₁ m₂ := hlocal
-      have hstep : ∀ i, ∀ hi : i < (x :: xs).length,
-          a.LocalOK (x :: xs)[i]
-            ((P :: T).getI i) ((P :: T).getI (i + 1)) ((P :: T).getI (i + 2)) := by
+      obtain ⟨cert, h0, h1, hloc, hacc⟩ := (ih m₁ m₂).mp ⟨f, hf, hmtr⟩
+      have hlocal' : a.LocalOK x left m₁ m₂ := hlocal
+      have hstep : ∀ i, ∀ hi : i < (x :: xs).length, a.LocalOK (x :: xs)[i]
+          ((left :: cert).getI i) ((left :: cert).getI (i + 1)) ((left :: cert).getI (i + 2)) := by
         intro i hi
         obtain _ | i := i
         · simpa [h0, h1] using hlocal
         · simpa using hloc i (by simpa using hi)
-      exact ⟨P :: T, by simp, by simpa using h0, hstep, by simpa using hacc⟩
-    · rintro ⟨T, h0, h1, hloc, hacc⟩
+      exact ⟨left :: cert, by simp, by simpa using h0, hstep, by simpa using hacc⟩
+    · rintro ⟨cert, h0, h1, hloc, hacc⟩
       have hstep : ∀ i, ∀ hi : i < xs.length,
-          a.LocalOK xs[i] (T.tail.getI i) (T.tail.getI (i + 1)) (T.tail.getI (i + 2)) := by
+          a.LocalOK xs[i] (cert.tail.getI i) (cert.tail.getI (i + 1)) (cert.tail.getI (i + 2)) := by
         intro i hi
         have h := hloc (i + 1) (by simpa using hi)
         rw [List.getElem_cons_succ] at h
         simpa using h
-      obtain ⟨f, hf, hmtr⟩ := (ih C (T.getI 2)).mpr
-        ⟨T.tail, by simpa using h1, by simp, hstep, by simpa using hacc⟩
-      have hlocal : a.LocalOK x P C (T.getI 2) := by
+      obtain ⟨f, hf, hmtr⟩ := (ih cur (cert.getI 2)).mpr
+        ⟨cert.tail, by simpa using h1, by simp, hstep, by simpa using hacc⟩
+      have hlocal : a.LocalOK x left cur (cert.getI 2) := by
         have h := hloc 0 (by simp)
         rw [List.getElem_cons_zero] at h
         simpa [h0, h1] using h
-      have htr : a.complToNA.Tr (P, C) x (C, T.getI 2) := ⟨rfl, hlocal⟩
-      exact ⟨f, hf, LTS.MTr.cons_iff.mpr ⟨(C, T.getI 2), htr, hmtr⟩⟩
+      have htr : a.complToNA.Tr (left, cur) x (cur, cert.getI 2) := ⟨rfl, hlocal⟩
+      exact ⟨f, hf, LTS.MTr.cons_iff.mpr ⟨(cur, cert.getI 2), htr, hmtr⟩⟩
 
 /-- The family of subsets carried by a list, which holds the subset for the position to the left
 of `0` in front, so that position `i` is entry `i + 1` of the list. -/
-def certOfList (T : List (Set State)) (i : ℕ) : Set State :=
-  T.getI (i + 1)
+def certOfList (cert : List (Set State)) (i : ℕ) : Set State :=
+  cert.getI (i + 1)
 
-/-- The subsets that `T` attaches to the positions of the input head, as a list, prefixed by
+/-- The subsets that `cert` attaches to the positions of the input head, as a list, prefixed by
 `Set.univ` for the position to the left of `0`. -/
-def certToList (input : List Symbol) (T : ℕ → Set State) : List (Set State) :=
-  Set.univ :: (List.range (input.length + 1)).map T
+def certToList (input : List Symbol) (cert : ℕ → Set State) : List (Set State) :=
+  Set.univ :: (List.range (input.length + 1)).map cert
 
-/-- Entry `i + 1` of `TwoWayNA.certToList` is the subset that `T` attaches to position `i`. -/
+/-- Entry `i + 1` of `TwoWayNA.certToList` is the subset that `cert` attaches to position `i`. -/
 @[simp]
-theorem getI_certToList {T : ℕ → Set State} {i : ℕ} (hi : i < input.length + 1) :
-    (certToList input T).getI (i + 1) = T i := by
+theorem getI_certToList {i : ℕ} (hi : i < input.length + 1) :
+    (certToList input cert).getI (i + 1) = cert i := by
   rw [certToList, List.getI_cons_succ, List.getI_eq_getElem (hn := by simpa using hi)]
   simp
 
@@ -282,37 +285,37 @@ theorem accepts_complToNA_iff (a : TwoWayNA State Symbol) (input : List Symbol)
   rw [not_accepts_iff_exists_isRejectionCert]
   constructor
   · rintro ⟨s, ⟨hs, hstart⟩, f, hf, hmtr⟩
-    obtain ⟨T, h0, h1, hloc, hacc⟩ := (exists_accepting_mTr_iff a input s.1 s.2).mp ⟨f, hf, hmtr⟩
-    have hstep : ∀ i : Fin input.length,
-        a.LocalOK input[i] (prevSet (certOfList T) i) (certOfList T i) (certOfList T (i + 1)) := by
+    obtain ⟨cert, h0, h1, hloc, hacc⟩ := (exists_accepting_mTr_iff a input s.1 s.2).mp ⟨f, hf, hmtr⟩
+    have hstep : ∀ i : Fin input.length, a.LocalOK input[i]
+        (leftSet (certOfList cert) i) (certOfList cert i) (certOfList cert (i + 1)) := by
       intro i
       obtain ⟨iv, hiv⟩ := i
       obtain _ | j := iv
-      · simpa [prevSet, certOfList, h0, hs] using hloc 0 hiv
-      · simpa [prevSet, certOfList] using hloc (j + 1) hiv
-    exact ⟨certOfList T,
+      · simpa [leftSet, certOfList, h0, hs] using hloc 0 hiv
+      · simpa [leftSet, certOfList] using hloc (j + 1) hiv
+    exact ⟨certOfList cert,
       { start_mem := by
           intro q hq
           simpa [certOfList, h1] using hstart hq
         step_closed := isStepClosed_iff_localOK.mpr hstep
         accept_notMem := by simpa [certOfList] using hacc }⟩
-  · rintro ⟨T, hT⟩
-    have hloc := isStepClosed_iff_localOK.mp hT.step_closed
+  · rintro ⟨cert, hCert⟩
+    have hloc := isStepClosed_iff_localOK.mp hCert.step_closed
     have hstep : ∀ i, ∀ hi : i < input.length, a.LocalOK input[i]
-        ((certToList input T).getI i) ((certToList input T).getI (i + 1))
-          ((certToList input T).getI (i + 2)) := by
+        ((certToList input cert).getI i) ((certToList input cert).getI (i + 1))
+          ((certToList input cert).getI (i + 2)) := by
       intro i hi
-      have e0 : (certToList input T).getI i = prevSet T i := by
+      have e0 : (certToList input cert).getI i = leftSet cert i := by
         cases i with
         | zero => rfl
         | succ j => exact getI_certToList (by omega)
-      have e1 : (certToList input T).getI (i + 1) = T i := getI_certToList (by omega)
-      have e2 : (certToList input T).getI (i + 2) = T (i + 1) := getI_certToList (by omega)
+      have e1 : (certToList input cert).getI (i + 1) = cert i := getI_certToList (by omega)
+      have e2 : (certToList input cert).getI (i + 2) = cert (i + 1) := getI_certToList (by omega)
       simpa [e0, e1, e2] using hloc ⟨i, hi⟩
-    obtain ⟨f, hf, hmtr⟩ := (exists_accepting_mTr_iff a input Set.univ (T 0)).mpr
-      ⟨certToList input T, rfl, getI_certToList (by omega), hstep,
-        by simpa using hT.accept_notMem⟩
-    exact ⟨(Set.univ, T 0), ⟨rfl, hT.start_mem⟩, f, hf, hmtr⟩
+    obtain ⟨f, hf, hmtr⟩ := (exists_accepting_mTr_iff a input Set.univ (cert 0)).mpr
+      ⟨certToList input cert, rfl, getI_certToList (by omega), hstep,
+        by simpa using hCert.accept_notMem⟩
+    exact ⟨(Set.univ, cert 0), ⟨rfl, hCert.start_mem⟩, f, hf, hmtr⟩
 
 /-- `a.complToNA` recognises the complement of the language of `a`. -/
 theorem language_complToNA (a : TwoWayNA State Symbol) :

From cf9f08efb5e59591a002c60eb72bb92531a6f1d2 Mon Sep 17 00:00:00 2001
From: crei <crei.github@gmail.com>
Date: Fri, 11 Sep 2026 15:47:24 +0200
Subject: [PATCH 12/13] Improve definition of complToNA.

---
 Cslib/Computability/Automata/TwoWayNA/ComplToNA.lean | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

diff --git a/Cslib/Computability/Automata/TwoWayNA/ComplToNA.lean b/Cslib/Computability/Automata/TwoWayNA/ComplToNA.lean
index 0af31eafe..c52e75259 100644
--- a/Cslib/Computability/Automata/TwoWayNA/ComplToNA.lean
+++ b/Cslib/Computability/Automata/TwoWayNA/ComplToNA.lean
@@ -209,9 +209,10 @@ scanning the input, keeping the pair `(cert (i - 1), cert i)` in its state after
 symbols.
 Reading the symbol at position `i` guesses `cert (i + 1)` and checks local consistency at `i`. -/
 def complToNA (a : TwoWayNA State Symbol) : NA.FinAcc (Set State × Set State) Symbol where
-  Tr PC x PC' := PC'.1 = PC.2 ∧ a.LocalOK x PC.1 PC.2 PC'.2
-  start := {PC | PC.1 = Set.univ ∧ a.start ⊆ PC.2}
-  accept := {PC | ∀ s ∈ PC.2, s ∉ a.accept}
+  Tr
+    | (prev, cur), x, (prev', cur') => prev' = cur ∧ a.LocalOK x prev cur cur'
+  start := {(prev, cur) | prev = Set.univ ∧ a.start ⊆ cur}
+  accept := {(_, cur) | ∀ s ∈ cur, s ∉ a.accept}
 
 /-- An accepting multistep transition of `a.complToNA` out of `(left, cur)` over `xs` is the same
 thing as a list of subsets starting with `left` and `cur` that is locally consistent at every

From d0cc930585269b415a65b7d55582de622cacf4e7 Mon Sep 17 00:00:00 2001
From: crei <crei.github@gmail.com>
Date: Fri, 11 Sep 2026 16:04:13 +0200
Subject: [PATCH 13/13] Use omega sequence.

---
 .../Automata/TwoWayNA/ComplToNA.lean          | 143 ++++++------------
 1 file changed, 49 insertions(+), 94 deletions(-)

diff --git a/Cslib/Computability/Automata/TwoWayNA/ComplToNA.lean b/Cslib/Computability/Automata/TwoWayNA/ComplToNA.lean
index c52e75259..ae2932350 100644
--- a/Cslib/Computability/Automata/TwoWayNA/ComplToNA.lean
+++ b/Cslib/Computability/Automata/TwoWayNA/ComplToNA.lean
@@ -8,6 +8,7 @@ module
 
 public import Cslib.Computability.Automata.NA.Basic
 public import Cslib.Computability.Automata.TwoWayNA.Basic
+public import Cslib.Foundations.Data.OmegaSequence.Init
 public import Cslib.Foundations.Semantics.LTS.Relation
 
 /-! # A finite acceptor for the complement of the language of a two-way automaton
@@ -51,15 +52,14 @@ input, keeping only the last two subsets in its state. This is `TwoWayNA.complTo
 
 ## Implementation notes
 
-A rejection certificate is indexed by `ℕ` rather than by `Fin (input.length + 1)`, the type of
-`TwoWayNACfg.pos`: positions past the end of the input are simply left unconstrained, which avoids
-casts when the certificate is compared along a run, whose configurations carry their own input.
+A rejection certificate is an `ωSequence`, i.e. indexed by `ℕ` rather than by
+`Fin (input.length + 1)`, the type of `TwoWayNACfg.pos`: positions past the end of the input are
+simply left unconstrained, which avoids casts when the certificate is compared along a run, whose
+configurations carry their own input. The subset for the missing position to the left of the input
+is supplied by prepending `Set.univ` with `ωSequence.cons`.
 
-Where a `List (Set State)` is more convenient is `TwoWayNA.exists_accepting_mTr_iff`, which is
-proved by induction on the input word and prepends a subset to the certificate at each step.
-`TwoWayNA.certOfList` and `TwoWayNA.certToList` translate between the two encodings, the latter
-prefixing `Set.univ` for the missing position to the left of the input, mirroring
-`TwoWayNA.prevSet`.
+`TwoWayNA.exists_accepting_mTr_iff` is proved by induction on the input word, prepending a subset
+to the certificate at each step with `ωSequence.cons` and dropping one with `ωSequence.tail`.
 
 ## References
 
@@ -68,18 +68,11 @@ prefixing `Set.univ` for the missing position to the left of the input, mirrorin
 
 @[expose] public section
 
-namespace List
-
-/-- Dropping the head of a list shifts total indexing by one. -/
-@[simp]
-private theorem getI_tail {α : Type*} [Inhabited α] (l : List α) (i : ℕ) :
-    l.tail.getI i = l.getI (i + 1) := by
-  cases l <;> simp
-
-end List
-
 namespace Cslib.Automata
 
+open scoped ωSequence
+open Acceptor
+
 variable {State Symbol : Type*} {a : TwoWayNA State Symbol} {input : List Symbol}
 
 namespace TwoWayNA
@@ -89,14 +82,15 @@ namespace TwoWayNA
 /-- Every step of `a` on `input` out of a state that `cert` attaches to the head position lands in a
 state that `cert` attaches to the new head position. The conjunct on the input restricts the
 invariant to the configurations that run on `input`. -/
-def IsStepClosed (a : TwoWayNA State Symbol) (input : List Symbol) (cert : ℕ → Set State) : Prop :=
+def IsStepClosed (a : TwoWayNA State Symbol) (input : List Symbol)
+    (cert : ωSequence (Set State)) : Prop :=
   (a.toCfgNA input).TrInv (fun c => c.input = input ∧ c.state ∈ cert c.pos)
 
 /-- A family of subsets of the state set, one for every position of the input head on `input`,
 which contains all initial states, is closed under the transitions of `a`, and contains no
 accepting state at the position just past the end of the input. -/
 structure IsRejectionCert (a : TwoWayNA State Symbol) (input : List Symbol)
-    (cert : ℕ → Set State) : Prop where
+    (cert : ωSequence (Set State)) : Prop where
   /-- Every initial state occurs at the initial head position. -/
   start_mem : ∀ s ∈ a.start, s ∈ cert 0
   /-- The family is an invariant of the transitions of `a`. -/
@@ -104,11 +98,11 @@ structure IsRejectionCert (a : TwoWayNA State Symbol) (input : List Symbol)
   /-- No accepting state occurs past the end of the input. -/
   accept_notMem : ∀ s ∈ cert input.length, s ∉ a.accept
 
-variable {cert : ℕ → Set State}
+variable {cert : ωSequence (Set State)}
 
 /-- If a rejection certificate for `input` exists, then `a` does not accept `input`. -/
 theorem IsRejectionCert.not_accepts (hT : a.IsRejectionCert input cert) :
-    ¬ Acceptor.Accepts a input := by
+    ¬ Accepts a input := by
   rintro ⟨μs, c, ⟨hstart, hpos, hinput⟩, c', ⟨hacc, hlast⟩, hmtr⟩
   obtain ⟨hinput', hmem⟩ := LTS.mtrInv_of_trInv hT.step_closed c μs c' hmtr
     ⟨hinput, by simpa [hpos] using hT.start_mem c.state hstart⟩
@@ -117,14 +111,13 @@ theorem IsRejectionCert.not_accepts (hT : a.IsRejectionCert input cert) :
 
 /-- The set of states that `a` can be in while its head sits at position `i` of `input`, having
 started in an initial configuration. -/
-def reachable (a : TwoWayNA State Symbol) (input : List Symbol) (i : ℕ) :
-    Set State :=
-  {q | ∃ c, c.IsInitialForInput a input ∧
+def reachable (a : TwoWayNA State Symbol) (input : List Symbol) : ωSequence (Set State) :=
+  fun i => {q | ∃ c, c.IsInitialForInput a input ∧
       ∃ h : i < input.length + 1,
       (a.toCfgNA input).CanReach c { input := input, pos := ⟨i, h⟩, state := q } }
 
 /-- If `a` does not accept `input`, then its reachable states form a rejection certificate. -/
-theorem isRejectionCert_reachable (h : ¬ Acceptor.Accepts a input) :
+theorem isRejectionCert_reachable (h : ¬ Accepts a input) :
     a.IsRejectionCert input (a.reachable input) where
   start_mem s hs :=
     ⟨{ input := input, pos := ⟨0, Nat.succ_pos _⟩, state := s },
@@ -144,17 +137,11 @@ theorem isRejectionCert_reachable (h : ¬ Acceptor.Accepts a input) :
 /-- A two-way automaton rejects an input exactly when a rejection certificate for it exists. -/
 theorem not_accepts_iff_exists_isRejectionCert (a : TwoWayNA State Symbol)
     (input : List Symbol) :
-    ¬ Acceptor.Accepts a input ↔ ∃ T, a.IsRejectionCert input T :=
+    ¬ Accepts a input ↔ ∃ T, a.IsRejectionCert input T :=
   ⟨fun h => ⟨_, isRejectionCert_reachable h⟩, by rintro ⟨_, hT⟩; exact hT.not_accepts⟩
 
 /-! ## Localising the closure condition -/
 
-/-- The subset that `cert` attaches to the position to the left of `i`, and everything at position
-`0`, which has no position to its left. -/
-def leftSet (cert : ℕ → Set State) : ℕ → Set State
-  | 0 => Set.univ
-  | i + 1 => cert i
-
 /-- Every move of `a` out of a state in `cur` while reading `x` lands in `left`, in `cur` or in
 `right`, according to whether it moves the head to the left, keeps it in place, or moves it to the
 right. -/
@@ -166,7 +153,8 @@ def LocalOK (a : TwoWayNA State Symbol) (x : Symbol) (left cur right : Set State
 every position carrying an input symbol. -/
 theorem isStepClosed_iff_localOK :
     a.IsStepClosed input cert ↔
-      ∀ i : Fin input.length, a.LocalOK input[i] (leftSet cert i) (cert i) (cert (i + 1)) := by
+      ∀ i : Fin input.length,
+        a.LocalOK input[i] ((Set.univ ::ω cert) i) (cert i) (cert (i + 1)) := by
   constructor
   · intro hcl i q hq m q' htr
     have hlt : (i : ℕ) < input.length := i.isLt
@@ -215,23 +203,22 @@ def complToNA (a : TwoWayNA State Symbol) : NA.FinAcc (Set State × Set State) S
   accept := {(_, cur) | ∀ s ∈ cur, s ∉ a.accept}
 
 /-- An accepting multistep transition of `a.complToNA` out of `(left, cur)` over `xs` is the same
-thing as a list of subsets starting with `left` and `cur` that is locally consistent at every
-position of `xs` and ends in a subset without accepting states. -/
+thing as a certificate starting with `left` and `cur` that is locally consistent at every position
+of `xs` and has no accepting state at the position just past `xs`. -/
 theorem exists_accepting_mTr_iff (a : TwoWayNA State Symbol) (xs : List Symbol)
     (left cur : Set State) :
     (∃ f ∈ a.complToNA.accept, a.complToNA.MTr (left, cur) xs f) ↔
-      ∃ cert : List (Set State), cert.getI 0 = left ∧ cert.getI 1 = cur ∧
-        (∀ i, ∀ hi : i < xs.length,
-          a.LocalOK xs[i] (cert.getI i) (cert.getI (i + 1)) (cert.getI (i + 2))) ∧
-          ∀ s ∈ cert.getI (xs.length + 1), s ∉ a.accept := by
+      ∃ cert : ωSequence (Set State), cert 0 = left ∧ cert 1 = cur ∧
+        (∀ i, ∀ hi : i < xs.length, a.LocalOK xs[i] (cert i) (cert (i + 1)) (cert (i + 2))) ∧
+          ∀ s ∈ cert (xs.length + 1), s ∉ a.accept := by
   induction xs generalizing left cur with
   | nil =>
     constructor
     · rintro ⟨f, hf, hmtr⟩
       rw [LTS.MTr.nil_iff] at hmtr
       subst hmtr
-      exact ⟨[left, cur], by simp, by simp, by simp, by simpa [complToNA] using hf⟩
-    · rintro ⟨T, h0, h1, -, hacc⟩
+      exact ⟨left ::ω ωSequence.const cur, rfl, rfl, by simp, by simpa [complToNA] using hf⟩
+    · rintro ⟨cert, h0, h1, -, hacc⟩
       exact ⟨(left, cur), by simpa [complToNA, ← h1] using hacc, by simp⟩
   | cons x xs ih =>
     constructor
@@ -239,88 +226,56 @@ theorem exists_accepting_mTr_iff (a : TwoWayNA State Symbol) (xs : List Symbol)
       rw [LTS.MTr.cons_iff] at hmtr
       obtain ⟨⟨m₁, m₂⟩, ⟨rfl, hlocal⟩, hmtr⟩ := hmtr
       obtain ⟨cert, h0, h1, hloc, hacc⟩ := (ih m₁ m₂).mp ⟨f, hf, hmtr⟩
-      have hlocal' : a.LocalOK x left m₁ m₂ := hlocal
       have hstep : ∀ i, ∀ hi : i < (x :: xs).length, a.LocalOK (x :: xs)[i]
-          ((left :: cert).getI i) ((left :: cert).getI (i + 1)) ((left :: cert).getI (i + 2)) := by
+          ((left ::ω cert) i) ((left ::ω cert) (i + 1)) ((left ::ω cert) (i + 2)) := by
         intro i hi
         obtain _ | i := i
         · simpa [h0, h1] using hlocal
         · simpa using hloc i (by simpa using hi)
-      exact ⟨left :: cert, by simp, by simpa using h0, hstep, by simpa using hacc⟩
+      exact ⟨left ::ω cert, rfl, by simpa using h0, hstep, by simpa using hacc⟩
     · rintro ⟨cert, h0, h1, hloc, hacc⟩
       have hstep : ∀ i, ∀ hi : i < xs.length,
-          a.LocalOK xs[i] (cert.tail.getI i) (cert.tail.getI (i + 1)) (cert.tail.getI (i + 2)) := by
+          a.LocalOK xs[i] (cert.tail i) (cert.tail (i + 1)) (cert.tail (i + 2)) := by
         intro i hi
         have h := hloc (i + 1) (by simpa using hi)
         rw [List.getElem_cons_succ] at h
-        simpa using h
-      obtain ⟨f, hf, hmtr⟩ := (ih cur (cert.getI 2)).mpr
-        ⟨cert.tail, by simpa using h1, by simp, hstep, by simpa using hacc⟩
-      have hlocal : a.LocalOK x left cur (cert.getI 2) := by
+        simpa [ωSequence.get_tail, Nat.add_right_comm] using h
+      obtain ⟨f, hf, hmtr⟩ := (ih cur (cert 2)).mpr
+        ⟨cert.tail, by simpa using h1, by simp [ωSequence.get_tail], hstep, by simpa using hacc⟩
+      have hlocal : a.LocalOK x left cur (cert 2) := by
         have h := hloc 0 (by simp)
         rw [List.getElem_cons_zero] at h
         simpa [h0, h1] using h
-      have htr : a.complToNA.Tr (left, cur) x (cur, cert.getI 2) := ⟨rfl, hlocal⟩
-      exact ⟨f, hf, LTS.MTr.cons_iff.mpr ⟨(cur, cert.getI 2), htr, hmtr⟩⟩
-
-/-- The family of subsets carried by a list, which holds the subset for the position to the left
-of `0` in front, so that position `i` is entry `i + 1` of the list. -/
-def certOfList (cert : List (Set State)) (i : ℕ) : Set State :=
-  cert.getI (i + 1)
-
-/-- The subsets that `cert` attaches to the positions of the input head, as a list, prefixed by
-`Set.univ` for the position to the left of `0`. -/
-def certToList (input : List Symbol) (cert : ℕ → Set State) : List (Set State) :=
-  Set.univ :: (List.range (input.length + 1)).map cert
-
-/-- Entry `i + 1` of `TwoWayNA.certToList` is the subset that `cert` attaches to position `i`. -/
-@[simp]
-theorem getI_certToList {i : ℕ} (hi : i < input.length + 1) :
-    (certToList input cert).getI (i + 1) = cert i := by
-  rw [certToList, List.getI_cons_succ, List.getI_eq_getElem (hn := by simpa using hi)]
-  simp
+      exact ⟨f, hf, LTS.MTr.cons_iff.mpr ⟨(cur, cert 2), ⟨rfl, hlocal⟩, hmtr⟩⟩
 
 /-- `a.complToNA` accepts exactly the words that `a` rejects. -/
 theorem accepts_complToNA_iff (a : TwoWayNA State Symbol) (input : List Symbol) :
-    Acceptor.Accepts a.complToNA input ↔ ¬ Acceptor.Accepts a input := by
+    Accepts a.complToNA input ↔ ¬ Accepts a input := by
   rw [not_accepts_iff_exists_isRejectionCert]
   constructor
   · rintro ⟨s, ⟨hs, hstart⟩, f, hf, hmtr⟩
     obtain ⟨cert, h0, h1, hloc, hacc⟩ := (exists_accepting_mTr_iff a input s.1 s.2).mp ⟨f, hf, hmtr⟩
-    have hstep : ∀ i : Fin input.length, a.LocalOK input[i]
-        (leftSet (certOfList cert) i) (certOfList cert i) (certOfList cert (i + 1)) := by
-      intro i
-      obtain ⟨iv, hiv⟩ := i
-      obtain _ | j := iv
-      · simpa [leftSet, certOfList, h0, hs] using hloc 0 hiv
-      · simpa [leftSet, certOfList] using hloc (j + 1) hiv
-    exact ⟨certOfList cert,
+    have hcert : Set.univ ::ω cert.tail = cert := by
+      rw [← hs, ← h0]
+      exact ωSequence.eta cert
+    have hstep : ∀ i : Fin input.length,
+        a.LocalOK input[i] ((Set.univ ::ω cert.tail) i) (cert.tail i) (cert.tail (i + 1)) :=
+      fun i => by simpa [hcert, ωSequence.get_tail] using hloc i i.isLt
+    exact ⟨cert.tail,
       { start_mem := by
           intro q hq
-          simpa [certOfList, h1] using hstart hq
+          simpa [h1] using hstart hq
         step_closed := isStepClosed_iff_localOK.mpr hstep
-        accept_notMem := by simpa [certOfList] using hacc }⟩
+        accept_notMem := by simpa using hacc }⟩
   · rintro ⟨cert, hCert⟩
     have hloc := isStepClosed_iff_localOK.mp hCert.step_closed
-    have hstep : ∀ i, ∀ hi : i < input.length, a.LocalOK input[i]
-        ((certToList input cert).getI i) ((certToList input cert).getI (i + 1))
-          ((certToList input cert).getI (i + 2)) := by
-      intro i hi
-      have e0 : (certToList input cert).getI i = leftSet cert i := by
-        cases i with
-        | zero => rfl
-        | succ j => exact getI_certToList (by omega)
-      have e1 : (certToList input cert).getI (i + 1) = cert i := getI_certToList (by omega)
-      have e2 : (certToList input cert).getI (i + 2) = cert (i + 1) := getI_certToList (by omega)
-      simpa [e0, e1, e2] using hloc ⟨i, hi⟩
     obtain ⟨f, hf, hmtr⟩ := (exists_accepting_mTr_iff a input Set.univ (cert 0)).mpr
-      ⟨certToList input cert, rfl, getI_certToList (by omega), hstep,
+      ⟨Set.univ ::ω cert, rfl, rfl, fun i hi => by simpa using hloc ⟨i, hi⟩,
         by simpa using hCert.accept_notMem⟩
     exact ⟨(Set.univ, cert 0), ⟨rfl, hCert.start_mem⟩, f, hf, hmtr⟩
 
 /-- `a.complToNA` recognises the complement of the language of `a`. -/
-theorem language_complToNA (a : TwoWayNA State Symbol) :
-    Acceptor.language a.complToNA = (Acceptor.language a)ᶜ := by
+theorem language_complToNA (a : TwoWayNA State Symbol) : language a.complToNA = (language a)ᶜ := by
   ext xs
   simp only [Acceptor.mem_language]
   exact accepts_complToNA_iff a xs