def Hex.GraphIso.Nauty.Sparse.prefixKey {n : Nat} (cs : List Nat) (key : Key n) : Key n

Prefix a native subtree key by the codes of its frozen ancestors.

Equations

• Hex.GraphIso.Nauty.Sparse.prefixKey cs key = { codes := cs ++ key.codes, graph := key.graph }

theorem Hex.GraphIso.Nauty.Sparse.prefixKey_nil {n : Nat} (key : Key n) : prefixKey [] key = key

theorem Hex.GraphIso.Nauty.Sparse.prefixKey_append {n : Nat} (cs ds : List Nat) (key : Key n) : prefixKey cs (prefixKey ds key) = prefixKey (cs ++ ds) key

theorem Hex.GraphIso.Nauty.Sparse.prefixKey_cmp {n : Nat} (cs : List Nat) (a b : Key n) : (prefixKey cs a).cmp (prefixKey cs b) = a.cmp b

A common ancestor prefix leaves the complete native comparison unchanged.

theorem Hex.GraphIso.Nauty.Sparse.prefixKey_le {n : Nat} (cs : List Nat) {a b : Key n} (h : a.Le b) : (prefixKey cs a).Le (prefixKey cs b)

theorem Hex.GraphIso.Nauty.Sparse.prefixKey_max {n : Nat} (cs : List Nat) (a b : Key n) : prefixKey cs (a.max b) = (prefixKey cs a).max (prefixKey cs b)