Ordered recursive DFS: finite execution and local invariants
ProvedCLRS.DFS.pure_execution_certificateLet be a finite directed multigraph with vertices and stored adjacency occurrences, including duplicates and self-loops. Let be any permutation of its vertices, represented by the supplied sequence prefix. Starting from white colors, zero timestamps and counters, and parent, finish-order and label entries, the ordinary ordered recursive DFS has a finite big-step execution ending in a state , with traversal event count , such that
Every vertex is black. There are predecessor trees, numbered from zero. The output satisfies the local DFS certificate: positive distinct discovery and finish times within ; no coinciding discovery/finish events; disjoint or nested vertex intervals; a nonroot parent is an adjacent vertex whose interval is the nearest strict enclosing interval; every edge target is discovered before its source finishes; roots respect their input priority; the finish-order prefix is a permutation strictly increasing in finish time; labels lie in and cover that range, are inherited by children, and order roots by discovery time.
The cost includes all vertex visits, all adjacency occurrences and all outer-loop iterations. The implementation's four fixed entry, constructor, initial-loop and return events are excluded. This is the purely mathematical execution lemma used by the concrete heap-level DFS proof; it also supplies the shared DFS prerequisite for Kosaraju's algorithm.
import Definitions.Def_CLRS_DFS_PureExecution set_option autoImplicit false open Algo2LeanGenerated CLRS.GraphTraversal CLRS.DFS CLRS.DFS.Pure
theorem CLRS.DFS.pure_execution_certificate (g : Graph) (input : Seq) (values : List Int)
(permutation : values.Perm ((List.range g.size).map Int.ofNat))
(observed : ∀ i : Nat, i < g.size → input i = values[i]!) :
∃ (a : Pure.State) (k : Nat),
Eval g (.roots values) initial a k ∧ Completed g input a ∧
k ≤ 6 * g.size + 2 * edgeCount g := by sorry