theorem Hex.GraphIso.Nauty.Generation.other_internal {n : Nat} {ctx : Ctx n} {inf tcLevel fuel level numcells tc : Nat} {st : SearchSt n} {targets : List Nat} {key : Key n} (hnum : (refine ctx level st.lab st.ptn st.active numcells).numcells < n) (hok : IterOk ctx level (refine ctx level st.lab st.ptn st.active numcells)) (heq : Equitable ctx level (refine ctx level st.lab st.ptn st.active numcells).lab (refine ctx level st.lab st.ptn st.active numcells).ptn) (hm : Matches ctx level st (tc :: targets) key) (hleaf : HasLeaf ctx tcLevel level (refine ctx level st.lab st.ptn st.active numcells) (tc :: targets) key) (hlevel : st.eqlevFirst = level - 1) (hclear : st.needshortprune = false) : have rs := refine ctx level st.lab st.ptn st.active numcells; have pre := otherLeafSt ctx level numcells st; have mt := specMaketargetcell ctx rs.lab rs.ptn level tcLevel; have target := { lab := pre.lab, ptn := pre.ptn, active := pre.active, orbits := pre.orbits, fixedpts := pre.fixedpts, autos := pre.autos, wsCap := pre.wsCap, firstcode := pre.firstcode, canoncode := pre.canoncode, firsttc := pre.firsttc, firstlab := pre.firstlab, canonlab := pre.canonlab, canong := pre.canong, samerows := pre.samerows, compCanon := pre.compCanon, eqlevFirst := pre.eqlevFirst, eqlevCanon := pre.eqlevCanon, gcaFirst := pre.gcaFirst, gcaCanon := pre.gcaCanon, canonlevel := pre.canonlevel, noncheaplevel := pre.noncheaplevel, allsamelevel := pre.allsamelevel, cosetindex := pre.cosetindex, stabvertex := pre.stabvertex, needshortprune := pre.needshortprune, numnodes := pre.numnodes, tctotal := pre.tctotal + mt.snd.snd, canupdates := pre.canupdates, numorbits := pre.numorbits, numgenerators := pre.numgenerators, numbadleaves := pre.numbadleaves, maxlevel := pre.maxlevel, genTrace := pre.genTrace }; have ready := if ¬cheapautom target.ptn level n = true then { lab := target.lab, ptn := target.ptn, active := target.active, orbits := target.orbits, fixedpts := target.fixedpts, autos := target.autos, wsCap := target.wsCap, firstcode := target.firstcode, canoncode := target.canoncode, firsttc := target.firsttc, firstlab := target.firstlab, canonlab := target.canonlab, canong := target.canong, samerows := target.samerows, compCanon := target.compCanon, eqlevFirst := target.eqlevFirst, eqlevCanon := target.eqlevCanon, gcaFirst := target.gcaFirst, gcaCanon := target.gcaCanon, canonlevel := target.canonlevel, noncheaplevel := level + 1, allsamelevel := target.allsamelevel, cosetindex := target.cosetindex, stabvertex := target.stabvertex, needshortprune := target.needshortprune, numnodes := target.numnodes, tctotal := target.tctotal, canupdates := target.canupdates, numorbits := target.numorbits, numgenerators := target.numgenerators, numbadleaves := target.numbadleaves, maxlevel := target.maxlevel, genTrace := target.genTrace } else target; have result := otherChildLoop ctx inf tcLevel fuel (n + 1) level rs.numcells mt.fst ((mt.snd.fst.nextElem none).getD 0) (mt.snd.fst.nextElem none) mt.snd.fst ready; otherNode ctx inf tcLevel (fuel + 1) level numcells st = match result.fst with | some r => (r, result.snd) | none => (Int.ofNat level - 1, result.snd)

A matching internal occurrence reaches the specification target sweep. Neither the canonical comparison nor the saved pruning boundaries can cause an immediate return from this node.