Network.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

def OAI.TwoWayComplementation.cellDiagram line 10
Source documentation
Single-cell diagram from stay, rightward, and leftward augmented transitions.
```
def cellDiagram (m : ℕ) (stay right left : SetRel (Fin m) (Fin m)) : Diagram m :=
…
```
Mentions: OAI.TwoWayComplementation.Diagram
def OAI.TwoWayComplementation.wordDiagram line 14
Source documentation
Multiply the single-letter diagrams in input order, using identity for the empty word.
```
def wordDiagram {Sigma : Type*} {m : ℕ} (d : Sigma → Diagram m) (w : List Sigma) : Diagram m :=
…
```
Mentions: OAI.TwoWayComplementation.Diagram
theorem OAI.TwoWayComplementation.wordDiagram_nil line 18
theorem OAI.TwoWayComplementation.wordDiagram_append line 21

theorem OAI.TwoWayComplementation.blockRelation_star_swap line 28

Source documentation

Swap the two vertex blocks without changing the finite-path semantics.

theorem blockRelation_star_swap {α β : Type*} (E : SetRel α α) (F : SetRel α β)
    (G : SetRel β α) (H : SetRel β β) (x y : α ⊕ β) :
    (x.swap, y.swap) ∈ relStar (blockRelation H G F E) ↔
      (x, y) ∈ relStar (blockRelation E F G H) := by
…

Mentions: OAI.TwoWayComplementation.relStar, OAI.TwoWayComplementation.blockRelation

theorem OAI.TwoWayComplementation.blockRelation_star_left line 44

Source documentation

The left-left version of block elimination.

theorem blockRelation_star_left {α β : Type*} (E : SetRel α α) (F : SetRel α β)
    (G : SetRel β α) (H : SetRel β β) (x y : α) :
    (Sum.inl x, Sum.inl y) ∈ relStar (blockRelation E F G H) ↔
      (x, y) ∈ relStar (E ∪ (F ○ relStar H ○ G)) := by
…

Mentions: OAI.TwoWayComplementation.relStar, OAI.TwoWayComplementation.blockRelation

theorem OAI.TwoWayComplementation.blockRelation_star_back line 52

Source documentation

The right-left version of block elimination.

theorem blockRelation_star_back {α β : Type*} (E : SetRel α α) (F : SetRel α β)
    (G : SetRel β α) (H : SetRel β β) (x : β) (y : α) :
    (Sum.inr x, Sum.inl y) ∈ relStar (blockRelation E F G H) ↔
      (x, y) ∈ relStar H ○ G ○ relStar (E ∪ (F ○ relStar H ○ G)) := by
…

Mentions: OAI.TwoWayComplementation.relStar, OAI.TwoWayComplementation.blockRelation

theorem OAI.TwoWayComplementation.relStar_entry_feedback line 60

Source documentation

Eliminate an internal graph while retaining arbitrary repeated feedback at its entry.

theorem relStar_entry_feedback {Q V : Type*} (I : SetRel Q V) (E : SetRel V V)
    (O R : SetRel V Q) (X : SetRel Q Q) :
    I ○ relStar (E ∪ (R ○ X ○ I)) ○ O =
      relStar (I ○ relStar E ○ R ○ X) ○ (I ○ relStar E ○ O) := by
…

Mentions: OAI.TwoWayComplementation.relStar

theorem OAI.TwoWayComplementation.relStar_general_feedback line 68

Source documentation

Internal paths either avoid the feedback edge or use it after a first internal segment.

theorem relStar_general_feedback {Q V : Type*} (I J : SetRel Q V) (E : SetRel V V)
    (O R : SetRel V Q) (X : SetRel Q Q) :
    I ○ relStar (E ∪ (R ○ X ○ J)) ○ O =
      (I ○ relStar E ○ O) ∪
        (I ○ relStar E ○ R ○ relStar (X ○ J ○ relStar E ○ R) ○ X ○ J ○ relStar E ○ O) := by
…

Mentions: OAI.TwoWayComplementation.relStar

structure OAI.TwoWayComplementation.Network line 79
Source documentation
A finite-path network with labelled entrances and exits at both boundaries.
```
structure Network (m : ℕ) (V : Type*) where
…
```
def OAI.TwoWayComplementation.Network.summary line 94
Source documentation
Summarize all finite internal paths between the four boundary pairs.
```
def summary {m : ℕ} {V : Type*} (N : Network m V) : Diagram m where
…
```
Mentions: OAI.TwoWayComplementation.Network, OAI.TwoWayComplementation.Diagram
def OAI.TwoWayComplementation.Network.join line 101
Source documentation
Join two networks, wiring the adjacent exits to entrances in both directions.
```
def join {m : ℕ} {V W : Type*} (N : Network m V) (M : Network m W) : Network m (V ⊕ W) where
…
```
Mentions: OAI.TwoWayComplementation.Network
theorem OAI.TwoWayComplementation.Network.summary_join line 109
Source documentation
Joining path networks implements exactly the four diagram multiplication formulas.
```
theorem summary_join {m : ℕ} {V W : Type*} (N : Network m V) (M : Network m W) :
    (N.join M).summary = Diagram.comp N.summary M.summary := by
…
```
Mentions: OAI.TwoWayComplementation.Network, OAI.TwoWayComplementation.Network.summary, OAI.TwoWayComplementation.Diagram.comp