def Hex.GraphIso.Nauty.Generation.NodeControl {n : Nat} (guide : Nat) (result : Int × SearchSt n) : Prop

An off-path node preserves its first-path guide and directs every outstanding short-prune request to a different frame.

Equations

• Hex.GraphIso.Nauty.Generation.NodeControl guide result = (result.snd.gcaFirst = guide ∧ (result.snd.needshortprune = true → result.fst ≠ Int.ofNat guide))

def Hex.GraphIso.Nauty.Generation.LoopControl {n : Nat} (guide : Nat) (result : Option Int × SearchSt n) : Prop

A loop with a live short-prune request has returned early to a frame different from its first-path guide.

Equations

• Hex.GraphIso.Nauty.Generation.LoopControl guide result = (result.snd.gcaFirst = guide ∧ (result.snd.needshortprune = true → ∃ (r : Int), result.fst = some r ∧ r ≠ Int.ofNat guide))

theorem Hex.GraphIso.Nauty.Generation.loop_control {n : Nat} {ctx : Ctx n} {inf tcLevel fuel : Nat} (hnode : ∀ (level numcells : Nat) (st : SearchSt n), st.needshortprune = false → NodeControl st.gcaFirst (otherNode ctx inf tcLevel fuel level numcells st)) (cfuel level numcells tc tv1 : Nat) (cursor : Option Nat) (tcell : VSet n) (st : SearchSt n) : st.needshortprune = false → LoopControl st.gcaFirst (otherChildLoop ctx inf tcLevel fuel cfuel level numcells tc tv1 cursor tcell st)

theorem Hex.GraphIso.Nauty.Generation.node_control {n : Nat} (ctx : Ctx n) (inf tcLevel fuel level numcells : Nat) (st : SearchSt n) : st.needshortprune = false → NodeControl st.gcaFirst (otherNode ctx inf tcLevel fuel level numcells st)

Throughout off-path recursion the first guide is unchanged, and an outstanding short-prune request returns to a different guide.

theorem Hex.GraphIso.Nauty.Generation.clear_at_guide {n : Nat} {ctx : Ctx n} {inf tcLevel fuel level numcells : Nat} {st : SearchSt n} (hc : st.needshortprune = false) (hr : (otherNode ctx inf tcLevel fuel level numcells st).fst = Int.ofNat st.gcaFirst) : (otherNode ctx inf tcLevel fuel level numcells st).snd.needshortprune = false

A sibling subtree entered with a clear request flag returns to its first-path guide with the flag still clear.