theorem WList.IsPrefix.tail {α : Type u_1} {β : Type u_2} {w₁ w₂ : WList α β} (h : w₁.IsPrefix w₂) (hne : w₁.Nonempty) : w₁.tail.IsPrefix w₂.tail

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

theorem WList.IsInfix.tail {α : Type u_1} {β : Type u_2} {w₁ w₂ : WList α β} (h : w₁.IsInfix w₂) (hne : w₁.Nonempty) : w₁.tail.IsInfix w₂.tail

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

theorem WList.IsSuffix.dropLast {α : Type u_1} {β : Type u_2} {w₁ w₂ : WList α β} (h : w₁.IsSuffix w₂) (hne : w₁.Nonempty) : w₁.dropLast.IsSuffix w₂.dropLast

theorem WList.IsInfix.dropLast {α : Type u_1} {β : Type u_2} {w₁ w₂ : WList α β} (h : w₁.IsInfix w₂) (hne : w₁.Nonempty) : w₁.dropLast.IsInfix w₂.dropLast

@[simp]

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

@[simp]

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

theorem WList.suffixFromVertex_isSuffix_of_idxOf_le {α : Type u_1} {β : Type u_2} [DecidableEq α] {w : WList α β} {vl uf : α} (hvl : vl ∈ w) (huf : uf ∈ w) (hle : w.idxOf vl ≤ w.idxOf uf) : (w.suffixFromVertex uf).IsSuffix (w.suffixFromVertex vl)

theorem WList.drop_eq_suffixFromVertex_of_idxOf {α : Type u_1} {β : Type u_2} {x : α} {w : WList α β} {n : ℕ} [DecidableEq α] (hx : x ∈ w) (hn : n = w.idxOf x) : w.drop n = w.suffixFromVertex x

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

theorem WList.prefixUntilVertex_concat_of_exists {α : Type u_1} {β : Type u_2} {v x : α} {e : β} {w : WList α β} [DecidableEq α] (h : v ∈ w) : (w.concat e x).prefixUntilVertex v = w.prefixUntilVertex v

theorem WList.suffixFromVertex_concat_of_exists {α : Type u_1} {β : Type u_2} {v x : α} {e : β} [DecidableEq α] (w : WList α β) (hb : v ∈ w) : (w.concat e x).suffixFromVertex v = (w.suffixFromVertex v).concat e x

theorem WList.suffixFromVertex_concat_of_forall {α : Type u_1} {β : Type u_2} {x : α} {e : β} [DecidableEq α] (w : WList α β) (hb : x ∉ w) : (w.concat e x).suffixFromVertex x = nil x

theorem WList.dedup_cons_eq_ite {α : Type u_1} {β : Type u_2} [DecidableEq α] (x : α) (e : β) (w : WList α β) : (cons x e w).dedup = if x ∈ w then (w.suffixFromVertex x).dedup else cons x e w.dedup

theorem WList.dedup_cons_of_mem {α : Type u_1} {β : Type u_2} {x : α} {w : WList α β} [DecidableEq α] (hxw : x ∈ w) (e : β) : (cons x e w).dedup = (w.suffixFromVertex x).dedup

theorem WList.dedup_cons_of_notMem {α : Type u_1} {β : Type u_2} {x : α} {w : WList α β} [DecidableEq α] (hxw : x ∉ w) (e : β) : (cons x e w).dedup = cons x e w.dedup

@[simp]

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

@[simp]

theorem WList.dedup_last {α : Type u_1} {β : Type u_2} [DecidableEq α] (w : WList α β) : w.dedup.last = w.last

theorem WList.dedup_isSublist {α : Type u_1} {β : Type u_2} [DecidableEq α] (w : WList α β) : w.dedup.IsSublist w

theorem WList.dedup_vertex_nodup {α : Type u_1} {β : Type u_2} [DecidableEq α] (w : WList α β) : w.dedup.vertex.Nodup

theorem WList.dedup_eq_self {α : Type u_1} {β : Type u_2} {w : WList α β} [DecidableEq α] (hw : w.vertex.Nodup) : w.dedup = w

theorem WList.dedup_eq_self_iff {α : Type u_1} {β : Type u_2} {w : WList α β} [DecidableEq α] : w.dedup = w ↔ w.vertex.Nodup

theorem WList.dedup_isSublist_deloop {α : Type u_1} {β : Type u_2} [DecidableEq α] (w : WList α β) : w.dedup.IsSublist w.deloop

def WList.cycleBypass {α : Type u_1} {β : Type u_2} [DecidableEq α] : WList α β → WList α β

Bypass repeated vertices while preserving endpoints and nonemptiness. For different endpoints, apply dedup to the entire list. For equal endpoints, retain the first edge and apply dedup to the tail.

Equations

• (WList.nil x_1).cycleBypass = WList.nil x_1
• (WList.cons x_1 e w).cycleBypass = if x_1 = w.last then WList.cons x_1 e w.dedup else (WList.cons x_1 e w).dedup

@[simp]

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

@[simp]

theorem WList.cycleBypass_last {α : Type u_1} {β : Type u_2} [DecidableEq α] (w : WList α β) : w.cycleBypass.last = w.last

theorem WList.cycleBypass_isSublist {α : Type u_1} {β : Type u_2} [DecidableEq α] (w : WList α β) : w.cycleBypass.IsSublist w

theorem WList.cycleBypass_nonempty {α : Type u_1} {β : Type u_2} [DecidableEq α] {w : WList α β} (hw : w.Nonempty) : w.cycleBypass.Nonempty

@[simp]

theorem WList.cycleBypass_nonempty_iff {α : Type u_1} {β : Type u_2} {w : WList α β} [DecidableEq α] : w.cycleBypass.Nonempty ↔ w.Nonempty

theorem WList.cycleBypass_eq_self_iff {α : Type u_1} {β : Type u_2} {w : WList α β} [DecidableEq α] : w.cycleBypass = w ↔ w.vertex.Nodup ∨ w.first = w.last ∧ w.tail.vertex.Nodup

cycleBypass fixes vertex-simple lists and closed lists with vertex-simple tails.

@[simp]

theorem WList.cycleBypass_cycleBypass {α : Type u_1} {β : Type u_2} [DecidableEq α] (w : WList α β) : w.cycleBypass.cycleBypass = w.cycleBypass