structure labeled_digraph (α σ : Type) : Type

• edge : σ × σ × α → Prop

def no_duplicate_edges {q b : ℕ} (M : labeled_digraph (Fin b) (Fin q)) : Prop

Equations

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

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

• nil {α σ : Type} {M : labeled_digraph α σ} {u : σ} : walk_labeled_digraph M u u []
• cons {α σ : Type} {M : labeled_digraph α σ} {u v w : σ} {a : α} {x : List α} (h : M.edge (u, v, a)) (p : walk_labeled_digraph M v w x) : walk_labeled_digraph M u w (a :: x)

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

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

noncomputable def walk_of_walk_labeled_digraph {α σ : Type} {M : labeled_digraph α σ} {u w : σ} {x : List α} (wa : walk_labeled_digraph M u w x) : unlabeled_walk_labeled_digraph M u w

Equations

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

def E_N_bounded_by {b : ℕ} (x : List (Fin b)) (e : ℕ) : Prop

Equations

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

theorem E_N_List_nil {b : ℕ} : E_N_bounded_by [] 0

def thewalk1 {b : ℕ} : have M := { edge := fun (x : Fin 1 × Fin 1 × Fin b.succ) => x.2.2 = 0 }; walk_labeled_digraph M 0 0 [0]

Equations

• thewalk1 = walk_labeled_digraph.cons ⋯ walk_labeled_digraph.nil

def thewalk2 {b : ℕ} : have M := { edge := fun (x : Fin 1 × Fin 1 × Fin b.succ) => x.2.2 = 0 }; walk_labeled_digraph M 0 0 [0, 0]

Equations

• thewalk2 = walk_labeled_digraph.cons ⋯ (walk_labeled_digraph.cons ⋯ walk_labeled_digraph.nil)

theorem prod_eq_zero {b : ℕ} : {x : Fin 1 × Fin 1 × Fin b.succ | x.2.2 = 0} = {(0, 0, 0)}

theorem E_N_one {b : ℕ} : E_N_bounded_by [0] 1

theorem E_N_two {b : ℕ} : E_N_bounded_by [0, 0] 1