inductive WList (α : Type u_3) (β : Type u_4) : Type (max u_3 u_4)

A WList α β is an alternating list [v₀, e₁, v₁, ... , eₙ, vₙ] where the vᵢ have type α and the eᵢ have type β. The first and last terms always have type α.

The definition does not depend on Graph, but the intended use case is where α and β are the vertex and edge types of some G : Graph α β, and the WList is though of as a walk of G. The abstract definition allows us to easily express the idea that a particular list of vertices and edges is a walk in more than one graph.

(Note that a WList α β may not correspond to an actual walk in any Graph α β. For instance, if all eᵢ are equal, and there are at least three different vᵢ, then such a graph would have to have an edge with more than two ends. )

• nil {α : Type u_3} {β : Type u_4} (u : α) : WList α β
• cons {α : Type u_3} {β : Type u_4} (u : α) (e : β) (w : WList α β) : WList α β

def WList.repr_aux {α : Type u_1} {β : Type u_2} [Repr α] [Repr β] (w : WList α β) (n : ℕ) : Std.Format

Equations

• (WList.nil x).repr_aux n = reprPrec x n
• (WList.cons x e w_2).repr_aux n = reprPrec x n ++ Std.Format.text " --" ++ reprPrec e n ++ Std.Format.text "-> " ++ w_2.repr_aux n

@[instance_reducible]

instance WList.instRepr {α : Type u_1} {β : Type u_2} [Repr α] [Repr β] : Repr (WList α β)

Equations

• WList.instRepr = { reprPrec := fun (w : WList α β) (n : ℕ) => Std.Format.text "W[" ++ w.repr_aux n ++ Std.Format.text "]" }

@[simp]

theorem WList.nil_inj_iff {α : Type u_1} {β : Type u_2} {x y : α} : nil x = nil y ↔ x = y

@[simp]

theorem WList.cons_inj_iff {α : Type u_1} {β : Type u_2} {x y : α} {e f : β} {w₁ w₂ : WList α β} : cons x e w₁ = cons y f w₂ ↔ x = y ∧ e = f ∧ w₁ = w₂

First and Last

def WList.first {α : Type u_1} {β : Type u_2} : WList α β → α

The first element of a WList

Equations

• (WList.nil x).first = x
• (WList.cons x e w_1).first = x

@[simp]

theorem WList.nil_first {α : Type u_1} {β : Type u_2} {x : α} : (nil x).first = x

@[simp]

theorem WList.first_cons {α : Type u_1} {β : Type u_2} {x : α} {e : β} {w : WList α β} : (cons x e w).first = x

def WList.second {α : Type u_1} {β : Type u_2} : WList α β → α

Equations

• (WList.nil x).second = x
• (WList.cons x e w_1).second = w_1.first

@[simp]

theorem WList.second_nil {α : Type u_1} {β : Type u_2} {x : α} : (nil x).second = x

@[simp]

theorem WList.second_cons {α : Type u_1} {β : Type u_2} {x : α} {e : β} {w : WList α β} : (cons x e w).second = w.first

@[simp]

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

def WList.last {α : Type u_1} {β : Type u_2} : WList α β → α

Equations

• (WList.nil x).last = x
• (WList.cons x e w_1).last = w_1.last

@[simp]

theorem WList.last_cons {α : Type u_1} {β : Type u_2} {x : α} {e : β} {w : WList α β} : (cons x e w).last = w.last

@[simp]

theorem WList.nil_last {α : Type u_1} {β : Type u_2} {x : α} : (nil x).last = x

Vertex/Edge Lists

def WList.vertex {α : Type u_1} {β : Type u_2} : WList α β → List α

The list of vertices of a WList

Equations

• (WList.nil x).vertex = [x]
• (WList.cons x e w_1).vertex = x :: w_1.vertex

@[simp]

theorem WList.vertex_ne_nil {α : Type u_1} {β : Type u_2} {w : WList α β} : w.vertex ≠ []

@[simp]

theorem WList.cons_vertex {α : Type u_1} {β : Type u_2} {x : α} {e : β} {w : WList α β} : (cons x e w).vertex = x :: w.vertex

@[simp]

theorem WList.nil_vertex {α : Type u_1} {β : Type u_2} {x : α} : (nil x).vertex = [x]

@[simp]

theorem WList.vertex_head {α : Type u_1} {β : Type u_2} {w : WList α β} : w.vertex.head ⋯ = w.first

@[simp]

theorem WList.vertex_getLast {α : Type u_1} {β : Type u_2} {w : WList α β} : w.vertex.getLast ⋯ = w.last

@[simp]

theorem WList.vertex_length_pos {α : Type u_1} {β : Type u_2} (w : WList α β) : 0 < w.vertex.length

@[simp]

theorem WList.vertex_getElem_zero {α : Type u_1} {β : Type u_2} (w : WList α β) : w.vertex[0] = w.first

@[simp]

theorem WList.cons_vertex_dropLast {α : Type u_1} {β : Type u_2} (x : α) (w : WList α β) : (x :: w.vertex).dropLast = x :: w.vertex.dropLast

def WList.edge {α : Type u_1} {β : Type u_2} : WList α β → List β

The list of edges of a WList

Equations

• (WList.nil x).edge = []
• (WList.cons x e w_1).edge = e :: w_1.edge

@[simp]

theorem WList.nil_edge {α : Type u_1} {β : Type u_2} (x : α) : (nil x).edge = []

@[simp]

theorem WList.cons_edge {α : Type u_1} {β : Type u_2} (x : α) (e : β) (w : WList α β) : (cons x e w).edge = e :: w.edge

theorem WList.ext_vertex_edge {α : Type u_1} {β : Type u_2} {w₁ w₂ : WList α β} (h_vertex : w₁.vertex = w₂.vertex) (h_edge : w₁.edge = w₂.edge) : w₁ = w₂

Two WLists with the same vertex and edge lists arae equal.

theorem WList.ext_vertex_edge_iff {α : Type u_1} {β : Type u_2} {w₁ w₂ : WList α β} : w₁ = w₂ ↔ w₁.vertex = w₂.vertex ∧ w₁.edge = w₂.edge

Membership

@[instance_reducible]

instance WList.instMembership {α : Type u_1} {β : Type u_2} : Membership α (WList α β)

Equations

• WList.instMembership = { mem := fun (w : WList α β) (x : α) => x ∈ w.vertex }

@[simp]

theorem WList.mem_vertex {α : Type u_1} {β : Type u_2} {x : α} {w : WList α β} : (x ∈ w.vertex) = (x ∈ w)

@[simp]

theorem WList.mem_nil_iff {α : Type u_1} {β : Type u_2} {u x : α} : x ∈ nil u ↔ x = u

@[simp]

theorem WList.mem_cons_iff {α : Type u_1} {β : Type u_2} {u x : α} {e : β} {w : WList α β} : x ∈ cons u e w ↔ x = u ∨ x ∈ w

theorem WList.eq_or_ne_mem_of_mem_cons {α : Type u_1} {β : Type u_2} {u x : α} {e : β} {w : WList α β} (h : x ∈ cons u e w) : x = u ∨ x ≠ u ∧ x ∈ w

@[instance_reducible]

instance WList.instDecidableMemOfDecidableEq {α : Type u_1} {β : Type u_2} {x : α} {w : WList α β} [DecidableEq α] : Decidable (x ∈ w)

Equations

• WList.instDecidableMemOfDecidableEq = { decide := decide (List.elem x w.vertex = true), reflects_decide := ⋯ }

@[simp]

theorem WList.first_mem {α : Type u_1} {β : Type u_2} {w : WList α β} : w.first ∈ w

@[simp]

theorem WList.second_mem {α : Type u_1} {β : Type u_2} {w : WList α β} : w.second ∈ w

@[simp]

theorem WList.last_mem {α : Type u_1} {β : Type u_2} {w : WList α β} : w.last ∈ w

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

w.UniqueMem x means that x : α appears in w exactly once.

• nil {α : Type u_1} {β : Type u_2} (x : α) : (WList.nil x).UniqueMem x
• cons_eq {α : Type u_1} {β : Type u_2} {x : α} (e : β) (w : WList α β) (h : x ∉ w) : (cons x e w).UniqueMem x
• cons_ne {α : Type u_1} {β : Type u_2} {x u : α} (h : u ≠ x) (e : β) (w : WList α β) (hw : w.UniqueMem x) : (cons u e w).UniqueMem x

Vertex/Edge Sets

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

Equations

• w.vertexSet = {x : α | x ∈ w}

def WList.«termV(_)» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• w.edgeSet = {e : β | e ∈ w.edge}

def WList.«termE(_)» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem WList.mem_vertexSet_iff {α : Type u_1} {β : Type u_2} {x : α} {w : WList α β} : x ∈ w.vertexSet ↔ x ∈ w

@[simp]

theorem WList.mem_edgeSet_iff {α : Type u_1} {β : Type u_2} {e : β} {w : WList α β} : e ∈ w.edgeSet ↔ e ∈ w.edge

@[simp]

theorem WList.nil_vertexSet {α : Type u_1} {β : Type u_2} {x : α} : (nil x).vertexSet = {x}

@[simp]

theorem WList.nil_edgeSet {α : Type u_1} {β : Type u_2} {x : α} : (nil x).edgeSet = ∅

@[simp]

theorem WList.cons_vertexSet {α : Type u_1} {β : Type u_2} {x : α} {e : β} {w : WList α β} : (cons x e w).vertexSet = insert x w.vertexSet

@[simp]

theorem WList.cons_edgeSet {α : Type u_1} {β : Type u_2} {x : α} {e : β} {w : WList α β} : (cons x e w).edgeSet = insert e w.edgeSet

@[simp]

theorem WList.edgeSet_finite {α : Type u_1} {β : Type u_2} (w : WList α β) : w.edgeSet.Finite

@[simp]

theorem WList.vertexSet_nonempty {α : Type u_1} {β : Type u_2} (w : WList α β) : w.vertexSet.Nonempty

@[simp]

theorem WList.vertexSet_finite {α : Type u_1} {β : Type u_2} (w : WList α β) : w.vertexSet.Finite

theorem WList.vertexSet_disjoint_iff {α : Type u_1} {β : Type u_2} {w₁ w₂ : WList α β} : Disjoint w₁.vertexSet w₂.vertexSet ↔ w₁.vertex.Disjoint w₂.vertex

theorem WList.edgeSet_disjoint_iff {α : Type u_1} {β : Type u_2} {w₁ w₂ : WList α β} : Disjoint w₁.edgeSet w₂.edgeSet ↔ w₁.edge.Disjoint w₂.edge

@[simp]

theorem WList.vertex_toFinset_toSet {α : Type u_1} {β : Type u_2} [DecidableEq α] (w : WList α β) : ↑w.vertex.toFinset = w.vertexSet

@[simp]

theorem WList.vertex_disjoint_iff {α : Type u_1} {β : Type u_2} {w₁ w₂ : WList α β} : w₁.vertex.Disjoint w₂.vertex ↔ Disjoint w₁.vertexSet w₂.vertexSet

@[simp]

theorem WList.edge_disjoint_iff {α : Type u_1} {β : Type u_2} {w₁ w₂ : WList α β} : w₁.edge.Disjoint w₂.edge ↔ Disjoint w₁.edgeSet w₂.edgeSet

Emptiness

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

Nil w means that w : WList α β has no edges

• nil {α : Type u_1} {β : Type u_2} (x : α) : (WList.nil x).Nil

@[simp]

theorem WList.nil_nil {α : Type u_1} {β : Type u_2} {x : α} : (nil x).Nil

@[simp]

theorem WList.not_nil_cons {α : Type u_1} {β : Type u_2} (w : WList α β) (x : α) (e : β) : ¬(cons x e w).Nil

theorem WList.Nil.eq_nil_of_mem {α : Type u_1} {β : Type u_2} {x : α} {w : WList α β} (h : w.Nil) (hxw : x ∈ w) : w = WList.nil x

theorem WList.Nil.eq_nil_first {α : Type u_1} {β : Type u_2} {w : WList α β} (h : w.Nil) : w = WList.nil w.first

theorem WList.Nil.eq_nil_last {α : Type u_1} {β : Type u_2} {w : WList α β} (h : w.Nil) : w = WList.nil w.last

theorem WList.Nil.first_eq_last {α : Type u_1} {β : Type u_2} {w : WList α β} (h : w.Nil) : w.first = w.last

theorem WList.nil_iff_eq_nil {α : Type u_1} {β : Type u_2} {w : WList α β} : w.Nil ↔ ∃ (x : α), w = nil x

theorem WList.Nil.exists_eq_nil {α : Type u_1} {β : Type u_2} {w : WList α β} : w.Nil → ∃ (x : α), w = WList.nil x

Alias of the forward direction of WList.nil_iff_eq_nil.

theorem WList.first_eq_last_iff {α : Type u_1} {β : Type u_2} {w : WList α β} (hnodup : w.vertex.Nodup) : w.first = w.last ↔ w.Nil

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

Nonempty w means that w : WList α β has at least one edge

• cons {α : Type u_1} {β : Type u_2} (x : α) (e : β) (w : WList α β) : (WList.cons x e w).Nonempty

@[simp]

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

@[simp]

theorem WList.nil_not_nonempty {α : Type u_1} {β : Type u_2} {x : α} : ¬(nil x).Nonempty

theorem WList.nil_injective {α : Type u_1} {β : Type u_2} : Function.Injective nil

@[simp]

theorem WList.not_nonempty_iff {α : Type u_1} {β : Type u_2} {w : WList α β} : ¬w.Nonempty ↔ w.Nil

theorem WList.Nil.not_nonempty {α : Sort u_1} : IsEmpty α → ¬Nonempty α

Alias of the reverse direction of not_nonempty_iff.

@[simp]

theorem WList.not_nil_iff {α : Type u_1} {β : Type u_2} {w : WList α β} : ¬w.Nil ↔ w.Nonempty

theorem WList.Nonempty.not_nil {α : Type u_1} {β : Type u_2} {w : WList α β} : w.Nonempty → ¬w.Nil

Alias of the reverse direction of WList.not_nil_iff.

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

theorem WList.nonempty_iff_exists_cons {α : Type u_1} {β : Type u_2} {w : WList α β} : w.Nonempty ↔ ∃ (x : α) (e : β) (w' : WList α β), w = cons x e w'

theorem WList.first_ne_last_iff {α : Type u_1} {β : Type u_2} {w : WList α β} (hnodup : w.vertex.Nodup) : w.first ≠ w.last ↔ w.Nonempty

theorem WList.nil_or_nonempty {α : Type u_1} {β : Type u_2} (w : WList α β) : w.Nil ∨ w.Nonempty

theorem WList.exists_eq_nil_or_nonempty {α : Type u_1} {β : Type u_2} (w : WList α β) : (∃ (x : α), w = nil x) ∨ w.Nonempty

@[instance_reducible]

instance WList.DecidableNonempty {α : Type u_1} {β : Type u_2} (w : WList α β) : Decidable w.Nonempty

Equations

• (WList.nil x).DecidableNonempty = ⋯.mpr instDecidableFalse
• (WList.cons x e w_2).DecidableNonempty = ⋯.mpr instDecidableTrue

def WList.Nonempty.firstEdge {α : Type u_1} {β : Type u_2} (w : WList α β) (hw : w.Nonempty) : β

The first edge of a nonempty WList

Equations

• WList.Nonempty.firstEdge (WList.nil x_2) hw = ⋯.elim
• WList.Nonempty.firstEdge (WList.cons x_2 e w) hw = e

@[simp]

theorem WList.Nonempty.firstEdge_cons {α : Type u_1} {β : Type u_2} (x : α) (e : β) (w : WList α β) : firstEdge (WList.cons x e w) ⋯ = e

@[simp]

theorem WList.Nonempty.firstEdge_mem {α : Type u_1} {β : Type u_2} {w : WList α β} (hw : w.Nonempty) : firstEdge w hw ∈ w.edge

theorem WList.Nonempty.edge_ne_nil {α : Type u_1} {β : Type u_2} {w : WList α β} (hw : w.Nonempty) : w.edge ≠ []

@[simp]

theorem WList.edge_ne_nil_iff {α : Type u_1} {β : Type u_2} {w : WList α β} : w.edge ≠ [] ↔ w.Nonempty

theorem WList.Nonempty.firstEdge_eq_head {α : Type u_1} {β : Type u_2} {w : WList α β} (hw : w.Nonempty) : firstEdge w hw = w.edge.head ⋯

@[simp]

theorem WList.Nonempty.edgeSet_nonempty {α : Type u_1} {β : Type u_2} {w : WList α β} (h : w.Nonempty) : w.edgeSet.Nonempty

theorem WList.nonempty_iff_exists_edge {α : Type u_1} {β : Type u_2} {w : WList α β} : w.Nonempty ↔ ∃ (e : β), e ∈ w.edge

theorem WList.Nonempty.exists_edge {α : Type u_1} {β : Type u_2} {w : WList α β} : w.Nonempty → ∃ (e : β), e ∈ w.edge

Alias of the forward direction of WList.nonempty_iff_exists_edge.

theorem WList.nil_iff_edge_nil {α : Type u_1} {β : Type u_2} {w : WList α β} : w.Nil ↔ w.edge = []

theorem WList.Nonempty.first_ne_last_of_nodup {α : Type u_1} {β : Type u_2} {w : WList α β} (hne : w.Nonempty) (hv : w.vertex.Nodup) : w.first ≠ w.last

theorem WList.induction_nonempty {α : Type u_1} {β : Type u_2} {motive : (w : WList α β) → w.Nonempty → Prop} (edge : ∀ (u v : α) (e : β), motive (cons u e (nil v)) ⋯) (cons : ∀ (u : α) (e : β) (w : WList α β) (hw : w.Nonempty), motive w hw → motive (cons u e w) ⋯) {w : WList α β} (hw : w.Nonempty) : motive w hw

Nontriviality

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

a WList is nontrivial if it has at least two edges.

• cons_cons {α : Type u_1} {β : Type u_2} (u : α) (e : β) (v : α) (f : β) (w : WList α β) : (cons u e (cons v f w)).Nontrivial

theorem WList.Nontrivial.nonempty {α : Type u_1} {β : Type u_2} {w : WList α β} (hw : w.Nontrivial) : w.Nonempty

@[simp]

theorem WList.not_nontrivial_nil {α : Type u_1} {β : Type u_2} {x : α} : ¬(nil x).Nontrivial

@[simp]

theorem WList.not_nontrivial_cons_nil {α : Type u_1} {β : Type u_2} {x y : α} {e : β} : ¬(cons x e (nil y)).Nontrivial

@[simp]

theorem WList.cons_nontrivial_iff {α : Type u_1} {β : Type u_2} {u : α} {e : β} {w : WList α β} : (cons u e w).Nontrivial ↔ w.Nonempty

theorem WList.Nontrivial.first_ne_second_of_nodup {α : Type u_1} {β : Type u_2} {w : WList α β} (hnt : w.Nontrivial) (hv : w.vertex.Nodup) : w.first ≠ w.second

theorem WList.Nontrivial.second_ne_last_of_nodup {α : Type u_1} {β : Type u_2} {w : WList α β} (hnt : w.Nontrivial) (hv : w.vertex.Nodup) : w.second ≠ w.last

@[instance_reducible]

instance WList.instDecidableNontrivial {α : Type u_1} {β : Type u_2} {w : WList α β} : Decidable w.Nontrivial

Equations

• WList.instDecidableNontrivial = ⋯.mpr inferInstance
• WList.instDecidableNontrivial = ⋯.mpr inferInstance

Length

def WList.length {α : Type u_1} {β : Type u_2} : WList α β → ℕ

The number of edges in a WList. Change this to length w.edge ??

Equations

• (WList.nil x).length = 0
• (WList.cons x e w_1).length = w_1.length + 1

@[simp]

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

@[simp]

theorem WList.length_vertex {α : Type u_1} {β : Type u_2} (w : WList α β) : w.vertex.length = w.length + 1

@[simp]

theorem WList.cons_length {α : Type u_1} {β : Type u_2} {x : α} {e : β} {w : WList α β} : (cons x e w).length = w.length + 1

@[simp]

theorem WList.nil_length {α : Type u_1} {β : Type u_2} {x : α} : (nil x).length = 0

@[simp]

theorem WList.length_eq_zero {α : Type u_1} {β : Type u_2} {w : WList α β} : w.length = 0 ↔ w.Nil

theorem WList.length_ne_zero_iff {α : Type u_1} {β : Type u_2} {w : WList α β} : w.length ≠ 0 ↔ w.Nonempty

@[simp]

theorem WList.length_pos_iff {α : Type u_1} {β : Type u_2} {w : WList α β} : 0 < w.length ↔ w.Nonempty

@[simp]

theorem WList.one_le_length_iff {α : Type u_1} {β : Type u_2} {w : WList α β} : 1 ≤ w.length ↔ w.Nonempty

theorem WList.Nonempty.length_pos {α : Type u_1} {β : Type u_2} {w : WList α β} (hw : w.Nonempty) : 0 < w.length

theorem WList.encard_vxSet_of_nodup {α : Type u_1} {β : Type u_2} {w : WList α β} (h : w.vertex.Nodup) : w.vertexSet.encard = ↑w.length + 1

@[simp]

theorem WList.one_lt_length_iff {α : Type u_1} {β : Type u_2} {w : WList α β} : 1 < w.length ↔ w.Nontrivial

@[simp]

theorem WList.two_le_length_iff {α : Type u_1} {β : Type u_2} {w : WList α β} : 2 ≤ w.length ↔ w.Nontrivial

theorem WList.Nontrivial.one_lt_length {α : Type u_1} {β : Type u_2} {w : WList α β} (hw : w.Nontrivial) : 1 < w.length

theorem WList.Nontrivial.two_le_length {α : Type u_1} {β : Type u_2} {w : WList α β} (hw : w.Nontrivial) : 2 ≤ w.length

theorem WList.Nonempty.nontrivial_of_length_ne_one {α : Type u_1} {β : Type u_2} {w : WList α β} (hw : w.Nonempty) (hne : w.length ≠ 1) : w.Nontrivial

theorem WList.length_eq_one_iff {α : Type u_1} {β : Type u_2} {w : WList α β} : w.length = 1 ↔ ∃ (u : α) (e : β) (v : α), w = cons u e (nil v)

theorem WList.length_eq_two_iff {α : Type u_1} {β : Type u_2} {w : WList α β} : w.length = 2 ↔ ∃ (a : α) (e : β) (b : α) (f : β) (c : α), w = cons a e (cons b f (nil c))

theorem WList.vertex_toFinset_card_le {α : Type u_1} {β : Type u_2} [DecidableEq α] (w : WList α β) : w.vertex.toFinset.card ≤ w.length + 1

theorem WList.edge_toFinset_card_le {α : Type u_1} {β : Type u_2} [DecidableEq β] (w : WList α β) : w.edge.toFinset.card ≤ w.length

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

w.DInc e x y means that w contains [x,e,y] as a contiguous sublist. (DInc stands for 'directed incidence')`

• cons_left {α : Type u_1} {β : Type u_2} (x : α) (e : β) (w : WList α β) : (WList.cons x e w).DInc e x w.first
• cons {α : Type u_1} {β : Type u_2} (u : α) (f : β) {w : WList α β} {e : β} {x y : α} (hw : w.DInc e x y) : (WList.cons u f w).DInc e x y

@[simp]

theorem WList.not_nil_dInc {α : Type u_1} {β : Type u_2} (u : α) (e : β) (x y : α) : ¬(nil u).DInc e x y

@[simp]

theorem WList.dInc_cons_iff {α : Type u_1} {β : Type u_2} {u x y : α} {e f : β} {w : WList α β} : (cons u f w).DInc e x y ↔ u = x ∧ f = e ∧ w.first = y ∨ w.DInc e x y

theorem WList.DInc.left_mem {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {w : WList α β} (h : w.DInc e x y) : x ∈ w.vertex

theorem WList.DInc.right_mem {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {w : WList α β} (h : w.DInc e x y) : y ∈ w.vertex

theorem WList.DInc.right_mem_vertex_tail {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {w : WList α β} (h : w.DInc e x y) : y ∈ w.vertex.tail

theorem WList.DInc.edge_mem {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {w : WList α β} (h : w.DInc e x y) : e ∈ w.edge

def WList.dIncFirst {α : Type u_1} {β : Type u_2} {e : β} [DecidableEq β] (w : WList α β) (he : e ∈ w.edge) : α × α

Equations

• (WList.nil u).dIncFirst he_2 = (u, u)
• (WList.cons u f w_2).dIncFirst he_2 = if hef : e = f then (u, w_2.first) else w_2.dIncFirst ⋯

theorem WList.dIncFirst_dInc {α : Type u_1} {β : Type u_2} {e : β} [DecidableEq β] (w : WList α β) (he : e ∈ w.edge) : w.DInc e (w.dIncFirst he).1 (w.dIncFirst he).2

theorem WList.exists_dInc_of_mem_edge {α : Type u_1} {β : Type u_2} {e : β} {w : WList α β} (he : e ∈ w.edge) : ∃ (x : α) (y : α), w.DInc e x y

theorem WList.mem_edge_iff_exists_dInc {α : Type u_1} {β : Type u_2} {e : β} {w : WList α β} : e ∈ w.edge ↔ ∃ (x : α) (y : α), w.DInc e x y

theorem WList.DInc.sublist {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {w : WList α β} (h : w.DInc e x y) : [x, y].Sublist w.vertex

theorem WList.DInc.ne_first {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {w : WList α β} (h : w.DInc e x y) (hnd : w.vertex.Nodup) : y ≠ w.first

theorem WList.DInc.ne_last {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {w : WList α β} (h : w.DInc e x y) (hnd : w.vertex.Nodup) : x ≠ w.last

theorem WList.DInc.nonempty {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {w : WList α β} (h : w.DInc e x y) : w.Nonempty

theorem WList.dInc_iff_eq_of_dInc_of_edge_nodup {α : Type u_1} {β : Type u_2} {u v x y : α} {e : β} {w : WList α β} (hw : w.edge.Nodup) (he : w.DInc e u v) : w.DInc e x y ↔ x = u ∧ y = v

theorem WList.dInc_iff_eq_of_dInc_of_vertex_nodup_left {α : Type u_1} {β : Type u_2} {u v y : α} {e f : β} {w : WList α β} (hw : w.vertex.Nodup) (hu : w.DInc e u v) : w.DInc f u y ↔ f = e ∧ y = v

theorem WList.exists_left_edge {α : Type u_1} {β : Type u_2} {y : α} {w : WList α β} (hyw : y ∈ w) (hy : y ≠ w.first) : ∃ (e : β) (x : α), w.DInc e x y

theorem WList.exists_right_edge {α : Type u_1} {β : Type u_2} {x : α} {w : WList α β} (hxw : x ∈ w) (hx : x ≠ w.last) : ∃ (e : β) (y : α), w.DInc e x y

@[instance_reducible]

instance WList.instDecidableDIncOfDecidableEq {α : Type u_1} {β : Type u_2} {w : WList α β} {e : β} {x y : α} [DecidableEq α] [DecidableEq β] : Decidable (w.DInc e x y)

Equations

• WList.instDecidableDIncOfDecidableEq = ⋯.mpr inferInstance
• WList.instDecidableDIncOfDecidableEq = ⋯.mpr (have this := WList.instDecidableDIncOfDecidableEq; inferInstance)

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

w.IsLink e x y means that w contains [x,e,y] or [y,e,x] as a contiguous sublist.

• cons_left {α : Type u_1} {β : Type u_2} (x : α) (e : β) (w : WList α β) : (WList.cons x e w).IsLink e x w.first
• cons_right {α : Type u_1} {β : Type u_2} (x : α) (e : β) (w : WList α β) : (WList.cons x e w).IsLink e w.first x
• cons {α : Type u_1} {β : Type u_2} (u : α) (f : β) {w : WList α β} {e : β} {x y : α} (hw : w.IsLink e x y) : (WList.cons u f w).IsLink e x y

@[simp]

theorem WList.IsLink.not_nil {α : Type u_1} {β : Type u_2} {u x y : α} {e : β} : ¬(nil u).IsLink e x y

theorem WList.DInc.isLink {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {w : WList α β} (h : w.DInc e x y) : w.IsLink e x y

theorem WList.IsLink.symm {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {w : WList α β} (h : w.IsLink e x y) : w.IsLink e y x

theorem WList.isLink_iff_dInc {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {w : WList α β} : w.IsLink e x y ↔ w.DInc e x y ∨ w.DInc e y x

theorem WList.IsLink.of_cons {α : Type u_1} {β : Type u_2} {u x y : α} {e f : β} {w : WList α β} (hw : (WList.cons u f w).IsLink e x y) (hef : e ≠ f) : w.IsLink e x y

theorem WList.isLink_cons_iff' {α : Type u_1} {β : Type u_2} {u x y : α} {e f : β} {w : WList α β} : (cons u f w).IsLink e x y ↔ f = e ∧ (x = u ∧ y = w.first ∨ x = w.first ∧ y = u) ∨ w.IsLink e x y

theorem WList.isLink_cons_iff {α : Type u_1} {β : Type u_2} {u x y : α} {e f : β} {w : WList α β} : (cons u f w).IsLink e x y ↔ f = e ∧ s(x, y) = s(u, w.first) ∨ w.IsLink e x y

theorem WList.IsLink.left_mem {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {w : WList α β} (h : w.IsLink e x y) : x ∈ w

theorem WList.IsLink.right_mem {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {w : WList α β} (h : w.IsLink e x y) : y ∈ w

theorem WList.IsLink.edge_mem {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {w : WList α β} (h : w.IsLink e x y) : e ∈ w.edge

theorem WList.IsLink.nonempty {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {w : WList α β} (h : w.IsLink e x y) : w.Nonempty

theorem WList.exists_isLink_of_mem_edge {α : Type u_1} {β : Type u_2} {e : β} {w : WList α β} (he : e ∈ w.edge) : ∃ (x : α) (y : α), w.IsLink e x y

theorem WList.IsLink.eq_firstEdge_of_isLink_first {α : Type u_1} {β : Type u_2} {x : α} {e : β} {w : WList α β} (he : w.IsLink e w.first x) (hnd : w.vertex.Nodup) : e = Nonempty.firstEdge w ⋯

theorem WList.Nonempty.mem_iff_exists_isLink {α : Type u_1} {β : Type u_2} {x : α} {w : WList α β} (hw : w.Nonempty) : x ∈ w ↔ ∃ (y : α) (e : β), w.IsLink e x y

@[instance_reducible]

instance WList.instDecidableIsLinkOfDecidableEq {α : Type u_1} {β : Type u_2} {w : WList α β} {e : β} {x y : α} [DecidableEq α] [DecidableEq β] : Decidable (w.IsLink e x y)

Equations

• WList.instDecidableIsLinkOfDecidableEq = ⋯.mpr inferInstance
• WList.instDecidableIsLinkOfDecidableEq = ⋯.mpr (have this := WList.instDecidableIsLinkOfDecidableEq; inferInstance)

def WList.Inc {α : Type u_1} {β : Type u_2} (w : WList α β) (e : β) (x : α) : Prop

WList.Inc is here for parity with Graph.Inc.

Equations

• w.Inc e x = ∃ (y : α), w.IsLink e x y

noncomputable def WList.Inc.other {α : Type u_1} {β : Type u_2} {x : α} {e : β} {w : WList α β} (h : w.Inc e x) : α

Equations

• h.other = Exists.choose h

@[simp]

theorem WList.Inc.nonempty {α : Type u_1} {β : Type u_2} {x : α} {e : β} {w : WList α β} (h : w.Inc e x) : w.Nonempty

@[simp]

theorem WList.Inc.not_nil {α : Type u_1} {β : Type u_2} {u x : α} {e : β} : ¬(nil u).Inc e x

@[simp]

theorem WList.Inc.edge_mem {α : Type u_1} {β : Type u_2} {x : α} {e : β} {w : WList α β} (h : w.Inc e x) : e ∈ w.edge

@[simp]

theorem WList.Inc.vertex_mem {α : Type u_1} {β : Type u_2} {x : α} {e : β} {w : WList α β} (h : w.Inc e x) : x ∈ w

@[simp]

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

@[simp]

theorem WList.inc_cons_right {α : Type u_1} {β : Type u_2} (x : α) (e : β) (w : WList α β) : (cons x e w).Inc e w.first

@[simp]

theorem WList.Inc.cons {α : Type u_1} {β : Type u_2} (u : α) (f : β) {w : WList α β} {e : β} {x : α} (hw : w.Inc e x) : (cons u f w).Inc e x

theorem WList.Inc.of_cons {α : Type u_1} {β : Type u_2} {u x : α} {e f : β} {w : WList α β} (hw : (cons u f w).Inc e x) (hef : e ≠ f) : w.Inc e x

@[simp]

theorem WList.inc_cons_iff {α : Type u_1} {β : Type u_2} {u x : α} {e f : β} {w : WList α β} : (cons u f w).Inc e x ↔ f = e ∧ (x = u ∨ x = w.first) ∨ w.Inc e x

@[simp]

theorem WList.IsLink.inc_left {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {w : WList α β} (h : w.IsLink e x y) : w.Inc e x

@[simp]

theorem WList.IsLink.inc_right {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {w : WList α β} (h : w.IsLink e x y) : w.Inc e y

@[simp]

theorem WList.DInc.inc_left {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {w : WList α β} (h : w.DInc e x y) : w.Inc e x

@[simp]

theorem WList.DInc.inc_right {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {w : WList α β} (h : w.DInc e x y) : w.Inc e y

def WList.WellFormed {α : Type u_1} {β : Type u_2} (w : WList α β) : Prop

A WList is WellFormed if each edge appears only with the same ends.

Equations

• w.WellFormed = ∀ ⦃e : β⦄ ⦃x₁ x₂ y₁ y₂ : α⦄, w.IsLink e x₁ x₂ → w.IsLink e y₁ y₂ → s(x₁, x₂) = s(y₁, y₂)

@[simp]

theorem WList.nil_wellFormed {α : Type u_1} {β : Type u_2} {x : α} : (nil x).WellFormed

theorem WList.WellFormed.of_cons {α : Type u_1} {β : Type u_2} {u : α} {f : β} {w : WList α β} (hw : (cons u f w).WellFormed) : w.WellFormed

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

theorem WList.wellFormed_of_nodup {α : Type u_1} {β : Type u_2} {w : WList α β} (hw : w.edge.Nodup) : w.WellFormed

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

The set of ends of e in w

Equations

• w.endsOf e = {x : α | ∃ (y : α), w.IsLink e x y}

Indices

def WList.get {α : Type u_1} {β : Type u_2} : WList α β → ℕ → α

The nth vertex of w, or the last vertex if n > w.length.

Equations

• (WList.nil x_2).get x✝ = x_2
• (WList.cons x_2 e w).get 0 = x_2
• (WList.cons u e w).get n.succ = w.get n

@[simp]

theorem WList.get_nil {α : Type u_1} {β : Type u_2} (x : α) (n : ℕ) : (nil x).get n = x

@[simp]

theorem WList.get_zero {α : Type u_1} {β : Type u_2} (w : WList α β) : w.get 0 = w.first

@[simp]

theorem WList.get_cons_add {α : Type u_1} {β : Type u_2} (x : α) (e : β) (w : WList α β) (n : ℕ) : (cons x e w).get (n + 1) = w.get n

@[simp]

theorem WList.get_length {α : Type u_1} {β : Type u_2} (w : WList α β) : w.get w.length = w.last

@[simp]

theorem WList.get_mem {α : Type u_1} {β : Type u_2} (w : WList α β) (n : ℕ) : w.get n ∈ w

theorem WList.get_of_length_le {α : Type u_1} {β : Type u_2} {w : WList α β} {n : ℕ} (hn : w.length ≤ n) : w.get n = w.last

theorem WList.get_eq_getD_vertex {α : Type u_1} {β : Type u_2} (w : WList α β) (n : ℕ) : w.get n = w.vertex.getD n w.last

theorem WList.get_eq_getElem_vertex {α : Type u_1} {β : Type u_2} (w : WList α β) {n : ℕ} (hn : n ≤ w.length) : w.get n = w.vertex[n]

theorem WList.DInc_get_get_succ {α : Type u_1} {β : Type u_2} {w : WList α β} {n : ℕ} (hn : n < w.length) : have hw := ⋯; w.DInc w.edge[n] (w.get n) (w.get (n + 1))

theorem WList.exists_dInc_get_get_succ {α : Type u_1} {β : Type u_2} {w : WList α β} {n : ℕ} (hn : n < w.length) : ∃ (e : β), w.DInc e (w.get n) (w.get (n + 1))

theorem WList.dinc_iff_get {α : Type u_1} {β : Type u_2} {w : WList α β} {e : β} {x y : α} : w.DInc e x y ↔ ∃ (i : ℕ) (hi : i < w.length), w.get i = x ∧ w.get (i + 1) = y ∧ w.edge[i] = e

theorem WList.isLink_iff_get {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {w : WList α β} : w.IsLink e x y ↔ ∃ (i : ℕ) (hi : i < w.length), w.edge[i] = e ∧ s(w.get i, w.get (i + 1)) = s(x, y)

theorem WList.isLink_iff_vertex_get {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {w : WList α β} : w.IsLink e x y ↔ ∃ (i : ℕ) (hi : i < w.length), w.edge[i] = e ∧ s(w.vertex[i], w.vertex[i + 1]) = s(x, y)

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

The index of a vertex in a WList. Equal to w.length + 1 if the vertex doesn't appear.

Equations

• (WList.nil u).idxOf x✝ = if u = x✝ then 0 else 1
• (WList.cons u e w).idxOf x✝ = if u = x✝ then 0 else w.idxOf x✝ + 1

@[simp]

theorem WList.idxOf_nil {α : Type u_1} {β : Type u_2} [DecidableEq α] (u x : α) : (nil u).idxOf x = if u = x then 0 else 1

theorem WList.idxOf_cons {α : Type u_1} {β : Type u_2} {x : α} [DecidableEq α] (u : α) (e : β) (w : WList α β) : (cons u e w).idxOf x = if u = x then 0 else w.idxOf x + 1

@[simp]

theorem WList.idxOf_cons_self {α : Type u_1} {β : Type u_2} [DecidableEq α] (u : α) (e : β) (w : WList α β) : (cons u e w).idxOf u = 0

@[simp]

theorem WList.idxOf_cons_eq_zero {α : Type u_1} {β : Type u_2} {u x : α} {e : β} [DecidableEq α] (w : WList α β) : (cons u e w).idxOf x = 0 ↔ u = x

@[simp]

theorem WList.idxOf_cons_ne {α : Type u_1} {β : Type u_2} {u x : α} [DecidableEq α] (hne : u ≠ x) (e : β) (w : WList α β) : (cons u e w).idxOf x = w.idxOf x + 1

theorem WList.idxOf_notMem {α : Type u_1} {β : Type u_2} {x : α} {w : WList α β} [DecidableEq α] (hx : x ∉ w) : w.idxOf x = w.length + 1

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

@[simp]

theorem WList.idxOf_le_length_iff_mem {α : Type u_1} {β : Type u_2} {x : α} {w : WList α β} [DecidableEq α] : w.idxOf x ≤ w.length ↔ x ∈ w

@[simp]

theorem WList.idxOf_first {α : Type u_1} {β : Type u_2} [DecidableEq α] (w : WList α β) : w.idxOf w.first = 0

theorem WList.idxOf_eq_idxOf_vertex {α : Type u_1} {β : Type u_2} [DecidableEq α] (w : WList α β) (x : α) : w.idxOf x = List.idxOf x w.vertex

theorem WList.get_idxOf {α : Type u_1} {β : Type u_2} {x : α} [DecidableEq α] (w : WList α β) (hxw : x ∈ w) : w.get (w.idxOf x) = x

theorem WList.idxOf_get {α : Type u_1} {β : Type u_2} {w : WList α β} [DecidableEq α] (hw : w.vertex.Nodup) {n : ℕ} (hn : n ≤ w.length) : w.idxOf (w.get n) = n

theorem WList.idxOf_last {α : Type u_1} {β : Type u_2} [DecidableEq α] (w : WList α β) (hw : w.vertex.Nodup) : w.idxOf w.last = w.length

@[simp]

theorem WList.range_get {α : Type u_1} {β : Type u_2} [DecidableEq α] (w : WList α β) : Set.range w.get = w.vertexSet

theorem WList.idxOf_inj_of_left_mem {α : Type u_1} {β : Type u_2} {x y : α} {w : WList α β} [DecidableEq α] (hx : x ∈ w) (heq : w.idxOf x = w.idxOf y) : x = y

theorem WList.idxOf_inj_of_right_mem {α : Type u_1} {β : Type u_2} {x y : α} {w : WList α β} [DecidableEq α] (hy : y ∈ w) (heq : w.idxOf x = w.idxOf y) : x = y

theorem WList.idxOf_inj {α : Type u_1} {β : Type u_2} {x y : α} {w : WList α β} [DecidableEq α] (hmem : x ∈ w ∨ y ∈ w) : w.idxOf x = w.idxOf y ↔ x = y

@[simp]

theorem WList.idxOf_le {α : Type u_1} {β : Type u_2} [DecidableEq α] (w : WList α β) (x : α) : w.idxOf x ≤ w.length + 1

@[simp]

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

@[simp]

theorem WList.idxOf_get_le {α : Type u_1} {β : Type u_2} [DecidableEq α] (w : WList α β) (n : ℕ) : w.idxOf (w.get n) ≤ n

theorem WList.get_ne_of_lt_idxOf {α : Type u_1} {β : Type u_2} {x : α} {w : WList α β} [DecidableEq α] {n : ℕ} (hlt : n < w.idxOf x) : w.get n ≠ x

@[simp]

theorem WList.idxOf_eq_zero_iff {α : Type u_1} {β : Type u_2} {x : α} {w : WList α β} [DecidableEq α] : w.idxOf x = 0 ↔ x = w.first

theorem WList.idxOf_cons_eq_one_iff {α : Type u_1} {β : Type u_2} {u x : α} {e : β} {w : WList α β} [DecidableEq α] : (cons u e w).idxOf x = 1 ↔ u ≠ x ∧ x = w.first

@[simp]

theorem WList.idxOf_eq_succ_length_iff {α : Type u_1} {β : Type u_2} {x : α} {w : WList α β} [DecidableEq α] : w.idxOf x = w.length + 1 ↔ x ∉ w

theorem WList.idxOf_eq_length {α : Type u_1} {β : Type u_2} {x : α} {w : WList α β} [DecidableEq α] (h : w.idxOf x = w.length) : x = w.last

@[simp]

theorem WList.idxOf_eq_length_iff {α : Type u_1} {β : Type u_2} {x : α} {w : WList α β} [DecidableEq α] (h : w.vertex.Nodup) : w.idxOf x = w.length ↔ x = w.last

def WList.zip {α : Type u_1} {β : Type u_2} (a : List α) (b : List β) (hab : b.length + 1 = a.length := by simp) : WList α β

Build a WList from given lists of edges and vertices of appropriate lengths

Equations

• WList.zip [] x x_1 = ⋯.elim
• WList.zip (x_3 :: a) [] h = WList.nil x_3
• WList.zip (x_3 :: a) (e :: b) h = WList.cons x_3 e (WList.zip a b ⋯)

@[simp]

theorem WList.zip_nil {α : Type u_1} {β : Type u_2} (a : List α) {hab : [].length + 1 = a.length} : WList.zip a [] hab = nil (a.head ⋯)

@[simp]

theorem WList.zip_cons_cons {α : Type u_1} {β : Type u_2} (a : List α) (b : List β) (x : α) (e : β) {hab : (e :: b).length + 1 = (x :: a).length} : WList.zip (x :: a) (e :: b) hab = cons x e (WList.zip a b ⋯)

@[simp]

theorem WList.zip_vertex {α : Type u_1} {β : Type u_2} (a : List α) (b : List β) (h : b.length + 1 = a.length) : (WList.zip a b h).vertex = a

@[simp]

theorem WList.zip_edge {α : Type u_1} {β : Type u_2} (a : List α) (b : List β) (h : b.length + 1 = a.length) : (WList.zip a b h).edge = b

@[simp]

theorem WList.eq_zip {α : Type u_1} {β : Type u_2} (w : WList α β) : WList.zip w.vertex w.edge ⋯ = w

@[simp]

theorem WList.zip_length {α : Type u_1} {β : Type u_2} (a : List α) (b : List β) (h : b.length + 1 = a.length) : (WList.zip a b h).length = b.length

@[simp]

theorem WList.mem_zip {α : Type u_1} {β : Type u_2} {a : List α} {b : List β} (h : b.length + 1 = a.length) {x : α} : x ∈ WList.zip a b h ↔ x ∈ a

@[simp]

theorem WList.zip_vertexSet {α : Type u_1} {β : Type u_2} (a : List α) (b : List β) (h : b.length + 1 = a.length) : (WList.zip a b h).vertexSet = {x : α | x ∈ a}

@[simp]

theorem WList.zip_edgeSet {α : Type u_1} {β : Type u_2} (a : List α) (b : List β) (h : b.length + 1 = a.length) : (WList.zip a b h).edgeSet = {e : β | e ∈ b}

@[simp]

theorem WList.zip_first {α : Type u_1} {β : Type u_2} (a : List α) (b : List β) (h : b.length + 1 = a.length) : (WList.zip a b h).first = a.head ⋯

@[simp]

theorem WList.zip_last {α : Type u_1} {β : Type u_2} (a : List α) (b : List β) (h : b.length + 1 = a.length) : (WList.zip a b h).last = a.getLast ⋯

@[simp]

theorem WList.zip_nonempty_iff {α : Type u_1} {β : Type u_2} (a : List α) (b : List β) (h : b.length + 1 = a.length) : (WList.zip a b h).Nonempty ↔ b ≠ []

theorem WList.zip_get_eq_getD {α : Type u_1} {β : Type u_2} (a : List α) (b : List β) (h : b.length + 1 = a.length) (i : ℕ) : (WList.zip a b h).get i = a.getD i (a.getLast ⋯)

theorem WList.zip_dInc_iff {α : Type u_1} {β : Type u_2} {x y : α} {e : β} (a : List α) (b : List β) (h : b.length + 1 = a.length) : (WList.zip a b h).DInc e x y ↔ ∃ (i : ℕ) (hi : i + 1 < a.length), e = b[i] ∧ x = a[i] ∧ y = a[i + 1]

theorem WList.zip_isLink_iff {α : Type u_1} {β : Type u_2} {x y : α} {e : β} (a : List α) (b : List β) (h : b.length + 1 = a.length) : (WList.zip a b h).IsLink e x y ↔ ∃ (i : ℕ) (hi : i + 1 < a.length), e = b[i] ∧ s(x, y) = s(a[i], a[i + 1])