OAI/Combinatorics/Automata/Network.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.OneWayLiveness.CellNetwork.Edge line 13

    Source documentation

    Edges of all crossing and stay candidates, together with all outward slots. Every outward slot is an edge to its own external leaf.

    abbrev Edge (n : ℕ) := (Fin (n + 1) × Slot Q) ⊕
…

    Mentions: OAI.OneWayLiveness.CellNetwork.Slot

  2. abbrev OAI.OneWayLiveness.CellNetwork.WholeInc line 15
  3. def OAI.OneWayLiveness.CellNetwork.outCell line 17
  4. def OAI.OneWayLiveness.CellNetwork.edgeInc line 21

    Source documentation

    Locate an oriented incidence in its cell, or at its external leaf.

    def edgeInc (n : ℕ) : Edge Q n × Bool → WholeInc Q n
  | (.inl (j,slot),b) =>
      if slot.1 ^^ b then .inl (j.castSucc, .inl (true,slot))
      else .inl (j.succ, .inl (false,slot))
  | (.inr (.inl (i,pq)),b) => .inl (i,.inr (pq,b))
  | (.inr (.inr (s,slot)),b) =>
      if b then .inl (outCell n s,.inl (s,slot)) else .inr (s,slot)

    Mentions: OAI.OneWayLiveness.CellNetwork.Edge, OAI.OneWayLiveness.CellNetwork.WholeInc, OAI.OneWayLiveness.CellNetwork.outCell

  5. def OAI.OneWayLiveness.CellNetwork.incEdge line 29
  6. lemma OAI.OneWayLiveness.CellNetwork.incEdge_edgeInc line 39
  7. lemma OAI.OneWayLiveness.CellNetwork.edgeInc_incEdge line 46
  8. def OAI.OneWayLiveness.CellNetwork.incidenceEquiv line 68
  9. abbrev OAI.OneWayLiveness.CellNetwork.Key line 76

    Source documentation

    A complete proposed successor, including its source and target state.

    abbrev Key := Move × Q × Q

    Mentions: OAI.OneWayLiveness.Move

  10. def OAI.OneWayLiveness.CellNetwork.sourceInc line 78
  11. lemma OAI.OneWayLiveness.CellNetwork.sourceInc_injective line 83
  12. def OAI.OneWayLiveness.CellNetwork.sourceAttach line 89
  13. lemma OAI.OneWayLiveness.CellNetwork.sourceAttach_injective line 93
  14. lemma OAI.OneWayLiveness.CellNetwork.sourceAttach_eq_state line 108
  15. def OAI.OneWayLiveness.CellNetwork.outward line 122

    Source documentation

    Only the side facing away from the input is outward.

    def outward : Symbol Alpha → Bool → Bool
  | .left, s => !s
  | .right, s => s
  | .letter _, _ => false

    Mentions: OAI.OneWayLiveness.Symbol

  16. def OAI.OneWayLiveness.CellNetwork.testSlot line 127
  17. def OAI.OneWayLiveness.CellNetwork.localVertex line 129
  18. def OAI.OneWayLiveness.CellNetwork.edgeKey line 143

    Source documentation

    An edge is uniquely determined by the cell, move and states of its source proposal, or by its outward slot.

    def edgeKey (n : ℕ) : Edge Q n → (Fin (n + 2) × Key Q) ⊕ (Bool × Slot Q)
  | .inl (j,(true,p,q)) => .inl (j.castSucc,(.right,p,q))
  | .inl (j,(false,p,q)) => .inl (j.succ,(.left,p,q))
  | .inr (.inl (i,(p,q))) => .inl (i,(.stay,p,q))
  | .inr (.inr z) => .inr z

    Mentions: OAI.OneWayLiveness.CellNetwork.Edge, OAI.OneWayLiveness.CellNetwork.Key, OAI.OneWayLiveness.CellNetwork.Slot

  19. lemma OAI.OneWayLiveness.CellNetwork.edgeKey_injective line 149
  20. abbrev OAI.OneWayLiveness.CellNetwork.Vertex line 157
  21. def OAI.OneWayLiveness.CellNetwork.decorate line 160
  22. lemma OAI.OneWayLiveness.CellNetwork.decorate_injective line 165
  23. def OAI.OneWayLiveness.CellNetwork.destination line 177
  24. def OAI.OneWayLiveness.CellNetwork.graph line 184
  25. def OAI.OneWayLiveness.CellNetwork.wholeVertex line 189
  26. lemma OAI.OneWayLiveness.CellNetwork.outward_internal line 193
  27. lemma OAI.OneWayLiveness.CellNetwork.graph_vertex line 203
  28. def OAI.OneWayLiveness.CellNetwork.wholePerm line 216

    Source documentation

    The same local cyclic orders are used at every occurrence of a symbol.

    def wholePerm (w : List Alpha) (r : Symbol Alpha → Equiv.Perm (Incidence Q)) :
    Equiv.Perm (WholeInc Q w.length) where
…

    Mentions: OAI.OneWayLiveness.Symbol, OAI.OneWayLiveness.CellNetwork.Incidence, OAI.OneWayLiveness.CellNetwork.WholeInc

  29. lemma OAI.OneWayLiveness.CellNetwork.wholePerm_pow line 227
  30. def OAI.OneWayLiveness.CellNetwork.orders line 234
  31. def OAI.OneWayLiveness.CellNetwork.wholeOrder line 237
  32. def OAI.OneWayLiveness.CellNetwork.graphOrder line 260
  33. lemma OAI.OneWayLiveness.CellNetwork.graphOrder_apply line 277
  34. def OAI.OneWayLiveness.CellNetwork.stateVertex line 284

    Source documentation

    State configurations embed without identifying any added leaves.

    def stateVertex (w : List Alpha) (c : Machine.Config (Q := Q) w) : Vertex Q w.length :=
…

    Mentions: OAI.OneWayLiveness.Machine.Config, OAI.OneWayLiveness.CellNetwork.Vertex

  35. lemma OAI.OneWayLiveness.CellNetwork.stateVertex_injective line 287
  36. lemma OAI.OneWayLiveness.CellNetwork.graph_step_from_state line 291
  37. lemma OAI.OneWayLiveness.CellNetwork.graph_reach_state line 356
  38. lemma OAI.OneWayLiveness.CellNetwork.graph_terminal line 375
  39. lemma OAI.OneWayLiveness.CellNetwork.scanned_outCell line 382
  40. lemma OAI.OneWayLiveness.CellNetwork.test_destination line 388
  41. lemma OAI.OneWayLiveness.CellNetwork.test_step line 396