Two-way complementation: model

Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Combinatorics/TwoWayAutomata/Model.lean

Imports, namespaces, module visibility, documentation, and formatting are adapted for complexitylib. The source theorem statements and mathematical arguments are retained.

def Complexity.FiniteAutomaton.Complementation.Internal.relStar {α : Type u_1} (R : SetRel α α) : SetRel α α

Reflexive transitive closure, including the empty path.

Equations

• Complexity.FiniteAutomaton.Complementation.Internal.relStar R = {(x, y) : α × α | Relation.ReflTransGen (fun (a b : α) => (a, b) ∈ R) x y}

structure Complexity.FiniteAutomaton.Complementation.Internal.TwoNFA (Sigma : Type u_1) (Q : Type u_2) : Type (max u_1 u_2)

A read-only 2NFA. The two endmarkers are Sum.inl 0 and Sum.inl 1. Move codes 0, 1, 2 mean left, stay, right.

• initial : Q

  The state in which the machine starts on the left endmarker.

• accepting : Set Q

  States whose occurrence on a finite run constitutes acceptance.

• transition : Q → Fin 2 ⊕ Sigma → Set (Q × Fin 3)

  Allowed next-state and move pairs, determined by the state and scanned symbol.

def Complexity.FiniteAutomaton.Complementation.Internal.tapeSymbol {Sigma : Type u_1} (w : List Sigma) (p : Fin (w.length + 2)) : Fin 2 ⊕ Sigma

Tape lookup includes two distinct endmarkers, even on empty input.

Equations

• Complexity.FiniteAutomaton.Complementation.Internal.tapeSymbol w p = if hleft : ↑p = 0 then Sum.inl 0 else if hright : ↑p = w.length + 1 then Sum.inl 1 else Sum.inr w[↑p - 1]

def Complexity.FiniteAutomaton.Complementation.Internal.TwoNFA.step {Sigma : Type u_1} {Q : Type u_2} (A : TwoNFA Sigma Q) (w : List Sigma) : SetRel (Q × Fin (w.length + 2)) (Q × Fin (w.length + 2))

One legal step: both head positions stay within the marked input.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.FiniteAutomaton.Complementation.Internal.TwoNFA.language {Sigma : Type u_1} {Q : Type u_2} (A : TwoNFA Sigma Q) : Set (List Sigma)

Existential finite-run acceptance, allowing a run of length zero.

Equations

• One or more equations did not get rendered due to their size.