Proof of `Treedepth and Δ-forestwidth` (1st statement)
groundedproofs/Lax461425Proofs/TreedepthForestwidth.lean · lax-461425
What this proof establishes
no assumptions
Assuming the claims on the left, the claim on the right holds — checked by the archive's pipeline. Proof code is not displayed here.
Description
The nodes are the vertices below a new root; the parent of a vertex is its immediate ancestor (the ancestor of largest rank), or the new root, and its bag consists of the vertex and its ancestors. Bags are chains, so ranks are injective on them; ranks decrease towards the root, so the depth is at most . A vertex leaves the bags exactly at the node .