def Hex.GraphIso.Nauty.LabelCarrier {n : Nat} (ctx : Ctx n) (ref cur : Array Nat) (store : Array (Array Nat)) : Prop

A checked generator maps one labelling pointwise onto another.

Equations

• Hex.GraphIso.Nauty.LabelCarrier ctx ref cur store = ∃ (γ : Array Nat), γ ∈ store ∧ Hex.GraphIso.Nauty.checkAutom ctx.g γ = true ∧ ∀ (i : Nat), i < n → γ[ref[i]!]! = cur[i]!

def Hex.GraphIso.Nauty.CellCarrier {n : Nat} (ctx : Ctx n) (ptn : Array Nat) (level : Nat) (base ref cur : Array Nat) (store : Array (Array Nat)) : Prop

A checked carrier whose witnessing generator stabilizes one ancestor frame. Direct generator unwinds need only this witness. Requiring every recorded generator to stabilize the frame is stronger, and it fails away from the first-path loop that consumes an orbit closure.

Equations

• One or more equations did not get rendered due to their size.

theorem Hex.GraphIso.Nauty.CellCarrier.toLabel {n : Nat} {ctx : Ctx n} {ptn : Array Nat} {level : Nat} {base ref cur : Array Nat} {store : Array (Array Nat)} (h : CellCarrier ctx ptn level base ref cur store) : LabelCarrier ctx ref cur store

theorem Hex.GraphIso.Nauty.LabelCarrier.leafRows {n : Nat} {ctx : Ctx n} {ref cur : Array Nat} {store : Array (Array Nat)} (h : LabelCarrier ctx ref cur store) (hgsz : ctx.g.size = n) (hrefsz : ref.size = n) (hrefok : LabOk ref n) (hcursz : cur.size = n) : Nauty.leafRows ctx cur = Nauty.leafRows ctx ref

A checked carrier identifies the relabelled leaf rows of its two permutation labellings.