A live first-reference descent uses either the canonical target rule or the saved first target at each level.
Equations
- One or more equations did not get rendered due to their size.
- Hex.GraphIso.Nauty.Guided ctx tcLevel store x✝¹ x✝ [] = True
Instances For
theorem
Hex.GraphIso.Nauty.Guided.depth
{n : Nat}
{ctx : Ctx n}
{tcLevel base last₁ last₂ : Nat}
{store : Array Int}
{root first current : RefineSt n}
{p₁ p₂ : List (Nat × Nat)}
(hfirst : DescPath ctx base root p₁ last₁ first)
(hok : IterOk ctx base root)
(hselect : Selects ctx tcLevel base root p₁)
(htarget : Targets store base (List.map Prod.fst p₁))
(hcurrent : DescPath ctx base root p₂ last₂ current)
(hguided : Guided ctx tcLevel store base root p₂)
(hdisc₁ : ∀ (q : Nat), q < n → first.ptn[q]! ≤ last₁)
(hdisc₂ : ∀ (q : Nat), q < n → current.ptn[q]! ≤ last₂)
(hlab : first.lab = current.lab)
:
Two discrete descents to the same labelling have the same depth when one records canonical targets and the other uses canonical or saved targets. The final labelling fixes their chosen vertices at every common target.