OAI/Combinatorics/TwoWayAutomata/PolynomialBound.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.TwoWayComplementation.no_polynomial_determinization line 8

   Source documentation

   No alphabet-uniform polynomial state bound determinizes all 2NFAs.

   theorem no_polynomial_determinization :
       ¬ ∃ p : Polynomial ℝ, ∀ n k : ℕ, ∀ A : TwoNFA (Fin k) (Fin n),
         ∃ s : ℕ, ∃ D : TwoNFA (Fin k) (Fin s),
           D.Deterministic ∧ D.language = A.language ∧
             (s : ℝ) ≤ p.eval (n : ℝ) := by
   …

   Mentions: OAI.TwoWayComplementation.TwoNFA