theorem Hex.GraphIso.Nauty.Equitable.reorder {n : Nat} {ctx : Ctx n} {level : Nat} {lab out ptn : Array Nat} (h : Equitable ctx level lab ptn) (hp : cellsPerm ptn level lab out) (hsize : ptn.size = n) (hend : ptn[ptn.size - 1]! ≤ level) : Equitable ctx level out ptn

Reordering labels within cells preserves equitability.

theorem Hex.GraphIso.Nauty.child_equitable {n k : Nat} {G : Colored n k} {ctx : Ctx n} {level numcells tc tv : Nat} {st : Search n} {cell : VSet n} (first : Bool) (hn0 : 0 < n) (hlevel : 1 ≤ level) (hok : SearchOk G level numcells st) (heq : Equitable ctx level st.lab st.ptn) (htarget : Generic.Target (fun (st : Search n) => st) level tc cell st) (htv : cell.mem tv = true) (hsymm : ∀ (u v : Nat), u < n → v < n → ctx.g[u]!.mem v = ctx.g[v]!.mem u) : have R := SearchState.refined ctx (level + 1) (numcells + 1) (child first level tc tv st); Equitable ctx (level + 1) R.lab R.ptn

An actual target-cell child refines to an equitable partition.

theorem Hex.GraphIso.Nauty.recover_equitable {n k : Nat} {G : Colored n k} {ctx : Ctx n} {level numcells : Nat} {st out : Search n} (hn0 : 0 < n) (hlevel : 1 ≤ level) (hok : SearchOk G level numcells st) (heq : Equitable ctx level st.lab st.ptn) (hout : SearchOut G level level st out) : have result := recover (n + 2) level out; Equitable ctx level result.lab result.ptn

Recovering a parent retains its equitability despite the child's labelling order.