theorem
Hex.GraphIso.Nauty.Generation.firstTail_counted
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{inf tcLevel specFuel runFuel level numcells tc len tv1 e : Nat}
{codes fs : List Nat}
{rsLab rsPtn : Array Nat}
{base : SearchSt n}
(hg : ctx.g = rowsOf G)
(hinf : inf = n + 2)
(hn0 : 0 < n)
(ih : OtherTotal G ctx inf tcLevel runFuel)
(hrun : n + 2 < level + 1 + runFuel)
(hspec : level + 1 + specFuel = n + 1)
(hpath : level = codes.length)
(loopFuel : Nat)
(cursor : Option Nat)
(tcell : VSet n)
(st : SearchSt n)
(best : Option (Key n))
(trail : FrameTrail)
(bs : List Nat)
(index : Nat)
:
FirstSweepHyp G ctx tcLevel specFuel level codes bs fs numcells rsLab rsPtn tc len tcell cursor e tv1 base st best
trail →
Counted (segN rsLab tc len)
(fun (v : Nat) => ∃ (γ : Array Nat), checkAutom ctx.g γ = true ∧ CellStab rsPtn level rsLab γ ∧ γ[v]! = tv1)
cursor index →
∃ (last : Option Nat), Counted (segN rsLab tc len)
(fun (v : Nat) => ∃ (γ : Array Nat), checkAutom ctx.g γ = true ∧ CellStab rsPtn level rsLab γ ∧ γ[v]! = tv1)
last
(firstChildLoop ctx inf tcLevel runFuel loopFuel level numcells tc tv1 (tcell.nextElem cursor) tcell index
st).snd.fst ∧ FirstTail G ctx inf tcLevel specFuel runFuel level numcells tc len tv1 e codes fs rsLab rsPtn base loopFuel
cursor tcell st best trail
The actual first-path sibling loop counts distinct original vertices with checked carriers to its guide. Early returns retain the old count; a successful visit or orbit skip performs the same Boolean increment as the executable.
theorem
Hex.GraphIso.Nauty.Generation.firstTail_trace
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{inf tcLevel specFuel runFuel level numcells tc len tv1 e loopFuel : Nat}
{codes bs fs : List Nat}
{rsLab rsPtn : Array Nat}
{base st : SearchSt n}
{cursor : Option Nat}
{tcell : VSet n}
{best : Option (Key n)}
{trail : FrameTrail}
(hg : ctx.g = rowsOf G)
(hinf : inf = n + 2)
(hn0 : 0 < n)
(ih : OtherTotal G ctx inf tcLevel runFuel)
(hrun : n + 2 < level + 1 + runFuel)
(hspec : level + 1 + specFuel = n + 1)
(hpath : level = codes.length)
(hh :
FirstSweepHyp G ctx tcLevel specFuel level codes bs fs numcells rsLab rsPtn tc len tcell cursor e tv1 base st best
trail)
:
FirstTail G ctx inf tcLevel specFuel runFuel level numcells tc len tv1 e codes fs rsLab rsPtn base loopFuel cursor tcell
st best trail
The counter proof also records the executed tail independently of its initial counter value.
theorem
Hex.GraphIso.Nauty.Generation.FirstTail.hyp
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{inf tcLevel specFuel runFuel level numcells tc len tv1 e loopFuel : Nat}
{codes fs : List Nat}
{rsLab rsPtn : Array Nat}
{base st : SearchSt n}
{cursor : Option Nat}
{tcell : VSet n}
{best : Option (Key n)}
{trail : FrameTrail}
(h :
FirstTail G ctx inf tcLevel specFuel runFuel level numcells tc len tv1 e codes fs rsLab rsPtn base loopFuel cursor
tcell st best trail)
:
Every recorded first-path tail exposes its current loop invariant.