def WList.internalVertexSet {α : Type u_1} {β : Type u_2} (w : WList α β) : Set α

The vertices of a wList other than its first and last vertices.

Equations

• w.internalVertexSet = {x : α | x ∈ w.vertex.tail.dropLast}

@[simp]

theorem WList.tail_last {α : Type u_1} {β : Type u_2} (w : WList α β) : w.tail.last = w.last

theorem WList.tail_edge {α : Type u_1} {β : Type u_2} (w : WList α β) : w.tail.edge = w.edge.tail

@[simp]

theorem WList.tail_length {α : Type u_1} {β : Type u_2} (w : WList α β) : w.tail.length = w.length - 1

theorem WList.Nonempty.length_eq_tail_vertex_length {α : Type u_1} {β : Type u_2} {w : WList α β} (hw : w.Nonempty) : w.length = w.tail.vertex.length

theorem WList.mem_tail_iff_of_nodup {α : Type u_1} {β : Type u_2} {x : α} {w : WList α β} (hw : w.vertex.Nodup) (hne : w.Nonempty) : x ∈ w.tail ↔ x ∈ w ∧ x ≠ w.first

theorem WList.first_notMem_tail_of_nodup {α : Type u_1} {β : Type u_2} {w : WList α β} (hw : w.vertex.Nodup) (hne : w.Nonempty) : w.first ∉ w.tail

theorem WList.tail_vertexSet_of_nodup {α : Type u_1} {β : Type u_2} {w : WList α β} (hw : w.vertex.Nodup) (hne : w.Nonempty) : w.tail.vertexSet = w.vertexSet \ {w.first}

theorem WList.Nonempty.cons_tail {α : Type u_1} {β : Type u_2} {w : WList α β} (hw : w.Nonempty) : WList.cons w.first (firstEdge w hw) w.tail = w

@[simp]

theorem WList.Nonempty.vertex_tail {α : Type u_1} {β : Type u_2} {w : WList α β} (hw : w.Nonempty) : w.tail.vertex = w.vertex.tail

@[simp]

theorem WList.tail_isSuffix {α : Type u_1} {β : Type u_2} (w : WList α β) : w.tail.IsSuffix w

@[simp]

theorem WList.eq_first_or_mem_tail {α : Type u_1} {β : Type u_2} {x : α} {w : WList α β} (h : x ∈ w) : x = w.first ∨ x ∈ w.tail

theorem WList.mem_iff_eq_first_or_mem_tail {α : Type u_1} {β : Type u_2} {x : α} {w : WList α β} : x ∈ w ↔ x = w.first ∨ x ∈ w.tail

theorem WList.mem_iff_eq_vertex_first_or_mem_tail {α : Type u_1} {β : Type u_2} {x : α} {w : WList α β} : x ∈ w ↔ x = w.first ∨ x ∈ w.vertex.tail

theorem WList.mem_iff_eq_first_or_mem_internalVertexSet_or_eq_last {α : Type u_1} {β : Type u_2} {x : α} {w : WList α β} : x ∈ w ↔ x = w.first ∨ x ∈ w.internalVertexSet ∨ x = w.last

A vertex of a wList is either its first vertex, an internal vertex, or its last vertex.

theorem WList.internalVertexSet_cons {α : Type u_1} {β : Type u_2} (x : α) (e : β) (w : WList α β) : (cons x e w).internalVertexSet = {z : α | z ∈ w.vertex.dropLast}

The internal vertices of cons x e w are the vertices of w other than its last one. This subsumes the nil/cons case split on the tail: w.vertex.dropLast is already empty when w is trivial.

theorem WList.mem_internalVertexSet_cons {α : Type u_1} {β : Type u_2} {z x : α} {e : β} {w : WList α β} : z ∈ (cons x e w).internalVertexSet ↔ z ∈ w.vertex.dropLast

theorem WList.internalVertexSet_cons_nil {α : Type u_1} {β : Type u_2} (x : α) (e : β) (y : α) : (cons x e (nil y)).internalVertexSet = ∅

theorem WList.internalVertexSet_cons_cons {α : Type u_1} {β : Type u_2} (x : α) (e : β) (y : α) (f : β) (w : WList α β) : (cons x e (cons y f w)).internalVertexSet = insert y (cons y f w).internalVertexSet

theorem WList.internalVertexSet_reverse {α : Type u_1} {β : Type u_2} (w : WList α β) : w.reverse.internalVertexSet = w.internalVertexSet

theorem WList.internalVertexSet_append_of_nonempty {α : Type u_1} {β : Type u_2} {w₁ w₂ : WList α β} (h₁ : w₁.Nonempty) (h₂ : w₂.Nonempty) : (w₁ ++ w₂).internalVertexSet = w₁.internalVertexSet ∪ insert w₂.first w₂.internalVertexSet

theorem WList.mem_of_mem_internalVertexSet {α : Type u_1} {β : Type u_2} {x : α} {w : WList α β} (hx : x ∈ w.internalVertexSet) : x ∈ w

An internal vertex is a vertex.

theorem WList.mem_internalVertexSet_of_mem_ne_ends {α : Type u_1} {β : Type u_2} {W : WList α β} {x : α} (hx : x ∈ W) (hne : x ≠ W.first ∧ x ≠ W.last) : x ∈ W.internalVertexSet

A vertex that is neither end is internal. No Nodup hypothesis is needed in this direction; see mem_internalVertexSet_iff_of_nodup for the converse.

theorem WList.exists_get_of_mem_internalVertexSet {α : Type u_1} {β : Type u_2} {x : α} {w : WList α β} (hx : x ∈ w.internalVertexSet) : ∃ (m : ℕ), 0 < m ∧ m < w.length ∧ w.get m = x

An internal vertex of w is w.get m for some 0 < m < w.length.

theorem WList.IsSublist.internalVertexSet_subset {α : Type u_1} {β : Type u_2} {w w₀ : WList α β} (h : w₀.IsSublist w) : w₀.internalVertexSet ⊆ w.vertexSet

The internal vertices of a sublist belong to the ambient wList.

theorem WList.IsSublist.internalVertexSet_subset_internalVertexSet {α : Type u_1} {β : Type u_2} {w w' : WList α β} (h : w'.IsSublist w) : w'.internalVertexSet ⊆ w.internalVertexSet

Internal vertices of a sublist are internal vertices of the original list.

theorem WList.IsSublist.le_tail_of_ne_first {α : Type u_1} {β : Type u_2} {w w₀ : WList α β} (h : w₀ ≤ w) (hne : w₀.first ≠ w.first) : w₀ ≤ w.tail

theorem WList.Nonempty.tail_concat {α : Type u_1} {β : Type u_2} {w : WList α β} (hw : w.Nonempty) (e : β) (x : α) : (w.concat e x).tail = w.tail.concat e x

theorem WList.tail_append {α : Type u_1} {β : Type u_2} {w₁ : WList α β} (hw₁ : w₁.Nonempty) (w₂ : WList α β) : (w₁ ++ w₂).tail = w₁.tail ++ w₂

theorem WList.Nonempty.tail_isLink_iff {α : Type u_1} {β : Type u_2} {x y : α} {f : β} {w : WList α β} (hw : w.Nonempty) (hnd : w.edge.Nodup) : w.tail.IsLink f x y ↔ w.IsLink f x y ∧ ¬f = firstEdge w hw

theorem WList.IsSuffix.eq_or_isSuffix_of_cons {α : Type u_1} {β : Type u_2} {w₁ w₂ : WList α β} (hsf : w₁.IsSuffix w₂) : w₁ = w₂ ∨ w₂.Nonempty ∧ w₁.IsSuffix w₂.tail

@[simp]

theorem WList.tail_eq_self_iff {α : Type u_1} {β : Type u_2} (w : WList α β) : w.tail = w ↔ w.Nil

theorem WList.IsSuffix.recOfTail {α : Type u_1} {β : Type u_2} {P : WList α β → Prop} (h : ∀ (w : WList α β), P w → P w.tail) {w₁ w₂ : WList α β} (hw₂ : P w₂) (hsf : w₁.IsSuffix w₂) : P w₁

theorem WList.idxOf_tail {α : Type u_1} {β : Type u_2} {x : α} {w : WList α β} [DecidableEq α] (hw : w.Nonempty) (hxf : w.first ≠ x) (hx : x ∈ w) : w.tail.idxOf x + 1 = w.idxOf x

theorem WList.Nonempty.dropLast_cons {α : Type u_1} {β : Type u_2} {w : WList α β} (hw : w.Nonempty) (x : α) (e : β) : (WList.cons x e w).dropLast = WList.cons x e w.dropLast

@[simp]

theorem WList.reverse_tail {α : Type u_1} {β : Type u_2} (w : WList α β) : w.reverse.tail = w.dropLast.reverse

@[simp]

theorem WList.reverse_dropLast {α : Type u_1} {β : Type u_2} (w : WList α β) : w.reverse.dropLast = w.tail.reverse

theorem WList.reverse_dropLast_reverse {α : Type u_1} {β : Type u_2} (w : WList α β) : w.reverse.dropLast.reverse = w.tail

theorem WList.reverse_tail_reverse {α : Type u_1} {β : Type u_2} (w : WList α β) : w.reverse.tail.reverse = w.dropLast

@[simp]

theorem WList.dropLast_concat {α : Type u_1} {β : Type u_2} (w : WList α β) (e : β) (x : α) : (w.concat e x).dropLast = w

theorem WList.Nonempty.concat_dropLast {α : Type u_1} {β : Type u_2} {w : WList α β} (hw : w.Nonempty) : w.dropLast.concat (lastEdge w hw) w.last = w

theorem WList.Nonempty.exists_concat {α : Type u_1} {β : Type u_2} {w : WList α β} (hw : w.Nonempty) : ∃ (w' : WList α β) (e : β) (x : α), w'.concat e x = w

theorem WList.Nontrivial.exists_cons_concat {α : Type u_1} {β : Type u_2} {w : WList α β} (hw : w.Nontrivial) : ∃ (x : α) (e : β) (w' : WList α β) (f : β) (y : α), w = cons x e (w'.concat f y)

@[simp]

theorem WList.dropLast_first {α : Type u_1} {β : Type u_2} (w : WList α β) : w.dropLast.first = w.first

@[simp]

theorem WList.dropLast_cons_concat {α : Type u_1} {β : Type u_2} {x y : α} {e e' : β} {w : WList α β} : (cons x e (w.concat e' y)).dropLast = cons x e w

@[simp]

theorem WList.Nonempty.vertex_dropLast {α : Type u_1} {β : Type u_2} {w : WList α β} (h : w.Nonempty) : w.dropLast.vertex = w.vertex.dropLast

@[simp]

theorem WList.dropLast_edge {α : Type u_1} {β : Type u_2} (w : WList α β) : w.dropLast.edge = w.edge.dropLast

@[simp]

theorem WList.dropLast_length {α : Type u_1} {β : Type u_2} (w : WList α β) : w.dropLast.length = w.length - 1

theorem WList.append_dropLast {α : Type u_1} {β : Type u_2} {w₂ : WList α β} (w₁ : WList α β) (hw₂ : w₂.Nonempty) : (w₁ ++ w₂).dropLast = w₁ ++ w₂.dropLast

theorem WList.mem_iff_eq_mem_dropLast_or_eq_last {α : Type u_1} {β : Type u_2} {u : α} {w : WList α β} : u ∈ w ↔ u ∈ w.dropLast ∨ u = w.last

theorem WList.mem_iff_eq_mem_vertex_dropLast_or_eq_last {α : Type u_1} {β : Type u_2} {u : α} {w : WList α β} : u ∈ w ↔ u ∈ w.vertex.dropLast ∨ u = w.last

theorem WList.eq_last_or_mem_dropLast {α : Type u_1} {β : Type u_2} {x : α} {w : WList α β} (h : x ∈ w) : x = w.last ∨ x ∈ w.dropLast

theorem WList.IsSublist.le_dropLast_of_ne_last {α : Type u_1} {β : Type u_2} {w w₀ : WList α β} (h : w₀ ≤ w) (hne : w₀.last ≠ w.last) : w₀ ≤ w.dropLast

theorem WList.dropLast_vertexSet_of_nodup {α : Type u_1} {β : Type u_2} {w : WList α β} (hw : w.vertex.Nodup) (hne : w.Nonempty) : w.dropLast.vertexSet = w.vertexSet \ {w.last}

theorem WList.mem_dropLast_iff_of_nodup {α : Type u_1} {β : Type u_2} {x : α} {w : WList α β} (hw : w.vertex.Nodup) (hne : w.Nonempty) : x ∈ w.dropLast ↔ x ∈ w ∧ x ≠ w.last

theorem WList.mem_vertex_dropLast_iff_of_nodup {α : Type u_1} {β : Type u_2} {x : α} {w : WList α β} (hw : w.vertex.Nodup) : x ∈ w.vertex.dropLast ↔ x ∈ w ∧ x ≠ w.last

Membership in the vertex list with the last vertex removed. Unlike mem_dropLast_iff_of_nodup this needs no Nonempty hypothesis: both sides are false when w is trivial.

theorem WList.mem_internalVertexSet_iff_of_nodup {α : Type u_1} {β : Type u_2} {x : α} {w : WList α β} (hw : w.vertex.Nodup) : x ∈ w.internalVertexSet ↔ x ∈ w ∧ x ≠ w.first ∧ x ≠ w.last

On a walk without repeated vertices, the internal vertices are exactly the vertices that are neither end.

theorem WList.first_notMem_internalVertexSet_of_nodup {α : Type u_1} {β : Type u_2} {w : WList α β} (hw : w.vertex.Nodup) : w.first ∉ w.internalVertexSet

theorem WList.last_notMem_internalVertexSet_of_nodup {α : Type u_1} {β : Type u_2} {w : WList α β} (hw : w.vertex.Nodup) : w.last ∉ w.internalVertexSet

theorem WList.dropLast_isPrefix {α : Type u_1} {β : Type u_2} (w : WList α β) : w.dropLast.IsPrefix w

theorem WList.dropLast_isPrefix_append_right {α : Type u_1} {β : Type u_2} {w₁ w₂ : WList α β} (hw₁ : w₁.Nonempty) : w₁.dropLast.IsPrefix (w₁ ++ w₂)

theorem WList.tail_dropLast {α : Type u_1} {β : Type u_2} {w : WList α β} (hw : w.length ≠ 1) : w.tail.dropLast = w.dropLast.tail

theorem WList.Nontrivial.tail_dropLast {α : Type u_1} {β : Type u_2} {w : WList α β} (hw : w.Nontrivial) : w.tail.dropLast = w.dropLast.tail

@[simp]

theorem WList.tail_nil_iff {α : Type u_1} {β : Type u_2} {w : WList α β} : w.tail.Nil ↔ w.length ≤ 1

@[simp]

theorem WList.tail_nonempty_iff {α : Type u_1} {β : Type u_2} {w : WList α β} : w.tail.Nonempty ↔ w.Nontrivial

theorem WList.Nontrivial.tail_nonempty {α : Type u_1} {β : Type u_2} {w : WList α β} : w.Nontrivial → w.tail.Nonempty

Alias of the reverse direction of WList.tail_nonempty_iff.

@[simp]

theorem WList.zip_tail {α : Type u_1} {β : Type u_2} (a : List α) {b : List β} (hb : b ≠ []) (h : b.length + 1 = a.length) : (WList.zip a b h).tail = WList.zip a.tail b.tail ⋯

@[simp]

theorem WList.zip_dropLast {α : Type u_1} {β : Type u_2} (a : List α) {b : List β} (hb : b ≠ []) (h : b.length + 1 = a.length) : (WList.zip a b h).dropLast = WList.zip a.dropLast b.dropLast ⋯

theorem WList.idxOf_dropLast {α : Type u_1} {β : Type u_2} {x : α} {w : WList α β} [DecidableEq α] (hw : w.Nonempty) (hx : x ∈ w) : w.dropLast.idxOf x = w.idxOf x

@[simp]

theorem WList.dropLast_nonempty_iff {α : Type u_1} {β : Type u_2} {w : WList α β} : w.dropLast.Nonempty ↔ w.Nontrivial

theorem WList.Nontrivial.dropLast_nonempty {α : Type u_1} {β : Type u_2} {w : WList α β} : w.Nontrivial → w.dropLast.Nonempty

Alias of the reverse direction of WList.dropLast_nonempty_iff.

@[simp]

theorem WList.dropLast_eq_self_iff {α : Type u_1} {β : Type u_2} (w : WList α β) : w.dropLast = w ↔ w.Nil

theorem WList.Nontrivial.dropLast_firstEdge {α : Type u_1} {β : Type u_2} {w : WList α β} (hw : w.Nontrivial) : Nonempty.firstEdge w.dropLast ⋯ = Nonempty.firstEdge w ⋯

theorem WList.Nonempty.firstEdge_notMem_tail {α : Type u_1} {β : Type u_2} {w : WList α β} (hw : w.Nonempty) (hnd : w.edge.Nodup) : firstEdge w hw ∉ w.tail.edge

theorem WList.Nonempty.lastEdge_notMem_dropLast {α : Type u_1} {β : Type u_2} {w : WList α β} (hw : w.Nonempty) (hnd : w.edge.Nodup) : lastEdge w hw ∉ w.dropLast.edge

theorem WList.Nontrivial.tail_lastEdge {α : Type u_1} {β : Type u_2} {w : WList α β} (hw : w.Nontrivial) : Nonempty.lastEdge w.tail ⋯ = Nonempty.lastEdge w ⋯

theorem WList.Nontrivial.firstEdge_ne_lastEdge {α : Type u_1} {β : Type u_2} {w : WList α β} (hw : w.Nontrivial) (hnd : w.edge.Nodup) : Nonempty.firstEdge w ⋯ ≠ Nonempty.lastEdge w ⋯

theorem WList.IsPrefix.eq_or_isPrefix_of_cons {α : Type u_1} {β : Type u_2} {w₁ w₂ : WList α β} (hsf : w₁.IsPrefix w₂) : w₁ = w₂ ∨ w₂.Nonempty ∧ w₁.IsPrefix w₂.dropLast

theorem WList.IsPrefix.recOfDropLast {α : Type u_1} {β : Type u_2} {P : WList α β → Prop} (h : ∀ (w : WList α β), P w → P w.dropLast) {w₁ w₂ : WList α β} (hw₂ : P w₂) (hpf : w₁.IsPrefix w₂) : P w₁

@[simp]

theorem WList.take_length {α : Type u_1} {β : Type u_2} (w : WList α β) (n : ℕ) : (w.take n).length = min n w.length

@[simp]

theorem WList.take_length_le {α : Type u_1} {β : Type u_2} (w : WList α β) (n : ℕ) : (w.take n).length ≤ n

@[simp]

theorem WList.take_length_le' {α : Type u_1} {β : Type u_2} (w : WList α β) (n : ℕ) : (w.take n).length ≤ w.length

@[simp]

theorem WList.take_eq_self {α : Type u_1} {β : Type u_2} (w : WList α β) : w.take w.length = w

@[simp]

theorem WList.take_first {α : Type u_1} {β : Type u_2} (w : WList α β) (n : ℕ) : (w.take n).first = w.first

@[simp]

theorem WList.take_last {α : Type u_1} {β : Type u_2} (w : WList α β) (n : ℕ) : (w.take n).last = w.get n

@[simp]

theorem WList.take_vertex {α : Type u_1} {β : Type u_2} (w : WList α β) (n : ℕ) : (w.take n).vertex = List.take (n + 1) w.vertex

@[simp]

theorem WList.take_edge {α : Type u_1} {β : Type u_2} (w : WList α β) (n : ℕ) : (w.take n).edge = List.take n w.edge

theorem WList.take_concat {α : Type u_1} {β : Type u_2} (w : WList α β) (e : β) (x : α) (n : ℕ) : (w.concat e x).take n = if n ≤ w.length then w.take n else w.concat e x

@[simp]

theorem WList.take_append_length {α : Type u_1} {β : Type u_2} {w₁ w₂ : WList α β} (heq : w₁.last = w₂.first) : (w₁ ++ w₂).take w₁.length = w₁

@[simp]

theorem WList.take_take {α : Type u_1} {β : Type u_2} (w : WList α β) (m n : ℕ) : (w.take n).take m = w.take (min m n)

theorem WList.take_take_comm {α : Type u_1} {β : Type u_2} (w : WList α β) (m n : ℕ) : (w.take n).take m = (w.take m).take n

theorem WList.IsPrefix.take {α : Type u_1} {β : Type u_2} {w₁ w₂ : WList α β} (h : w₁.IsPrefix w₂) (n : ℕ) : (w₁.take n).IsPrefix (w₂.take n)

@[simp]

theorem WList.drop_length {α : Type u_1} {β : Type u_2} (w : WList α β) (n : ℕ) : (w.drop n).length = w.length - n

theorem WList.drop_eq_nil_of_length_le {α : Type u_1} {β : Type u_2} {w : WList α β} {n : ℕ} (h : w.length ≤ n) : w.drop n = nil w.last

@[simp]

theorem WList.drop_length_eq {α : Type u_1} {β : Type u_2} (w : WList α β) : w.drop w.length = nil w.last

@[simp]

theorem WList.drop_first {α : Type u_1} {β : Type u_2} (w : WList α β) (n : ℕ) : (w.drop n).first = w.get n

theorem WList.drop_first_of_length_lt {α : Type u_1} {β : Type u_2} {w : WList α β} {n : ℕ} (h : w.length < n) : (w.drop n).first = w.last

@[simp]

theorem WList.drop_last {α : Type u_1} {β : Type u_2} (w : WList α β) (n : ℕ) : (w.drop n).last = w.last

@[simp]

theorem WList.drop_vertex {α : Type u_1} {β : Type u_2} {n : ℕ} (w : WList α β) (hn : n ≤ w.length) : (w.drop n).vertex = List.drop n w.vertex

@[simp]

theorem WList.drop_edge {α : Type u_1} {β : Type u_2} (w : WList α β) (n : ℕ) : (w.drop n).edge = List.drop n w.edge

theorem WList.drop_concat_comm {α : Type u_1} {β : Type u_2} {x : α} {e : β} {w : WList α β} {n : ℕ} (hn : n ≤ w.length) : (w.concat e x).drop n = (w.drop n).concat e x

@[simp]

theorem WList.drop_append_length {α : Type u_1} {β : Type u_2} (w₁ w₂ : WList α β) : (w₁ ++ w₂).drop w₁.length = w₂

@[simp]

theorem WList.drop_drop {α : Type u_1} {β : Type u_2} (w : WList α β) (m n : ℕ) : (w.drop n).drop m = w.drop (m + n)

theorem WList.drop_drop_comm {α : Type u_1} {β : Type u_2} {w : WList α β} (m n : ℕ) : (w.drop m).drop n = (w.drop n).drop m

theorem WList.get_append_add {α : Type u_1} {β : Type u_2} (w₁ w₂ : WList α β) (m : ℕ) : (w₁ ++ w₂).get (w₁.length + m) = w₂.get m

@[simp]

theorem WList.take_drop {α : Type u_1} {β : Type u_2} (w : WList α β) (n : ℕ) : w.take n ++ w.drop n = w

@[simp]

theorem WList.dropLast_take {α : Type u_1} {β : Type u_2} {w : WList α β} {n : ℕ} (hn : n ≤ w.length) : (w.take n).dropLast = w.take (n - 1)

@[simp]

theorem WList.drop_one {α : Type u_1} {β : Type u_2} (w : WList α β) : w.drop 1 = w.tail

@[simp]

theorem WList.drop_length_eq_zero_iff {α : Type u_1} {β : Type u_2} (w : WList α β) (n : ℕ) : (w.drop n).length = 0 ↔ w.length ≤ n

Relationships with prefixUntil and suffixFrom

theorem WList.IsPrefix.take_eq {α : Type u_1} {β : Type u_2} {w₁ w₂ : WList α β} (h : w₁.IsPrefix w₂) : w₂.take w₁.length = w₁

theorem WList.take_isPrefix {α : Type u_1} {β : Type u_2} (w : WList α β) (n : ℕ) : (w.take n).IsPrefix w

theorem WList.IsPrefix.eq_take_length {α : Type u_1} {β : Type u_2} {w₁ w₂ : WList α β} (h : w₁.IsPrefix w₂) : w₁ = w₂.take w₁.length

theorem WList.drop_isSuffix {α : Type u_1} {β : Type u_2} (w : WList α β) (n : ℕ) : (w.drop n).IsSuffix w

theorem WList.drop_isSuffix_drop {α : Type u_1} {β : Type u_2} {w : WList α β} {m n : ℕ} (hmn : m ≤ n) : (w.drop n).IsSuffix (w.drop m)

theorem WList.IsSuffix.eq_drop_length {α : Type u_1} {β : Type u_2} {w₁ w₂ : WList α β} (h : w₁.IsSuffix w₂) : w₁ = w₂.drop (w₂.length - w₁.length)

theorem WList.IsPrefix.drop {α : Type u_1} {β : Type u_2} {w₁ w₂ : WList α β} (h : w₁.IsPrefix w₂) {n : ℕ} (hn : n ≤ w₁.length) : (w₁.drop n).IsPrefix (w₂.drop n)

theorem WList.IsSuffix.drop {α : Type u_1} {β : Type u_2} {w₁ w₂ : WList α β} (h : w₁.IsSuffix w₂) (n : ℕ) : (w₁.drop n).IsSuffix (w₂.drop n)

theorem WList.IsInfix.drop {α : Type u_1} {β : Type u_2} {w₁ w₂ : WList α β} (h : w₁.IsInfix w₂) {n : ℕ} (hn : n ≤ w₁.length) : (w₁.drop n).IsInfix (w₂.drop n)

@[simp]

theorem WList.prefixUntilVertex_take {α : Type u_1} {β : Type u_2} {x : α} [DecidableEq α] {w : WList α β} (hx : x ∈ w) {n : ℕ} (hn : w.idxOf x ≤ n) (hn' : n ≤ w.length) : (w.take n).prefixUntilVertex x = w.prefixUntilVertex x

theorem WList.idxOf_eq_length_prefixUntilVertex {α : Type u_1} {β : Type u_2} {x : α} {w : WList α β} [DecidableEq α] (hx : x ∈ w) : w.idxOf x = (w.prefixUntilVertex x).length

theorem WList.prefixUntilVertex_idxOf {α : Type u_1} {β : Type u_2} {x y : α} {w : WList α β} [DecidableEq α] (hx : x ∈ w) (hle : w.idxOf y ≤ w.idxOf x) : w.idxOf y = (w.prefixUntilVertex x).idxOf y

theorem WList.suffixFromVertex_index {α : Type u_1} {β : Type u_2} {x y : α} {w : WList α β} [DecidableEq α] (hx : x ∈ w) (hle : w.idxOf x ≤ w.idxOf y) : w.idxOf y = (w.suffixFromVertex x).idxOf y + w.idxOf x

theorem WList.prefixUntilVertex_tail {α : Type u_1} {β : Type u_2} {v : α} [DecidableEq α] (w : WList α β) (hv : v ≠ w.first) (hvw : v ∈ w) : w.tail.prefixUntilVertex v = (w.prefixUntilVertex v).tail