Two-way complementation: representation

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

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

theorem Complexity.FiniteAutomaton.Complementation.Internal.TwoNFA.diagram_representation {Sigma : Type u_1} {s : ℕ} (A : TwoNFA Sigma (Fin s)) : ∃ (τ : List Sigma → Diagram (s + 1)) (l : Diagram (s + 1)) (r : Diagram (s + 1)) (a : Fin (s + 1)) (b : Fin (s + 1)), τ [] = Diagram.identity (s + 1) ∧ (∀ (u v : List Sigma), τ (u ++ v) = (τ u).comp (τ v)) ∧ ∀ (w : List Sigma), w ∈ A.language ↔ (a, b) ∈ ((l.comp (τ w)).comp r).forward

Every 2NFA has an exact diagram representation with one additional state label.