OAI/Combinatorics/Automata/Normalization.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.OneWayLiveness.Machine line 8

   Source documentation

   A deterministic automaton on an arbitrary state type.

   structure Machine (Alpha Q : Type) where
   …

2. abbrev OAI.OneWayLiveness.Machine.Config line 18
3. def OAI.OneWayLiveness.Machine.Step line 20
4. def OAI.OneWayLiveness.Machine.Accepts line 23
5. def OAI.OneWayLiveness.DMachine.toMachine line 28
6. lemma OAI.OneWayLiveness.DMachine.toMachine_accepts line 31
7. def OAI.OneWayLiveness.Machine.positiveCopy line 38

   Source documentation

   A fresh nonaccepting initial state copies the original initial row.

   def positiveCopy : Machine Alpha (Option Q) where
   …

   Mentions: OAI.OneWayLiveness.Machine

8. lemma OAI.OneWayLiveness.Machine.positiveCopy_step line 57
9. lemma OAI.OneWayLiveness.Machine.positiveCopy_reach line 72
10. lemma OAI.OneWayLiveness.Machine.positiveCopy_accepts line 95
11. def OAI.OneWayLiveness.Machine.sinkCopy line 118

    Source documentation

    Sink normalization also replaces missing transitions at accepting states.

    noncomputable def sinkCopy : Machine Alpha (Option Q) := by
    …

    Mentions: OAI.OneWayLiveness.Machine

12. lemma OAI.OneWayLiveness.Machine.sinkCopy_step_old line 152
13. lemma OAI.OneWayLiveness.scanned_eq_left_iff line 178
14. lemma OAI.OneWayLiveness.scanned_eq_right_iff line 183
15. def OAI.OneWayLiveness.Machine.terminal line 191
16. lemma OAI.OneWayLiveness.Machine.sinkCopy_sweep line 193
17. lemma OAI.OneWayLiveness.Machine.sinkCopy_reach_iff line 207
18. lemma OAI.OneWayLiveness.Machine.sinkCopy_accepts line 238
19. lemma OAI.OneWayLiveness.Machine.sinkCopy_terminal line 242