def Hex.GraphIso.Nauty.Sparse.Literal.Compact.checkNode {n : Nat} (G : SparseGraph n) (tcLevel : Nat) : Nat → Nat → Array Nat → Array Nat → VSet n → Nat → CertNode → Key n → Option Bool

Literal compact replay using the exported sparse refinement operations and exactly the same checked sibling-reference scan as native replay.

Equations

• One or more equations did not get rendered due to their size.
• Hex.GraphIso.Nauty.Sparse.Literal.Compact.checkNode G tcLevel 0 x✝⁶ x✝⁵ x✝⁴ x✝³ x✝² x✝¹ x✝ = none
• Hex.GraphIso.Nauty.Sparse.Literal.Compact.checkNode G tcLevel fuel.succ x✝⁶ x✝⁵ x✝⁴ x✝³ x✝² x✝¹ x✝ = Hex.GraphIso.Nauty.Sparse.Literal.checkNode G tcLevel (fuel + 1) x✝⁶ x✝⁵ x✝⁴ x✝³ x✝² x✝¹ x✝

theorem Hex.GraphIso.Nauty.Sparse.Literal.Compact.checkNode_eq : @checkNode = @Sparse.Compact.checkNode

def Hex.GraphIso.Nauty.Sparse.Literal.Compact.checkKey {n k : Nat} (G : Sparse.Colored n k) (cert : CertNode) (B : Key n) : Bool

Equations

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

theorem Hex.GraphIso.Nauty.Sparse.Literal.Compact.checkKey_eq : @checkKey = @Sparse.Compact.checkKey

theorem Hex.GraphIso.Nauty.Sparse.Literal.Compact.checkKey_sound {n k : Nat} {G : Sparse.Colored n k} {cert : CertNode} {B : Key n} (h : checkKey G cert B = true) : canonSpecKey G = B

theorem Hex.GraphIso.Nauty.Sparse.Literal.Compact.not_isomorphic_of_checkKeys {n k : Nat} {G H : Sparse.Colored n k} {cg ch : CertNode} {bg bh : Key n} (hg : checkKey G cg bg = true) (hh : checkKey H ch bh = true) (hd : checkDiff bg bh = true) : ¬Sparse.Isomorphic G H

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

Literal replay of the compact certificate and its attaining label.

Equations

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

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

theorem Hex.GraphIso.Nauty.Sparse.Literal.Compact.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