def Hex.GraphIso.Nauty.PairsOk {n k : Nat} (G : Colored n k) (ctx : Ctx n) (st : Search n) : Prop

Every workspace pair has checked realizers preserving the initial colours.

Equations

• One or more equations did not get rendered due to their size.

theorem Hex.GraphIso.Nauty.PairsOk.congr {n k : Nat} {G : Colored n k} {ctx : Ctx n} {st out : Search n} (h : PairsOk G ctx st) (ha : out.autos = st.autos) : PairsOk G ctx out

Equal workspaces have the same valid pairs.

theorem Hex.GraphIso.Nauty.PairsOk.push {n k : Nat} {G : Colored n k} {ctx : Ctx n} {st : Search n} {pair : VSet n × VSet n} (h : PairsOk G ctx st) (hp : PairOk ctx.g (initPtn n (n + 2) (initialPartition G).snd) (initialPartition G).fst 1 pair.fst pair.snd) : PairsOk G ctx (pushAuto st pair)

Appending or replacing a pair preserves the workspace ledger.

theorem Hex.GraphIso.Nauty.admit_autos {n : Nat} {κ : Type} (st : SearchState n κ) : (admit st).autos = (pushAuto st (fmperm st.workperm n)).autos

Admission records the scratch permutation's explicit pair.

theorem Hex.GraphIso.Nauty.PairsOk.admit {n k : Nat} {G : Colored n k} {ctx : Ctx n} {st : Search n} (h : PairsOk G ctx st) (hn0 : 0 < n) (hc : checkAutom ctx.g st.workperm = true) (hs : ColorStab G st.workperm) : PairsOk G ctx (Nauty.admit st)

A checked admission preserving the initial colours supplies a valid explicit pair.

theorem Hex.GraphIso.Nauty.PairsOk.prune {n k : Nat} {G : Colored n k} {ctx : Ctx n} {st : Search n} {level : Nat} (h : PairsOk G ctx st) (hp : level ≠ st.noncheaplevel → PairOk ctx.g (initPtn n (n + 2) (initialPartition G).snd) (initialPartition G).fst 1 (fmptn st.lab st.ptn st.noncheaplevel n).fst (fmptn st.lab st.ptn st.noncheaplevel n).snd) : PairsOk G ctx (pruneReturn level st).snd

The shared prune tail changes the workspace only by its frozen implicit pair.

theorem Hex.GraphIso.Nauty.pruneReturn_autos {n : Nat} {κ : Type} (level : Nat) (st : SearchState n κ) : (pruneReturn level st).snd.autos = if (level != st.noncheaplevel) = true then (pushAuto st (fmptn st.lab st.ptn st.noncheaplevel n)).autos else st.autos

The prune tail inserts exactly its implicit pair when the level differs from its boundary.

theorem Hex.GraphIso.Nauty.leafExit_autos {n : Nat} {κ : Type} (leaf : Leaf) (level : Nat) (st : SearchState n κ) : (leafExit leaf level st).snd.autos = match leaf with | Generic.Leaf.internal => st.autos | Generic.Leaf.autoFirst => (admit st).autos | Generic.Leaf.autoCanon => (admit st).autos | Generic.Leaf.bad => (pruneReturn level st).snd.autos | Generic.Leaf.better sr => (pruneReturn level st).snd.autos

Workspace effects depend only on the admission kind and the incoming pair fields.

theorem Hex.GraphIso.Nauty.PairsOk.leaf {n k : Nat} {G : Colored n k} {ctx : Ctx n} {st : Search n} {level : Nat} (h : PairsOk G ctx st) (hn0 : 0 < n) (leaf : Leaf) (hc : leaf = Generic.Leaf.autoFirst ∨ leaf = Generic.Leaf.autoCanon → checkAutom ctx.g st.workperm = true) (hs : leaf = Generic.Leaf.autoFirst ∨ leaf = Generic.Leaf.autoCanon → ColorStab G st.workperm) (hp : level ≠ st.noncheaplevel → PairOk ctx.g (initPtn n (n + 2) (initialPartition G).snd) (initialPartition G).fst 1 (fmptn st.lab st.ptn st.noncheaplevel n).fst (fmptn st.lab st.ptn st.noncheaplevel n).snd) : PairsOk G ctx (leafExit leaf level st).snd

All leaf actions preserve the ledger once the explicit and implicit admissions are justified.

theorem Hex.GraphIso.Nauty.classify_autos {n : Nat} (ctx : Ctx n) (level numcells : Nat) (st : Search n) : (classify ctx level numcells st).snd.autos = st.autos

Classification preserves the workspace while filling scratch and row-cache fields.

theorem Hex.GraphIso.Nauty.initial_pairs {n k : Nat} (G : Colored n k) (ctx : Ctx n) : PairsOk G ctx (initial n (initialPartition G).fst (initialPartition G).snd)

The empty initial workspace satisfies the ledger.