theorem
Hex.GraphIso.Nauty.childSt_singleton
{n : Nat}
{ctx : Ctx n}
{st : RefineSt n}
{level tc e o a : Nat}
(h : IterOk ctx level st)
(hcell : (tc, e) ∈ cells st.ptn level n)
(hne : tc < e)
(ho : o ≤ e - tc)
(ha : IsCell st.ptn level a 1)
:
A subtree step retains every existing singleton and its vertex.
theorem
Hex.GraphIso.Nauty.DescPath.singleton
{n : Nat}
{ctx : Ctx n}
{level last a : Nat}
{root leaf : RefineSt n}
{path : List (Nat × Nat)}
(h : DescPath ctx level root path last leaf)
(hok : IterOk ctx level root)
(ha : IsCell root.ptn level a 1)
:
Every descent retains its entry singletons and their vertices.
theorem
Hex.GraphIso.Nauty.DescPath.picked
{n : Nat}
{ctx : Ctx n}
{level last tc o : Nat}
{root leaf : RefineSt n}
{path : List (Nat × Nat)}
(h : DescPath ctx level root ((tc, o) :: path) last leaf)
(hok : IterOk ctx level root)
:
The final labelling records the first individualized vertex at the first target position.