structure Hex.GraphIso.Nauty.Sparse.Local {n k : Nat} (G : Sparse.Colored n k) (level numcells : Nat) (st out : State n) : Prop

Local bookkeeping preserves the equitable parent and its call frame.

• ready : Ready G level numcells out
• frame : FrameOut G level level st out

theorem Hex.GraphIso.Nauty.Sparse.Local.trans {n k : Nat} {G : Sparse.Colored n k} {level numcells : Nat} {st mid out : State n} (h : Local G level numcells st mid) (h' : Local G level numcells mid out) : Local G level numcells st out

theorem Hex.GraphIso.Nauty.Sparse.Ready.step {n k : Nat} {G : Sparse.Colored n k} {level numcells : Nat} {st : State n} (h : Ready G level numcells st) {out : State n} (hl : out.lab = st.lab) (hp : out.ptn = st.ptn) (hf : out.firstlab = st.firstlab ∨ out.firstlab = st.lab) (hc : out.canonlab = st.canonlab ∨ out.canonlab = st.lab) (hs : Scratch.Valid n out.lab out.ptn level out.canong.scratch) : Local G level numcells st out

theorem Hex.GraphIso.Nauty.Sparse.Ready.record {n k : Nat} {G : Sparse.Colored n k} {level numcells : Nat} {st : State n} (h : Ready G level numcells st) (code : Nat) : Local G level numcells st (recordFirst level code st)

theorem Hex.GraphIso.Nauty.Sparse.Ready.compare {n k : Nat} {G : Sparse.Colored n k} {level numcells : Nat} {st : State n} (h : Ready G level numcells st) (code : Nat) : Local G level numcells st (compareCodes level code st)

theorem Hex.GraphIso.Nauty.Sparse.Ready.terminal {n k : Nat} {G : Sparse.Colored n k} {level numcells : Nat} {st : State n} (h : Ready G level numcells st) : Local G level numcells st (firstterminal level st)

theorem Hex.GraphIso.Nauty.Sparse.Ready.leaf {n k : Nat} {G : Sparse.Colored n k} {level numcells : Nat} {st : State n} (h : Ready G level numcells st) (leaf : Leaf) : Local G level numcells st (leafExit leaf level st).snd

theorem Hex.GraphIso.Nauty.Sparse.Ready.cheap {n k : Nat} {G : Sparse.Colored n k} {level numcells : Nat} {st : State n} (h : Ready G level numcells st) (first : Bool) : Local G level numcells st (cheapCheck first level st)