def Hex.GraphIso.Nauty.Sparse.Literal.relabelColored {n k : Nat} (G : Sparse.Colored n k) (l : Label n) : Sparse.Colored n k

Construct the checked native result with exported sparse relabelling.

Equations

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

theorem Hex.GraphIso.Nauty.Sparse.Literal.relabelColored_eq : @relabelColored = @Sparse.Colored.relabel

def Hex.GraphIso.Nauty.Sparse.Literal.colorSeq {n k : Nat} (G : Sparse.Colored n k) : List Nat

Canonical colours obtained by the exported stable bucket initializer.

Equations

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

theorem Hex.GraphIso.Nauty.Sparse.Literal.colorSeq_eq : @colorSeq = @Sparse.colorSeq

def Hex.GraphIso.Nauty.Sparse.Literal.checkCanon {n k : Nat} (G : Sparse.Colored n k) (c : CertCandidate n) : Option (Sparse.CanonResult n k)

Literal result replay: parse the label, check the tree, and compare native sparse graphs and ordered colours.

Equations

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

theorem Hex.GraphIso.Nauty.Sparse.Literal.checkCanon_eq : @checkCanon = @Sparse.checkCanon

theorem Hex.GraphIso.Nauty.Sparse.Literal.checkCanon_sound {n k : Nat} {G : Sparse.Colored n k} {c : CertCandidate n} {r : Sparse.CanonResult n k} (h : checkCanon G c = some r) : canonSpecKey G = c.key ∧ r.form = G.relabel r.label ∧ r.form = Sparse.canon G