OAI/Combinatorics/Automata/Model.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.OneWayLiveness.BRel line 7

    Also declared: ComparatorChallenges/OneWayLiveness.lean:7 (same declaration text).

  2. instance OAI.OneWayLiveness.BRel.(instance at line 11) line 11
  3. instance OAI.OneWayLiveness.BRel.(instance at line 12) line 12
  4. instance OAI.OneWayLiveness.BRel.(instance at line 13) line 13
  5. theorem OAI.OneWayLiveness.BRel.one_holds line 14
  6. theorem OAI.OneWayLiveness.BRel.mul_holds line 15
  7. theorem OAI.OneWayLiveness.BRel.zero_holds line 17
  8. instance OAI.OneWayLiveness.BRel.(instance at line 18) line 18
  9. def OAI.OneWayLiveness.BRel.restrictedId line 27
  10. def OAI.OneWayLiveness.BRel.live line 28

    Also declared: ComparatorChallenges/OneWayLiveness.lean:24 (same declaration text).

  11. instance OAI.OneWayLiveness.BRel.(instance at line 29) line 29
  12. abbrev OAI.OneWayLiveness.Alphabet line 33

    Also declared: ComparatorChallenges/OneWayLiveness.lean:27 (same declaration text).

  13. def OAI.OneWayLiveness.OWL line 34

    Also declared: ComparatorChallenges/OneWayLiveness.lean:28 (same declaration text).

  14. inductive OAI.OneWayLiveness.Symbol line 36

    Also declared: ComparatorChallenges/OneWayLiveness.lean:30 (same declaration text).

  15. inductive OAI.OneWayLiveness.Move line 41

    Also declared: ComparatorChallenges/OneWayLiveness.lean:35 (same declaration text).

  16. def OAI.OneWayLiveness.Move.Rel line 45

    Also declared: ComparatorChallenges/OneWayLiveness.lean:39 (same declaration text).

  17. def OAI.OneWayLiveness.scanned line 51

    Source documentation

    The finite word including both endmarkers.

    Also declared: ComparatorChallenges/OneWayLiveness.lean:45 (same declaration text).

    def scanned {Alpha : Type*} (w : List Alpha) (i : Fin (w.length + 2)) : Symbol Alpha :=
…

    Mentions: OAI.OneWayLiveness.Symbol

  18. abbrev OAI.OneWayLiveness.Configuration line 56

    Also declared: ComparatorChallenges/OneWayLiveness.lean:50 (same declaration text).

  19. structure OAI.OneWayLiveness.DMachine line 58

    Also declared: ComparatorChallenges/OneWayLiveness.lean:52 (same declaration text).

  20. structure OAI.OneWayLiveness.NMachine line 65

    Also declared: ComparatorChallenges/OneWayLiveness.lean:59 (same declaration text).

  21. def OAI.OneWayLiveness.DMachine.Step line 72

    Also declared: ComparatorChallenges/OneWayLiveness.lean:66 (same declaration text).

  22. def OAI.OneWayLiveness.NMachine.Step line 76

    Also declared: ComparatorChallenges/OneWayLiveness.lean:70 (same declaration text).

  23. def OAI.OneWayLiveness.FiniteRun line 81

    Source documentation

    The positive convention explicitly excludes a length-zero computation.

    Also declared: ComparatorChallenges/OneWayLiveness.lean:75 (same declaration text).

    def FiniteRun {C : Type*} (positive : Bool) (step : C → C → Prop) (c c' : C) : Prop :=
…
  24. def OAI.OneWayLiveness.DMachine.Accepts line 84

    Also declared: ComparatorChallenges/OneWayLiveness.lean:78 (same declaration text).

  25. def OAI.OneWayLiveness.NMachine.Accepts line 88

    Also declared: ComparatorChallenges/OneWayLiveness.lean:82 (same declaration text).

  26. def OAI.OneWayLiveness.NMachine.NoLeft line 92

    Also declared: ComparatorChallenges/OneWayLiveness.lean:86 (same declaration text).

  27. def OAI.OneWayLiveness.NMachine.Recognizes line 95

    Also declared: ComparatorChallenges/OneWayLiveness.lean:89 (same declaration text).

  28. def OAI.OneWayLiveness.DMachine.Recognizes line 98

    Also declared: ComparatorChallenges/OneWayLiveness.lean:92 (same declaration text).

  29. def OAI.OneWayLiveness.PolynomialSimulation line 102

    Source documentation

    An alphabet-independent polynomial bound for deterministic simulation.

    def PolynomialSimulation (positive : Bool) : Prop :=
…