structure labeled_digraph' (α : Type) (σ : Type) : Type

A slightly different signature from labeled_digraph in Exercise2_4

• edge : σ → σ → α → Prop

structure labeledDigraph (α : Type) (σ : Type) : Type

An edge-labeled digraph on σ consists of a digraph on σ for each label. M.Lab a).Adj u v means that in M, there is an adjacency from u to v labeled a.

• Lab : α → Digraph σ

inductive walkLabeled {α : Type} {σ : Type} (M : labeledDigraph α σ) : σ → σ → List α → Type

• nil: {α σ : Type} → {M : labeledDigraph α σ} → {u : σ} → walkLabeled M u u []
• cons: {α σ : Type} → {M : labeledDigraph α σ} → {u v w : σ} → {a : α} → {x : List α} → (M.Lab a).Adj u v → walkLabeled M v w x → walkLabeled M u w (a :: x)

inductive walk_labeled {α : Type} {σ : Type} (M : labeled_digraph' α σ) : σ → σ → List α → Type

• nil: {α σ : Type} → {M : labeled_digraph' α σ} → {u : σ} → walk_labeled M u u []
• cons: {α σ : Type} → {M : labeled_digraph' α σ} → {u v w : σ} → {a : α} → {x : List α} → M.edge u v a → walk_labeled M v w x → walk_labeled M u w (a :: x)

inductive walk {α : Type} {σ : Type} (M : labeled_digraph' α σ) : σ → σ → Type

• nil: {α σ : Type} → {M : labeled_digraph' α σ} → {u : σ} → walk M u u
• cons: {α σ : Type} → {M : labeled_digraph' α σ} → {u v w : σ} → (∃ (a : α), M.edge u v a) → walk M v w → walk M u w

noncomputable def walk_of_walk_labeled {α : Type} {σ : Type} {M : labeled_digraph' α σ} {u : σ} {w : σ} {x : List α} (wa : walk_labeled M u w x) : walk M u w

Equations

• One or more equations did not get rendered due to their size.

def kayleigh2_digraph (x : Mathlib.Vector (Fin 2) 3) : labeled_digraph' (Fin 2) (Fin 2)

Equations

• kayleigh2_digraph x = { edge := fun (q1 q2 b : Fin 2) => (q1, q2, b) = (0, 1, x.get 0) ∨ (q1, q2, b) = (1, 1, x.get 1) ∨ (q1, q2, b) = (1, 0, x.get 2) }

def kayleighsequence2 : Mathlib.Vector (Fin 2) 4

Equations

• kayleighsequence2 = ⟨[0, 1, 1, 0], kayleighsequence2.proof_2⟩

def kayleighwalk2 (x0 : Fin 2) (x1 : Fin 2) (x2 : Fin 2) : walk_labeled (kayleigh2_digraph ⟨[x0, x1, x2], ⋯⟩) (kayleighsequence2.get 0) (kayleighsequence2.get 3) [x0, x1, x2]

Equations

• kayleighwalk2 x0 x1 x2 = walk_labeled.cons ⋯ (walk_labeled.cons ⋯ (walk_labeled.cons ⋯ walk_labeled.nil))

def no_duplicate_edges' (M : labeled_digraph' (Fin 2) (Fin 2)) : Prop

Equations

• no_duplicate_edges' M = ∀ (q1 q2 a b : Fin 2), M.edge q1 q2 a → M.edge q1 q2 b → a = b

theorem kayleigh2_no_duplicates (x0 : Fin 2) (x1 : Fin 2) (x2 : Fin 2) : no_duplicate_edges' (kayleigh2_digraph ⟨[x0, x1, x2], ⋯⟩)

theorem a_nice_case_of_hyde_theorem (x0 : Fin 2) (x1 : Fin 2) (x2 : Fin 2) : let M := kayleigh2_digraph ⟨[x0, x1, x2], ⋯⟩; ∃ (w : walk_labeled M 0 0 [x0, x1, x2]), ∀ (y0 y1 y2 : Fin 2) (w' : walk_labeled M 0 0 [y0, y1, y2]), walk_of_walk_labeled w = walk_of_walk_labeled w'