theorem Hex.GraphIso.Nauty.processnode_coset {n : Nat} (ctx : Ctx n) (level numcells : Nat) (st : SearchSt n) : (processnode ctx level numcells st).snd.cosetindex = st.cosetindex

Leaf classification never changes the first-path coset cursor.

theorem Hex.GraphIso.Nauty.otherNodePrep_coset {n : Nat} (level code : Nat) (st : SearchSt n) : (otherNodePrep level code st).cosetindex = st.cosetindex

Comparison preparation never changes the first-path coset cursor.

theorem Hex.GraphIso.Nauty.recover_coset (n inf level : Nat) (st : SearchSt n) : (recover n inf level st).cosetindex = st.cosetindex

Parent-frame recovery never changes the first-path coset cursor.

theorem Hex.GraphIso.Nauty.leafFinish_coset {n : Nat} (level : Nat) (st : SearchSt n) : (leafFinish level st).cosetindex = st.cosetindex

Completed-leaf cleanup never changes the first-path coset cursor.