theorem Hex.GraphIso.Nauty.Sparse.produceNode_replays {n : Nat} {G : SparseGraph n} {tcLevel fuel level numcells : Nat} {lab ptn : Array Nat} {active : VSet n} {B : Key n} (hp : lab.toList.Perm (List.range n)) (ho : NodeOk n level lab ptn active) (hc : numcells = bcount ptn level n) (hl : level ≤ numcells) (hf : n < fuel + numcells) (hb : ∀ (l : SpecLeaf n), l ∈ specLeaves G tcLevel fuel level lab ptn active numcells → (SpecLeaf.key G l).Le B) : ∃ (a : Bool), checkNode G tcLevel fuel level lab ptn active numcells (produceNode G tcLevel fuel level lab ptn active numcells B) B = some a

Expanding a sufficiently fueled valid native subtree always produces an accepted proof of any genuine upper bound. All child premises follow from the executed refinement, target selection and individualization.