structure digraph (σ : Type) : Type

• edge : σ → σ → Prop

inductive walk_digraph {σ : Type} (M : digraph σ) : σ → σ → Type

• nil {σ : Type} {M : digraph σ} {u : σ} : walk_digraph M u u
• cons {σ : Type} {M : digraph σ} {u v w : σ} (h : M.edge v w) (p : walk_digraph M u v) : walk_digraph M u w

def digraph_of_seq4 {σ : Type} (s0 s1 s2 s3 : σ) : digraph σ

Equations

• digraph_of_seq4 s0 s1 s2 s3 = { edge := fun (q0 q1 : σ) => (q0, q1) = (s0, s1) ∨ (q0, q1) = (s1, s2) ∨ (q0, q1) = (s2, s3) }

def walk_of_digraph_of_seq4 {σ : Type} (s0 s1 s2 s3 : σ) : walk_digraph (digraph_of_seq4 s0 s1 s2 s3) s0 s3

Equations

• walk_of_digraph_of_seq4 s0 s1 s2 s3 = walk_digraph.cons ⋯ (walk_digraph.cons ⋯ (walk_digraph.cons ⋯ walk_digraph.nil))