theorem Hex.GraphIso.Nauty.Generic.nodeStep_ne_done {n : Nat} {σ γ : Type} [Policy σ n] (ctx : γ) (tcLevel : Nat) (next : SweepFn σ n) (first : Bool) (level numcells : Nat) (st : σ) : (nodeStep ctx tcLevel next first level numcells st).fst ≠ Exit.done

A node consumes every completed local action or sweep. Its own return always unwinds or reports exhausted fuel.

theorem Hex.GraphIso.Nauty.Generic.node_ne_done {n : Nat} {σ γ : Type} [Policy σ n] (first : Bool) (ctx : γ) (inf tcLevel fuel level numcells : Nat) (st : σ) : (node first ctx inf tcLevel fuel level numcells st).fst ≠ Exit.done

No recursive node returns the sweep-completion exit.

theorem Hex.GraphIso.Nauty.Max.SweepInput.child_exit {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel fuel cfuel : Nat} {first : Bool} {level numcells tc tv1 tv index : Nat} {cell : VSet n} {st : Search n} {l : Loop n} {bs fs : List Nat} {parents : Parents n} (h : SweepInput G ctx tcLevel fuel cfuel first level numcells tc tv1 (some tv) cell index st l bs fs parents) (hgsz : ctx.g.size = n) (hsymm : ∀ (u v : Nat), u < n → v < n → ctx.g[u]!.mem v = ctx.g[v]!.mem u) (hloop : ∀ (v : Nat), v < n → ctx.g[v]!.mem v = false) : ∃ (target : Nat), ∃ (short : Bool), ∃ (out : Search n), Nauty.node (first && tv == tv1) ctx (n + 2) tcLevel fuel (level + 1) (numcells + 1) (child first level tc tv st) = (Generic.Exit.unwind target short, out)

Adequate child fuel and the node's exit shape leave only an unwind.