diff --git a/Cslib.lean b/Cslib.lean
index 11234c94b..0c4dab5e5 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.ComplToNA
+public import Cslib.Computability.Automata.TwoWayNA.OfNA
 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..edd70a119 100644
--- a/Cslib/Computability/Automata/TwoWayNA/Basic.lean
+++ b/Cslib/Computability/Automata/TwoWayNA/Basic.lean
@@ -27,7 +27,8 @@ 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.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
 
@@ -84,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
@@ -101,16 +102,33 @@ 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)
-    (input : List Symbol) :
-    (a.toCfgNAFinAcc input).toLTS.TrInv (fun c => c.input = input) := by
-  intro c μ c' h_tr rfl
-  simp_all [TwoWayNA.toCfgNAFinAcc]
-
 @[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
+
+/-- 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).TrInv (fun c => c.input = input) := by
+  intro c μ c' h_tr rfl
+  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}
+    (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.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
+  exact List.getElem?_eq_some_iff.mp hx.symm
 
 end Cslib.Automata
diff --git a/Cslib/Computability/Automata/TwoWayNA/ComplToNA.lean b/Cslib/Computability/Automata/TwoWayNA/ComplToNA.lean
new file mode 100644
index 000000000..ae2932350
--- /dev/null
+++ b/Cslib/Computability/Automata/TwoWayNA/ComplToNA.lean
@@ -0,0 +1,285 @@
+/-
+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.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
+
+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.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.
+
+This result is the main ingredient in proving equivalence of two-way and one-way automata, which
+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 `cert i ⊆ State`, one for every head position `i ∈ {0, …, n}`, subject to three
+conditions:
+
+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, `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
+`a` rejects (`TwoWayNA.not_accepts_iff_exists_isRejectionCert`).
+
+## 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 `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`.
+
+## Implementation notes
+
+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`.
+
+`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
+
+* [M. Y. Vardi, *A note on the reduction of two-way automata to one-way automata*][Vardi1989]
+-/
+
+@[expose] public section
+
+namespace Cslib.Automata
+
+open scoped ωSequence
+open Acceptor
+
+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 `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 : ω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 : ω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`. -/
+  step_closed : a.IsStepClosed input cert
+  /-- No accepting state occurs past the end of the input. -/
+  accept_notMem : ∀ s ∈ cert input.length, s ∉ a.accept
+
+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) :
+    ¬ 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⟩
+  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) : ω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 : ¬ 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' htr := by
+    rintro ⟨hc_input, c₀, hstart, hlt, hreach⟩
+    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]
+    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) :
+    ¬ Accepts a input ↔ ∃ T, a.IsRejectionCert input T :=
+  ⟨fun h => ⟨_, isRejectionCert_reachable h⟩, by rintro ⟨_, hT⟩; exact hT.not_accepts⟩
+
+/-! ## Localising the closure condition -/
+
+/-- 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 `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 cert ↔
+      ∀ 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
+    cases m with
+    | zero =>
+      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[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[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.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
+    cases m with
+    | zero =>
+      have hpos' : (c'.pos : ℕ) = (c.pos : ℕ) := by simp at hpos; omega
+      rwa [hpos']
+    | pos =>
+      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⟩
+      have hpos' : (c'.pos : ℕ) = j := by omega
+      rw [hpos']
+      rwa [show ((⟨(c.pos : ℕ), hlt⟩ : Fin input.length) : ℕ) = j + 1 from hj] at hthis
+
+/-! ## The finite acceptor for the complement -/
+
+/-- 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
+    | (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 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 : ω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 ::ω ω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
+    · rintro ⟨f, hf, hmtr⟩
+      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 hstep : ∀ i, ∀ hi : i < (x :: xs).length, a.LocalOK (x :: xs)[i]
+          ((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, 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 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 [ω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
+      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) :
+    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 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 [h1] using hstart hq
+        step_closed := isStepClosed_iff_localOK.mpr hstep
+        accept_notMem := by simpa using hacc }⟩
+  · rintro ⟨cert, hCert⟩
+    have hloc := isStepClosed_iff_localOK.mp hCert.step_closed
+    obtain ⟨f, hf, hmtr⟩ := (exists_accepting_mTr_iff a input Set.univ (cert 0)).mpr
+      ⟨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) : language a.complToNA = (language a)ᶜ := by
+  ext xs
+  simp only [Acceptor.mem_language]
+  exact accepts_complToNA_iff a xs
+
+end TwoWayNA
+
+end Cslib.Automata
diff --git a/Cslib/Computability/Automata/TwoWayNA/OfNA.lean b/Cslib/Computability/Automata/TwoWayNA/OfNA.lean
new file mode 100644
index 000000000..5a556b013
--- /dev/null
+++ b/Cslib/Computability/Automata/TwoWayNA/OfNA.lean
@@ -0,0 +1,106 @@
+/-
+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,
+`NA.FinAcc.toTwoWayNA`.
+
+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 `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
+
+namespace Cslib.Automata
+
+variable {State Symbol : Type*} {input : List 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 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
+
+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 (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 [hpos', List.take_succ_eq_append_getElem hlt]
+  exact LTS.MTr.stepR _ hmtr htr
+
+/-- 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⟩
+    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_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⟩
+    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⟩
+    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_toTwoWayNA (a : NA.FinAcc State Symbol) : language a.toTwoWayNA = language a := by
+  ext xs
+  simpa [Acceptor.mem_language] using accepts_toTwoWayNA_iff a xs
+
+end TwoWayNA
+
+end Cslib.Automata
diff --git a/Cslib/Computability/Languages/RegularLanguage.lean b/Cslib/Computability/Languages/RegularLanguage.lean
index ae70a9fee..f14436718 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.ComplToNA
 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.complToNA, a.language_complToNA⟩
+    simpa using hc.compl
+
 /-- The empty language is regular. -/
 @[simp]
 theorem IsRegular.zero : (0 : Language Symbol).IsRegular := by