Vertex addresses in depth-first order

The root address is []. Each child contributes its vertex addresses prefixed by its zero-based child index. Thus equal child subtrees still contribute distinct vertex occurrences.

The depth of an address is its list length. For valid vertices, prefix ancestry includes equality; strict ancestry uses a proper prefix. The parent of a nonempty vertex address is obtained with List.dropLast.

def BGW.PlaneTree.vertices : PlaneTree → List (List ℕ)

All vertex addresses, listed in root-first depth-first order.

Equations

• BGW.PlaneTree.vertices = BGW.PlaneTree.fold fun (vs : List (List (List ℕ))) => [] :: (List.mapIdx (fun (i : ℕ) (v : List (List ℕ)) => List.map (fun (u : List ℕ) => i :: u) v) vs).flatten

@[simp]

theorem BGW.PlaneTree.vertices_node (ts : List PlaneTree) : (node ts).vertices = [] :: (List.mapIdx (fun (i : ℕ) (t : PlaneTree) => List.map (fun (u : List ℕ) => i :: u) t.vertices) ts).flatten

@[simp]

theorem BGW.PlaneTree.vertices_leaf : leaf.vertices = [[]]

theorem BGW.PlaneTree.mem_vertices_iff (t : PlaneTree) (u : List ℕ) : u ∈ t.vertices ↔ t.IsVertex u

The enumeration contains exactly the addresses at which fringe lookup succeeds.

@[simp]

theorem BGW.PlaneTree.length_vertices (t : PlaneTree) : t.vertices.length = t.size

The address enumeration has one entry for each vertex counted by size.

theorem BGW.PlaneTree.nodup_vertices (t : PlaneTree) : t.vertices.Nodup

Each vertex address occurs exactly once, including when subtrees are equal.

def BGW.PlaneTree.generationSize (t : PlaneTree) (h : ℕ) : ℕ

The number of vertices at depth h, with the root at depth zero.

Equations

• t.generationSize h = List.countP (fun (u : List ℕ) => decide (u.length = h)) t.vertices

@[simp]

theorem BGW.PlaneTree.generationSize_zero (t : PlaneTree) : t.generationSize 0 = 1