theorem WList.prefixUntil_eq_nil {α : Type u_1} {β : Type u_2} {w : WList α β} {P : α → Prop} [DecidablePred P] (hP : P w.first) : w.prefixUntil P = nil w.first

@[simp]

theorem WList.prefixUntil_first {α : Type u_1} {β : Type u_2} (w : WList α β) (P : α → Prop) [DecidablePred P] : (w.prefixUntil P).first = w.first

theorem WList.prefixUntil_prop_last_iff {α : Type u_1} {β : Type u_2} (w : WList α β) (P : α → Prop) [DecidablePred P] : P (w.prefixUntil P).last ↔ ∃ x ∈ w, P x

theorem WList.prefixUntil_prop_last {α : Type u_1} {β : Type u_2} {w : WList α β} {P : α → Prop} [DecidablePred P] (h : ∃ u ∈ w, P u) : P (w.prefixUntil P).last

theorem WList.prefixUntil_not_prop {α : Type u_1} {β : Type u_2} {x : α} {w : WList α β} {P : α → Prop} [DecidablePred P] (hx : x ∈ w.prefixUntil P) (hne : (w.prefixUntil P).last ≠ x) : ¬P x

theorem WList.prefixUntil_last_eq_of_prop {α : Type u_1} {β : Type u_2} {v : α} {w : WList α β} {P : α → Prop} [DecidablePred P] (hv : v ∈ w.prefixUntil P) (hvP : P v) : (w.prefixUntil P).last = v

theorem WList.Nonempty.prefixUntil_nil_iff {α : Type u_1} {β : Type u_2} {w : WList α β} {P : α → Prop} [DecidablePred P] (hw : w.Nonempty) : (w.prefixUntil P).Nil ↔ P w.first

theorem WList.Nonempty.prefixUntil_nonempty_iff {α : Type u_1} {β : Type u_2} {w : WList α β} {P : α → Prop} [DecidablePred P] (hw : w.Nonempty) : (w.prefixUntil P).Nonempty ↔ ¬P w.first

theorem WList.prefixUntil_isPrefix {α : Type u_1} {β : Type u_2} (w : WList α β) (P : α → Prop) [DecidablePred P] : (w.prefixUntil P).IsPrefix w

theorem WList.prefixUntil_isPrefix_of_prop {α : Type u_1} {β : Type u_2} {w : WList α β} {P : α → Prop} [DecidablePred P] {w' : WList α β} (hw' : w'.IsPrefix w) (h : ∃ u ∈ w', P u) : (w.prefixUntil P).IsPrefix w'

theorem WList.prefixUntil_last_eq_iff_prop {α : Type u_1} {β : Type u_2} {v : α} {w : WList α β} {P : α → Prop} [DecidablePred P] (h : ∃ u ∈ w, P u) : P v ∧ v ∈ w.prefixUntil P ↔ (w.prefixUntil P).last = v

theorem WList.prefixUntil_inter_eq_last {α : Type u_1} {β : Type u_2} {S : Set α} {w : WList α β} [DecidablePred fun (x : α) => x ∈ S] (h : ∃ u ∈ w, u ∈ S) : S ∩ (w.prefixUntil fun (x : α) => x ∈ S).vertexSet = {(w.prefixUntil fun (x : α) => x ∈ S).last}

@[simp]

theorem WList.prefixUntil_eq_self_iff {α : Type u_1} {β : Type u_2} (w : WList α β) (P : α → Prop) [DecidablePred P] : w.prefixUntil P = w ↔ ∀ u ∈ w.vertex.dropLast, ¬P u

theorem WList.prefixUntil_eq_self_of_forall {α : Type u_1} {β : Type u_2} {w : WList α β} {P : α → Prop} [DecidablePred P] (h : ∀ u ∈ w, ¬P u) : w.prefixUntil P = w

theorem WList.prefixUntil_concat_of_exists {α : Type u_1} {β : Type u_2} {x : α} {e : β} {P : α → Prop} [DecidablePred P] {w : WList α β} (h : ∃ u ∈ w, P u) : (w.concat e x).prefixUntil P = w.prefixUntil P

theorem WList.prefixUntil_concat_of_forall {α : Type u_1} {β : Type u_2} {x : α} {e : β} {P : α → Prop} [DecidablePred P] {w : WList α β} (h : ∀ u ∈ w, ¬P u) : (w.concat e x).prefixUntil P = w.concat e x

theorem WList.prefixUntil_concat {α : Type u_1} {β : Type u_2} {x : α} {e : β} (w : WList α β) (P : α → Prop) [DecidablePred P] : (w.concat e x).prefixUntil P = if (w.vertex.all fun (x : α) => decide ¬P x) = true then w.concat e x else w.prefixUntil P

theorem WList.IsPrefix.prefixUntil_eq_prefixUntil_of_exists {α : Type u_1} {β : Type u_2} {w w' : WList α β} {P : α → Prop} [DecidablePred P] (hw' : w'.IsPrefix w) (h : ∃ u ∈ w', P u) : w'.prefixUntil P = w.prefixUntil P

theorem WList.prefixUntil_eq_of_prefix {α : Type u_1} {β : Type u_2} {w : WList α β} {P : α → Prop} [DecidablePred P] {w' : WList α β} (hP : ∃ u ∈ w, P u) (h : w'.IsPrefix (w.prefixUntil P)) (hl : (w.prefixUntil P).last ∈ w') : w.prefixUntil P = w'

theorem WList.prefixUntil_vertex_dropLast_not_prop {α : Type u_1} {β : Type u_2} {x : α} {w : WList α β} {P : α → Prop} [DecidablePred P] (hx : x ∈ (w.prefixUntil P).vertex.dropLast) : ¬P x

theorem WList.disjoint_internalVertexSet_cons_prefixUntil {α : Type u_1} {β : Type u_2} (w : WList α β) (P : α → Prop) [DecidablePred P] (x : α) (e : β) : Disjoint (cons x e (w.prefixUntil P)).internalVertexSet {y : α | P y}

The internal vertices of cons x e (w.prefixUntil P) are exactly the dropLast vertices of the prefix, so none of them satisfy P.

theorem WList.Nonempty.mem_first_vertex_dropLast {α : Type u_1} {β : Type u_2} {w : WList α β} (hw : w.Nonempty) : w.first ∈ w.vertex.dropLast

The first vertex of a nonempty walk belongs to vertex.dropLast.

theorem WList.Nontrivial.mem_first_vertex_dropLast {α : Type u_1} {β : Type u_2} {w : WList α β} (hw : w.Nontrivial) : w.first ∈ w.vertex.dropLast

The first vertex of a nontrivial walk belongs to vertex.dropLast.

theorem WList.Nontrivial.prefixUntil_not_prop_first {α : Type u_1} {β : Type u_2} {w : WList α β} {P : α → Prop} [DecidablePred P] (h : (w.prefixUntil P).Nontrivial) : ¬P (w.prefixUntil P).first

The first vertex of a nontrivial prefixUntil P does not satisfy P.

theorem WList.DInc.not_prop_left_of_prefixUntil {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {w : WList α β} {P : α → Prop} [DecidablePred P] (h : (w.prefixUntil P).DInc e x y) : ¬P x

The left endpoint of any directed edge of w.prefixUntil P fails P.

theorem WList.Nontrivial.second_mem_internalVertexSet {α : Type u_1} {β : Type u_2} {w : WList α β} (hw : w.Nontrivial) : w.second ∈ w.internalVertexSet

On a nontrivial walk, the second vertex is internal.

theorem WList.Nontrivial.not_prop_both_of_dInc {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {w : WList α β} {P : α → Prop} (hw : w.Nontrivial) (hdisj : Disjoint w.internalVertexSet {z : α | P z}) (h : w.DInc e x y) : ¬(P x ∧ P y)

If w is nontrivial and its internal vertices avoid the P-points, then no directed edge of w has both ends satisfying P.

Nontrivial is essential: a single edge between two P-points has empty internal set.

theorem WList.vertex_prefixUntil {α : Type u_1} {β : Type u_2} (w : WList α β) (P : α → Prop) [DecidablePred P] : (w.prefixUntil P).vertex = List.take (List.findIdx (fun (b : α) => decide (P b)) w.vertex + 1) w.vertex

theorem WList.prefixUntilVertex_cons_of_ne {α : Type u_1} {β : Type u_2} {x y : α} [DecidableEq α] (w : WList α β) (hne : x ≠ y) (e : β) : (cons x e w).prefixUntilVertex y = cons x e (w.prefixUntilVertex y)

theorem WList.prefixUntilVertex_isPrefix {α : Type u_1} {β : Type u_2} [DecidableEq α] (w : WList α β) (x : α) : (w.prefixUntilVertex x).IsPrefix w

theorem WList.prefixUntil_eq_prefixUntilVertex_last {α : Type u_1} {β : Type u_2} {w : WList α β} {P : α → Prop} [DecidablePred P] [DecidableEq α] (h : ∃ u ∈ w, P u) : w.prefixUntilVertex (w.prefixUntil P).last = w.prefixUntil P

theorem WList.prefixUntil_eq_prefixUntilVertex_last_of_nodup {α : Type u_1} {β : Type u_2} {w : WList α β} {P : α → Prop} [DecidablePred P] [DecidableEq α] (hnd : w.vertex.Nodup) : w.prefixUntilVertex (w.prefixUntil P).last = w.prefixUntil P

@[simp]

theorem WList.prefixUntilVertex_last {α : Type u_1} {β : Type u_2} {x : α} {w : WList α β} [DecidableEq α] (hxw : x ∈ w) : (w.prefixUntilVertex x).last = x

@[simp]

theorem WList.prefixUntilVertex_first {α : Type u_1} {β : Type u_2} (w : WList α β) (x : α) [DecidableEq α] : (w.prefixUntilVertex x).first = w.first

@[simp]

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

@[simp]

theorem WList.suffixFrom_last {α : Type u_1} {β : Type u_2} {P : α → Prop} [DecidablePred P] (w : WList α β) : (w.suffixFrom P).last = w.last

theorem WList.suffixFrom_prop_first_iff {α : Type u_1} {β : Type u_2} (w : WList α β) (P : α → Prop) [DecidablePred P] : P (w.suffixFrom P).first ↔ ∃ x ∈ w, P x

theorem WList.suffixFrom_prop_first {α : Type u_1} {β : Type u_2} {P : α → Prop} [DecidablePred P] {w : WList α β} (h : ∃ u ∈ w, P u) : P (w.suffixFrom P).first

theorem WList.suffixFrom_eq_nil_of_forall {α : Type u_1} {β : Type u_2} {P : α → Prop} [DecidablePred P] {w : WList α β} (h : ∀ u ∈ w, ¬P u) : w.suffixFrom P = nil w.last

theorem WList.suffixFrom_eq_nil_iff {α : Type u_1} {β : Type u_2} {w : WList α β} {P : α → Prop} [DecidablePred P] : w.suffixFrom P = nil w.last ↔ ∀ u ∈ w.vertex.dropLast, ¬P u

theorem WList.suffixFrom_eq_self_iff {α : Type u_1} {β : Type u_2} (w : WList α β) (P : α → Prop) [DecidablePred P] : w.suffixFrom P = w ↔ w.Nil ∨ P w.first

theorem WList.suffixFrom_concat_of_forall {α : Type u_1} {β : Type u_2} {x : α} {e : β} (w : WList α β) (P : α → Prop) [DecidablePred P] (h : ∀ u ∈ w, ¬P u) : (w.concat e x).suffixFrom P = nil x

theorem WList.suffixFrom_concat_of_exists {α : Type u_1} {β : Type u_2} {x : α} {e : β} (w : WList α β) (P : α → Prop) [DecidablePred P] (h : ∃ u ∈ w, P u) : (w.concat e x).suffixFrom P = (w.suffixFrom P).concat e x

theorem WList.suffixFrom_concat {α : Type u_1} {β : Type u_2} {x : α} {e : β} (w : WList α β) (P : α → Prop) [DecidablePred P] : (w.concat e x).suffixFrom P = if (w.vertex.all fun (x : α) => decide ¬P x) = true then nil x else (w.suffixFrom P).concat e x

@[simp]

theorem WList.prefixUntil_append_suffixFrom {α : Type u_1} {β : Type u_2} (w : WList α β) (P : α → Prop) [DecidablePred P] : w.prefixUntil P ++ w.suffixFrom P = w

theorem WList.IsSuffix.suffixFrom_eq_suffixFrom_of_forall {α : Type u_1} {β : Type u_2} {w₁ w₂ : WList α β} {P : α → Prop} [DecidablePred P] (hP : ∀ u ∈ w₂, P u → u ∈ w₁) (hnd : w₂.vertex.Nodup) (h : w₁.IsSuffix w₂) : w₁.suffixFrom P = w₂.suffixFrom P

@[simp]

theorem WList.prefixUntil_last_eq_suffixFrom_first {α : Type u_1} {β : Type u_2} (w : WList α β) (P : α → Prop) [DecidablePred P] : (w.prefixUntil P).last = (w.suffixFrom P).first

theorem WList.prefixUntil_dropLast_vertex_append_suffixFrom_vertex {α : Type u_1} {β : Type u_2} (w : WList α β) (P : α → Prop) [DecidablePred P] : (w.prefixUntil P).vertex.dropLast ++ (w.suffixFrom P).vertex = w.vertex

theorem WList.prefixUntil_vertex_append_suffixFrom_tail_vertex {α : Type u_1} {β : Type u_2} (w : WList α β) (P : α → Prop) [DecidablePred P] : (w.prefixUntil P).vertex ++ (w.suffixFrom P).vertex.tail = w.vertex

theorem WList.suffixFrom_vertex_filter_eq_vertex_filter {α : Type u_1} {β : Type u_2} (w : WList α β) (P Q : α → Prop) [DecidablePred P] [DecidablePred Q] : List.filter (fun (b : α) => decide (Q b)) (w.suffixFrom P).vertex = List.filter (fun (b : α) => decide (Q b)) w.vertex ∨ List.filter (fun (b : α) => decide (P b)) (w.suffixFrom Q).vertex = List.filter (fun (b : α) => decide (P b)) w.vertex

theorem WList.prefixUntilLast_append_suffixFromLast {α : Type u_1} {β : Type u_2} (w : WList α β) (P : α → Prop) [DecidablePred P] : w.prefixUntilLast P ++ w.suffixFromLast P = w

theorem WList.vertex_suffixFrom {α : Type u_1} {β : Type u_2} (w : WList α β) (P : α → Prop) [DecidablePred P] : (w.suffixFrom P).vertex = List.drop (min (List.findIdx (fun (b : α) => decide (P b)) w.vertex) w.length) w.vertex

theorem WList.suffixFromVertex_cons_of_ne {α : Type u_1} {β : Type u_2} {x y : α} [DecidableEq α] (w : WList α β) (hne : x ≠ y) (e : β) : (cons x e w).suffixFromVertex y = w.suffixFromVertex y

theorem WList.suffixFromVertex_append_right_of_notMem {α : Type u_1} {β : Type u_2} [DecidableEq α] {P Q : WList α β} {uf : α} (huf : uf ∉ P) : (P ++ Q).suffixFromVertex uf = Q.suffixFromVertex uf

theorem WList.suffixFromVertex_cons_or {α : Type u_1} {β : Type u_2} [DecidableEq α] (u : α) (e : β) (w : WList α β) (x : α) : u = x ∧ (cons u e w).suffixFromVertex x = cons u e w ∨ u ≠ x ∧ (cons u e w).suffixFromVertex x = w.suffixFromVertex x

@[simp]

theorem WList.suffixFromVertex_of_notMem {α : Type u_1} {β : Type u_2} [DecidableEq α] (w : WList α β) (x : α) (hx : x ∉ w) : w.suffixFromVertex x = nil w.last

@[simp]

theorem WList.suffixFromVertex_first {α : Type u_1} {β : Type u_2} {x : α} {w : WList α β} [DecidableEq α] (hxw : x ∈ w) : (w.suffixFromVertex x).first = x

theorem WList.suffixFrom_eq_suffixFromVertex_first {α : Type u_1} {β : Type u_2} {w : WList α β} {P : α → Prop} [DecidablePred P] [DecidableEq α] (h : ∃ u ∈ w, P u) : w.suffixFromVertex (w.suffixFrom P).first = w.suffixFrom P

theorem WList.suffixFrom_eq_suffixFromVertex_first_of_nodup {α : Type u_1} {β : Type u_2} {w : WList α β} {P : α → Prop} [DecidablePred P] [DecidableEq α] (hnd : w.vertex.Nodup) : w.suffixFromVertex (w.suffixFrom P).first = w.suffixFrom P

@[simp]

theorem WList.suffixFromVertex_last {α : Type u_1} {β : Type u_2} (w : WList α β) (x : α) [DecidableEq α] : (w.suffixFromVertex x).last = w.last

@[simp]

theorem WList.suffixFromVertex_eq_self_iff {α : Type u_1} {β : Type u_2} [DecidableEq α] (w : WList α β) (x : α) : w.suffixFromVertex x = w ↔ w.Nil ∨ w.first = x

@[simp]

theorem WList.prefixUntilVertex_append_suffixFromVertex {α : Type u_1} {β : Type u_2} [DecidableEq α] (w : WList α β) (x : α) : w.prefixUntilVertex x ++ w.suffixFromVertex x = w

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

@[simp]

theorem WList.suffixFromVertex_first_eq {α : Type u_1} {β : Type u_2} [DecidableEq α] (w : WList α β) : w.suffixFromVertex w.first = w

theorem WList.suffixFromVertex_second_eq {α : Type u_1} {β : Type u_2} {x : α} {w : WList α β} [DecidableEq α] (e : β) (hx : x ≠ w.first) : (cons x e w).suffixFromVertex w.first = w

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

@[simp]

theorem WList.prefixUntilVertex_last_eq_suffixFromVertex_first {α : Type u_1} {β : Type u_2} {x : α} {w : WList α β} [DecidableEq α] (hx : x ∈ w) : (w.prefixUntilVertex x).last = (w.suffixFromVertex x).first

@[simp]

theorem WList.suffixFromVertex_idempotent {α : Type u_1} {β : Type u_2} [DecidableEq α] (p : WList α β) (x : α) : (p.suffixFromVertex x).suffixFromVertex x = p.suffixFromVertex x

@[simp]

theorem WList.prefixUntilLast_isPrefix {α : Type u_1} {β : Type u_2} (w : WList α β) (P : α → Prop) [DecidablePred P] : (w.prefixUntilLast P).IsPrefix w

theorem WList.prefixUntilLast_prop_last_iff {α : Type u_1} {β : Type u_2} (w : WList α β) (P : α → Prop) [DecidablePred P] : P (w.prefixUntilLast P).last ↔ ∃ x ∈ w, P x

theorem WList.prefixUntilLast_prop_last {α : Type u_1} {β : Type u_2} {w : WList α β} {P : α → Prop} [DecidablePred P] (h : ∃ x ∈ w, P x) : P (w.prefixUntilLast P).last

@[simp]

theorem WList.prefixUntilLast_first {α : Type u_1} {β : Type u_2} (w : WList α β) (P : α → Prop) [DecidablePred P] : (w.prefixUntilLast P).first = w.first

theorem WList.prefixUntilLast_vertex_filter_eq_vertex_filter {α : Type u_1} {β : Type u_2} (w : WList α β) (P Q : α → Prop) [DecidablePred P] [DecidablePred Q] : List.filter (fun (b : α) => decide (Q b)) (w.prefixUntilLast P).vertex = List.filter (fun (b : α) => decide (Q b)) w.vertex ∨ List.filter (fun (b : α) => decide (P b)) (w.prefixUntilLast Q).vertex = List.filter (fun (b : α) => decide (P b)) w.vertex

@[simp]

theorem WList.prefixUntil_isPrefix_prefixUntilLast {α : Type u_1} {β : Type u_2} (w : WList α β) (P : α → Prop) [DecidablePred P] (h : ∃ x ∈ w, P x) : (w.prefixUntil P).IsPrefix (w.prefixUntilLast P)

w.prefixUntil P is a prefix of w.prefixUntilLast P if P occurs in w. Otherwise, w.prefixUntil P = w and w.prefixUntilLast P = nil w.first.

theorem WList.prefixUntilLast_eq_prefixUntil_of_nodup {α : Type u_1} {β : Type u_2} {x : α} {w : WList α β} [DecidableEq α] (hnd : w.vertex.Nodup) (h : List.count x w.vertex = 1) : (w.prefixUntilLast fun (x_1 : α) => x_1 = x) = w.prefixUntilVertex x

@[simp]

theorem WList.suffixFromLast_isSuffix {α : Type u_1} {β : Type u_2} (w : WList α β) (P : α → Prop) [DecidablePred P] : (w.suffixFromLast P).IsSuffix w

theorem WList.suffixFromLast_prop_first_iff {α : Type u_1} {β : Type u_2} (w : WList α β) (P : α → Prop) [DecidablePred P] : P (w.suffixFromLast P).first ↔ ∃ x ∈ w, P x

theorem WList.suffixFromLast_prop_first {α : Type u_1} {β : Type u_2} {w : WList α β} {P : α → Prop} [DecidablePred P] (h : ∃ x ∈ w, P x) : P (w.suffixFromLast P).first

@[simp]

theorem WList.suffixFromLast_last {α : Type u_1} {β : Type u_2} (w : WList α β) (P : α → Prop) [DecidablePred P] : (w.suffixFromLast P).last = w.last

theorem WList.suffixFromLast_first_eq_of_prop {α : Type u_1} {β : Type u_2} {v : α} {w : WList α β} {P : α → Prop} [DecidablePred P] (hv : v ∈ w.suffixFromLast P) (hvP : P v) : (w.suffixFromLast P).first = v

theorem WList.suffixFromLast_first_eq_iff_prop {α : Type u_1} {β : Type u_2} {v : α} {w : WList α β} {P : α → Prop} [DecidablePred P] (h : ∃ x ∈ w, P x) : P v ∧ v ∈ w.suffixFromLast P ↔ (w.suffixFromLast P).first = v

theorem WList.suffixFromLast_not_prop {α : Type u_1} {β : Type u_2} {x : α} {w : WList α β} {P : α → Prop} [DecidablePred P] (hx : x ∈ w.suffixFromLast P) (hne : (w.suffixFromLast P).first ≠ x) : ¬P x

theorem WList.suffixFromLast_inter_eq_first {α : Type u_1} {β : Type u_2} {S : Set α} {w : WList α β} [DecidablePred fun (x : α) => x ∈ S] (h : ∃ u ∈ w, u ∈ S) : S ∩ (w.suffixFromLast fun (x : α) => x ∈ S).vertexSet = {(w.suffixFromLast fun (x : α) => x ∈ S).first}

@[simp]

theorem WList.suffixFromLast_eq_self_iff {α : Type u_1} {β : Type u_2} (w : WList α β) (P : α → Prop) [DecidablePred P] : w.suffixFromLast P = w ↔ ∀ x ∈ w.vertex.tail, ¬P x

theorem WList.suffixFromLast_eq_self_of_forall {α : Type u_1} {β : Type u_2} {w : WList α β} {P : α → Prop} [DecidablePred P] (h : ∀ x ∈ w, ¬P x) : w.suffixFromLast P = w

theorem WList.IsSuffix.suffixFromLast_eq_suffixFromLast_of_exists {α : Type u_1} {β : Type u_2} {w w' : WList α β} {P : α → Prop} [DecidablePred P] (hw' : w'.IsSuffix w) (h : ∃ u ∈ w', P u) : w'.suffixFromLast P = w.suffixFromLast P

theorem WList.IsPrefix.prefixUntilLast_eq_prefixUntilLast_of_forall {α : Type u_1} {β : Type u_2} {w₁ w₂ : WList α β} {P : α → Prop} [DecidablePred P] (hP : ∀ u ∈ w₂, P u → u ∈ w₁) (hnd : w₂.vertex.Nodup) (h : w₁.IsPrefix w₂) : w₁.prefixUntilLast P = w₂.prefixUntilLast P

@[simp]

theorem WList.suffixFrom_isSuffix_suffixFromLast {α : Type u_1} {β : Type u_2} {P : α → Prop} [DecidablePred P] {w : WList α β} (h : ∃ x ∈ w, P x) : (w.suffixFromLast P).IsSuffix (w.suffixFrom P)

theorem WList.suffixFrom_eq_suffixFromLast_of_nodup {α : Type u_1} {β : Type u_2} {x : α} {w : WList α β} [DecidableEq α] (hnd : w.vertex.Nodup) (h : List.count x w.vertex = 1) : (w.suffixFrom fun (x_1 : α) => x_1 = x) = w.suffixFromLast fun (x_1 : α) => x_1 = x

theorem WList.suffixFromLast_vertex_tail_not_prop {α : Type u_1} {β : Type u_2} {x : α} {w : WList α β} {P : α → Prop} [DecidablePred P] (hx : x ∈ (w.suffixFromLast P).vertex.tail) : ¬P x

theorem WList.prefixUntilEdge_isPrefix_dropLast {α : Type u_1} {β : Type u_2} {Q : β → Prop} [DecidablePred Q] {w : WList α β} (hQ : ∃ e ∈ w.edgeSet, Q e) : (w.prefixUntilEdge Q).IsPrefix w.dropLast

theorem WList.prefixUntilEdge_vertex_isPrefix_dropLast {α : Type u_1} {β : Type u_2} {Q : β → Prop} [DecidablePred Q] {w : WList α β} (hQ : ∃ e ∈ w.edgeSet, Q e) : (w.prefixUntilEdge Q).vertex.Sublist w.vertex.dropLast

theorem WList.suffixFromEdge_isSuffix_tail {α : Type u_1} {β : Type u_2} {Q : β → Prop} [DecidablePred Q] {w : WList α β} (hQ : ∃ e ∈ w.edgeSet, Q e) : (w.suffixFromEdge Q).IsSuffix w.tail

theorem WList.suffixFromEdge_vertex_isSuffix_tail {α : Type u_1} {β : Type u_2} {Q : β → Prop} [DecidablePred Q] {w : WList α β} (hQ : ∃ e ∈ w.edgeSet, Q e) : (w.suffixFromEdge Q).vertex <:+ w.vertex.tail

theorem WList.prefixUntilEdgeLabel_edge_notMem {α : Type u_1} {β : Type u_2} {e : β} {w : WList α β} [DecidableEq β] : e ∉ (w.prefixUntilEdgeLabel e).edge

theorem WList.prefixUntilEdgeLabel_append_cons_suffixFromEdgeLabel {α : Type u_1} {β : Type u_2} {e : β} {w : WList α β} [DecidableEq β] (he : e ∈ w.edge) : w.prefixUntilEdgeLabel e ++ cons (w.prefixUntilEdgeLabel e).last e (w.suffixFromEdgeLabel e) = w

theorem WList.suffixFromEdgeLabel_edge_notMem {α : Type u_1} {β : Type u_2} {e : β} {w : WList α β} [DecidableEq β] (hnd : w.edge.Nodup) : e ∉ (w.suffixFromEdgeLabel e).edge

theorem WList.isLink_prefixUntilEdgeLabel_suffixFromEdgeLabel {α : Type u_1} {β : Type u_2} {e : β} {w : WList α β} [DecidableEq β] (he : e ∈ w.edge) : w.IsLink e (w.prefixUntilEdgeLabel e).last (w.suffixFromEdgeLabel e).first

theorem WList.IsSublist.exists_append_append {α : Type u_1} {β : Type u_2} {w w₀ : WList α β} (hw₀ : w₀.IsSublist w) (hw : w.vertex.Nodup) : ∃ (w₁ : WList α β) (w₂ : WList α β), w₁.last = w₀.first ∧ w₀.last = w₂.first ∧ w = w₁ ++ w₀ ++ w₂

theorem WList.IsSublist.exists_isPrefix_isSuffix {α : Type u_1} {β : Type u_2} {w w₀ : WList α β} (hw₀ : w₀.IsSublist w) (hw : w.vertex.Nodup) : ∃ (w' : WList α β), w'.IsPrefix w ∧ w₀.IsSuffix w'

If w₀ is a sublist w and w has no vertex repetitions, then w₀ is a suffix of a prefix of w.

theorem WList.isSublist_iff_isInfix {α : Type u_1} {β : Type u_2} {w w₀ : WList α β} (hnd : w.vertex.Nodup) : w₀ ≤ w ↔ w₀.IsInfix w

theorem WList.exists_sublist_of_mem_mem {α : Type u_1} {β : Type u_2} {x y : α} {w : WList α β} (hx : x ∈ w) (hy : y ∈ w) : ∃ (w₀ : WList α β), w₀.IsSublist w ∧ (x = w₀.first ∧ y = w₀.last ∨ x = w₀.last ∧ y = w₀.first)