theorem Hex.GraphIso.Nauty.keyMax_assoc {n : Nat} (x y z : Key n) : keyMax (keyMax x y) z = keyMax x (keyMax y z)

Taking the maximum of specification keys is associative.

theorem Hex.GraphIso.Nauty.keysMax_keyMax {n : Nat} (l : List (Key n)) (b c : Key n) : keysMax (keyMax b c) l = keyMax b (keysMax c l)

theorem Hex.GraphIso.Nauty.foldl_incMax {n : Nat} {f : Option (Key n) → Nat → Option (Key n)} {key : Nat → Key n} (os : List Nat) : (∀ (acc : Option (Key n)) (o : Nat), o ∈ os → f acc o = some (incMax acc (key o))) → ∀ (t : Key n), List.foldl f (some t) os = some (keysMax t (List.map key os))

theorem Hex.GraphIso.Nauty.foldl_incMax_cons {n : Nat} {f : Option (Key n) → Nat → Option (Key n)} {key : Nat → Key n} {o : Nat} {os : List Nat} (h : ∀ (acc : Option (Key n)) (x : Nat), x ∈ o :: os → f acc x = some (incMax acc (key x))) (tail0 : Option (Key n)) : List.foldl f tail0 (o :: os) = some (incMax tail0 (keysMax (key o) (List.map key os)))