structure Hex.GraphIso.Nauty.Sparse.Generation.Matches {n : Nat} (G : SparseGraph n) (level : Nat) (st : State n) (targets : List Nat) (key : Key n) : Prop

Literal matching with the stored native first reference, including the sentinel and the parsed first label's normalized sparse graph.

• codes : StoredCodes st.firstcode level key.codes
• targets : Targets st.firsttc level targets
• graph : ∃ (label : Label n), Label.ofArray? n st.firstlab = some label ∧ key.graph = G.relabel label.perm

theorem Hex.GraphIso.Nauty.Sparse.Generation.Matches.congr {n : Nat} {G : SparseGraph n} {level : Nat} {st out : State n} {targets : List Nat} {key : Key n} (h : Matches G level st targets key) (he : SearchState.reference out = SearchState.reference st) : Matches G level out targets key

theorem Hex.GraphIso.Nauty.Sparse.Generation.Matches.tail {n : Nat} {G : SparseGraph n} {level : Nat} {st : State n} {targets : List Nat} {key : Key n} {tc code : Nat} (h : Matches G level st (tc :: targets) { codes := code :: key.codes, graph := key.graph }) : Matches G (level + 1) st targets key

theorem Hex.GraphIso.Nauty.Sparse.Generation.Matches.cons {n : Nat} {G : SparseGraph n} {level : Nat} {st : State n} {targets : List Nat} {key : Key n} {tc code : Nat} (h : Matches G (level + 1) st targets key) (hc : st.firstcode[level]! = code) (ht : st.firsttc[level]! = Int.ofNat tc) : Matches G level st (tc :: targets) { codes := code :: key.codes, graph := key.graph }

theorem Hex.GraphIso.Nauty.Sparse.Generation.Matches.head {n : Nat} {G : SparseGraph n} {level : Nat} {st : State n} {targets : List Nat} {key : Key n} {tcLevel : Nat} {root : RefineSt n} (h : Matches G level st targets key) (ho : HasLeaf G tcLevel level root targets key) : st.firstcode[level]! = root.longcode ∧ (discreteAt root.ptn level n ≠ true → st.firsttc[level]! = Int.ofNat (targetcell (Graph.ofGraph G) root.lab root.ptn level tcLevel (-1)))

A matching selected occurrence identifies the stored current code and, when open, the stored native unhinted target.

theorem Hex.GraphIso.Nauty.Sparse.FirstRef.occurs {n : Nat} {G : SparseGraph n} {tcLevel level : Nat} {root : RefineSt n} {st : State n} (h : FirstRef G tcLevel level root st) (hr : RefineSt.Ready G level root) : ∃ (targets : List Nat), ∃ (key : Key n), Generation.HasLeaf G tcLevel level root targets key ∧ Generation.Matches G level st targets key

The saved selected first descent occurs with exactly its stored target/code chain and parsed first-reference graph.