OAI/Combinatorics/Automata/Tours.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.OneWayLiveness.permutation_single_entrance line 9

   Source documentation

   A finite permutation cannot leave a set without later re-entering it. When there is only one entrance, its entrance dart lies on the same tour.

   lemma permutation_single_entrance {D : Type*} [Finite D] (τ : Equiv.Perm D)
       (U : Set D) (a b : D) (ha : a ∈ U) (ha' : τ a ∉ U)
       (hin : ∀ d, d ∉ U → τ d ∈ U → d = b) : τ.SameCycle a b := by
   …

2. structure OAI.OneWayLiveness.CyclicOrder line 26

   Source documentation

   A cyclic order on every nonempty fiber of a finite incidence map.

   structure CyclicOrder {D V : Type*} (vertex : D → V) where
   …

3. def OAI.OneWayLiveness.CyclicOrder.choose line 31
4. lemma OAI.OneWayLiveness.sameCycle_permCongr line 64
5. structure OAI.OneWayLiveness.FunctionalEdges line 74

   Source documentation

   Oriented edges of a finite functional graph. Loops and distinct parallel edges are permitted a priori; the source map nevertheless is injective.

   structure FunctionalEdges (V E : Type*) where
   …

6. def OAI.OneWayLiveness.FunctionalEdges.Step line 81
7. abbrev OAI.OneWayLiveness.FunctionalEdges.Reach line 82
8. lemma OAI.OneWayLiveness.FunctionalEdges.deterministic line 83
9. lemma OAI.OneWayLiveness.FunctionalEdges.reach_of_terminal line 89
10. lemma OAI.OneWayLiveness.FunctionalEdges.successor_reaches line 94
11. lemma OAI.OneWayLiveness.FunctionalEdges.edge_cut line 101
12. lemma OAI.OneWayLiveness.FunctionalEdges.edge_not_return line 111
13. abbrev OAI.OneWayLiveness.FunctionalEdges.Dart line 127
14. def OAI.OneWayLiveness.FunctionalEdges.flip line 129
15. def OAI.OneWayLiveness.FunctionalEdges.vertex line 135
16. lemma OAI.OneWayLiveness.FunctionalEdges.vertex_false line 137
17. lemma OAI.OneWayLiveness.FunctionalEdges.vertex_true line 138
18. lemma OAI.OneWayLiveness.FunctionalEdges.flip_apply line 139
19. abbrev OAI.OneWayLiveness.FunctionalEdges.Rotation line 142

    Source documentation

    Every incoming-to-outgoing cyclic order at a vertex is permitted.

    abbrev Rotation := CyclicOrder G.vertex
    …

    Mentions: OAI.OneWayLiveness.CyclicOrder

20. def OAI.OneWayLiveness.FunctionalEdges.Rotation.tour line 146
21. lemma OAI.OneWayLiveness.FunctionalEdges.Rotation.tour_vertex line 148
22. lemma OAI.OneWayLiveness.FunctionalEdges.Rotation.edge_sameCycle line 150
23. lemma OAI.OneWayLiveness.FunctionalEdges.Rotation.tour_flip line 170
24. lemma OAI.OneWayLiveness.FunctionalEdges.Rotation.flip_sameCycle line 174
25. lemma OAI.OneWayLiveness.FunctionalEdges.Rotation.perm_sameCycle line 181
26. lemma OAI.OneWayLiveness.FunctionalEdges.Rotation.vertex_pow line 185
27. lemma OAI.OneWayLiveness.FunctionalEdges.Rotation.vertex_sameCycle line 190
28. lemma OAI.OneWayLiveness.FunctionalEdges.Rotation.reach_sameCycle line 201
29. lemma OAI.OneWayLiveness.FunctionalEdges.Rotation.basin_sameCycle line 220

    Source documentation

    All incidences in the basin of a terminal vertex lie on its one tour.

    lemma basin_sameCycle [Finite E] {t : V} (ht : ∀ e, G.src e ≠ t) (d d' r : E × Bool)
        (hd : G.Reach (G.vertex d) t) (hd' : G.Reach (G.vertex d') t)
        (hr : G.vertex r = t) : R.tour.SameCycle d d' := by
    …

30. lemma OAI.OneWayLiveness.FunctionalEdges.Rotation.color_eq_of_sameCycle line 226