theorem Hex.GraphIso.Nauty.Max.firstPath_generates {n k : Nat} {G : Colored n k} {tcLevel fuel level numcells last : Nat} {st leaf : Search n} (hp : Generic.FirstPath { g := rowsOf G } tcLevel fuel level numcells st last leaf) (hn : ∀ (q : Nat), q < fuel → (contract G tcLevel).nodeValid q (Generic.nodeCall { g := rowsOf G } (n + 2) tcLevel q)) {cs bs fs : List Nat} {parents : Parents n} (hi : NodeInput G { g := rowsOf G } tcLevel fuel true { level := level, numcells := numcells, codes := cs, entry := st } bs fs parents) {base : List (Fin n)} {gs : List (Perm n)} (hbase : ∀ (b : Fin n), st.fixedpts.mem ↑b = true ↔ b ∈ base) (htrace : Generation.Realizes G gs (node true { g := rowsOf G } (n + 2) tcLevel fuel level numcells st).snd.genTrace.toList) (p : Perm n) : IsIso G G p → Perm.Fixes base p → Perm.Generated gs p

Every automorphism fixing the individualized base is generated by the actual first node's containing trace. The induction uses the actual guiding child and the image coverage of the actual sibling sweep.