theorem Hex.GraphIso.Nauty.Sparse.SpecLeaf.prepend_key {n : Nat} (G : SparseGraph n) (c : Nat) (l : SpecLeaf n) : key G (prepend c l) = prefixKey [c] (key G l)

structure Hex.GraphIso.Nauty.Sparse.Replay.Valid {n : Nat} (G : SparseGraph n) (B : Key n) (leaves : List (SpecLeaf n)) (attained : Bool) : Prop

A successful replay bounds every leaf and records whether the claimed key is attained. The label witness comes from an executed tree leaf.

• bound (l : SpecLeaf n) : l ∈ leaves → (SpecLeaf.key G l).Le B
• attains : attained = true ↔ ∃ (l : SpecLeaf n), l ∈ leaves ∧ SpecLeaf.key G l = B

def Hex.GraphIso.Nauty.Sparse.Replay.all {α : Type u_1} (check : α → Option Bool) : List α → Option Bool

Combine all child checks, propagating rejection and recording attainment. The explicit recursion also reduces after importing the checker.

Equations

• Hex.GraphIso.Nauty.Sparse.Replay.all check [] = some false
• Hex.GraphIso.Nauty.Sparse.Replay.all check (x_1 :: xs) = do let a ← check x_1 let b ← Hex.GraphIso.Nauty.Sparse.Replay.all check xs pure (a || b)

theorem Hex.GraphIso.Nauty.Sparse.Replay.all_cons {α : Type u_1} {check : α → Option Bool} {x : α} {xs : List α} {a : Bool} : all check (x :: xs) = some a ↔ ∃ (b : Bool), ∃ (c : Bool), check x = some b ∧ all check xs = some c ∧ (b || c) = a

theorem Hex.GraphIso.Nauty.Sparse.Replay.valid_nil {n : Nat} (G : SparseGraph n) (B : Key n) : Valid G B [] false

theorem Hex.GraphIso.Nauty.Sparse.Replay.Valid.append {n : Nat} {G : SparseGraph n} {B : Key n} {xs ys : List (SpecLeaf n)} {a b : Bool} (hx : Valid G B xs a) (hy : Valid G B ys b) : Valid G B (xs ++ ys) (a || b)

theorem Hex.GraphIso.Nauty.Sparse.Replay.all_valid {n : Nat} {α : Type u_1} {G : SparseGraph n} {B : Key n} {check : α → Option Bool} {leaves : α → List (SpecLeaf n)} {xs : List α} {a : Bool} (hcheck : ∀ (x : α), x ∈ xs → ∀ (b : Bool), check x = some b → Valid G B (leaves x) b) (h : all check xs = some a) : Valid G B (List.flatMap leaves xs) a

theorem Hex.GraphIso.Nauty.Sparse.Replay.all_exists {α : Type u_1} {check : α → Option Bool} {xs : List α} (h : ∀ (x : α), x ∈ xs → ∃ (a : Bool), check x = some a) : ∃ (a : Bool), all check xs = some a

def Hex.GraphIso.Nauty.Sparse.Replay.leaf {n : Nat} (G : SparseGraph n) (B : Key n) (l : SpecLeaf n) : Option Bool

Check one actual leaf against a claimed upper bound.

Equations

• Hex.GraphIso.Nauty.Sparse.Replay.leaf G B l = match (Hex.GraphIso.Nauty.Sparse.SpecLeaf.key G l).cmp B with | Ordering.gt => none | Ordering.eq => some true | Ordering.lt => some false

theorem Hex.GraphIso.Nauty.Sparse.Replay.leaf_valid {n : Nat} {G : SparseGraph n} {B : Key n} {l : SpecLeaf n} {a : Bool} (h : leaf G B l = some a) : Valid G B [l] a

theorem Hex.GraphIso.Nauty.Sparse.Replay.leaf_exists {n : Nat} {G : SparseGraph n} {B : Key n} {l : SpecLeaf n} (h : (SpecLeaf.key G l).Le B) : ∃ (a : Bool), leaf G B l = some a

theorem Hex.GraphIso.Nauty.Sparse.Replay.Valid.prepend {n : Nat} {G : SparseGraph n} {B : Key n} {xs : List (SpecLeaf n)} {a : Bool} (h : Valid G B xs a) (c : Nat) : Valid G (prefixKey [c] B) (List.map (SpecLeaf.prepend c) xs) a