OAI/Combinatorics/Automata/PathNFA.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.OneWayLiveness.NMachineOn line 8

    Source documentation

    A nondeterministic automaton on an arbitrary state type.

    structure NMachineOn (Alpha Q : Type) where
…
  2. abbrev OAI.OneWayLiveness.NMachineOn.Config line 17
  3. def OAI.OneWayLiveness.NMachineOn.Step line 19
  4. def OAI.OneWayLiveness.NMachineOn.Accepts line 22
  5. def OAI.OneWayLiveness.NMachineOn.relabel line 25
  6. lemma OAI.OneWayLiveness.NMachineOn.relabel_accepts line 32
  7. lemma OAI.OneWayLiveness.NMachineOn.relabel_noLeft line 54
  8. abbrev OAI.OneWayLiveness.PathNFA.State line 62

    Source documentation

    none is the initial state. Boolean states are accept and reject.

    abbrev State (H : Type) := Option (H ⊕ Bool)
  9. abbrev OAI.OneWayLiveness.PathNFA.path line 63
  10. abbrev OAI.OneWayLiveness.PathNFA.accept line 64
  11. def OAI.OneWayLiveness.PathNFA.rules line 66
  12. lemma OAI.OneWayLiveness.PathNFA.rules_noLeft line 72
  13. def OAI.OneWayLiveness.PathNFA.machine line 80
  14. lemma OAI.OneWayLiveness.PathNFA.product_path line 91

    Source documentation

    A numbered path through a product, extended arbitrarily after its endpoint.

    lemma product_path (w : List (BRel H)) (a b : H) :
    w.prod.holds a b ↔ ∃ p : ℕ → H, p 0 = a ∧ p w.length = b ∧
      ∀ i (hi : i < w.length), w[i].holds (p i) (p (i+1)) := by
…

    Mentions: OAI.OneWayLiveness.BRel

  15. def OAI.OneWayLiveness.PathNFA.Good line 119

    Source documentation

    The accumulated product on every prefix reached by a path state.

    def Good (w : List (BRel H)) (c : NMachineOn.Config (Q := State H) w) : Prop :=
…

    Mentions: OAI.OneWayLiveness.BRel, OAI.OneWayLiveness.NMachineOn.Config, OAI.OneWayLiveness.PathNFA.State

  16. lemma OAI.OneWayLiveness.PathNFA.scanned_letter_data line 126
  17. lemma OAI.OneWayLiveness.PathNFA.scanned_letter_cell line 132
  18. lemma OAI.OneWayLiveness.PathNFA.good_step line 136
  19. lemma OAI.OneWayLiveness.PathNFA.accepts_iff line 192
  20. theorem OAI.OneWayLiveness.small_nfa line 243

    Source documentation

    The explicit path automaton has h+3 states, including the unused rejector. It accepts only after at least two transitions, so both conventions agree.

    theorem small_nfa (h : ℕ) :
    ∃ N : NMachine (Alphabet h) (h+3), N.NoLeft ∧
      ∀ positive : Bool, N.Recognizes positive (OWL h) := by
…

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