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 : σ} → M.edge v w → 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))