OAI/Combinatorics/TwoWayAutomata/Representation.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.TwoWayComplementation.TwoNFA.diagram_representation line 10

   Source documentation

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

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

   Mentions: OAI.TwoWayComplementation.TwoNFA, OAI.TwoWayComplementation.Diagram, OAI.TwoWayComplementation.Diagram.identity, OAI.TwoWayComplementation.Diagram.comp