From e70ed7dece1193075f59a28fed72b8222c2714b0 Mon Sep 17 00:00:00 2001
From: crei <crei.github@gmail.com>
Date: Mon, 24 Aug 2026 14:25:15 +0200
Subject: [PATCH 1/8] Two-way automaton.

---
 Cslib.lean                                    |   1 +
 Cslib/Computability/Automata/TwoNA/Basic.lean | 133 ++++++++++++++++++
 references.bib                                |  10 ++
 3 files changed, 144 insertions(+)
 create mode 100644 Cslib/Computability/Automata/TwoNA/Basic.lean

diff --git a/Cslib.lean b/Cslib.lean
index a4d250711..c10c8d778 100644
--- a/Cslib.lean
+++ b/Cslib.lean
@@ -27,6 +27,7 @@ public import Cslib.Computability.Automata.NA.Sum
 public import Cslib.Computability.Automata.NA.ToDA
 public import Cslib.Computability.Automata.NA.Total
 public import Cslib.Computability.Automata.Transducers.Transducer
+public import Cslib.Computability.Automata.TwoNA.Basic
 public import Cslib.Computability.Distributed.FLP.Algorithm
 public import Cslib.Computability.Distributed.FLP.CanReachVia
 public import Cslib.Computability.Distributed.FLP.Consensus
diff --git a/Cslib/Computability/Automata/TwoNA/Basic.lean b/Cslib/Computability/Automata/TwoNA/Basic.lean
new file mode 100644
index 000000000..9b5e0c2b7
--- /dev/null
+++ b/Cslib/Computability/Automata/TwoNA/Basic.lean
@@ -0,0 +1,133 @@
+/-
+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.Acceptors.Acceptor
+public import Mathlib.Data.List.Chain
+public import Mathlib.Data.Sign.Basic
+
+/-! # Nondeterministic Two-Way Automaton
+
+A Nondeterministic Two-Way Automaton (TwoNA) reads a finite input word on a tape and may move its
+input head in either direction. A transition reads the symbol under the head and, besides changing
+the state, moves the head one cell to the left, keeps it in place, or moves it one cell to the
+right.
+
+Once it leaves the word to the right, the automaton cannot move back to the word. A run is accepting
+if it ends in an accepting state with the head just past the end of the input.
+
+## Main definitions
+
+* `TwoNA`, the automaton itself: The transition relation and the sets of initial and accepting
+  states.
+* `TwoNACfg`, a configuration of a `TwoNA` running on a fixed input: a state together with a head
+  position.
+* `TwoNA.Step`, The single-step relation between configurations.
+* `TwoNA.Run`, a run of a `TwoNA` on a fixed input: a nonempty chain of configurations linked by
+  steps that starts in an initial configuration.
+
+## Implementation notes
+
+The definition of `TwoNA` is kept close to [Vardi][Vardi1989]'s, because the main point is to
+prove equivalence to `NA.FinAcc`. This means we do not allow the head to move off the input to the
+left, but also do not provide an end marker. Once the head moves off to the right, it cannot move
+back into the word.
+
+Runs are `List.IsChain` chains of configurations, anchored at an initial configuration.
+
+## References
+
+* [Moshe Y. Vardi, *A Note on the Reduction of Two-Way Automata to One-Way Automata*][Vardi1989]
+
+-/
+
+@[expose] public section
+
+namespace Cslib.Automata
+
+variable {State Symbol : Type*}
+
+/-- A nondeterministic two-way automaton: a transition relation that reads an input symbol and
+moves the input head, together with a set of initial and a set of accepting states. -/
+structure TwoNA (State Symbol : Type*) where
+  /-- The transition relation. `Tr q x m q'` means that, while reading the symbol `x`, the
+  automaton can move from state `q` to state `q'` and move its head according to `m`. -/
+  Tr (q : State) (x : Symbol) (m : SignType) (q' : State) : Prop
+  /-- The set of initial states of the automaton. -/
+  start : Set State
+  /-- The set of accepting states of the automaton. -/
+  accept : Set State
+
+/-- The configuration of a two-way nondeterministic automaton. -/
+@[ext]
+structure TwoNACfg (State Symbol : Type*) (input : List Symbol) where
+  /-- The state of the automaton. -/
+  state : State
+  /-- The input head position of the automaton: it can be on any symbol of the input or on the
+  position one step to the right of the input. -/
+  pos : Fin (input.length + 1)
+
+namespace TwoNA
+
+variable {a : TwoNA State Symbol} {input : List Symbol} {c c' : TwoNACfg State Symbol input}
+
+/-- A single step of `a` on `input`. It is possible only while the head is on an actual input
+symbol, and it is performed by a transition of `a` that reads the symbol under the head: such a
+transition determines the new state and a head movement `m`, by which the head position changes.
+A leftward move at position `0` would take the head off the input, so no such step exists. -/
+def Step (a : TwoNA State Symbol) (input : List Symbol)
+    (c c' : TwoNACfg State Symbol input) : Prop :=
+  ∃ m, ∃ _ : (c.pos : ℕ) < input.length,
+    a.Tr c.state input[c.pos] m c'.state ∧ (c'.pos : ℤ) = (c.pos : ℤ) + (m.cast : ℤ)
+
+/-- A run of `a` on `input`: a nonempty chain of configurations, each obtained from the previous
+one by a step, that starts in an initial state with the head on the first symbol of the input. -/
+structure Run (a : TwoNA State Symbol) (input : List Symbol) where
+  /-- The chain of configurations. -/
+  chain : List (TwoNACfg State Symbol input)
+  /-- Consecutive configurations are linked by a step. -/
+  isChain : chain.IsChain (a.Step input)
+  /-- There is at least one configuration. -/
+  ne : chain ≠ []
+  /-- The head starts on the first symbol of the input. -/
+  head_pos : (chain.head ne).pos = 0
+  /-- The run starts in an initial state. -/
+  head_mem_start : (chain.head ne).state ∈ a.start
+
+/-- The configuration a run starts in. -/
+def Run.head (r : a.Run input) : TwoNACfg State Symbol input := r.chain.head r.ne
+
+/-- The configuration a run ends in. -/
+def Run.last (r : a.Run input) : TwoNACfg State Symbol input := (r.chain).getLast r.ne
+
+/-- A run is accepting if it ends in an accepting state with the head just past the end of the
+input. -/
+def Run.IsAccepting (r : a.Run input) : Prop := r.last.state ∈ a.accept ∧ r.last.pos = Fin.last _
+
+/-- Extend a run by one more step. -/
+def Run.snoc (r : a.Run input) (c : TwoNACfg State Symbol input) (h : a.Step input r.last c) :
+    a.Run input where
+  chain := r.chain ++ [c]
+  isChain := r.isChain.append (List.isChain_singleton c)
+    (by simp_all [Run.last, List.getLast?_eq_some_getLast r.ne])
+  ne := by simp
+  head_pos := by simpa [List.head_append_of_ne_nil r.ne] using r.head_pos
+  head_mem_start := by simpa [List.head_append_of_ne_nil r.ne] using r.head_mem_start
+
+@[simp]
+theorem Run.last_snoc (r : a.Run input) (c : TwoNACfg State Symbol input)
+    (h : a.Step input r.last c) : (r.snoc c h).last = c := by
+  simp [Run.snoc, Run.last]
+
+end TwoNA
+
+/-- A `TwoNA` accepts an input if it has an accepting run on it. -/
+@[simp, scoped grind =]
+instance : Acceptor (TwoNA State Symbol) Symbol where
+  Accepts (a : TwoNA State Symbol) (xs : List Symbol) := ∃ r : a.Run xs, r.IsAccepting
+
+end Cslib.Automata
diff --git a/references.bib b/references.bib
index d2a7dfb13..48aa4fd76 100644
--- a/references.bib
+++ b/references.bib
@@ -551,3 +551,13 @@ @book{Papadimitriou94
   publisher={Addison-Wesley},
   address={Reading, Massachusetts}
 }
+
+@article{Vardi1989,
+  author       = {Moshe Y. Vardi},
+  title        = {A Note on the Reduction of Two-Way Automata to One-Way Automata},
+  journal      = {Information Processing Letters},
+  volume       = {30},
+  number       = {5},
+  pages        = {261--264},
+  year         = {1989}
+}

From 7a37face4234cc822a60c8d72bfc97f1a3beef7b Mon Sep 17 00:00:00 2001
From: crei <crei.github@gmail.com>
Date: Thu, 27 Aug 2026 14:03:15 +0200
Subject: [PATCH 2/8] Base TwoNA on top of NA.

---
 Cslib/Computability/Automata/TwoNA/Basic.lean | 97 ++++++-------------
 1 file changed, 27 insertions(+), 70 deletions(-)

diff --git a/Cslib/Computability/Automata/TwoNA/Basic.lean b/Cslib/Computability/Automata/TwoNA/Basic.lean
index 9b5e0c2b7..0a87df2de 100644
--- a/Cslib/Computability/Automata/TwoNA/Basic.lean
+++ b/Cslib/Computability/Automata/TwoNA/Basic.lean
@@ -6,9 +6,11 @@ Authors: Christian Reitwiessner
 
 module
 
+public import Cslib.Computability.Automata.NA.Basic
 public import Cslib.Computability.Automata.Acceptors.Acceptor
 public import Mathlib.Data.List.Chain
 public import Mathlib.Data.Sign.Basic
+public import Cslib.Foundations.Data.List.IsChainFromTo
 
 /-! # Nondeterministic Two-Way Automaton
 
@@ -22,13 +24,10 @@ if it ends in an accepting state with the head just past the end of the input.
 
 ## Main definitions
 
-* `TwoNA`, the automaton itself: The transition relation and the sets of initial and accepting
-  states.
+* `TwoNA`, the automaton itself
 * `TwoNACfg`, a configuration of a `TwoNA` running on a fixed input: a state together with a head
   position.
 * `TwoNA.Step`, The single-step relation between configurations.
-* `TwoNA.Run`, a run of a `TwoNA` on a fixed input: a nonempty chain of configurations linked by
-  steps that starts in an initial configuration.
 
 ## Implementation notes
 
@@ -37,8 +36,6 @@ prove equivalence to `NA.FinAcc`. This means we do not allow the head to move of
 left, but also do not provide an end marker. Once the head moves off to the right, it cannot move
 back into the word.
 
-Runs are `List.IsChain` chains of configurations, anchored at an initial configuration.
-
 ## References
 
 * [Moshe Y. Vardi, *A Note on the Reduction of Two-Way Automata to One-Way Automata*][Vardi1989]
@@ -51,16 +48,9 @@ namespace Cslib.Automata
 
 variable {State Symbol : Type*}
 
-/-- A nondeterministic two-way automaton: a transition relation that reads an input symbol and
-moves the input head, together with a set of initial and a set of accepting states. -/
-structure TwoNA (State Symbol : Type*) where
-  /-- The transition relation. `Tr q x m q'` means that, while reading the symbol `x`, the
-  automaton can move from state `q` to state `q'` and move its head according to `m`. -/
-  Tr (q : State) (x : Symbol) (m : SignType) (q' : State) : Prop
-  /-- The set of initial states of the automaton. -/
-  start : Set State
-  /-- The set of accepting states of the automaton. -/
-  accept : Set State
+/-- A nondeterministic two-way automaton is a nondeterministic automaton whose labels
+consist of an input symbol and an input head movement. -/
+def TwoNA (State Symbol : Type*) := NA State (Symbol × SignType)
 
 /-- The configuration of a two-way nondeterministic automaton. -/
 @[ext]
@@ -71,63 +61,30 @@ structure TwoNACfg (State Symbol : Type*) (input : List Symbol) where
   position one step to the right of the input. -/
   pos : Fin (input.length + 1)
 
-namespace TwoNA
+def TwoNACfg.IsInitial (a : TwoNA State Symbol) {input : List Symbol}
+    (c : TwoNACfg State Symbol input) : Prop :=
+  c.state ∈ a.start ∧ c.pos = 0
 
-variable {a : TwoNA State Symbol} {input : List Symbol} {c c' : TwoNACfg State Symbol input}
-
-/-- A single step of `a` on `input`. It is possible only while the head is on an actual input
-symbol, and it is performed by a transition of `a` that reads the symbol under the head: such a
-transition determines the new state and a head movement `m`, by which the head position changes.
-A leftward move at position `0` would take the head off the input, so no such step exists. -/
-def Step (a : TwoNA State Symbol) (input : List Symbol)
+def TwoNA.Step (a : TwoNA State Symbol) (input : List Symbol)
     (c c' : TwoNACfg State Symbol input) : Prop :=
   ∃ m, ∃ _ : (c.pos : ℕ) < input.length,
-    a.Tr c.state input[c.pos] m c'.state ∧ (c'.pos : ℤ) = (c.pos : ℤ) + (m.cast : ℤ)
-
-/-- A run of `a` on `input`: a nonempty chain of configurations, each obtained from the previous
-one by a step, that starts in an initial state with the head on the first symbol of the input. -/
-structure Run (a : TwoNA State Symbol) (input : List Symbol) where
-  /-- The chain of configurations. -/
-  chain : List (TwoNACfg State Symbol input)
-  /-- Consecutive configurations are linked by a step. -/
-  isChain : chain.IsChain (a.Step input)
-  /-- There is at least one configuration. -/
-  ne : chain ≠ []
-  /-- The head starts on the first symbol of the input. -/
-  head_pos : (chain.head ne).pos = 0
-  /-- The run starts in an initial state. -/
-  head_mem_start : (chain.head ne).state ∈ a.start
-
-/-- The configuration a run starts in. -/
-def Run.head (r : a.Run input) : TwoNACfg State Symbol input := r.chain.head r.ne
-
-/-- The configuration a run ends in. -/
-def Run.last (r : a.Run input) : TwoNACfg State Symbol input := (r.chain).getLast r.ne
-
-/-- A run is accepting if it ends in an accepting state with the head just past the end of the
-input. -/
-def Run.IsAccepting (r : a.Run input) : Prop := r.last.state ∈ a.accept ∧ r.last.pos = Fin.last _
-
-/-- Extend a run by one more step. -/
-def Run.snoc (r : a.Run input) (c : TwoNACfg State Symbol input) (h : a.Step input r.last c) :
-    a.Run input where
-  chain := r.chain ++ [c]
-  isChain := r.isChain.append (List.isChain_singleton c)
-    (by simp_all [Run.last, List.getLast?_eq_some_getLast r.ne])
-  ne := by simp
-  head_pos := by simpa [List.head_append_of_ne_nil r.ne] using r.head_pos
-  head_mem_start := by simpa [List.head_append_of_ne_nil r.ne] using r.head_mem_start
-
-@[simp]
-theorem Run.last_snoc (r : a.Run input) (c : TwoNACfg State Symbol input)
-    (h : a.Step input r.last c) : (r.snoc c h).last = c := by
-  simp [Run.snoc, Run.last]
-
-end TwoNA
-
-/-- A `TwoNA` accepts an input if it has an accepting run on it. -/
+    a.Tr c.state (input[c.pos], m) c'.state ∧ (c'.pos : ℤ) = (c.pos : ℤ) + (m.cast : ℤ)
+
+/-- A nondeterministic two-way automaton that accepts finite strings (lists of symbols). -/
+structure TwoNAFinAcc (State Symbol : Type*) extends TwoNA State Symbol where
+  /-- The set of accepting states. -/
+  accept : Set State
+
+def TwoNACfg.IsAccepting (a : TwoNAFinAcc State Symbol) {input : List Symbol}
+    (c : TwoNACfg State Symbol input) : Prop :=
+  c.state ∈ a.accept ∧ c.pos = Fin.last _
+
 @[simp, scoped grind =]
-instance : Acceptor (TwoNA State Symbol) Symbol where
-  Accepts (a : TwoNA State Symbol) (xs : List Symbol) := ∃ r : a.Run xs, r.IsAccepting
+instance : Acceptor (TwoNAFinAcc State Symbol) Symbol where
+  Accepts (a : TwoNAFinAcc State Symbol) (xs : List Symbol) :=
+    ∃ (chain : List (TwoNACfg State Symbol xs)) (s s' : TwoNACfg State Symbol xs),
+      chain.IsChainFromTo (TwoNA.Step a.toNA xs) s s' ∧
+      s.IsInitial a.toNA ∧ s'.IsAccepting a
+
 
 end Cslib.Automata

From db280cb87a4141e2dd9edb54f959cd54d0d2493d Mon Sep 17 00:00:00 2001
From: crei <crei.github@gmail.com>
Date: Thu, 27 Aug 2026 16:47:19 +0200
Subject: [PATCH 3/8] Define TwoNA via LTS on configurations.

---
 Cslib/Computability/Automata/TwoNA/Basic.lean | 68 +++++++++++++------
 .../Foundations/Semantics/LTS/Execution.lean  | 11 ++-
 2 files changed, 58 insertions(+), 21 deletions(-)

diff --git a/Cslib/Computability/Automata/TwoNA/Basic.lean b/Cslib/Computability/Automata/TwoNA/Basic.lean
index 0a87df2de..0b007b28d 100644
--- a/Cslib/Computability/Automata/TwoNA/Basic.lean
+++ b/Cslib/Computability/Automata/TwoNA/Basic.lean
@@ -48,9 +48,19 @@ namespace Cslib.Automata
 
 variable {State Symbol : Type*}
 
-/-- A nondeterministic two-way automaton is a nondeterministic automaton whose labels
-consist of an input symbol and an input head movement. -/
-def TwoNA (State Symbol : Type*) := NA State (Symbol × SignType)
+/-- The type of the transition relation of a two-way automaton. -/
+def TwoNATr (State Symbol : Type*) := State → Symbol → SignType → State → Prop
+
+/-- A nondeterministic two-way automaton: a transition relation that reads an input symbol and
+moves the input head, together with a set of initial and a set of accepting states. -/
+structure TwoNA (State Symbol : Type*) where
+  /-- The transition relation. `Tr q x m q'` means that, while reading the symbol `x`, the
+  automaton can move from state `q` to state `q'` and move its head according to `m`. -/
+  Tr : TwoNATr State Symbol
+  /-- The set of initial states of the automaton. -/
+  start : Set State
+  /-- The set of accepting states of the automaton. -/
+  accept : Set State
 
 /-- The configuration of a two-way nondeterministic automaton. -/
 @[ext]
@@ -61,30 +71,50 @@ structure TwoNACfg (State Symbol : Type*) (input : List Symbol) where
   position one step to the right of the input. -/
   pos : Fin (input.length + 1)
 
+
 def TwoNACfg.IsInitial (a : TwoNA State Symbol) {input : List Symbol}
     (c : TwoNACfg State Symbol input) : Prop :=
   c.state ∈ a.start ∧ c.pos = 0
 
-def TwoNA.Step (a : TwoNA State Symbol) (input : List Symbol)
-    (c c' : TwoNACfg State Symbol input) : Prop :=
-  ∃ m, ∃ _ : (c.pos : ℕ) < input.length,
-    a.Tr c.state (input[c.pos], m) c'.state ∧ (c'.pos : ℤ) = (c.pos : ℤ) + (m.cast : ℤ)
-
-/-- A nondeterministic two-way automaton that accepts finite strings (lists of symbols). -/
-structure TwoNAFinAcc (State Symbol : Type*) extends TwoNA State Symbol where
-  /-- The set of accepting states. -/
-  accept : Set State
-
-def TwoNACfg.IsAccepting (a : TwoNAFinAcc State Symbol) {input : List Symbol}
+def TwoNACfg.IsAccepting (a : TwoNA State Symbol) {input : List Symbol}
     (c : TwoNACfg State Symbol input) : Prop :=
   c.state ∈ a.accept ∧ c.pos = Fin.last _
 
+------------------- via LTS -------------------------
+
+def TwoNATr.toCfgTr {State Symbol : Type*} (tr : TwoNATr State Symbol) (input : List Symbol) :
+    TwoNACfg State Symbol input → Symbol × SignType → TwoNACfg State Symbol input → Prop
+  | c, (x, m), c' =>
+    some x = input[c.pos]? ∧
+    tr c.state x m c'.state ∧
+    (c'.pos : ℤ) = (c.pos : ℤ) + (m.cast : ℤ)
+
+def TwoNA.toCfgLTS {State Symbol : Type*} (a : TwoNA State Symbol) (input : List Symbol) :
+    NA.FinAcc (TwoNACfg State Symbol input) (Symbol × SignType) where
+  Tr := a.Tr.toCfgTr input
+  start := { c | c.IsInitial a }
+  accept := { c | c.IsAccepting a }
+
 @[simp, scoped grind =]
-instance : Acceptor (TwoNAFinAcc State Symbol) Symbol where
-  Accepts (a : TwoNAFinAcc State Symbol) (xs : List Symbol) :=
-    ∃ (chain : List (TwoNACfg State Symbol xs)) (s s' : TwoNACfg State Symbol xs),
-      chain.IsChainFromTo (TwoNA.Step a.toNA xs) s s' ∧
-      s.IsInitial a.toNA ∧ s'.IsAccepting a
+instance : Acceptor (TwoNA State Symbol) Symbol where
+  Accepts (a : TwoNA State Symbol) (input : List Symbol) :=
+    ∃ μs, Acceptor.Accepts (a.toCfgLTS input) μs
+
+------------------ alternative ---------------------------
 
+def TwoNA.Step {State Symbol : Type*} (a : TwoNA State Symbol) {input : List Symbol}
+    (c c' : TwoNACfg State Symbol input) : Prop :=
+  ∃ x m,
+    a.Tr c.state x m c'.state ∧
+    some x = input[c.pos]? ∧
+    (c'.pos : ℤ) = (c.pos : ℤ) + (m.cast : ℤ)
+
+@[simp, scoped grind =]
+instance : Acceptor (TwoNA State Symbol) Symbol where
+  Accepts (a : TwoNA State Symbol) (input : List Symbol) :=
+    ∃ (init final : TwoNACfg State Symbol input),
+    ∃ cfgs : List (TwoNACfg State Symbol input),
+    init.IsInitial a ∧ final.IsAccepting a ∧
+    cfgs.IsChainFromTo a.Step init final
 
 end Cslib.Automata
diff --git a/Cslib/Foundations/Semantics/LTS/Execution.lean b/Cslib/Foundations/Semantics/LTS/Execution.lean
index fd49f191e..cac09cbb9 100644
--- a/Cslib/Foundations/Semantics/LTS/Execution.lean
+++ b/Cslib/Foundations/Semantics/LTS/Execution.lean
@@ -7,6 +7,7 @@ Authors: Fabrizio Montesi, Ching-Tsun Chou
 module
 
 public import Cslib.Foundations.Semantics.LTS.Basic
+public import Cslib.Foundations.Data.List.IsChainFromTo
 
 /-!
 # Finite executions of LTS
@@ -84,10 +85,16 @@ theorem Execution.to_mTr (hexec : lts.Execution s1 μs s2 ss) :
         apply this
       · grind
 
+/-- The states visited by an execution form a chain from the initial to the final state
+in the underlying unlabelled relation. -/
+theorem Execution.isChainFromTo (hexec : lts.Execution s1 μs s2 ss) :
+    ss.IsChainFromTo lts.UnlabelledTr s1 s2 := by
+  grind [List.IsChainFromTo, Execution, List.isChain_iff_getElem, UnlabelledTr]
+
 /-- The states visited by an execution form a chain in the underlying unlabelled relation. -/
 theorem Execution.isChain (hexec : lts.Execution s1 μs s2 ss) :
-    ss.IsChain lts.UnlabelledTr := by
-  grind [Execution, List.isChain_iff_getElem, UnlabelledTr]
+    ss.IsChain lts.UnlabelledTr :=
+  (Execution.isChainFromTo hexec).isChain
 
 open scoped Execution
 /-- Correspondence of multistep transitions and executions. -/

From 33dd1d0f7c52f018df5b2f20a5526fc365762c00 Mon Sep 17 00:00:00 2001
From: Ching-Tsun Chou <chingtsun.chou@gmail.com>
Date: Thu, 27 Aug 2026 15:27:36 -0700
Subject: [PATCH 4/8] An alternative design of two-way automata

---
 .../Automata/TwoNA/BasicAlt.lean              | 81 +++++++++++++++++++
 1 file changed, 81 insertions(+)
 create mode 100644 Cslib/Computability/Automata/TwoNA/BasicAlt.lean

diff --git a/Cslib/Computability/Automata/TwoNA/BasicAlt.lean b/Cslib/Computability/Automata/TwoNA/BasicAlt.lean
new file mode 100644
index 000000000..d1a356b13
--- /dev/null
+++ b/Cslib/Computability/Automata/TwoNA/BasicAlt.lean
@@ -0,0 +1,81 @@
+/-
+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.Acceptors.Acceptor
+public import Mathlib.Data.List.Chain
+public import Mathlib.Data.Sign.Basic
+public import Cslib.Foundations.Data.List.IsChainFromTo
+
+/-! # Nondeterministic Two-Way Automaton
+-/
+
+@[expose] public section
+
+namespace Cslib.Automata
+
+variable {State Symbol : Type*}
+
+/-- The word to be accepted is put in the state component `input`. This is necessary
+because the `Acceptor` framework refers only to the automaton and nothing else.  So
+you can't make the word to be accepted a parameter of the automaton. -/
+@[ext]
+structure TwoWayState (State Symbol : Type*) where
+  state : State
+  input : List Symbol
+  inpPos : ℕ
+
+/-- Another alternative is to use `Unit` for this type.  But I thik exposing the contents of
+the state transitions can potentially faciliate proofs because an execution in the sense
+of `LTS.Execution` would then include all nondeterministic choices made by an execution. -/
+@[ext]
+structure TwoWaySymbol (Symbol : Type*) where
+  symbol : Symbol
+  dir : SignType
+
+abbrev TwoWayLTS (State Symbol : Type*) :=
+  LTS (TwoWayState State Symbol) (TwoWaySymbol Symbol)
+
+structure TwoWayNA (State Symbol : Type*) where
+  LTS : TwoWayLTS State Symbol
+  start : Set (TwoWayState State Symbol)
+  accept : Set (TwoWayState State Symbol)
+  /-- We require that the state component `input` never changes. -/
+  input_inv : ∀ s x t, LTS.Tr s x t → t.input = s.input
+
+namespace TwoWayNA
+
+/-- The word to be accepted is put in the state component `input` at the beginning.
+The read pointer `inpPos` is at 0 at the beginning and just beyond `input` at the end.
+You can choose to change that requirement. -/
+instance : Acceptor (TwoWayNA State Symbol) Symbol where
+  Accepts (a : TwoWayNA State Symbol) (xs : List Symbol) : Prop :=
+    ∃ s, s ∈ a.start ∧ s.input = xs ∧ s.inpPos = 0 ∧
+      ∃ ys t, a.LTS.MTr s ys t ∧ t ∈ a.accept ∧ t.inpPos = s.input.length
+
+end TwoWayNA
+
+def TwoWayTr (State Symbol : Type*) := State → Symbol → SignType → State → Prop
+
+def twoWayLTS.mk (tr : TwoWayTr State Symbol) : TwoWayLTS State Symbol where
+  Tr s' x' t' := ∃ _ : s'.inpPos < s'.input.length,
+    s'.input[s'.inpPos] = x'.symbol ∧ t'.input = s'.input ∧
+    tr s'.state x'.symbol x'.dir t'.state ∧
+    match x'.dir with
+    | SignType.zero => t'.inpPos = s'.inpPos
+    | SignType.pos => t'.inpPos = s'.inpPos.succ
+    | SignType.neg => t'.inpPos = s'.inpPos.pred
+
+def twoWayNA.mk (tr : TwoWayTr State Symbol) (start accept : Set State)
+    : TwoWayNA State Symbol where
+  LTS := twoWayLTS.mk tr
+  start := (fun s' ↦ s'.state) ⁻¹' start
+  accept := (fun s' ↦ s'.state) ⁻¹' accept
+  input_inv s' x' t' := by grind [twoWayLTS.mk]
+
+end Cslib.Automata

From 355da3c510015410aa9c521984b3f32f52df80ab Mon Sep 17 00:00:00 2001
From: crei <crei.github@gmail.com>
Date: Fri, 28 Aug 2026 16:03:17 +0200
Subject: [PATCH 5/8] Bundle input into configurations.

---
 Cslib/Computability/Automata/TwoNA/Basic.lean | 38 ++++++++++---------
 1 file changed, 20 insertions(+), 18 deletions(-)

diff --git a/Cslib/Computability/Automata/TwoNA/Basic.lean b/Cslib/Computability/Automata/TwoNA/Basic.lean
index 0b007b28d..94113902e 100644
--- a/Cslib/Computability/Automata/TwoNA/Basic.lean
+++ b/Cslib/Computability/Automata/TwoNA/Basic.lean
@@ -64,7 +64,9 @@ structure TwoNA (State Symbol : Type*) where
 
 /-- The configuration of a two-way nondeterministic automaton. -/
 @[ext]
-structure TwoNACfg (State Symbol : Type*) (input : List Symbol) where
+structure TwoNACfg (State Symbol : Type*) where
+  /-- The original input to the automaton. -/
+  input : List Symbol
   /-- The state of the automaton. -/
   state : State
   /-- The input head position of the automaton: it can be on any symbol of the input or on the
@@ -72,27 +74,27 @@ structure TwoNACfg (State Symbol : Type*) (input : List Symbol) where
   pos : Fin (input.length + 1)
 
 
-def TwoNACfg.IsInitial (a : TwoNA State Symbol) {input : List Symbol}
-    (c : TwoNACfg State Symbol input) : Prop :=
-  c.state ∈ a.start ∧ c.pos = 0
+def TwoNACfg.IsInitialForInput (a : TwoNA State Symbol) (c : TwoNACfg State Symbol)
+    (input : List Symbol) : Prop :=
+  c.state ∈ a.start ∧ c.pos = 0 ∧ c.input = input
 
-def TwoNACfg.IsAccepting (a : TwoNA State Symbol) {input : List Symbol}
-    (c : TwoNACfg State Symbol input) : Prop :=
+def TwoNACfg.IsAccepting (a : TwoNA State Symbol) (c : TwoNACfg State Symbol) : Prop :=
   c.state ∈ a.accept ∧ c.pos = Fin.last _
 
 ------------------- via LTS -------------------------
 
-def TwoNATr.toCfgTr {State Symbol : Type*} (tr : TwoNATr State Symbol) (input : List Symbol) :
-    TwoNACfg State Symbol input → Symbol × SignType → TwoNACfg State Symbol input → Prop
+def TwoNATr.toCfgTr {State Symbol : Type*} (tr : TwoNATr State Symbol) :
+    TwoNACfg State Symbol → Symbol × SignType → TwoNACfg State Symbol → Prop
   | c, (x, m), c' =>
-    some x = input[c.pos]? ∧
+    c.input = c'.input ∧
+    some x = c.input[c.pos]? ∧
     tr c.state x m c'.state ∧
     (c'.pos : ℤ) = (c.pos : ℤ) + (m.cast : ℤ)
 
 def TwoNA.toCfgLTS {State Symbol : Type*} (a : TwoNA State Symbol) (input : List Symbol) :
-    NA.FinAcc (TwoNACfg State Symbol input) (Symbol × SignType) where
-  Tr := a.Tr.toCfgTr input
-  start := { c | c.IsInitial a }
+    NA.FinAcc (TwoNACfg State Symbol) (Symbol × SignType) where
+  Tr := a.Tr.toCfgTr
+  start := { c | c.IsInitialForInput a input }
   accept := { c | c.IsAccepting a }
 
 @[simp, scoped grind =]
@@ -102,19 +104,19 @@ instance : Acceptor (TwoNA State Symbol) Symbol where
 
 ------------------ alternative ---------------------------
 
-def TwoNA.Step {State Symbol : Type*} (a : TwoNA State Symbol) {input : List Symbol}
-    (c c' : TwoNACfg State Symbol input) : Prop :=
+def TwoNA.Step {State Symbol : Type*} (a : TwoNA State Symbol) (c c' : TwoNACfg State Symbol) :=
   ∃ x m,
+    c.input = c'.input ∧
+    some x = c.input[c.pos]? ∧
     a.Tr c.state x m c'.state ∧
-    some x = input[c.pos]? ∧
     (c'.pos : ℤ) = (c.pos : ℤ) + (m.cast : ℤ)
 
 @[simp, scoped grind =]
 instance : Acceptor (TwoNA State Symbol) Symbol where
   Accepts (a : TwoNA State Symbol) (input : List Symbol) :=
-    ∃ (init final : TwoNACfg State Symbol input),
-    ∃ cfgs : List (TwoNACfg State Symbol input),
-    init.IsInitial a ∧ final.IsAccepting a ∧
+    ∃ init final, ∃ cfgs : List (TwoNACfg State Symbol),
+    init.IsInitialForInput a input ∧
+    final.IsAccepting a ∧
     cfgs.IsChainFromTo a.Step init final
 
 end Cslib.Automata

From 4e8d6e42bc8f76fe0b92e075ca8ea02677f61242 Mon Sep 17 00:00:00 2001
From: crei <crei.github@gmail.com>
Date: Sat, 29 Aug 2026 09:07:14 +0200
Subject: [PATCH 6/8] Rename files.

---
 Cslib.lean                                                     | 2 +-
 Cslib/Computability/Automata/{TwoNA => TwoWayNA}/Basic.lean    | 0
 Cslib/Computability/Automata/{TwoNA => TwoWayNA}/BasicAlt.lean | 0
 3 files changed, 1 insertion(+), 1 deletion(-)
 rename Cslib/Computability/Automata/{TwoNA => TwoWayNA}/Basic.lean (100%)
 rename Cslib/Computability/Automata/{TwoNA => TwoWayNA}/BasicAlt.lean (100%)

diff --git a/Cslib.lean b/Cslib.lean
index 7be5363e4..7d2baa571 100644
--- a/Cslib.lean
+++ b/Cslib.lean
@@ -28,7 +28,7 @@ public import Cslib.Computability.Automata.NA.Sum
 public import Cslib.Computability.Automata.NA.ToDA
 public import Cslib.Computability.Automata.NA.Total
 public import Cslib.Computability.Automata.Transducers.Transducer
-public import Cslib.Computability.Automata.TwoNA.Basic
+public import Cslib.Computability.Automata.TwoWayNA.Basic
 public import Cslib.Computability.Distributed.FLP.Algorithm
 public import Cslib.Computability.Distributed.FLP.CanReachVia
 public import Cslib.Computability.Distributed.FLP.Consensus
diff --git a/Cslib/Computability/Automata/TwoNA/Basic.lean b/Cslib/Computability/Automata/TwoWayNA/Basic.lean
similarity index 100%
rename from Cslib/Computability/Automata/TwoNA/Basic.lean
rename to Cslib/Computability/Automata/TwoWayNA/Basic.lean
diff --git a/Cslib/Computability/Automata/TwoNA/BasicAlt.lean b/Cslib/Computability/Automata/TwoWayNA/BasicAlt.lean
similarity index 100%
rename from Cslib/Computability/Automata/TwoNA/BasicAlt.lean
rename to Cslib/Computability/Automata/TwoWayNA/BasicAlt.lean

From f505fe93314dc3c1f73f02144023d11146bc496c Mon Sep 17 00:00:00 2001
From: crei <crei.github@gmail.com>
Date: Sat, 29 Aug 2026 09:27:23 +0200
Subject: [PATCH 7/8] Cleanup.

---
 .../Automata/TwoWayNA/Basic.lean              | 88 +++++++------------
 1 file changed, 34 insertions(+), 54 deletions(-)

diff --git a/Cslib/Computability/Automata/TwoWayNA/Basic.lean b/Cslib/Computability/Automata/TwoWayNA/Basic.lean
index 94113902e..a14db60b4 100644
--- a/Cslib/Computability/Automata/TwoWayNA/Basic.lean
+++ b/Cslib/Computability/Automata/TwoWayNA/Basic.lean
@@ -14,24 +14,24 @@ public import Cslib.Foundations.Data.List.IsChainFromTo
 
 /-! # Nondeterministic Two-Way Automaton
 
-A Nondeterministic Two-Way Automaton (TwoNA) reads a finite input word on a tape and may move its
-input head in either direction. A transition reads the symbol under the head and, besides changing
-the state, moves the head one cell to the left, keeps it in place, or moves it one cell to the
-right.
+A Nondeterministic Two-Way Automaton (`TwoWayNA`) reads a finite input word on a tape and may move
+its input head in either direction. A transition reads the symbol under the head and, besides
+changing the state, moves the head one cell to the left, keeps it in place, or moves it one cell to
+the right.
 
-Once it leaves the word to the right, the automaton cannot move back to the word. A run is accepting
-if it ends in an accepting state with the head just past the end of the input.
+The input head cannot leave the input word to the left and once it leaves the word to the right,
+it stops. A run is accepting if and only if it ends in an accepting state with the head just past
+the end of the input.
 
 ## Main definitions
 
-* `TwoNA`, the automaton itself
-* `TwoNACfg`, a configuration of a `TwoNA` running on a fixed input: a state together with a head
-  position.
-* `TwoNA.Step`, The single-step relation between configurations.
+* `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.
 
 ## Implementation notes
 
-The definition of `TwoNA` is kept close to [Vardi][Vardi1989]'s, because the main point is to
+The definition of `TwoWayNA` is kept close to [Vardi][Vardi1989]'s, because the main point is to
 prove equivalence to `NA.FinAcc`. This means we do not allow the head to move off the input to the
 left, but also do not provide an end marker. Once the head moves off to the right, it cannot move
 back into the word.
@@ -48,15 +48,13 @@ namespace Cslib.Automata
 
 variable {State Symbol : Type*}
 
-/-- The type of the transition relation of a two-way automaton. -/
-def TwoNATr (State Symbol : Type*) := State → Symbol → SignType → State → Prop
-
 /-- A nondeterministic two-way automaton: a transition relation that reads an input symbol and
 moves the input head, together with a set of initial and a set of accepting states. -/
-structure TwoNA (State Symbol : Type*) where
+structure TwoWayNA (State Symbol : Type*) where
   /-- The transition relation. `Tr q x m q'` means that, while reading the symbol `x`, the
-  automaton can move from state `q` to state `q'` and move its head according to `m`. -/
-  Tr : TwoNATr State Symbol
+  automaton attempts to transition from state `q` to state `q'` and move its head according to
+  `m`. -/
+  Tr (q : State) (x : Symbol) (m : SignType) (q' : State) : Prop
   /-- The set of initial states of the automaton. -/
   start : Set State
   /-- The set of accepting states of the automaton. -/
@@ -64,7 +62,7 @@ structure TwoNA (State Symbol : Type*) where
 
 /-- The configuration of a two-way nondeterministic automaton. -/
 @[ext]
-structure TwoNACfg (State Symbol : Type*) where
+structure TwoWayNACfg (State Symbol : Type*) where
   /-- The original input to the automaton. -/
   input : List Symbol
   /-- The state of the automaton. -/
@@ -73,50 +71,32 @@ structure TwoNACfg (State Symbol : Type*) where
   position one step to the right of the input. -/
   pos : Fin (input.length + 1)
 
-
-def TwoNACfg.IsInitialForInput (a : TwoNA State Symbol) (c : TwoNACfg State Symbol)
+/-- This defines the set of initial configurations on a specific input. -/
+def TwoWayNACfg.IsInitialForInput (a : TwoWayNA State Symbol) (c : TwoWayNACfg State Symbol)
     (input : List Symbol) : Prop :=
   c.state ∈ a.start ∧ c.pos = 0 ∧ c.input = input
 
-def TwoNACfg.IsAccepting (a : TwoNA State Symbol) (c : TwoNACfg State Symbol) : Prop :=
+/-- If a configuration is a accepting. -/
+def TwoWayNACfg.IsAccepting (a : TwoWayNA State Symbol) (c : TwoWayNACfg State Symbol) : Prop :=
   c.state ∈ a.accept ∧ c.pos = Fin.last _
 
-------------------- via LTS -------------------------
-
-def TwoNATr.toCfgTr {State Symbol : Type*} (tr : TwoNATr State Symbol) :
-    TwoNACfg State Symbol → Symbol × SignType → TwoNACfg State Symbol → Prop
-  | c, (x, m), c' =>
-    c.input = c'.input ∧
-    some x = c.input[c.pos]? ∧
-    tr c.state x m c'.state ∧
-    (c'.pos : ℤ) = (c.pos : ℤ) + (m.cast : ℤ)
-
-def TwoNA.toCfgLTS {State Symbol : Type*} (a : TwoNA State Symbol) (input : List Symbol) :
-    NA.FinAcc (TwoNACfg State Symbol) (Symbol × SignType) where
-  Tr := a.Tr.toCfgTr
+/-- 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)
+    (input : List Symbol) :
+    NA.FinAcc (TwoWayNACfg State Symbol) (Symbol × SignType) where
+  Tr
+    | c, (x, m), c' =>
+      c.input = c'.input ∧
+      some x = c.input[c.pos]? ∧
+      a.Tr c.state x m c'.state ∧
+      (c'.pos : ℤ) = (c.pos : ℤ) + (m.cast : ℤ)
   start := { c | c.IsInitialForInput a input }
   accept := { c | c.IsAccepting a }
 
 @[simp, scoped grind =]
-instance : Acceptor (TwoNA State Symbol) Symbol where
-  Accepts (a : TwoNA State Symbol) (input : List Symbol) :=
-    ∃ μs, Acceptor.Accepts (a.toCfgLTS input) μs
-
------------------- alternative ---------------------------
-
-def TwoNA.Step {State Symbol : Type*} (a : TwoNA State Symbol) (c c' : TwoNACfg State Symbol) :=
-  ∃ x m,
-    c.input = c'.input ∧
-    some x = c.input[c.pos]? ∧
-    a.Tr c.state x m c'.state ∧
-    (c'.pos : ℤ) = (c.pos : ℤ) + (m.cast : ℤ)
-
-@[simp, scoped grind =]
-instance : Acceptor (TwoNA State Symbol) Symbol where
-  Accepts (a : TwoNA State Symbol) (input : List Symbol) :=
-    ∃ init final, ∃ cfgs : List (TwoNACfg State Symbol),
-    init.IsInitialForInput a input ∧
-    final.IsAccepting a ∧
-    cfgs.IsChainFromTo a.Step init final
+instance : Acceptor (TwoWayNA State Symbol) Symbol where
+  Accepts (a : TwoWayNA State Symbol) (input : List Symbol) :=
+    ∃ μs, Acceptor.Accepts (a.toCfgNAFinAcc input) μs
 
 end Cslib.Automata

From 9fe8b571fa5304f8b57b08f98a4c691b91058aac Mon Sep 17 00:00:00 2001
From: crei <crei.github@gmail.com>
Date: Wed, 2 Sep 2026 10:30:44 +0200
Subject: [PATCH 8/8] Add more comments.

---
 .../Automata/TwoWayNA/Basic.lean              | 19 +++++++++++++------
 1 file changed, 13 insertions(+), 6 deletions(-)

diff --git a/Cslib/Computability/Automata/TwoWayNA/Basic.lean b/Cslib/Computability/Automata/TwoWayNA/Basic.lean
index a14db60b4..b7188b6a6 100644
--- a/Cslib/Computability/Automata/TwoWayNA/Basic.lean
+++ b/Cslib/Computability/Automata/TwoWayNA/Basic.lean
@@ -19,9 +19,9 @@ its input head in either direction. A transition reads the symbol under the head
 changing the state, moves the head one cell to the left, keeps it in place, or moves it one cell to
 the right.
 
-The input head cannot leave the input word to the left and once it leaves the word to the right,
-it stops. A run is accepting if and only if it ends in an accepting state with the head just past
-the end of the input.
+The input head cannot leave the input word to the left (in the sense that execution gets stuck in
+this case) and once it leaves the word to the right, it stops. A run is accepting if and only if it
+ends in an accepting state with the head just past the end of the input.
 
 ## Main definitions
 
@@ -32,9 +32,11 @@ the end of the input.
 ## Implementation notes
 
 The definition of `TwoWayNA` is kept close to [Vardi][Vardi1989]'s, because the main point is to
-prove equivalence to `NA.FinAcc`. This means we do not allow the head to move off the input to the
-left, but also do not provide an end marker. Once the head moves off to the right, it cannot move
-back into the word.
+prove that it accepts the same languages as `NA.FinAcc` via his proof. This means we do not allow
+the head to move off the input to the left (in the sense that if the transition relation has an
+entry that would cause that, there is no successor configuration, the computation is stuck), but
+also do not provide an end marker. Once the head moves off to the right, the machine instantly
+stops, so it also cannot move back into the word.
 
 ## References
 
@@ -88,8 +90,13 @@ def TwoWayNA.toCfgNAFinAcc {State Symbol : Type*} (a : TwoWayNA State Symbol)
   Tr
     | c, (x, m), c' =>
       c.input = c'.input ∧
+      -- This also enforces that `c`'s input head position has to be inside the word.
       some x = c.input[c.pos]? ∧
       a.Tr c.state x m c'.state ∧
+      -- By doing input head position arithmetic and comparison in the integers, we get the
+      -- desired restrictions since `0 ≤ c'.pos < n + 1` and `0 ≤ c.pos < n`:
+      -- The input head after the transition cannot be left of the word but it is fine to be
+      -- one position right of the word (in which case no further transition is possible).
       (c'.pos : ℤ) = (c.pos : ℤ) + (m.cast : ℤ)
   start := { c | c.IsInitialForInput a input }
   accept := { c | c.IsAccepting a }