structure labeled_digraph' (α σ : Type) : Type

A slightly different signature from labeled_digraph in Exercise2_4

• edge : σ → σ → α → Prop

structure labeledDigraph (α σ : 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} (M : labeledDigraph α σ) : σ → σ → List α → Type

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

inductive walk_labeled {α σ : 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 α} (h : M.edge u v a) (p : walk_labeled M v w x) : walk_labeled M u w (a :: x)

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

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

noncomputable def walk_of_walk_labeled {α σ : 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 : List.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 : List.Vector (Fin 2) 4

Equations

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

def kayleighwalk2 (x0 x1 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 x1 x2 : Fin 2) : no_duplicate_edges' (kayleigh2_digraph ⟨[x0, x1, x2], ⋯⟩)

theorem a_nice_case_of_hyde_theorem (x0 x1 x2 : Fin 2) : have 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'