theorem
Hex.GraphIso.Nauty.Generic.sweep_first_bounded
{n : Nat}
{σ γ : Type}
[Policy σ n]
{ctx : γ}
{inf tcLevel bound : Nat}
{P : σ → Prop}
(h : BoundedPolicy ctx inf tcLevel bound P)
(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 : σ)
(hlevel : bound ≤ level)
(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)
:
An invariant established by the first child survives the entire sweep, including a return past the receiving frame.
theorem
Hex.GraphIso.Nauty.Generic.FirstPath.bounded
{n : Nat}
{σ γ : Type}
[Policy σ n]
{ctx : γ}
{inf tcLevel bound : Nat}
{P : σ → Prop}
(h : BoundedPolicy ctx inf tcLevel bound P)
(hfirst : ∀ (level tv : Nat) (st : σ), P st → P (Policy.afterChildFirst level tv st))
{fuel level numcells last : Nat}
{st leaf : σ}
(path : FirstPath ctx tcLevel fuel level numcells st last leaf)
(hlevel : bound ≤ level)
(hterminal : P (Policy.firstterminal last leaf))
:
An invariant established at the first leaf survives the full search.