theorem Hex.GraphIso.Nauty.Sparse.Compare.Result.order {n : Nat} {A B : SparseGraph n} {r : Int × Nat} (h : Result A B r) : r.fst = ordInt (graphCmp A B)

The first unequal row determines the entire sparse graph-key comparison.

theorem Hex.GraphIso.Nauty.Sparse.testcanlab_fst {n : Nat} (G H : SparseGraph n) (R : Rows n) (lab : Array Nat) (l : Label n) (hl : Label.ofArray? n lab = some l) (hR : R.Prefix H n) : (testcanlab (Graph.ofGraph G) R lab).fst = ordInt (graphCmp (G.relabel l.perm) H)

The executed comparison sign agrees with the sparse canonical graph key.

theorem Hex.GraphIso.Nauty.Sparse.testcanlab_eq_zero {n : Nat} (G H : SparseGraph n) (R : Rows n) (lab : Array Nat) (l : Label n) (hl : Label.ofArray? n lab = some l) (hR : R.Prefix H n) : (testcanlab (Graph.ofGraph G) R lab).fst = 0 ↔ G.relabel l.perm = H

A tie means literal equality of the normalized native sparse graphs.