theorem Hex.GraphIso.Nauty.Sparse.Max.FirstInput.short_drop {n k : Nat} {G : Sparse.Colored n k} {tcLevel fuel tv last : Nat} {f : Frame n} {parents : Parents n} {leaf : State n} (h : FirstInput G tcLevel f parents) (hi : (visit (Graph.ofGraph G.graph) f.level f.numcells f.entry).fst < n) (htv : (Generic.prepareFirst (Graph.ofGraph G.graph) tcLevel f.level f.numcells f.entry).snd.snd.fst.nextElem none = some tv) (path : have p := Frame.firstParent G.graph tcLevel f [] tv; have ch := Parent.child G.graph tcLevel p; Generic.FirstPath (Graph.ofGraph G.graph) tcLevel fuel ch.level ch.numcells ch.entry last leaf) (hexit : have p := Frame.firstParent G.graph tcLevel f [] tv; have ch := Parent.child G.graph tcLevel p; (Generic.node true (Graph.ofGraph G.graph) (n + 2) tcLevel fuel ch.level ch.numcells ch.entry).fst = Generic.Exit.unwind f.level true) : have p := Frame.firstParent G.graph tcLevel f [] tv; have ch := Parent.child G.graph tcLevel p; have raw := (Generic.node true (Graph.ofGraph G.graph) (n + 2) tcLevel fuel ch.level ch.numcells ch.entry).snd; have left := Generic.Policy.leaveChild tv (afterChildFirst f.level tv raw); ∀ (v : Nat), v < n → p.cell.mem v = true → (Generic.Policy.shortprune p.cell left).mem v = false → ∃ (gamma : Array Nat), checkAutom (Graph.context G.graph).g gamma = true ∧ CellStab p.state.ptn f.level p.state.lab gamma ∧ gamma[v]! < v

A short pair returned by the actual first child is valid at its parent. The first leaf supplies the saved labels and trace, while the complete first call supplies pair soundness. First-child bookkeeping does not change the pair read by the filter.