OAI/Combinatorics/Automata/Recognition.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.OneWayLiveness.scanned_list line 9

   Source documentation

   The scanned cells are the two fixed markers surrounding the ordinary word.

   lemma scanned_list {Alpha : Type} (w : List Alpha) :
       List.ofFn (scanned w) = Symbol.left :: (w.map Symbol.letter ++ [Symbol.right]) := by
   …

   Mentions: OAI.OneWayLiveness.scanned

2. lemma OAI.OneWayLiveness.CellNetwork.fullDiagram_markers line 29
3. def OAI.OneWayLiveness.CellNetwork.recognitionTest line 40
4. lemma OAI.OneWayLiveness.CellNetwork.recognitionTest_iff line 44
5. lemma OAI.OneWayLiveness.Machine.liveness_rank_bound line 57
6. theorem OAI.OneWayLiveness.deterministic_lower_bound line 80

   Source documentation

   The representation uses four ports per ordered state pair. One sink state suffices under reflexive acceptance; a fresh initial row handles positive runs.

   theorem deterministic_lower_bound (h : ℕ) (hh : 2 ≤ h) (positive : Bool) (s : ℕ)
       (D : DMachine (Alphabet h) s) (hD : D.Recognizes positive (OWL h)) :
       2 ^ ((h - 2) / 31) ≤ 4 * (s + if positive then 2 else 1)^2 := by
   …

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