OAI/Combinatorics/Automata/Diagrams.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.OneWayLiveness.Pairing.prod_compatible_chain line 10
2. lemma OAI.OneWayLiveness.Pairing.ofFn_compatible_chain line 40
3. structure OAI.OneWayLiveness.CellNetwork.ColorData line 54
4. def OAI.OneWayLiveness.CellNetwork.bodyDiagram line 62
5. def OAI.OneWayLiveness.CellNetwork.fullDiagram line 65
6. lemma OAI.OneWayLiveness.CellNetwork.fullDiagram_compatible line 68
7. def OAI.OneWayLiveness.CellNetwork.Flat line 83
8. def OAI.OneWayLiveness.CellNetwork.Separated line 85
9. def OAI.OneWayLiveness.CellNetwork.ColorData.wholeTip line 92

   Source documentation

   Restoring a reflection at every outer leaf extends the tip assignment.

   def wholeTip : WholeInc Q w.length → Bool → Bool
     | .inl (i,j),t => C.tip i (j,t)
     | .inr (s,slot),t => C.boundary (if s then w.length+2 else 0) (slot,tipRole s (!t))

   Mentions: OAI.OneWayLiveness.CellNetwork.WholeInc, OAI.OneWayLiveness.CellNetwork.tipRole

10. lemma OAI.OneWayLiveness.CellNetwork.ColorData.wholeTip_join line 96
11. lemma OAI.OneWayLiveness.CellNetwork.ColorData.wholeTip_lane line 105
12. lemma OAI.OneWayLiveness.CellNetwork.ColorData.tour_invariant line 129
13. lemma OAI.OneWayLiveness.CellNetwork.reach_excludes_separation line 139
14. lemma OAI.OneWayLiveness.CellNetwork.vertex_color_flip line 168

    Source documentation

    A vertex coloring which is constant along all edges also respects all local joins, regardless of cycles in other components.

    lemma vertex_color_flip (finish : Q) (w : List Alpha) (c : Vertex Q w.length → Bool)
        (hc : ∀ e, c ((graph M finish w).src e) = c ((graph M finish w).dst e))
        (d : Edge Q w.length × Bool) :
        c (wholeVertex M finish w (edgeInc Q w.length d)) =
          c (wholeVertex M finish w (edgeInc Q w.length ((graph M finish w).flip d))) := by
    …

    Mentions: OAI.OneWayLiveness.CellNetwork.Vertex, OAI.OneWayLiveness.CellNetwork.graph, OAI.OneWayLiveness.CellNetwork.Edge, OAI.OneWayLiveness.CellNetwork.wholeVertex, OAI.OneWayLiveness.CellNetwork.edgeInc

15. lemma OAI.OneWayLiveness.CellNetwork.vertex_color_adjacent line 180
16. def OAI.OneWayLiveness.CellNetwork.boundaryColor line 191
17. lemma OAI.OneWayLiveness.CellNetwork.boundaryColor_right line 198
18. lemma OAI.OneWayLiveness.CellNetwork.boundaryColor_left line 205
19. def OAI.OneWayLiveness.CellNetwork.vertexColorData line 221
20. lemma OAI.OneWayLiveness.CellNetwork.boundaryColor_test line 233
21. lemma OAI.OneWayLiveness.CellNetwork.separation_of_not_reach line 244
22. lemma OAI.OneWayLiveness.CellNetwork.diagram_recognizes_reach line 277

    Source documentation

    The Boolean test recovers exactly acceptance, not a halting assumption. Only the normalized distinguished right state is required to be terminal.

    lemma diagram_recognizes_reach (finish : Q) (ht : M.transition finish .right = none)
        (w : List Alpha) :
        (¬ ∃ l r, (fullDiagram M finish w).Compatible (Sum.elim l r) ∧ Separated M finish l r) ↔
          Relation.ReflTransGen (M.Step w) (outCell w.length false,M.initial)
            (outCell w.length true,finish) := by
    …

    Mentions: OAI.OneWayLiveness.CellNetwork.fullDiagram, OAI.OneWayLiveness.CellNetwork.Separated, OAI.OneWayLiveness.CellNetwork.outCell