@[simp]

theorem List.singleton_isPrefix_iff {α : Type u_1} {x : α} {w : List α} (hw : w ≠ []) : [x] <+: w ↔ w.head hw = x

@[simp]

theorem List.singleton_isSuffix_iff {α : Type u_1} {x : α} {w : List α} (hw : w ≠ []) : [x] <:+ w ↔ w.getLast hw = x

@[simp]

theorem List.concat_suffix_concat {α : Type u_1} {x y : α} {l₁ l₂ : List α} : l₁.concat x <:+ l₂.concat y ↔ x = y ∧ l₁ <:+ l₂

@[simp]

theorem List.tail_eq_self_iff {α : Type u_1} {l : List α} : l.tail = l ↔ l = []

@[simp]

theorem List.dropLast_eq_self_iff {α : Type u_1} {l : List α} : l.dropLast = l ↔ l = []

inductive WList.IsSublist {α : Type u_1} {β : Type u_2} : WList α β → WList α β → Prop

w₁.IsSublist w₂ means that w₁ is a wList using some of the vertices and edges of w₂ in the same order that they appear in w₂. Examples include prefixes, suffixes and wLists obtained from w₂ by shortcuts.

• nil {α : Type u_1} {β : Type u_2} {x : α} {w : WList α β} (h : x ∈ w) : (WList.nil x).IsSublist w
• cons {α : Type u_1} {β : Type u_2} (x : α) (e : β) {w₁ w₂ : WList α β} (h : w₁.IsSublist w₂) : w₁.IsSublist (WList.cons x e w₂)
• cons₂ {α : Type u_1} {β : Type u_2} (x : α) (e : β) {w₁ w₂ : WList α β} (h : w₁.IsSublist w₂) (h_eq : w₁.first = w₂.first) : (WList.cons x e w₁).IsSublist (WList.cons x e w₂)

@[simp]

theorem WList.nil_isSublist_iff {α : Type u_1} {β : Type u_2} {x : α} {w : WList α β} : (nil x).IsSublist w ↔ x ∈ w

@[simp]

theorem WList.isSublist_nil_iff {α : Type u_1} {β : Type u_2} {x : α} {w : WList α β} : w.IsSublist (nil x) ↔ w = nil x

@[simp]

theorem WList.isSublist_refl {α : Type u_1} {β : Type u_2} (w : WList α β) : w.IsSublist w

theorem WList.IsSublist.sublist {α : Type u_1} {β : Type u_2} {w₁ w₂ : WList α β} (h : w₁.IsSublist w₂) : w₁.vertex.Sublist w₂.vertex

theorem WList.IsSublist.subset {α : Type u_1} {β : Type u_2} {w₁ w₂ : WList α β} (h : w₁.IsSublist w₂) : w₁.vertexSet ⊆ w₂.vertexSet

theorem WList.IsSublist.mem {α : Type u_1} {β : Type u_2} {x : α} {w₁ w₂ : WList α β} (h : w₁.IsSublist w₂) (hx : x ∈ w₁) : x ∈ w₂

theorem WList.IsSublist.edge_sublist {α : Type u_1} {β : Type u_2} {w₁ w₂ : WList α β} (h : w₁.IsSublist w₂) : w₁.edge.Sublist w₂.edge

theorem WList.IsSublist.edge_subset {α : Type u_1} {β : Type u_2} {w₁ w₂ : WList α β} (h : w₁.IsSublist w₂) : w₁.edgeSet ⊆ w₂.edgeSet

theorem WList.IsSublist.mem_edge {α : Type u_1} {β : Type u_2} {e : β} {w₁ w₂ : WList α β} (h : w₁.IsSublist w₂) (he : e ∈ w₁.edge) : e ∈ w₂.edge

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

theorem WList.IsSublist.length_le {α : Type u_1} {β : Type u_2} {w₁ w₂ : WList α β} (h : w₁.IsSublist w₂) : w₁.length ≤ w₂.length

theorem WList.IsSublist.eq_of_length_ge {α : Type u_1} {β : Type u_2} {w₁ w₂ : WList α β} (h : w₁.IsSublist w₂) (hge : w₂.length ≤ w₁.length) : w₁ = w₂

theorem WList.IsSublist.length_lt {α : Type u_1} {β : Type u_2} {w₁ w₂ : WList α β} (h : w₁.IsSublist w₂) (hne : w₁ ≠ w₂) : w₁.length < w₂.length

theorem WList.IsSublist.trans {α : Type u_1} {β : Type u_2} {w₁ w₂ w₃ : WList α β} (h : w₁.IsSublist w₂) (h' : w₂.IsSublist w₃) : w₁.IsSublist w₃

theorem WList.IsSublist.antisymm {α : Type u_1} {β : Type u_2} {w₁ w₂ : WList α β} (h : w₁.IsSublist w₂) (h' : w₂.IsSublist w₁) : w₁ = w₂

@[instance_reducible]

instance WList.instPartialOrder {α : Type u_1} {β : Type u_2} : PartialOrder (WList α β)

The sublist order as a partial order on WList α β, for access to order API.

Equations

• WList.instPartialOrder = { le := WList.IsSublist, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯, le_antisymm := ⋯ }

@[simp]

theorem WList.le_iff_isSublist {α : Type u_1} {β : Type u_2} {w₁ w₂ : WList α β} : w₁ ≤ w₂ ↔ w₁.IsSublist w₂

theorem WList.length_monotone {α : Type u_1} {β : Type u_2} : Monotone length

theorem WList.Nil.eq_of_le {α : Type u_1} {β : Type u_2} {w₁ w₂ : WList α β} (h : w₁ ≤ w₂) (hnil : w₂.Nil) : w₁ = w₂

@[simp]

theorem WList.isSublist_cons_self {α : Type u_1} {β : Type u_2} (w : WList α β) (x : α) (e : β) : w.IsSublist (cons x e w)

theorem WList.IsSublist.concat {α : Type u_1} {β : Type u_2} {w₁ w₂ : WList α β} (h : w₁.IsSublist w₂) (e : β) (x : α) : w₁.IsSublist (w₂.concat e x)

theorem WList.IsSublist.concat₂ {α : Type u_1} {β : Type u_2} {w₁ w₂ : WList α β} (h : w₁.IsSublist w₂) (hlast : w₁.last = w₂.last) (e : β) (x : α) : (w₁.concat e x).IsSublist (w₂.concat e x)

@[simp]

theorem WList.isSublist_concat_self {α : Type u_1} {β : Type u_2} (w : WList α β) (e : β) (x : α) : w.IsSublist (w.concat e x)

theorem WList.IsSublist.append_right {α : Type u_1} {β : Type u_2} {w w₁ w₂ : WList α β} (h : w₁.IsSublist w₂) (hw : w₂.last = w.first) : w₁.IsSublist (w₂ ++ w)

theorem WList.IsSublist.append_left {α : Type u_1} {β : Type u_2} {w₁ w₂ : WList α β} (h : w₁.IsSublist w₂) (w : WList α β) : w₁.IsSublist (w ++ w₂)

theorem WList.IsSublist.append_right₂ {α : Type u_1} {β : Type u_2} {w w₁ w₂ : WList α β} (h : w₁.IsSublist w₂) (hlast : w₁.last = w₂.last) (hw : w₂.last = w.first) : (w₁ ++ w).IsSublist (w₂ ++ w)

theorem WList.IsSublist.append_left₂ {α : Type u_1} {β : Type u_2} {w₁ w₂ : WList α β} (h : w₁.IsSublist w₂) (hfirst : w₁.first = w₂.first) (w : WList α β) : (w ++ w₁).IsSublist (w ++ w₂)

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

theorem WList.IsSublist.of_reverse {α : Type u_1} {β : Type u_2} {w₁ w₂ : WList α β} (h : w₁.reverse.IsSublist w₂.reverse) : w₁.IsSublist w₂

theorem WList.DInc.of_isSublist {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {w₁ w₂ : WList α β} (h : w₁.DInc e x y) (hle : w₁.IsSublist w₂) : w₂.DInc e x y

theorem WList.IsLink.of_isSublist {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {w₁ w₂ : WList α β} (h : w₁.IsLink e x y) (hle : w₁.IsSublist w₂) : w₂.IsLink e x y

theorem WList.WellFormed.sublist {α : Type u_1} {β : Type u_2} {w₁ w₂ : WList α β} (h : w₂.WellFormed) (hle : w₁.IsSublist w₂) : w₁.WellFormed

theorem WList.cons_wellFormed_iff {α : Type u_1} {β : Type u_2} {x : α} {e : β} {w : WList α β} : (cons x e w).WellFormed ↔ w.WellFormed ∧ ∀ (y₁ y₂ : α), w.IsLink e y₁ y₂ → s(y₁, y₂) = s(x, w.first)

Prefixes

inductive WList.IsPrefix {α : Type u_1} {β : Type u_2} : WList α β → WList α β → Prop

IsPrefix w₁ w₂ means that w₁ is a prefix of w₂.

• nil {α : Type u_1} {β : Type u_2} (w : WList α β) : (WList.nil w.first).IsPrefix w
• cons {α : Type u_1} {β : Type u_2} (x : α) (e : β) (w₁ w₂ : WList α β) (h : w₁.IsPrefix w₂) : (WList.cons x e w₁).IsPrefix (WList.cons x e w₂)

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

theorem WList.isPrefix_append_right {α : Type u_1} {β : Type u_2} {w₁ w₂ : WList α β} (hw : w₁.last = w₂.first) : w₁.IsPrefix (w₁ ++ w₂)

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

theorem WList.isPrefix_iff_exists_eq_append {α : Type u_1} {β : Type u_2} {w₁ w₂ : WList α β} : w₁.IsPrefix w₂ ↔ ∃ (w₁' : WList α β), w₁.last = w₁'.first ∧ w₁ ++ w₁' = w₂

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

theorem WList.IsPrefix.prefix {α : Type u_1} {β : Type u_2} {w₁ w₂ : WList α β} (h : w₁.IsPrefix w₂) : w₁.vertex <+: w₂.vertex

theorem WList.IsPrefix.mem {α : Type u_1} {β : Type u_2} {x : α} {w₁ w₂ : WList α β} (h : w₁.IsPrefix w₂) (hx : x ∈ w₁) : x ∈ w₂

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

theorem WList.IsPrefix.edge_prefix {α : Type u_1} {β : Type u_2} {w₁ w₂ : WList α β} (h : w₁.IsPrefix w₂) : w₁.edge <+: w₂.edge

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

theorem WList.IsPrefix.mem_edge {α : Type u_1} {β : Type u_2} {e : β} {w₁ w₂ : WList α β} (h : w₁.IsPrefix w₂) (he : e ∈ w₁.edge) : e ∈ w₂.edge

@[simp]

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

@[simp]

theorem WList.isPrefix_nil_iff {α : Type u_1} {β : Type u_2} {x : α} {w : WList α β} : w.IsPrefix (nil x) ↔ w = nil x

@[simp]

theorem WList.nil_isPrefix_iff {α : Type u_1} {β : Type u_2} {x : α} {w : WList α β} : (nil x).IsPrefix w ↔ w.first = x

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

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

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

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

instance WList.instIsPartialOrderIsPrefix {α : Type u_1} {β : Type u_2} : IsPartialOrder (WList α β) IsPrefix

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

@[simp]

theorem WList.isPrefix_concat_self {α : Type u_1} {β : Type u_2} (w : WList α β) (e : β) (x : α) : w.IsPrefix (w.concat e x)

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

theorem WList.IsPrefix.idxOf_eq_of_mem {α : Type u_1} {β : Type u_2} {x : α} {w₁ w₂ : WList α β} [DecidableEq α] (h : w₁.IsPrefix w₂) (hx : x ∈ w₁) : w₁.idxOf x = w₂.idxOf x

theorem WList.IsPrefix.eq_of_last_mem {α : Type u_1} {β : Type u_2} {w₁ w₂ : WList α β} (h : w₁.IsPrefix w₂) (hnd : w₂.vertex.Nodup) (hl : w₂.last ∈ w₁) : w₁ = w₂

inductive WList.IsSuffix {α : Type u_1} {β : Type u_2} : WList α β → WList α β → Prop

• nil {α : Type u_1} {β : Type u_2} (w : WList α β) : (WList.nil w.last).IsSuffix w
• concat {α : Type u_1} {β : Type u_2} (e : β) (x : α) (w₁ w₂ : WList α β) (h : w₁.IsSuffix w₂) : (w₁.concat e x).IsSuffix (w₂.concat e x)

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

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

@[simp]

theorem WList.reverse_isPrefix_reverse_iff {α : Type u_1} {β : Type u_2} {w₁ w₂ : WList α β} : w₁.reverse.IsPrefix w₂.reverse ↔ w₁.IsSuffix w₂

@[simp]

theorem WList.reverse_isSuffix_reverse_iff {α : Type u_1} {β : Type u_2} {w₁ w₂ : WList α β} : w₁.reverse.IsSuffix w₂.reverse ↔ w₁.IsPrefix w₂

@[simp]

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

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

theorem WList.IsSuffix.suffix {α : Type u_1} {β : Type u_2} {w₁ w₂ : WList α β} (h : w₁.IsSuffix w₂) : w₁.vertex <:+ w₂.vertex

theorem WList.IsSuffix.mem {α : Type u_1} {β : Type u_2} {x : α} {w₁ w₂ : WList α β} (h : w₁.IsSuffix w₂) (hx : x ∈ w₁) : x ∈ w₂

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

theorem WList.IsSuffix.edge_suffix {α : Type u_1} {β : Type u_2} {w₁ w₂ : WList α β} (h : w₁.IsSuffix w₂) : w₁.edge <:+ w₂.edge

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

theorem WList.IsSuffix.mem_edge {α : Type u_1} {β : Type u_2} {e : β} {w₁ w₂ : WList α β} (h : w₁.IsSuffix w₂) (he : e ∈ w₁.edge) : e ∈ w₂.edge

@[simp]

theorem WList.isSuffix_nil_iff {α : Type u_1} {β : Type u_2} {x : α} {w : WList α β} : w.IsSuffix (nil x) ↔ w = nil x

@[simp]

theorem WList.nil_isSuffix_iff {α : Type u_1} {β : Type u_2} {x : α} {w : WList α β} : (nil x).IsSuffix w ↔ w.last = x

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

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

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

theorem WList.IsSuffix.eq_of_length_ge {α : Type u_1} {β : Type u_2} {w₁ w₂ : WList α β} (h : w₁.IsSuffix w₂) (hge : w₂.length ≤ w₁.length) : w₁ = w₂

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

instance WList.instIsPartialOrderIsSuffix {α : Type u_1} {β : Type u_2} : IsPartialOrder (WList α β) IsSuffix

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

@[simp]

theorem WList.isSuffix_cons_self {α : Type u_1} {β : Type u_2} (w : WList α β) (e : β) (x : α) : w.IsSuffix (cons x e w)

@[simp]

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

theorem WList.isSuffix_iff_exists_eq_append {α : Type u_1} {β : Type u_2} {w₁ w₂ : WList α β} : w₁.IsSuffix w₂ ↔ ∃ (w' : WList α β), w'.last = w₁.first ∧ w' ++ w₁ = w₂

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

theorem WList.IsSuffix.eq_of_first_mem {α : Type u_1} {β : Type u_2} {w₁ w₂ : WList α β} (h : w₁.IsSuffix w₂) (hnd : w₂.vertex.Nodup) (hl : w₂.first ∈ w₁) : w₁ = w₂

theorem WList.DInc.exists_isSuffix {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {w : WList α β} (h : w.DInc e x y) : ∃ (w' : WList α β), (WList.cons x e w').IsSuffix w ∧ w'.first = y

theorem WList.IsSuffix.nonmepty_of_ne {α : Type u_1} {β : Type u_2} {w₁ w₂ : WList α β} (hsf : w₁.IsSuffix w₂) (hne : w₁ ≠ w₂) : w₂.Nonempty

Infixes

def WList.IsInfix {α : Type u_1} {β : Type u_2} (w₁ w₂ : WList α β) : Prop

IsInfix w₁ w₂ means that w₁ appears as a contiguous sub-wList of w₂. More precisely, w₂ decomposes as wL ++ w₁ ++ wR with the obvious endpoint compatibilities.

Equations

• w₁.IsInfix w₂ = ∃ (wL : WList α β) (wR : WList α β), wL.last = w₁.first ∧ w₁.last = wR.first ∧ wL ++ w₁ ++ wR = w₂

theorem WList.IsInfix.infix {α : Type u_1} {β : Type u_2} {w₁ w₂ : WList α β} (h : w₁.IsInfix w₂) : w₁.vertex <:+: w₂.vertex

@[simp]

theorem WList.IsInfix.refl {α : Type u_1} {β : Type u_2} (w : WList α β) : w.IsInfix w

@[simp]

theorem WList.IsInfix.isSublist {α : Type u_1} {β : Type u_2} {w₁ w₂ : WList α β} (h : w₁.IsInfix w₂) : w₁ ≤ w₂

theorem WList.IsInfix.mem {α : Type u_1} {β : Type u_2} {x : α} {w₁ w₂ : WList α β} (h : w₁.IsInfix w₂) (hx : x ∈ w₁) : x ∈ w₂

theorem WList.IsInfix.subset {α : Type u_1} {β : Type u_2} {w₁ w₂ : WList α β} (h : w₁.IsInfix w₂) : w₁.vertexSet ⊆ w₂.vertexSet

theorem WList.IsInfix.edgeSet_subset {α : Type u_1} {β : Type u_2} {w₁ w₂ : WList α β} (h : w₁.IsInfix w₂) : w₁.edgeSet ⊆ w₂.edgeSet

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

theorem WList.IsInfix.eq_of_length_ge {α : Type u_1} {β : Type u_2} {w₁ w₂ : WList α β} (h : w₁.IsInfix w₂) (hge : w₂.length ≤ w₁.length) : w₁ = w₂

theorem WList.IsInfix.length_lt {α : Type u_1} {β : Type u_2} {w₁ w₂ : WList α β} (h : w₁.IsInfix w₂) (hne : w₁ ≠ w₂) : w₁.length < w₂.length

theorem WList.IsInfix.trans {α : Type u_1} {β : Type u_2} {w₁ w₂ w₃ : WList α β} (h₁ : w₁.IsInfix w₂) (h₂ : w₂.IsInfix w₃) : w₁.IsInfix w₃

theorem WList.IsInfix.antisymm {α : Type u_1} {β : Type u_2} {w₁ w₂ : WList α β} (h : w₁.IsInfix w₂) (h' : w₂.IsInfix w₁) : w₁ = w₂

instance WList.IsInfix.instIsPartialOrder {α : Type u_1} {β : Type u_2} : IsPartialOrder (WList α β) IsInfix

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

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

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

@[simp]

theorem WList.reverse_infix_reverse_iff {α : Type u_1} {β : Type u_2} {w₁ w₂ : WList α β} : w₁.reverse.IsInfix w₂.reverse ↔ w₁.IsInfix w₂

theorem WList.reverse_infix_iff {α : Type u_1} {β : Type u_2} {w₁ w₂ : WList α β} : w₁.reverse.IsInfix w₂ ↔ w₁.IsInfix w₂.reverse

@[simp]

theorem WList.isInfix_nil_iff {α : Type u_1} {β : Type u_2} {x : α} {w : WList α β} : w.IsInfix (nil x) ↔ w = nil x

@[simp]

theorem WList.nil_isInfix_iff {α : Type u_1} {β : Type u_2} {x : α} {w : WList α β} : (nil x).IsInfix w ↔ x ∈ w

theorem WList.isInfix_iff_exists_isSuffix_isPrefix {α : Type u_1} {β : Type u_2} (w₁ w₂ : WList α β) : w₁.IsInfix w₂ ↔ ∃ (w : WList α β), w₁.IsSuffix w ∧ w.IsPrefix w₂

theorem WList.isInfix_iff_exists_isPrefix_isSuffix {α : Type u_1} {β : Type u_2} (w₁ w₂ : WList α β) : w₁.IsInfix w₂ ↔ ∃ (w : WList α β), w₁.IsPrefix w ∧ w.IsSuffix w₂

theorem WList.IsInfix.eq_of_first_eq_last_eq {α : Type u_1} {β : Type u_2} {w₁ w₂ : WList α β} (hnd : w₂.vertex.Nodup) (hf : w₁.first = w₂.first) (hl : w₁.last = w₂.last) (h : w₁.IsInfix w₂) : w₁ = w₂

Decomposed wLists

def WList.appendList {α : Type u_1} {β : Type u_2} [Inhabited α] (L : List (WList α β)) : WList α β

Equations

• L⁺ = List.foldl (fun (x1 x2 : WList α β) => x1 ++ x2) (WList.nil default) L

def WList.«term_⁺» : Lean.TrailingParserDescr

Equations

• WList.«term_⁺» = Lean.ParserDescr.trailingNode `WList.«term_⁺» 1022 0 (Lean.ParserDescr.symbol "⁺")

@[simp]

theorem WList.foldl_append_nil {α : Type u_1} {β : Type u_2} {x : α} [Inhabited α] {L : List (WList α β)} (hne : L ≠ []) : List.foldl (fun (x1 x2 : WList α β) => x1 ++ x2) (nil x) L = L⁺

@[simp]

theorem WList.foldl_append_replicate_nil {α : Type u_1} {β : Type u_2} {x : α} (n : ℕ) : List.foldl (fun (x1 x2 : WList α β) => x1 ++ x2) (nil x) (List.replicate n (nil x)) = nil x

@[simp]

theorem WList.appendList_replicate_nil {α : Type u_1} {β : Type u_2} {x : α} [Inhabited α] {n : ℕ} (hn : n ≠ 0) : List.replicate n (nil x)⁺ = nil x

@[simp]

theorem WList.appendList_nil {α : Type u_1} {β : Type u_2} [Inhabited α] : []⁺ = nil default

@[simp]

theorem WList.appendList_ret {α : Type u_1} {β : Type u_2} [Inhabited α] {l : WList α β} : [l]⁺ = l

@[simp]

theorem WList.appendList_cons {α : Type u_1} {β : Type u_2} [Inhabited α] {l : WList α β} {L : List (WList α β)} (h : l.last = L⁺.first) : (l :: L)⁺ = l ++ L⁺

@[simp]

theorem WList.appendList_nil_cons {α : Type u_1} {β : Type u_2} [Inhabited α] (x : α) {L : List (WList α β)} (hne : L ≠ []) : (nil x :: L)⁺ = L⁺

@[simp]

theorem WList.appendList_concat {α : Type u_1} {β : Type u_2} [Inhabited α] (l : WList α β) (L : List (WList α β)) : L.concat l⁺ = L⁺ ++ l

theorem WList.appendList_append {α : Type u_1} {β : Type u_2} [Inhabited α] {L : List (WList α β)} (L₁ : List (WList α β)) (hne : L ≠ []) : (L₁ ++ L)⁺ = L₁⁺ ++ L⁺

theorem WList.length_appendList_take_succ {α : Type u_1} {β : Type u_2} [Inhabited α] {L : List (WList α β)} {i : ℕ} (hi : i < L.length) : List.take (i + 1) L⁺.length = List.take i L⁺.length + L[i].length

theorem WList.length_appendList_take_mono {α : Type u_1} {β : Type u_2} [Inhabited α] (L : List (WList α β)) : Monotone fun (i : ℕ) => List.take i L⁺.length

theorem WList.length_appendList_take_lt {α : Type u_1} {β : Type u_2} [Inhabited α] {L : List (WList α β)} {i j : ℕ} (hne : ∀ P ∈ L, P.Nonempty) (hij : i < j) (hj : j ≤ L.length) : List.take i L⁺.length < List.take j L⁺.length

@[simp]

theorem WList.appendList_first {α : Type u_1} {β : Type u_2} [Inhabited α] {L : List (WList α β)} (hne : L ≠ []) (h : List.IsChain (fun (x1 x2 : WList α β) => x1.last = x2.first) L) : L⁺.first = (L.head hne).first

@[simp]

theorem WList.appendList_reverse {α : Type u_1} {β : Type u_2} [Inhabited α] {L : List (WList α β)} (h : List.IsChain (fun (x1 x2 : WList α β) => x1.last = x2.first) L) : L⁺.reverse = (List.map reverse L).reverse⁺

@[simp]

theorem WList.appendList_cons_cons {α : Type u_1} {β : Type u_2} [Inhabited α] {l₁ l₂ : WList α β} {L : List (WList α β)} (h : List.IsChain (fun (x1 x2 : WList α β) => x1.last = x2.first) (l₁ :: l₂ :: L)) : (l₁ :: l₂ :: L)⁺ = l₁ ++ (l₂ :: L)⁺

@[simp]

theorem WList.appendList_edge {α : Type u_1} {β : Type u_2} [Inhabited α] (L : List (WList α β)) : L⁺.edge = List.foldl (fun (x1 x2 : List β) => x1 ++ x2) [] (List.map edge L)

structure WList.DecomposeTo {α : Type u_1} {β : Type u_2} [Inhabited α] (w : WList α β) (L : List (WList α β)) : Prop

A decomposed wList is a list of wLists that appends to the original wList and the last vertex of each wList is the first vertex of the next wList.

As there is no 'emtpy' wList, we start the fold with the default value of α. Hence, without the nonempty assumption, wList nil default decompose to the empty list.

• nonempty : L ≠ []
• append : w = L⁺
• chain_eq : List.IsChain (fun (x1 x2 : WList α β) => x1.last = x2.first) L

@[simp]

theorem WList.DecomposeTo.nil_right {α : Type u_1} {β : Type u_2} {w : WList α β} [Inhabited α] : ¬w.DecomposeTo []

@[simp]

theorem WList.DecomposeTo.nil_cons {α : Type u_1} {β : Type u_2} {x : α} {w : WList α β} {L : List (WList α β)} [Inhabited α] (h : w.DecomposeTo (nil x :: L)) (hne : L ≠ []) : w.DecomposeTo L

theorem WList.DecomposeTo.append_cons {α : Type u_1} {β : Type u_2} {w : WList α β} {L : List (WList α β)} {w' : WList α β} [Inhabited α] (h : (w ++ w').DecomposeTo (w :: L)) (hL : L ≠ []) : w'.DecomposeTo L

@[simp]

theorem WList.DecomposeTo.head_first_eq_first {α : Type u_1} {β : Type u_2} [Inhabited α] {w : WList α β} {L : List (WList α β)} (h : w.DecomposeTo L) : (L.head ⋯).first = w.first

@[simp]

theorem WList.DecomposeTo.append_cons_iff {α : Type u_1} {β : Type u_2} {w : WList α β} {L : List (WList α β)} {w' : WList α β} [Inhabited α] (heq : w.last = w'.first) (hL : L ≠ []) : (w ++ w').DecomposeTo (w :: L) ↔ w'.DecomposeTo L

theorem WList.DecomposeTo.head_isPrefix {α : Type u_1} {β : Type u_2} {w : WList α β} {L : List (WList α β)} [Inhabited α] (h : w.DecomposeTo L) : (L.head ⋯).IsPrefix w

theorem WList.DecomposeTo.isSublist_of_mem {α : Type u_1} {β : Type u_2} [Inhabited α] {L : List (WList α β)} {w l : WList α β} (h : w.DecomposeTo L) (hl : l ∈ L) : l.IsSublist w

@[simp]

theorem WList.DecomposeTo.nil_decomposeTo_iff {α : Type u_1} {β : Type u_2} {x : α} {L : List (WList α β)} [Inhabited α] : (nil x).DecomposeTo L ↔ L ≠ [] ∧ ∀ l ∈ L, l = nil x

theorem WList.DecomposeTo.reverse {α : Type u_1} {β : Type u_2} {w : WList α β} {L : List (WList α β)} [Inhabited α] (h : w.DecomposeTo L) : w.reverse.DecomposeTo (List.map WList.reverse L).reverse

theorem WList.DecomposeTo.getLast_isSuffix {α : Type u_1} {β : Type u_2} {w : WList α β} {L : List (WList α β)} [Inhabited α] (h : w.DecomposeTo L) : (L.getLast ⋯).IsSuffix w

theorem WList.DecomposeTo.disjoint_of_edge_nodup {α : Type u_1} {β : Type u_2} [Inhabited α] {w : WList α β} {L : List (WList α β)} (h : w.DecomposeTo L) (hw : w.edge.Nodup) : List.Pairwise (Function.onFun Disjoint WList.edgeSet) L