theorem
Hex.GraphIso.Nauty.childSt_frame
{n : Nat}
{ctx : Ctx n}
{st : RefineSt n}
{level tc e o : Nat}
(h : IterOk ctx level st)
(hcell : (tc, e) ∈ cells st.ptn level n)
(hne : tc < e)
(ho : o ≤ e - tc)
:
A subtree step preserves its parent's cell contents and every boundary already closed at the parent.
theorem
Hex.GraphIso.Nauty.DescPath.frame
{n : Nat}
{ctx : Ctx n}
{base last : Nat}
{root leaf : RefineSt n}
{path : List (Nat × Nat)}
(h : DescPath ctx base root path last leaf)
(hok : IterOk ctx base root)
:
Every descent preserves the ordered cell contents of its frozen entry partition and its already closed boundaries.
theorem
Hex.GraphIso.Nauty.Guided.leaf_checked
{n : Nat}
{ctx : Ctx n}
{tcLevel base last₁ last₂ : Nat}
{store : Array Int}
{perm : Array Nat}
{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₂)
(hgsz : ctx.g.size = n)
(hcheck : checkAutom ctx.g perm = true)
(hmap : ∀ (i : Nat), i < n → perm[first.lab[i]!]! = current.lab[i]!)
:
A checked scatter between the leaves stabilizes their common ancestor, and hence forces equal depth for guided descents.
theorem
Hex.GraphIso.Nauty.Guided.depth_checked
{n : Nat}
{ctx : Ctx n}
{tcLevel base last₁ last₂ : Nat}
{store : Array Int}
{perm : Array Nat}
{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₂)
(hgsz : ctx.g.size = n)
(hcheck : checkAutom ctx.g perm = true)
(hmap : ∀ (i : Nat), i < n → perm[first.lab[i]!]! = current.lab[i]!)
:
Checked guided leaves have equal descent depth.