structure labeled_digraph (α : Type) (σ : 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} {σ : 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 α} → M.edge (u, v, a) → walk_labeled_digraph M v w x → walk_labeled_digraph M u w (a :: x)

inductive unlabeled_walk_labeled_digraph {α : Type} {σ : 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 : σ} → (∃ (a : α), M.edge (u, v, a)) → unlabeled_walk_labeled_digraph M v w → unlabeled_walk_labeled_digraph M u w

noncomputable def walk_of_walk_labeled_digraph {α : Type} {σ : 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 : ℕ} : let 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 : ℕ} : let 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 : ℕ} : Finset.filter (fun (x : Fin 1 × Fin 1 × Fin b.succ) => x.2.2 = 0) Finset.univ = {(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