def Hex.GraphIso.Nauty.Generation.PrefixEq {n : Nat} (level : Nat) (st out : SearchSt n) : Prop

The stored first-reference codes and target hints before a level agree.

Equations

• Hex.GraphIso.Nauty.Generation.PrefixEq level st out = ∀ (i : Nat), i < level → out.firstcode[i]! = st.firstcode[i]! ∧ out.firsttc[i]! = st.firsttc[i]!

theorem Hex.GraphIso.Nauty.Generation.PrefixEq.refl {n : Nat} (level : Nat) (st : SearchSt n) : PrefixEq level st st

theorem Hex.GraphIso.Nauty.Generation.PrefixEq.trans {n level : Nat} {a b c : SearchSt n} (h : PrefixEq level a b) (h' : PrefixEq level b c) : PrefixEq level a c

theorem Hex.GraphIso.Nauty.Generation.PrefixEq.mono {n level level' : Nat} {st out : SearchSt n} (h : PrefixEq level st out) (hle : level' ≤ level) : PrefixEq level' st out

theorem Hex.GraphIso.Nauty.Generation.FirstFields.prefix {n : Nat} {st out : SearchSt n} (h : FirstFields st out) (level : Nat) : PrefixEq level st out

theorem Hex.GraphIso.Nauty.Generation.first_prefix {n : Nat} (ctx : Ctx n) (inf tcLevel fuel level numcells : Nat) (st : SearchSt n) : PrefixEq level st (firstPathNode ctx inf tcLevel fuel level numcells st).snd

First-path recursion writes reference codes and target hints only at its own level and below. This is unconditional, including fuel exhaustion.