OAI/Combinatorics/Automata/Cells.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.OneWayLiveness.Pairing.transport_compatible line 9
  2. def OAI.OneWayLiveness.Pairing.close line 18

    Source documentation

    Close all internal tips with a matching of local joins.

    noncomputable def close (lanes : Pairing (P ⊕ I)) (joins : Pairing I) : Pairing P :=
…

    Mentions: OAI.OneWayLiveness.Pairing

  3. lemma OAI.OneWayLiveness.Pairing.close_compatible line 21
  4. lemma OAI.OneWayLiveness.Pairing.ofInvolution_compatible line 33
  5. abbrev OAI.OneWayLiveness.CellNetwork.Slot line 45

    Source documentation

    true directs the prospective successor to the right.

    abbrev Slot := Bool × Q × Q
  6. abbrev OAI.OneWayLiveness.CellNetwork.Port line 46
  7. abbrev OAI.OneWayLiveness.CellNetwork.Boundary line 47
  8. abbrev OAI.OneWayLiveness.CellNetwork.Incidence line 48
  9. abbrev OAI.OneWayLiveness.CellNetwork.Tip line 49
  10. abbrev OAI.OneWayLiveness.CellNetwork.LocalVertex line 50
  11. def OAI.OneWayLiveness.CellNetwork.tipRole line 54

    Source documentation

    A lane's absolute label changes its incoming/outgoing role between opposite sides of a cell.

    def tipRole (side lane : Bool) : Bool := side ^^ lane
  12. lemma OAI.OneWayLiveness.CellNetwork.tipRole_twice line 55
  13. lemma OAI.OneWayLiveness.CellNetwork.tipRole_ne line 56
  14. def OAI.OneWayLiveness.CellNetwork.laneMate line 60

    Source documentation

    All stay candidates are allowed locally; a nontransition candidate will be attached to a fresh leaf. This leaves the external degree unchanged.

    def laneMate : ((Boundary Q × Bool) ⊕ Tip Q) → ((Boundary Q × Bool) ⊕ Tip Q)
  | .inl (b,l) => .inr (.inl b, tipRole b.1 l)
  | .inr (.inl b,t) => .inl (b, tipRole b.1 t)
  | .inr (.inr (pq,r),t) => .inr (.inr (pq,!r),!t)

    Mentions: OAI.OneWayLiveness.CellNetwork.Boundary, OAI.OneWayLiveness.CellNetwork.Tip, OAI.OneWayLiveness.CellNetwork.tipRole

  15. lemma OAI.OneWayLiveness.CellNetwork.laneMate_involutive line 65
  16. lemma OAI.OneWayLiveness.CellNetwork.laneMate_ne line 67
  17. def OAI.OneWayLiveness.CellNetwork.lanes line 70
  18. def OAI.OneWayLiveness.CellNetwork.joinMate line 73
  19. lemma OAI.OneWayLiveness.CellNetwork.joinMate_involutive line 77
  20. lemma OAI.OneWayLiveness.CellNetwork.joinMate_ne line 79
  21. def OAI.OneWayLiveness.CellNetwork.joins line 82
  22. lemma OAI.OneWayLiveness.CellNetwork.lanes_compatible line 85
  23. lemma OAI.OneWayLiveness.CellNetwork.joins_compatible line 97
  24. def OAI.OneWayLiveness.CellNetwork.portsEquiv line 108

    Source documentation

    The two sides use exactly the same slot/lane labels.

    def portsEquiv : (Boundary Q × Bool) ≃ (Port Q ⊕ Port Q) where
…

    Mentions: OAI.OneWayLiveness.CellNetwork.Boundary, OAI.OneWayLiveness.CellNetwork.Port

  25. def OAI.OneWayLiveness.CellNetwork.diagram line 114
  26. lemma OAI.OneWayLiveness.CellNetwork.diagram_compatible line 117