OAI/Combinatorics/Automata/Main.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.OneWayLiveness.main_theorem line 10

   Source documentation

   The one-way nondeterministic upper bound and two-way deterministic lower bound, under both acceptance conventions.

   standard axioms: Classical.choice, Quot.sound, propext what this means

   Statement uses: Nat, LE.le, OfNat.ofNat, And, Exists, OAI.OneWayLiveness.NMachine, OAI.OneWayLiveness.Alphabet, HAdd.hAdd, OAI.OneWayLiveness.NMachine.NoLeft, Bool, OAI.OneWayLiveness.NMachine.Recognizes, OAI.OneWayLiveness.OWL, OAI.OneWayLiveness.DMachine, OAI.OneWayLiveness.DMachine.Recognizes, HPow.hPow, HDiv.hDiv, HSub.hSub, HMul.hMul, ite, Eq and 1 more

   Proof uses: And.intro, OAI.OneWayLiveness.small_nfa, OAI.OneWayLiveness.deterministic_lower_bound

   30 instances, coercions and auxiliary constants left out.

   Distinct definitions of this name: ComparatorChallenges/OneWayLiveness.lean:95 (same statement text; different proof or body). Qualify references as OAI.OneWayLiveness.main_theorem@path.

   theorem main_theorem (h : ℕ) (hh : 2 ≤ h) :
       (∃ N : NMachine (Alphabet h) (h + 3), N.NoLeft ∧
         ∀ positive : Bool, N.Recognizes positive (OWL h)) ∧
       (∀ (positive : Bool) (s : ℕ) (D : DMachine (Alphabet h) s),
         D.Recognizes positive (OWL h) →
         2 ^ ((h - 2) / 31) ≤ 4 * (s + if positive then 2 else 1) ^ 2) :=
   …

   Mentions: OAI.OneWayLiveness.NMachine, OAI.OneWayLiveness.Alphabet, OAI.OneWayLiveness.OWL, OAI.OneWayLiveness.DMachine

2. theorem OAI.OneWayLiveness.no_polynomial_simulation line 21

   Source documentation

   No alphabet-independent polynomial deterministic simulation exists, under either acceptance convention.

   theorem no_polynomial_simulation (positive : Bool) : ¬ PolynomialSimulation positive := by
   …

   Mentions: OAI.OneWayLiveness.PolynomialSimulation