def Hex.GraphIso.Nauty.Generic.prepareFirst {n : Nat} {σ γ : Type} [Policy σ n] (ctx : γ) (tcLevel level numcells : Nat) (st : σ) : Nat × Int × VSet n × Nat × σ

Refine the first path, save its code, and select its target.

Equations

• One or more equations did not get rendered due to their size.

theorem Hex.GraphIso.Nauty.Generic.sweep_first_stable {n : Nat} {σ γ : Type} [Policy σ n] {ctx : γ} {inf tcLevel : Nat} {P : σ → Prop} {validCode : Nat → Prop} {validLeaf : Leaf → σ → Prop} (h : StablePolicy ctx inf tcLevel P validCode validLeaf) (hfirst : ∀ (level tv : Nat) (st : σ), P st → P (Policy.afterChildFirst level tv st)) (fuel cfuel level numcells tc tv index : Nat) (cell : VSet n) (st : σ) (horbit : Policy.orbit st tv = tv) (hchild : P (node true ctx inf tcLevel fuel (level + 1) (numcells + 1) (Policy.child true level tc tv st)).snd) : P (sweep true ctx inf tcLevel fuel (cfuel + 1) level numcells tc tv (some tv) cell index st).snd.snd

An invariant established by the first child survives the entire sweep, including a return past the receiving frame.

inductive Hex.GraphIso.Nauty.Generic.FirstPath {n : Nat} {σ γ : Type} [Policy σ n] (ctx : γ) (tcLevel : Nat) : Nat → Nat → Nat → σ → Nat → σ → Prop

A successful first descent records each preparation and the child actually selected before any sibling search can run.

• leaf {n : Nat} {σ γ : Type} [Policy σ n] {ctx : γ} {tcLevel : Nat} (fuel level numcells : Nat) (st : σ) (hdiscrete : (prepareFirst ctx tcLevel level numcells st).fst = n) : FirstPath ctx tcLevel (fuel + 1) level numcells st level (prepareFirst ctx tcLevel level numcells st).snd.snd.snd.snd
• step {n : Nat} {σ γ : Type} [Policy σ n] {ctx : γ} {tcLevel fuel level numcells last : Nat} {st leaf : σ} {tv : Nat} (hopen : (prepareFirst ctx tcLevel level numcells st).fst ≠ n) (htv : (prepareFirst ctx tcLevel level numcells st).snd.snd.fst.nextElem none = some tv) (horbit : Policy.orbit (Policy.cheapCheck true level (prepareFirst ctx tcLevel level numcells st).snd.snd.snd.snd) tv = tv) (tail : FirstPath ctx tcLevel fuel (level + 1) ((prepareFirst ctx tcLevel level numcells st).fst + 1) (Policy.child true level (prepareFirst ctx tcLevel level numcells st).snd.fst.toNat tv (Policy.cheapCheck true level (prepareFirst ctx tcLevel level numcells st).snd.snd.snd.snd)) last leaf) : FirstPath ctx tcLevel (fuel + 1) level numcells st last leaf

theorem Hex.GraphIso.Nauty.Generic.FirstPath.stable {n : Nat} {σ γ : Type} [Policy σ n] {ctx : γ} {inf tcLevel : Nat} {P : σ → Prop} {validCode : Nat → Prop} {validLeaf : Leaf → σ → Prop} (h : StablePolicy ctx inf tcLevel P validCode validLeaf) (hfirst : ∀ (level tv : Nat) (st : σ), P st → P (Policy.afterChildFirst level tv st)) (hfinish : ∀ (level size index : Nat) (st : σ), P st → P (Policy.afterSweep true level size index st)) {fuel level numcells last : Nat} {st leaf : σ} (path : FirstPath ctx tcLevel fuel level numcells st last leaf) (hterminal : P (Policy.firstterminal last leaf)) : P (node true ctx inf tcLevel fuel level numcells st).snd

An invariant established at the first leaf survives the full search.

theorem Hex.GraphIso.Nauty.Generic.sweep_first_reference {n : Nat} {σ α γ : Type} [Policy σ n] {ctx : γ} {inf tcLevel : Nat} {project : σ → α} (h : ReferencePolicy ctx inf tcLevel project) (hfirst : ∀ (level tv : Nat) (st : σ), project (Policy.afterChildFirst level tv st) = project st) (fuel cfuel level numcells tc tv index : Nat) (cell : VSet n) (st : σ) (horbit : Policy.orbit st tv = tv) : project (sweep true ctx inf tcLevel fuel (cfuel + 1) level numcells tc tv (some tv) cell index st).snd.snd = project (node true ctx inf tcLevel fuel (level + 1) (numcells + 1) (Policy.child true level tc tv st)).snd

The first child determines the reference retained by its entire sweep.

theorem Hex.GraphIso.Nauty.Generic.FirstPath.reference {n : Nat} {σ α γ : Type} [Policy σ n] {ctx : γ} {inf tcLevel : Nat} {project : σ → α} (h : ReferencePolicy ctx inf tcLevel project) (hfirst : ∀ (level tv : Nat) (st : σ), project (Policy.afterChildFirst level tv st) = project st) {fuel level numcells last : Nat} {st leaf : σ} (path : FirstPath ctx tcLevel fuel level numcells st last leaf) : project (node true ctx inf tcLevel fuel level numcells st).snd = project (Policy.firstterminal last leaf)

The full search saves precisely the leaf reached by its first descent.