theorem
Hex.GraphIso.Nauty.Generation.HasLeaf.ofPerm
{n : Nat}
{ctx : Ctx n}
{tcLevel level : Nat}
{U V : RefineSt n}
{targets : List Nat}
{key : Key n}
(hsize : ctx.g.size = n)
(hok : IterOk ctx level U)
(hperm : StPerm level V U)
(h : HasLeaf ctx tcLevel level U targets key)
:
HasLeaf ctx tcLevel level V targets key
Cell-equivalent refined states have the same reference occurrences, including the sequence of target positions.
theorem
Hex.GraphIso.Nauty.Generation.HasLeaf.reorderChild
{n : Nat}
{ctx : Ctx n}
{tcLevel level tc e oU oV : Nat}
{st : RefineSt n}
{lab : Array Nat}
{targets : List Nat}
{key : Key n}
(hsize : ctx.g.size = n)
(hok : IterOk ctx level st)
(hlvl : level < n)
(hlab : lab.size = n)
(hperm : cellsPerm st.ptn level lab st.lab)
(hcell : (tc, e) ∈ cells st.ptn level n)
(hne : tc < e)
(hoU : oU ≤ e - tc)
(hoV : oV ≤ e - tc)
(hat : lab[tc + oV]! = st.lab[tc + oU]!)
(h : HasLeaf ctx tcLevel (level + 1) (childSt ctx level st tc st.lab[tc + oU]!) targets key)
:
Selecting the same vertex from a reordered target cell preserves the reference occurrence in the resulting refined child.
theorem
Hex.GraphIso.Nauty.Generation.HasLeaf.childFields
{n : Nat}
{ctx : Ctx n}
{tcLevel level tc tv : Nat}
{st : RefineSt n}
{child : SearchSt n}
{targets : List Nat}
{key : Key n}
(hlab : child.lab = (breakout n st.lab st.ptn (level + 1) tc tv).fst)
(hptn : child.ptn = st.ptn.set! tc (level + 1))
(hactive : child.active = VSet.empty.insert tc)
:
The child reference statement follows the arrays passed to the executable refinement; bookkeeping fields of its input state play no role.
theorem
Hex.GraphIso.Nauty.Generation.RefPath.ofPerm
{n : Nat}
{ctx : Ctx n}
{tcLevel boundary level : Nat}
{U V : RefineSt n}
{targets : List Nat}
{key : Key n}
(hsize : ctx.g.size = n)
(hok : IterOk ctx level U)
(hperm : StPerm level V U)
(h : RefPath ctx tcLevel boundary level U targets key)
:
RefPath ctx tcLevel boundary level V targets key
Cell-equivalent refined states have the same reference occurrences, including the sequence of target positions.
theorem
Hex.GraphIso.Nauty.Generation.RefPath.reorderChild
{n : Nat}
{ctx : Ctx n}
{tcLevel boundary level tc e oU oV : Nat}
{st : RefineSt n}
{lab : Array Nat}
{targets : List Nat}
{key : Key n}
(hsize : ctx.g.size = n)
(hok : IterOk ctx level st)
(hlvl : level < n)
(hlab : lab.size = n)
(hperm : cellsPerm st.ptn level lab st.lab)
(hcell : (tc, e) ∈ cells st.ptn level n)
(hne : tc < e)
(hoU : oU ≤ e - tc)
(hoV : oV ≤ e - tc)
(hat : lab[tc + oV]! = st.lab[tc + oU]!)
(h : RefPath ctx tcLevel boundary (level + 1) (childSt ctx level st tc st.lab[tc + oU]!) targets key)
:
Selecting the same vertex from a reordered target cell preserves the reference occurrence in the resulting refined child.
theorem
Hex.GraphIso.Nauty.Generation.RefPath.childFields
{n : Nat}
{ctx : Ctx n}
{tcLevel boundary level tc tv : Nat}
{st : RefineSt n}
{child : SearchSt n}
{targets : List Nat}
{key : Key n}
(hlab : child.lab = (breakout n st.lab st.ptn (level + 1) tc tv).fst)
(hptn : child.ptn = st.ptn.set! tc (level + 1))
(hactive : child.active = VSet.empty.insert tc)
:
The child reference statement follows the arrays passed to the executable refinement; bookkeeping fields of its input state play no role.