structure Hex.GraphIso.Kernel.Key : Type

A canonical key with bitset rows: the literal reading of Nauty.Key that the kernel replay produces and compares.

• codes : List Nat

  The refinement codes along the path, ending with the sentinel.

• rows : List Nat

  The leaf's g^lab rows, as bitsets, in nauty's row order.

@[instance_reducible]

instance Hex.GraphIso.Kernel.instInhabitedKey : Inhabited Key

Equations

• Hex.GraphIso.Kernel.instInhabitedKey = { default := Hex.GraphIso.Kernel.instInhabitedKey.default }

def Hex.GraphIso.Kernel.instReprKey.repr : Key → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Hex.GraphIso.Kernel.instReprKey : Repr Key

Equations

• Hex.GraphIso.Kernel.instReprKey = { reprPrec := Hex.GraphIso.Kernel.instReprKey.repr }

def Hex.GraphIso.Kernel.instDecidableEqKey.decEq (x✝ x✝¹ : Key) : Decidable (x✝ = x✝¹)

Equations

• Hex.GraphIso.Kernel.instDecidableEqKey.decEq { codes := a, rows := a_1 } { codes := b, rows := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[instance_reducible]

instance Hex.GraphIso.Kernel.instDecidableEqKey : DecidableEq Key

Equations

• Hex.GraphIso.Kernel.instDecidableEqKey = Hex.GraphIso.Kernel.instDecidableEqKey.decEq

def Hex.GraphIso.Kernel.Key.toKey (n : Nat) (K : Key) : Nauty.Key n

The packed key of a literal whose rows are bitsets over n vertices.

Equations

• Hex.GraphIso.Kernel.Key.toKey n K = { codes := K.codes, rows := List.map Hex.GraphIso.Nauty.VSet.ofNat K.rows }

theorem Hex.GraphIso.Nauty.atD_eq_getD {α : Type} (l : List α) (i : Nat) (d : α) : atD l i d = l.getD i d

theorem Hex.GraphIso.Nauty.getBang_eq_atD (a : Array Nat) (i : Nat) : a[i]! = atD a.toList i 0

theorem Hex.GraphIso.Nauty.setBang_toList (a : Array Nat) (i v : Nat) : (a.set! i v).toList = a.toList.set i v

theorem Hex.GraphIso.Nauty.getBang_toNat_eq_atD {n : Nat} (g : Array (VSet n)) (i : Nat) : g[i]!.toNat = atD (List.map VSet.toNat g.toList) i 0

A packed row read as a bitset is the list read of the bitset rows; out of range both sides are empty.

structure Hex.GraphIso.Nauty.CtxL : Type

Ctx with the adjacency rows as a bare list of single-Nat bitsets.

• n : Nat

  The number of vertices.

• g : List Nat

  Row v is the neighbour set of vertex v, as a bitset.

def Hex.GraphIso.Nauty.Ctx.toL {n : Nat} (ctx : Ctx n) : CtxL

The list view of a context.

Equations

• ctx.toL = { n := n, g := List.map Hex.GraphIso.Nauty.VSet.toNat ctx.g.toList }

@[simp]

theorem Hex.GraphIso.Nauty.toL_n {n : Nat} (ctx : Ctx n) : ctx.toL.n = n

@[simp]

theorem Hex.GraphIso.Nauty.toL_g {n : Nat} (ctx : Ctx n) : ctx.toL.g = List.map VSet.toNat ctx.g.toList

structure Hex.GraphIso.Nauty.RefineStL : Type

RefineSt with list labelling and partition and a bitset active set.

• lab : List Nat
• ptn : List Nat
• active : Nat
• numcells : Nat
• hint : Nat
• maxpos : Nat
• longcode : Nat

def Hex.GraphIso.Nauty.RefineSt.toL {n : Nat} (st : RefineSt n) : RefineStL

The list view of a refine state.

Equations

• st.toL = { lab := st.lab.toList, ptn := st.ptn.toList, active := st.active.toNat, numcells := st.numcells, hint := st.hint, maxpos := st.maxpos, longcode := st.longcode }

@[simp]

theorem Hex.GraphIso.Nauty.toL_lab {n : Nat} (st : RefineSt n) : st.toL.lab = st.lab.toList

@[simp]

theorem Hex.GraphIso.Nauty.toL_ptn {n : Nat} (st : RefineSt n) : st.toL.ptn = st.ptn.toList

@[simp]

theorem Hex.GraphIso.Nauty.toL_active {n : Nat} (st : RefineSt n) : st.toL.active = st.active.toNat

@[simp]

theorem Hex.GraphIso.Nauty.toL_numcells {n : Nat} (st : RefineSt n) : st.toL.numcells = st.numcells

@[simp]

theorem Hex.GraphIso.Nauty.toL_hint {n : Nat} (st : RefineSt n) : st.toL.hint = st.hint

@[simp]

theorem Hex.GraphIso.Nauty.toL_maxpos {n : Nat} (st : RefineSt n) : st.toL.maxpos = st.maxpos

@[simp]

theorem Hex.GraphIso.Nauty.toL_longcode {n : Nat} (st : RefineSt n) : st.toL.longcode = st.longcode

def Hex.GraphIso.Nauty.cellEndGoL (ptn : List Nat) (level : Nat) : Nat → Nat → Nat

Equations

• Hex.GraphIso.Nauty.cellEndGoL ptn level 0 x✝ = x✝
• Hex.GraphIso.Nauty.cellEndGoL ptn level fuel.succ x✝ = if Hex.GraphIso.atD ptn x✝ 0 > level then Hex.GraphIso.Nauty.cellEndGoL ptn level fuel (x✝ + 1) else x✝

def Hex.GraphIso.Nauty.cellEndL (ptn : List Nat) (level i : Nat) : Nat

Equations

• Hex.GraphIso.Nauty.cellEndL ptn level i = Hex.GraphIso.Nauty.cellEndGoL ptn level (ptn.length - i) i

theorem Hex.GraphIso.Nauty.cellEndGoL_eq (ptn : Array Nat) (level fuel j : Nat) : cellEndGoL ptn.toList level fuel j = cellEnd.go ptn level fuel j

theorem Hex.GraphIso.Nauty.cellEndL_eq (ptn : Array Nat) (level i : Nat) : cellEndL ptn.toList level i = cellEnd ptn level i

def Hex.GraphIso.Nauty.cellsGoL (ptn : List Nat) (level nn : Nat) : Nat → Nat → List (Nat × Nat)

Equations

• One or more equations did not get rendered due to their size.
• Hex.GraphIso.Nauty.cellsGoL ptn level nn 0 x✝ = []

def Hex.GraphIso.Nauty.cellsL (ptn : List Nat) (level nn : Nat) : List (Nat × Nat)

Equations

• Hex.GraphIso.Nauty.cellsL ptn level nn = Hex.GraphIso.Nauty.cellsGoL ptn level nn nn 0

theorem Hex.GraphIso.Nauty.cellsGoL_eq (ptn : Array Nat) (level nn fuel c1 : Nat) : cellsGoL ptn.toList level nn fuel c1 = cells.go ptn level nn fuel c1

theorem Hex.GraphIso.Nauty.cellsL_eq (ptn : Array Nat) (level nn : Nat) : cellsL ptn.toList level nn = cells ptn level nn

def Hex.GraphIso.Nauty.splitCellLoopL (gRow : Nat) : Nat → List Nat → Int → Int → List Nat × Int × Int

Equations

• One or more equations did not get rendered due to their size.
• Hex.GraphIso.Nauty.splitCellLoopL gRow 0 x✝² x✝¹ x✝ = (x✝², x✝¹, x✝)

theorem Hex.GraphIso.Nauty.splitCellLoopL_eq {n : Nat} (gRow : VSet n) (fuel : Nat) (lab : Array Nat) (c1 c2 : Int) : splitCellLoopL gRow.toNat fuel lab.toList c1 c2 = ((splitCellLoop gRow fuel lab c1 c2).fst.toList, (splitCellLoop gRow fuel lab c1 c2).snd)

def Hex.GraphIso.Nauty.trivialSplitL (nn level cell1 cell2 : Nat) (c1 c2 : Int) (st : RefineStL) : RefineStL

Equations

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

theorem Hex.GraphIso.Nauty.trivialSplitL_eq {n : Nat} (level cell1 cell2 : Nat) (c1 c2 : Int) (st : RefineSt n) : trivialSplitL n level cell1 cell2 c1 c2 st.toL = (trivialSplit level cell1 cell2 c1 c2 st).toL

def Hex.GraphIso.Nauty.trivialCellL (nn level gRow cell1 cell2 : Nat) (st : RefineStL) : RefineStL

Equations

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

theorem Hex.GraphIso.Nauty.trivialCellL_eq {n : Nat} (level : Nat) (gRow : VSet n) (cell1 cell2 : Nat) (st : RefineSt n) : trivialCellL n level gRow.toNat cell1 cell2 st.toL = (trivialCell level gRow cell1 cell2 st).toL

def Hex.GraphIso.Nauty.refineTrivialGoL (nn level gRow : Nat) : List (Nat × Nat) → RefineStL → RefineStL

Equations

• Hex.GraphIso.Nauty.refineTrivialGoL nn level gRow [] x✝ = x✝
• Hex.GraphIso.Nauty.refineTrivialGoL nn level gRow ((cell1, cell2) :: rest) x✝ = Hex.GraphIso.Nauty.refineTrivialGoL nn level gRow rest (Hex.GraphIso.Nauty.trivialCellL nn level gRow cell1 cell2 x✝)

def Hex.GraphIso.Nauty.refineTrivialL (ctx : CtxL) (level split1 : Nat) (st : RefineStL) : RefineStL

Equations

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

theorem Hex.GraphIso.Nauty.refineTrivialGoL_eq {n : Nat} (level : Nat) (gRow : VSet n) (cs : List (Nat × Nat)) (st : RefineSt n) : refineTrivialGoL n level gRow.toNat cs st.toL = (refineTrivial.go level gRow cs st).toL

theorem Hex.GraphIso.Nauty.refineTrivialL_eq {n : Nat} (ctx : Ctx n) (level split1 : Nat) (st : RefineSt n) : refineTrivialL ctx.toL level split1 st.toL = (refineTrivial ctx level split1 st).toL

def Hex.GraphIso.Nauty.worksetOfL (nn : Nat) (lab : List Nat) (lo hi : Nat) : Nat

Equations

• Hex.GraphIso.Nauty.worksetOfL nn lab lo hi = List.foldl (fun (w o : Nat) => Hex.GraphIso.Nauty.NatSet.insert nn w (Hex.GraphIso.atD lab (lo + o) 0)) 0 (List.range (hi + 1 - lo))

theorem Hex.GraphIso.Nauty.worksetOfL_eq {n : Nat} (lab : Array Nat) (lo hi : Nat) : worksetOfL n lab.toList lo hi = (worksetOf n lab lo hi).toNat

def Hex.GraphIso.Nauty.countsOfL (ctx : CtxL) (lab : List Nat) (workset cell1 cell2 : Nat) : List Nat

Equations

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

theorem Hex.GraphIso.Nauty.countsOfL_eq {n : Nat} (ctx : Ctx n) (lab : Array Nat) (workset : VSet n) (cell1 cell2 : Nat) : countsOfL ctx.toL lab.toList workset.toNat cell1 cell2 = countsOf ctx lab workset cell1 cell2

def Hex.GraphIso.Nauty.windowStepL (nn level cell1 cell2 v c1 c2 : Nat) (maxcell : Int) (st : RefineStL) : RefineStL

Equations

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

theorem Hex.GraphIso.Nauty.windowStepL_eq {n : Nat} (level cell1 cell2 v c1 c2 : Nat) (maxcell : Int) (st : RefineSt n) : windowStepL n level cell1 cell2 v c1 c2 maxcell st.toL = (windowStep level cell1 cell2 v c1 c2 maxcell st).toL

def Hex.GraphIso.Nauty.windowScanL (nn level cell1 cell2 : Nat) (counts : List Nat) : List Nat → Nat → Int → RefineStL → RefineStL

Equations

• One or more equations did not get rendered due to their size.
• Hex.GraphIso.Nauty.windowScanL nn level cell1 cell2 counts [] x✝² x✝¹ x✝ = x✝

theorem Hex.GraphIso.Nauty.windowScanL_eq {n : Nat} (level cell1 cell2 : Nat) (counts vs : List Nat) (c1 : Nat) (maxcell : Int) (st : RefineSt n) : windowScanL n level cell1 cell2 counts vs c1 maxcell st.toL = (windowScan level cell1 cell2 counts vs c1 maxcell st).toL

def Hex.GraphIso.Nauty.segmentOfL (lab : List Nat) (cell1 : Nat) (counts values : List Nat) : List Nat

Equations

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

theorem Hex.GraphIso.Nauty.segmentOfL_eq (lab : Array Nat) (cell1 : Nat) (counts values : List Nat) : segmentOfL lab.toList cell1 counts values = segmentOf lab cell1 counts values

def Hex.GraphIso.Nauty.writeSegmentL (lab : List Nat) (cell1 : Nat) : List Nat → List Nat

Equations

• Hex.GraphIso.Nauty.writeSegmentL lab cell1 [] = lab
• Hex.GraphIso.Nauty.writeSegmentL lab cell1 (x_1 :: rest) = Hex.GraphIso.Nauty.writeSegmentL (lab.set cell1 x_1) (cell1 + 1) rest

theorem Hex.GraphIso.Nauty.writeSegmentL_eq (seg : List Nat) (lab : Array Nat) (cell1 : Nat) : writeSegmentL lab.toList cell1 seg = (writeSegment lab cell1 seg).toList

def Hex.GraphIso.Nauty.nontrivialFixL (nn cell1 : Nat) (st : RefineStL) : RefineStL

Equations

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

theorem Hex.GraphIso.Nauty.nontrivialFixL_eq {n : Nat} (cell1 : Nat) (st : RefineSt n) : nontrivialFixL n cell1 st.toL = (nontrivialFix cell1 st).toL

def Hex.GraphIso.Nauty.nontrivialCellL (ctx : CtxL) (level workset cell1 cell2 : Nat) (st : RefineStL) : RefineStL

Equations

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

theorem Hex.GraphIso.Nauty.nontrivialCellL_eq {n : Nat} (ctx : Ctx n) (level : Nat) (workset : VSet n) (cell1 cell2 : Nat) (st : RefineSt n) : nontrivialCellL ctx.toL level workset.toNat cell1 cell2 st.toL = (nontrivialCell ctx level workset cell1 cell2 st).toL

def Hex.GraphIso.Nauty.refineNontrivialGoL (ctx : CtxL) (level workset : Nat) : List (Nat × Nat) → RefineStL → RefineStL

Equations

• One or more equations did not get rendered due to their size.
• Hex.GraphIso.Nauty.refineNontrivialGoL ctx level workset [] x✝ = x✝

def Hex.GraphIso.Nauty.refineNontrivialL (ctx : CtxL) (level split1 split2 : Nat) (st : RefineStL) : RefineStL

Equations

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

theorem Hex.GraphIso.Nauty.refineNontrivialGoL_eq {n : Nat} (ctx : Ctx n) (level : Nat) (workset : VSet n) (cs : List (Nat × Nat)) (st : RefineSt n) : refineNontrivialGoL ctx.toL level workset.toNat cs st.toL = (refineNontrivial.go ctx level workset cs st).toL

theorem Hex.GraphIso.Nauty.refineNontrivialL_eq {n : Nat} (ctx : Ctx n) (level split1 split2 : Nat) (st : RefineSt n) : refineNontrivialL ctx.toL level split1 split2 st.toL = (refineNontrivial ctx level split1 split2 st).toL

def Hex.GraphIso.Nauty.refineStepL (ctx : CtxL) (level split1 : Nat) (st : RefineStL) : RefineStL

Equations

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

theorem Hex.GraphIso.Nauty.refineStepL_eq {n : Nat} (ctx : Ctx n) (level split1 : Nat) (st : RefineSt n) : refineStepL ctx.toL level split1 st.toL = (refineStep ctx level split1 st).toL

def Hex.GraphIso.Nauty.pickSplitL (active hint : Nat) : Option Nat

pickSplit over a bitset active set.

Equations

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

theorem Hex.GraphIso.Nauty.pickSplitL_eq {n : Nat} (active : VSet n) (hint : Nat) : pickSplitL active.toNat hint = pickSplit active hint

def Hex.GraphIso.Nauty.refineLoopL (ctx : CtxL) (level : Nat) : Nat → RefineStL → RefineStL

Equations

• One or more equations did not get rendered due to their size.
• Hex.GraphIso.Nauty.refineLoopL ctx level 0 x✝ = x✝

theorem Hex.GraphIso.Nauty.refineLoopL_eq {n : Nat} (ctx : Ctx n) (level fuel : Nat) (st : RefineSt n) : refineLoopL ctx.toL level fuel st.toL = (refineLoop ctx level fuel st).toL

def Hex.GraphIso.Nauty.refineL (ctx : CtxL) (level : Nat) (lab ptn : List Nat) (active numcells : Nat) : RefineStL

Equations

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

theorem Hex.GraphIso.Nauty.refineL_eq {n : Nat} (ctx : Ctx n) (level : Nat) (lab ptn : Array Nat) (active : VSet n) (numcells : Nat) : refineL ctx.toL level lab.toList ptn.toList active.toNat numcells = (refine ctx level lab ptn active numcells).toL

def Hex.GraphIso.Nauty.discreteAtL (ptn : List Nat) (level nn : Nat) : Bool

Equations

• Hex.GraphIso.Nauty.discreteAtL ptn level nn = (Hex.GraphIso.Nauty.cellsL ptn level nn).all fun (p : Nat × Nat) => p.fst == p.snd

theorem Hex.GraphIso.Nauty.discreteAtL_eq (ptn : Array Nat) (level nn : Nat) : discreteAtL ptn.toList level nn = discreteAt ptn level nn

def Hex.GraphIso.Nauty.joinTestL (ctx : CtxL) (lab : List Nat) (wset c1 c2 : Nat) : Bool

Equations

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

theorem Hex.GraphIso.Nauty.joinTestL_eq {n : Nat} (ctx : Ctx n) (lab : Array Nat) (wset : VSet n) (c1 c2 : Nat) : joinTestL ctx.toL lab.toList wset.toNat c1 c2 = joinTest ctx lab wset c1 c2

def Hex.GraphIso.Nauty.specBestcellRowL (ctx : CtxL) (lab ptn : List Nat) (level : Nat) (startArr : List Nat) (workset v2 : Nat) : List Nat → List Nat → List Nat

Equations

• One or more equations did not get rendered due to their size.
• Hex.GraphIso.Nauty.specBestcellRowL ctx lab ptn level startArr workset v2 [] x✝ = x✝

theorem Hex.GraphIso.Nauty.specBestcellRowL_eq {n : Nat} (ctx : Ctx n) (lab ptn : Array Nat) (level : Nat) (startArr : Array Nat) (workset : VSet n) (v2 : Nat) (vs : List Nat) (bucket : Array Nat) : specBestcellRowL ctx.toL lab.toList ptn.toList level startArr.toList workset.toNat v2 vs bucket.toList = (specBestcellRow ctx lab ptn level startArr workset v2 vs bucket).toList

def Hex.GraphIso.Nauty.specBestcellRowsL (ctx : CtxL) (lab ptn : List Nat) (level : Nat) (startArr : List Nat) : List Nat → List Nat → List Nat

Equations

• One or more equations did not get rendered due to their size.
• Hex.GraphIso.Nauty.specBestcellRowsL ctx lab ptn level startArr [] x✝ = x✝

theorem Hex.GraphIso.Nauty.specBestcellRowsL_eq {n : Nat} (ctx : Ctx n) (lab ptn : Array Nat) (level : Nat) (startArr : Array Nat) (vs : List Nat) (bucket : Array Nat) : specBestcellRowsL ctx.toL lab.toList ptn.toList level startArr.toList vs bucket.toList = (specBestcellRows ctx lab ptn level startArr vs bucket).toList

def Hex.GraphIso.Nauty.argmaxLoopL (bucket : List Nat) : List Nat → Nat → Nat → Nat

Equations

• One or more equations did not get rendered due to their size.
• Hex.GraphIso.Nauty.argmaxLoopL bucket [] x✝¹ x✝ = x✝¹

theorem Hex.GraphIso.Nauty.argmaxLoopL_eq (bucket : Array Nat) (vs : List Nat) (v1 v2 : Nat) : argmaxLoopL bucket.toList vs v1 v2 = argmaxLoop bucket vs v1 v2

def Hex.GraphIso.Nauty.specBestcellL (ctx : CtxL) (lab ptn : List Nat) (level : Nat) : Nat

Equations

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

theorem Hex.GraphIso.Nauty.specBestcellL_eq {n : Nat} (ctx : Ctx n) (lab ptn : Array Nat) (level : Nat) : specBestcellL ctx.toL lab.toList ptn.toList level = specBestcell ctx lab ptn level

def Hex.GraphIso.Nauty.specTargetcellL (ctx : CtxL) (lab ptn : List Nat) (level tcLevel : Nat) : Nat

Equations

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

theorem Hex.GraphIso.Nauty.specTargetcellL_eq {n : Nat} (ctx : Ctx n) (lab ptn : Array Nat) (level tcLevel : Nat) : specTargetcellL ctx.toL lab.toList ptn.toList level tcLevel = specTargetcell ctx lab ptn level tcLevel

def Hex.GraphIso.Nauty.specMaketargetcellL (ctx : CtxL) (lab ptn : List Nat) (level tcLevel : Nat) : Nat × Nat × Nat

Equations

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

theorem Hex.GraphIso.Nauty.specMaketargetcellL_eq {n : Nat} (ctx : Ctx n) (lab ptn : Array Nat) (level tcLevel : Nat) : specMaketargetcellL ctx.toL lab.toList ptn.toList level tcLevel = ((specMaketargetcell ctx lab ptn level tcLevel).fst, (specMaketargetcell ctx lab ptn level tcLevel).snd.fst.toNat, (specMaketargetcell ctx lab ptn level tcLevel).snd.snd)

def Hex.GraphIso.Nauty.breakoutGoL (tv : Nat) : Nat → List Nat → Nat → Nat → List Nat

Equations

• One or more equations did not get rendered due to their size.
• Hex.GraphIso.Nauty.breakoutGoL tv 0 x✝² x✝¹ x✝ = x✝²

def Hex.GraphIso.Nauty.breakoutL (nn : Nat) (lab ptn : List Nat) (level tc tv : Nat) : List Nat × List Nat × Nat

Equations

• Hex.GraphIso.Nauty.breakoutL nn lab ptn level tc tv = (Hex.GraphIso.Nauty.breakoutGoL tv (lab.length + 1) lab tc tv, ptn.set tc level, Hex.GraphIso.Nauty.NatSet.insert nn 0 tc)

theorem Hex.GraphIso.Nauty.breakoutGoL_eq (tv fuel : Nat) (lab : Array Nat) (i prev : Nat) : breakoutGoL tv fuel lab.toList i prev = (breakout.go tv fuel lab i prev).toList

theorem Hex.GraphIso.Nauty.breakoutL_eq {n : Nat} (lab ptn : Array Nat) (level tc tv : Nat) : breakoutL n lab.toList ptn.toList level tc tv = ((breakout n lab ptn level tc tv).fst.toList, (breakout n lab ptn level tc tv).snd.fst.toList, (breakout n lab ptn level tc tv).snd.snd.toNat)

def Hex.GraphIso.Nauty.segNL (lab : List Nat) (lo len : Nat) : List Nat

Equations

• Hex.GraphIso.Nauty.segNL lab lo len = List.map (fun (o : Nat) => Hex.GraphIso.atD lab (lo + o) 0) (List.range len)

theorem Hex.GraphIso.Nauty.segNL_eq (lab : Array Nat) (lo len : Nat) : segNL lab.toList lo len = segN lab lo len

def Hex.GraphIso.Nauty.checkCellsPermL (ptn lab₁ lab₂' : List Nat) (level nn : Nat) : Bool

Equations

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

theorem Hex.GraphIso.Nauty.checkCellsPermL_eq (ptn lab₁ lab₂' : Array Nat) (level nn : Nat) : checkCellsPermL ptn.toList lab₁.toList lab₂'.toList level nn = checkCellsPerm ptn lab₁ lab₂' level nn

def Hex.GraphIso.Nauty.invPermGoL : List Nat → List Nat → List Nat → List Nat

Equations

• Hex.GraphIso.Nauty.invPermGoL x✝¹ [] x✝ = x✝
• Hex.GraphIso.Nauty.invPermGoL x✝¹ (i :: rest) x✝ = Hex.GraphIso.Nauty.invPermGoL x✝¹ rest (x✝.set (Hex.GraphIso.atD x✝¹ i 0) i)

def Hex.GraphIso.Nauty.invPermL (lab : List Nat) : List Nat

Equations

• Hex.GraphIso.Nauty.invPermL lab = Hex.GraphIso.Nauty.invPermGoL lab (List.range lab.length) (List.replicate lab.length 0)

theorem Hex.GraphIso.Nauty.invPermGoL_eq (lab : Array Nat) (idx : List Nat) (inv : Array Nat) : invPermGoL lab.toList idx inv.toList = (invPerm.go lab idx inv).toList

theorem Hex.GraphIso.Nauty.invPermL_eq (lab : Array Nat) : invPermL lab.toList = (invPerm lab).toList

def Hex.GraphIso.Nauty.permsetL (s : Nat) (perm : List Nat) (nn : Nat) : Nat

Equations

• Hex.GraphIso.Nauty.permsetL s perm nn = Hex.GraphIso.Nauty.NatSet.image nn (fun (v : Nat) => Hex.GraphIso.atD perm v 0) s

theorem Hex.GraphIso.Nauty.permsetL_eq {n : Nat} (s : VSet n) (perm : Array Nat) : permsetL s.toNat perm.toList n = (s.permset perm).toNat

def Hex.GraphIso.Nauty.leafRowsL (ctx : CtxL) (lab : List Nat) : List Nat

Equations

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

theorem Hex.GraphIso.Nauty.leafRowsL_eq {n : Nat} (ctx : Ctx n) (lab : Array Nat) : leafRowsL ctx.toL lab.toList = List.map VSet.toNat (leafRows ctx lab)

def Hex.GraphIso.Nauty.Key.toL {n : Nat} (B : Key n) : Kernel.Key

The literal reading of a packed key.

Equations

• B.toL = { codes := B.codes, rows := List.map Hex.GraphIso.Nauty.VSet.toNat B.rows }

theorem Hex.GraphIso.Nauty.toL_toKey {n : Nat} {K : Kernel.Key} (h : ∀ (r : Nat), r ∈ K.rows → r < 2 ^ n) : (Kernel.Key.toKey n K).toL = K

def Hex.GraphIso.Nauty.keyCmpL (k1 k2 : Kernel.Key) : Ordering

Equations

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

theorem Hex.GraphIso.Nauty.listCmp_map {α β : Type} (cmp : β → β → Ordering) (f : α → β) (l1 l2 : List α) : listCmp cmp (List.map f l1) (List.map f l2) = listCmp (fun (a b : α) => cmp (f a) (f b)) l1 l2

theorem Hex.GraphIso.Nauty.keyCmpL_eq {n : Nat} (codes1 codes2 : List Nat) (rows1 rows2 : List (VSet n)) : keyCmpL { codes := codes1, rows := List.map VSet.toNat rows1 } { codes := codes2, rows := List.map VSet.toNat rows2 } = keyCmp { codes := codes1, rows := rows1 } { codes := codes2, rows := rows2 }

theorem Hex.GraphIso.Nauty.keyCmpL_toL {n : Nat} (k1 k2 : Key n) : keyCmpL k1.toL k2.toL = keyCmp k1 k2

def Hex.GraphIso.Nauty.checkDiffL (K1 K2 : Kernel.Key) : Bool

checkDiff on literal keys.

Equations

• Hex.GraphIso.Nauty.checkDiffL K1 K2 = (Hex.GraphIso.Nauty.keyCmpL K1 K2 != Ordering.eq)

theorem Hex.GraphIso.Nauty.checkDiffL_toL {n : Nat} (k1 k2 : Key n) : checkDiffL k1.toL k2.toL = checkDiff k1 k2

def Hex.GraphIso.Nauty.checkAutomL (g : List Nat) (nn : Nat) (γ : Array Nat) : Bool

checkAutom with bitset rows.

Equations

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

theorem Hex.GraphIso.Nauty.checkAutomL_eq {n : Nat} (g : Array (VSet n)) (γ : Array Nat) : checkAutomL (List.map VSet.toNat g.toList) n γ = checkAutom g γ

def Hex.GraphIso.Nauty.validGammasL (g : List Nat) (nn : Nat) (cert : CertNode) : List (Array Nat)

validGammas with bitset rows.

Equations

• Hex.GraphIso.Nauty.validGammasL g nn cert = List.filter (fun (γ : Array Nat) => Hex.GraphIso.Nauty.checkAutomL g nn γ) (Hex.GraphIso.Nauty.certGammas (nn + 2) cert [])

theorem Hex.GraphIso.Nauty.validGammasL_eq {n : Nat} (g : Array (VSet n)) (cert : CertNode) : validGammasL (List.map VSet.toNat g.toList) n cert = validGammas g cert

def Hex.GraphIso.Nauty.checkNodeL (ctx : CtxL) (tcLevel : Nat) (brows : List Nat) (vgens : List (Array Nat)) : Nat → Nat → List Nat → List Nat → Nat → Nat → CertNode → List Nat → Option Bool

Equations

• One or more equations did not get rendered due to their size.
• Hex.GraphIso.Nauty.checkNodeL ctx tcLevel brows vgens 0 x✝⁶ x✝⁵ x✝⁴ x✝³ x✝² x✝¹ x✝ = none
• Hex.GraphIso.Nauty.checkNodeL ctx tcLevel brows vgens fuel.succ x✝⁵ x✝⁴ x✝³ x✝² x✝¹ x✝ [] = none
• Hex.GraphIso.Nauty.checkNodeL ctx tcLevel brows vgens fuel.succ x✝⁴ x✝³ x✝² x✝¹ x✝ (Hex.GraphIso.Nauty.CertNode.autom o γ) (x_9 :: rest) = none

theorem Hex.GraphIso.Nauty.checkNodeL_eq {n : Nat} (ctx : Ctx n) (tcLevel : Nat) (brows : List (VSet n)) (vgens : List (Array Nat)) (fuel level : Nat) (lab ptn : Array Nat) (active : VSet n) (numcells : Nat) (cert : CertNode) (bcodes : List Nat) : checkNodeL ctx.toL tcLevel (List.map VSet.toNat brows) vgens fuel level lab.toList ptn.toList active.toNat numcells cert bcodes = checkNode ctx tcLevel brows vgens fuel level lab ptn active numcells cert bcodes

structure Hex.GraphIso.Nauty.CtxP : Type

The replay context over packed rows: w/m are the field width and mask for positions and vertices, g the rows packed with width n, and rm the row mask.

• n : Nat

  The number of vertices.

• w : Nat

  The field width of packed position and vertex vectors.

• m : Nat

  2 ^ w - 1.

• g : Nat

  The adjacency rows, row v in bits [n * v, n * (v + 1)).

• rm : Nat

  2 ^ n - 1.

structure Hex.GraphIso.Nauty.CtxRep (ctx : CtxP) (ctxL : CtxL) : Prop

The correspondence between a packed context and a list context.

• n : ctx.n = ctxL.n
• m : ctx.m = 2 ^ ctx.w - 1
• rm : ctx.rm = 2 ^ ctx.n - 1
• g : Rep ctx.n ctx.n ctx.g ctxL.g
• nlt : ctx.n + 2 < 2 ^ ctx.w

  Positions, vertices, the initial partition's infinity n + 2, and every level the replay's fuel of n reaches fit a field.

def Hex.GraphIso.Nauty.lget (ctx : CtxP) (a i : Nat) : Nat

Read a packed position or vertex vector.

Equations

• Hex.GraphIso.Nauty.lget ctx a i = Hex.GraphIso.Nauty.pget ctx.w ctx.m a i

def Hex.GraphIso.Nauty.lset (ctx : CtxP) (a i v : Nat) : Nat

Write a packed position or vertex vector.

Equations

• Hex.GraphIso.Nauty.lset ctx a i v = Hex.GraphIso.Nauty.pset ctx.w ctx.m ctx.n a i v

def Hex.GraphIso.Nauty.rowP (ctx : CtxP) (v : Nat) : Nat

The row of vertex v.

Equations

• Hex.GraphIso.Nauty.rowP ctx v = Hex.GraphIso.Nauty.pget ctx.n ctx.rm ctx.g v

theorem Hex.GraphIso.Nauty.lget_eq {ctx : CtxP} {ctxL : CtxL} (h : CtxRep ctx ctxL) {a : Nat} {l : List Nat} (hr : Rep ctx.w ctx.n a l) (i : Nat) : lget ctx a i = atD l i 0

theorem Hex.GraphIso.Nauty.lget_lt {ctx : CtxP} {ctxL : CtxL} (h : CtxRep ctx ctxL) (a i : Nat) : lget ctx a i < 2 ^ ctx.w

theorem Hex.GraphIso.Nauty.lset_rep {ctx : CtxP} {ctxL : CtxL} (h : CtxRep ctx ctxL) {a : Nat} {l : List Nat} (hr : Rep ctx.w ctx.n a l) (i : Nat) {v : Nat} (hv : v < 2 ^ ctx.w) : Rep ctx.w ctx.n (lset ctx a i v) (l.set i v)

theorem Hex.GraphIso.Nauty.rowP_eq {ctx : CtxP} {ctxL : CtxL} (h : CtxRep ctx ctxL) (v : Nat) : rowP ctx v = atD ctxL.g v 0

structure Hex.GraphIso.Nauty.RefineStP : Type

RefineSt with packed labelling and partition.

• lab : Nat
• ptn : Nat
• active : Nat
• numcells : Nat
• hint : Nat
• maxpos : Nat
• longcode : Nat

structure Hex.GraphIso.Nauty.RepSt (w n : Nat) (st : RefineStP) (stL : RefineStL) : Prop

The correspondence between packed and list refine states.

• lab : Rep w n st.lab stL.lab
• ptn : Rep w n st.ptn stL.ptn
• active : st.active = stL.active
• numcells : st.numcells = stL.numcells
• hint : st.hint = stL.hint
• maxpos : st.maxpos = stL.maxpos
• longcode : st.longcode = stL.longcode

theorem Hex.GraphIso.Nauty.RepSt.mk' {w n : Nat} {st : RefineStP} {stL : RefineStL} (hlab : Rep w n st.lab stL.lab) (hptn : Rep w n st.ptn stL.ptn) (hrest : st.active = stL.active ∧ st.numcells = stL.numcells ∧ st.hint = stL.hint ∧ st.maxpos = stL.maxpos ∧ st.longcode = stL.longcode) : RepSt w n st stL

RepSt from the two packed correspondences and the scalar field equalities in one conjunction.

theorem Hex.GraphIso.Nauty.cond_and {α : Type} (a b : Bool) (x y : α) : (bif a && b then x else y) = if a = true ∧ b = true then x else y

theorem Hex.GraphIso.Nauty.cond_or {α : Type} (a b : Bool) (x y : α) : (bif a || b then x else y) = if a = true ∨ b = true then x else y

def Hex.GraphIso.Nauty.maxK (a b : Nat) : Nat

Nat.max, raw.

Equations

• Hex.GraphIso.Nauty.maxK a b = bif a.ble b then b else a

theorem Hex.GraphIso.Nauty.maxK_eq (a b : Nat) : maxK a b = a.max b

def Hex.GraphIso.Nauty.minK (a b : Nat) : Nat

Nat.min, raw.

Equations

• Hex.GraphIso.Nauty.minK a b = bif a.ble b then a else b

theorem Hex.GraphIso.Nauty.minK_eq (a b : Nat) : minK a b = a.min b

def Hex.GraphIso.Nauty.multOfK (counts : List Nat) (v : Nat) : Nat

multOf, raw.

Equations

• Hex.GraphIso.Nauty.multOfK counts v = Hex.GraphIso.Nauty.multOfK.go v counts 0

def Hex.GraphIso.Nauty.multOfK.go (v : Nat) : List Nat → Nat → Nat

Equations

• Hex.GraphIso.Nauty.multOfK.go v [] a✝ = a✝
• Hex.GraphIso.Nauty.multOfK.go v (c :: rest) a✝ = Hex.GraphIso.Nauty.multOfK.go v rest (bif c.beq v then a✝.add 1 else a✝)

theorem Hex.GraphIso.Nauty.multOfK_go_eq (v : Nat) (counts : List Nat) (acc : Nat) : multOfK.go v counts acc = List.countP.go (fun (x : Nat) => x == v) counts acc

theorem Hex.GraphIso.Nauty.multOfK_eq (counts : List Nat) (v : Nat) : multOfK counts v = multOf counts v

def Hex.GraphIso.Nauty.countValuesK (counts : List Nat) : List Nat

countValues, raw.

Equations

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

theorem Hex.GraphIso.Nauty.countValuesK_eq (counts : List Nat) : countValuesK counts = countValues counts

def Hex.GraphIso.Nauty.pickSplitK (active hint : Nat) : Option Nat

pickSplit, raw.

Equations

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

theorem Hex.GraphIso.Nauty.pickSplitK_eq (active hint : Nat) : pickSplitK active hint = pickSplitL active hint

theorem Hex.GraphIso.Nauty.popCount_le_of_lt {nn s : Nat} (hs : s < 2 ^ nn) : popCount s ≤ nn

The bound on a bit set's population.

def Hex.GraphIso.Nauty.cellEndGoP (ctx : CtxP) (ptn level fuel : Nat) : Nat → Nat

Equations

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

theorem Hex.GraphIso.Nauty.cellEndGoP_succ (ctx : CtxP) (ptn level fuel j : Nat) : cellEndGoP ctx ptn level (fuel + 1) j = bif level.blt (lget ctx ptn j) then cellEndGoP ctx ptn level fuel (j.add 1) else j

def Hex.GraphIso.Nauty.cellEndP (ctx : CtxP) (ptn level i : Nat) : Nat

Equations

• Hex.GraphIso.Nauty.cellEndP ctx ptn level i = Hex.GraphIso.Nauty.cellEndGoP ctx ptn level (ctx.n.sub i) i

theorem Hex.GraphIso.Nauty.cellEndGoP_eq {ctx : CtxP} {ctxL : CtxL} (h : CtxRep ctx ctxL) {ptnP : Nat} {ptn : List Nat} (hp : Rep ctx.w ctx.n ptnP ptn) (level fuel j : Nat) : cellEndGoP ctx ptnP level fuel j = cellEndGoL ptn level fuel j

theorem Hex.GraphIso.Nauty.cellEndP_eq {ctx : CtxP} {ctxL : CtxL} (h : CtxRep ctx ctxL) {ptnP : Nat} {ptn : List Nat} (hp : Rep ctx.w ctx.n ptnP ptn) (level i : Nat) : cellEndP ctx ptnP level i = cellEndL ptn level i

def Hex.GraphIso.Nauty.cellsGoP (ctx : CtxP) (ptn level fuel : Nat) : Nat → List (Nat × Nat)

Equations

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

theorem Hex.GraphIso.Nauty.cellsGoP_succ (ctx : CtxP) (ptn level fuel c1 : Nat) : cellsGoP ctx ptn level (fuel + 1) c1 = bif c1.blt ctx.n then have c2 := cellEndP ctx ptn level c1; (c1, c2) :: cellsGoP ctx ptn level fuel (c2.add 1) else []

def Hex.GraphIso.Nauty.cellsP (ctx : CtxP) (ptn level : Nat) : List (Nat × Nat)

Equations

• Hex.GraphIso.Nauty.cellsP ctx ptn level = Hex.GraphIso.Nauty.cellsGoP ctx ptn level ctx.n 0

theorem Hex.GraphIso.Nauty.cellsGoP_eq {ctx : CtxP} {ctxL : CtxL} (h : CtxRep ctx ctxL) {ptnP : Nat} {ptn : List Nat} (hp : Rep ctx.w ctx.n ptnP ptn) (level fuel c1 : Nat) : cellsGoP ctx ptnP level fuel c1 = cellsGoL ptn level ctxL.n fuel c1

theorem Hex.GraphIso.Nauty.cellsP_eq {ctx : CtxP} {ctxL : CtxL} (h : CtxRep ctx ctxL) {ptnP : Nat} {ptn : List Nat} (hp : Rep ctx.w ctx.n ptnP ptn) (level : Nat) : cellsP ctx ptnP level = cellsL ptn level ctxL.n

def Hex.GraphIso.Nauty.splitCellLoopP (ctx : CtxP) (gRow fuel : Nat) : Nat → Nat → Nat → Nat × Nat × Nat

The two-pointer partition with d = c2 + 1, so the right pointer stays a natural (d = 0 is nauty's c2 = -1).

Equations

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

theorem Hex.GraphIso.Nauty.splitCellLoopP_zero (ctx : CtxP) (gRow lab c1 d : Nat) : splitCellLoopP ctx gRow 0 lab c1 d = (lab, c1, d)

theorem Hex.GraphIso.Nauty.splitCellLoopP_succ (ctx : CtxP) (gRow fuel lab c1 d : Nat) : splitCellLoopP ctx gRow (fuel + 1) lab c1 d = bif c1.blt d then bif elemK gRow (lget ctx lab c1) then splitCellLoopP ctx gRow fuel lab (c1.add 1) d else splitCellLoopP ctx gRow fuel (lset ctx (lset ctx lab c1 (lget ctx lab (d.sub 1))) (d.sub 1) (lget ctx lab c1)) c1 (d.sub 1) else (lab, c1, d)

theorem Hex.GraphIso.Nauty.splitCellLoopP_eq {ctx : CtxP} {ctxL : CtxL} (h : CtxRep ctx ctxL) (gRow fuel : Nat) {labP : Nat} {lab : List Nat} : Rep ctx.w ctx.n labP lab → ∀ (c1 d : Nat), Rep ctx.w ctx.n (splitCellLoopP ctx gRow fuel labP c1 d).fst (splitCellLoopL gRow fuel lab (↑c1) (↑d - 1)).fst ∧ ↑(splitCellLoopP ctx gRow fuel labP c1 d).snd.fst = (splitCellLoopL gRow fuel lab (↑c1) (↑d - 1)).snd.fst ∧ ↑(splitCellLoopP ctx gRow fuel labP c1 d).snd.snd = (splitCellLoopL gRow fuel lab (↑c1) (↑d - 1)).snd.snd + 1

def Hex.GraphIso.Nauty.trivialSplitP (ctx : CtxP) (level cell1 cell2 c1 d : Nat) (st : RefineStP) : RefineStP

Equations

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

theorem Hex.GraphIso.Nauty.trivialSplitP_eq {ctx : CtxP} {ctxL : CtxL} (h : CtxRep ctx ctxL) {level : Nat} (hlev : level < 2 ^ ctx.w) (cell1 cell2 c1 d : Nat) {st : RefineStP} {stL : RefineStL} (hst : RepSt ctx.w ctx.n st stL) : RepSt ctx.w ctx.n (trivialSplitP ctx level cell1 cell2 c1 d st) (trivialSplitL ctxL.n level cell1 cell2 (↑c1) (↑d - 1) stL)

def Hex.GraphIso.Nauty.trivialCellP (ctx : CtxP) (level gRow cell1 cell2 : Nat) (st : RefineStP) : RefineStP

Equations

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

theorem Hex.GraphIso.Nauty.trivialCellP_eq {ctx : CtxP} {ctxL : CtxL} (h : CtxRep ctx ctxL) {level : Nat} (hlev : level < 2 ^ ctx.w) (gRow cell1 cell2 : Nat) {st : RefineStP} {stL : RefineStL} (hst : RepSt ctx.w ctx.n st stL) : RepSt ctx.w ctx.n (trivialCellP ctx level gRow cell1 cell2 st) (trivialCellL ctxL.n level gRow cell1 cell2 stL)

def Hex.GraphIso.Nauty.refineTrivialGoP (ctx : CtxP) (level gRow : Nat) : List (Nat × Nat) → RefineStP → RefineStP

Equations

• One or more equations did not get rendered due to their size.
• Hex.GraphIso.Nauty.refineTrivialGoP ctx level gRow [] x✝ = x✝

def Hex.GraphIso.Nauty.refineTrivialP (ctx : CtxP) (level split1 : Nat) (st : RefineStP) : RefineStP

Equations

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

theorem Hex.GraphIso.Nauty.refineTrivialGoP_eq {ctx : CtxP} {ctxL : CtxL} (h : CtxRep ctx ctxL) {level : Nat} (hlev : level < 2 ^ ctx.w) (gRow : Nat) (cs : List (Nat × Nat)) {st : RefineStP} {stL : RefineStL} : RepSt ctx.w ctx.n st stL → RepSt ctx.w ctx.n (refineTrivialGoP ctx level gRow cs st) (refineTrivialGoL ctxL.n level gRow cs stL)

theorem Hex.GraphIso.Nauty.refineTrivialP_eq {ctx : CtxP} {ctxL : CtxL} (h : CtxRep ctx ctxL) {level : Nat} (hlev : level < 2 ^ ctx.w) (split1 : Nat) {st : RefineStP} {stL : RefineStL} (hst : RepSt ctx.w ctx.n st stL) : RepSt ctx.w ctx.n (refineTrivialP ctx level split1 st) (refineTrivialL ctxL level split1 stL)

def Hex.GraphIso.Nauty.worksetOfP (ctx : CtxP) (lab lo hi : Nat) : Nat

Equations

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

theorem Hex.GraphIso.Nauty.worksetOfP_eq {ctx : CtxP} {ctxL : CtxL} (h : CtxRep ctx ctxL) {labP : Nat} {lab : List Nat} (hl : Rep ctx.w ctx.n labP lab) (lo hi : Nat) : worksetOfP ctx labP lo hi = worksetOfL ctxL.n lab lo hi

def Hex.GraphIso.Nauty.countsOfP (ctx : CtxP) (lab workset cell1 cell2 : Nat) : List Nat

Equations

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

theorem Hex.GraphIso.Nauty.countsOfP_eq {ctx : CtxP} {ctxL : CtxL} (h : CtxRep ctx ctxL) {labP : Nat} {lab : List Nat} (hl : Rep ctx.w ctx.n labP lab) (workset cell1 cell2 : Nat) : countsOfP ctx labP workset cell1 cell2 = countsOfL ctxL lab workset cell1 cell2

def Hex.GraphIso.Nauty.windowStepP (ctx : CtxP) (level cell1 cell2 v c1 c2 maxcell1 : Nat) (st : RefineStP) : RefineStP

windowStep with maxcell1 = maxcell + 1, so nauty's -1 seed is 0.

Equations

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

theorem Hex.GraphIso.Nauty.windowStepP_eq {ctx : CtxP} {ctxL : CtxL} (h : CtxRep ctx ctxL) {level : Nat} (hlev : level < 2 ^ ctx.w) (cell1 cell2 v c1 c2 maxcell1 : Nat) (maxcell : Int) (hmax : ↑maxcell1 = maxcell + 1) {st : RefineStP} {stL : RefineStL} (hst : RepSt ctx.w ctx.n st stL) : RepSt ctx.w ctx.n (windowStepP ctx level cell1 cell2 v c1 c2 maxcell1 st) (windowStepL ctxL.n level cell1 cell2 v c1 c2 maxcell stL)

def Hex.GraphIso.Nauty.windowScanP (ctx : CtxP) (level cell1 cell2 : Nat) (counts : List Nat) : List Nat → Nat → Nat → RefineStP → RefineStP

Equations

• One or more equations did not get rendered due to their size.
• Hex.GraphIso.Nauty.windowScanP ctx level cell1 cell2 counts [] x✝² x✝¹ x✝ = x✝

theorem Hex.GraphIso.Nauty.windowScanP_eq {ctx : CtxP} {ctxL : CtxL} (h : CtxRep ctx ctxL) {level : Nat} (hlev : level < 2 ^ ctx.w) (cell1 cell2 : Nat) (counts vs : List Nat) (c1 maxcell1 : Nat) (maxcell : Int) : ↑maxcell1 = maxcell + 1 → ∀ {st : RefineStP} {stL : RefineStL}, RepSt ctx.w ctx.n st stL → RepSt ctx.w ctx.n (windowScanP ctx level cell1 cell2 counts vs c1 maxcell1 st) (windowScanL ctxL.n level cell1 cell2 counts vs c1 maxcell stL)

def Hex.GraphIso.Nauty.segmentOfP (ctx : CtxP) (lab cell1 : Nat) (counts values : List Nat) : List Nat

Equations

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

theorem Hex.GraphIso.Nauty.segmentOfP_eq {ctx : CtxP} {ctxL : CtxL} (h : CtxRep ctx ctxL) {labP : Nat} {lab : List Nat} (hl : Rep ctx.w ctx.n labP lab) (cell1 : Nat) (counts values : List Nat) : segmentOfP ctx labP cell1 counts values = segmentOfL lab cell1 counts values

theorem Hex.GraphIso.Nauty.segmentOfP_small {ctx : CtxP} {ctxL : CtxL} (h : CtxRep ctx ctxL) (labP cell1 : Nat) (counts values : List Nat) : Small ctx.w (segmentOfP ctx labP cell1 counts values)

def Hex.GraphIso.Nauty.writeSegmentP (ctx : CtxP) (lab cell1 : Nat) : List Nat → Nat

Equations

• Hex.GraphIso.Nauty.writeSegmentP ctx lab cell1 [] = lab
• Hex.GraphIso.Nauty.writeSegmentP ctx lab cell1 (x_1 :: rest) = Hex.GraphIso.Nauty.writeSegmentP ctx (Hex.GraphIso.Nauty.lset ctx lab cell1 x_1) (cell1.add 1) rest

theorem Hex.GraphIso.Nauty.writeSegmentP_rep {ctx : CtxP} {ctxL : CtxL} (h : CtxRep ctx ctxL) (seg : List Nat) : Small ctx.w seg → ∀ {labP : Nat} {lab : List Nat}, Rep ctx.w ctx.n labP lab → ∀ (cell1 : Nat), Rep ctx.w ctx.n (writeSegmentP ctx labP cell1 seg) (writeSegmentL lab cell1 seg)

def Hex.GraphIso.Nauty.nontrivialFixP (n cell1 : Nat) (st : RefineStP) : RefineStP

Equations

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

theorem Hex.GraphIso.Nauty.nontrivialFixP_eq {ctx : CtxP} {ctxL : CtxL} (h : CtxRep ctx ctxL) (cell1 : Nat) {st : RefineStP} {stL : RefineStL} (hst : RepSt ctx.w ctx.n st stL) : RepSt ctx.w ctx.n (nontrivialFixP ctx.n cell1 st) (nontrivialFixL ctxL.n cell1 stL)

def Hex.GraphIso.Nauty.nontrivialCellP (ctx : CtxP) (level workset cell1 cell2 : Nat) (st : RefineStP) : RefineStP

Equations

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

theorem Hex.GraphIso.Nauty.nontrivialCellP_eq {ctx : CtxP} {ctxL : CtxL} (h : CtxRep ctx ctxL) {level : Nat} (hlev : level < 2 ^ ctx.w) (workset cell1 cell2 : Nat) {st : RefineStP} {stL : RefineStL} (hst : RepSt ctx.w ctx.n st stL) : RepSt ctx.w ctx.n (nontrivialCellP ctx level workset cell1 cell2 st) (nontrivialCellL ctxL level workset cell1 cell2 stL)

def Hex.GraphIso.Nauty.refineNontrivialGoP (ctx : CtxP) (level workset : Nat) : List (Nat × Nat) → RefineStP → RefineStP

Equations

• One or more equations did not get rendered due to their size.
• Hex.GraphIso.Nauty.refineNontrivialGoP ctx level workset [] x✝ = x✝

def Hex.GraphIso.Nauty.refineNontrivialP (ctx : CtxP) (level split1 split2 : Nat) (st : RefineStP) : RefineStP

Equations

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

theorem Hex.GraphIso.Nauty.refineNontrivialGoP_eq {ctx : CtxP} {ctxL : CtxL} (h : CtxRep ctx ctxL) {level : Nat} (hlev : level < 2 ^ ctx.w) (workset : Nat) (cs : List (Nat × Nat)) {st : RefineStP} {stL : RefineStL} : RepSt ctx.w ctx.n st stL → RepSt ctx.w ctx.n (refineNontrivialGoP ctx level workset cs st) (refineNontrivialGoL ctxL level workset cs stL)

theorem Hex.GraphIso.Nauty.refineNontrivialP_eq {ctx : CtxP} {ctxL : CtxL} (h : CtxRep ctx ctxL) {level : Nat} (hlev : level < 2 ^ ctx.w) (split1 split2 : Nat) {st : RefineStP} {stL : RefineStL} (hst : RepSt ctx.w ctx.n st stL) : RepSt ctx.w ctx.n (refineNontrivialP ctx level split1 split2 st) (refineNontrivialL ctxL level split1 split2 stL)

def Hex.GraphIso.Nauty.refineStepP (ctx : CtxP) (level split1 : Nat) (st : RefineStP) : RefineStP

Equations

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

theorem Hex.GraphIso.Nauty.refineStepP_eq {ctx : CtxP} {ctxL : CtxL} (h : CtxRep ctx ctxL) {level : Nat} (hlev : level < 2 ^ ctx.w) (split1 : Nat) {st : RefineStP} {stL : RefineStL} (hst : RepSt ctx.w ctx.n st stL) : RepSt ctx.w ctx.n (refineStepP ctx level split1 st) (refineStepL ctxL level split1 stL)

def Hex.GraphIso.Nauty.refineLoopP (ctx : CtxP) (level fuel : Nat) : RefineStP → RefineStP

Equations

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

theorem Hex.GraphIso.Nauty.refineLoopP_succ (ctx : CtxP) (level fuel : Nat) (st : RefineStP) : refineLoopP ctx level (fuel + 1) st = bif st.numcells.blt ctx.n then match pickSplitK st.active st.hint with | some split1 => refineLoopP ctx level fuel (refineStepP ctx level split1 st) | none => st else st

theorem Hex.GraphIso.Nauty.refineLoopP_eq {ctx : CtxP} {ctxL : CtxL} (h : CtxRep ctx ctxL) {level : Nat} (hlev : level < 2 ^ ctx.w) (fuel : Nat) {st : RefineStP} {stL : RefineStL} : RepSt ctx.w ctx.n st stL → RepSt ctx.w ctx.n (refineLoopP ctx level fuel st) (refineLoopL ctxL level fuel stL)

def Hex.GraphIso.Nauty.refineP (ctx : CtxP) (level lab ptn active numcells : Nat) : RefineStP

Equations

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

theorem Hex.GraphIso.Nauty.refineP_eq {ctx : CtxP} {ctxL : CtxL} (h : CtxRep ctx ctxL) {level : Nat} (hlev : level < 2 ^ ctx.w) {labP : Nat} {lab : List Nat} (hl : Rep ctx.w ctx.n labP lab) {ptnP : Nat} {ptn : List Nat} (hp : Rep ctx.w ctx.n ptnP ptn) (active numcells : Nat) : RepSt ctx.w ctx.n (refineP ctx level labP ptnP active numcells) (refineL ctxL level lab ptn active numcells)

def Hex.GraphIso.Nauty.listContainsK : List Nat → Nat → Bool

Equations

• Hex.GraphIso.Nauty.listContainsK [] x✝ = false
• Hex.GraphIso.Nauty.listContainsK (c :: rest) x✝ = bif x✝.beq c then true else Hex.GraphIso.Nauty.listContainsK rest x✝

theorem Hex.GraphIso.Nauty.listContainsK_eq (l : List Nat) (a : Nat) : listContainsK l a = l.contains a

def Hex.GraphIso.Nauty.listEraseK : List Nat → Nat → List Nat

Equations

• Hex.GraphIso.Nauty.listEraseK [] x✝ = []
• Hex.GraphIso.Nauty.listEraseK (c :: rest) x✝ = bif c.beq x✝ then rest else c :: Hex.GraphIso.Nauty.listEraseK rest x✝

theorem Hex.GraphIso.Nauty.listEraseK_eq (l : List Nat) (b : Nat) : listEraseK l b = l.erase b

def Hex.GraphIso.Nauty.isPermK : List Nat → List Nat → Bool

List.isPerm, raw.

Equations

• Hex.GraphIso.Nauty.isPermK [] x✝ = x✝.isEmpty
• Hex.GraphIso.Nauty.isPermK (a :: l₁) x✝ = (Hex.GraphIso.Nauty.listContainsK x✝ a && Hex.GraphIso.Nauty.isPermK l₁ (Hex.GraphIso.Nauty.listEraseK x✝ a))

theorem Hex.GraphIso.Nauty.isPermK_eq (l₁ l₂ : List Nat) : isPermK l₁ l₂ = l₁.isPerm l₂

theorem Hex.GraphIso.Nauty.find?_congr {α : Type} {p q : α → Bool} (l : List α) : (∀ (x : α), x ∈ l → p x = q x) → List.find? p l = List.find? q l

theorem Hex.GraphIso.Nauty.map_atD_range {α : Type} (l : List Nat) (f : Nat → α) : List.map (fun (i : Nat) => f (atD l i 0)) (List.range l.length) = List.map f l

theorem Hex.GraphIso.Nauty.map_getBang_range {γ : Array Nat} {nn : Nat} (h : γ.size = nn) : List.map (fun (v : Nat) => γ[v]!) (List.range nn) = γ.toList

def Hex.GraphIso.Nauty.discreteAtP (ctx : CtxP) (ptn level : Nat) : Bool

Equations

• Hex.GraphIso.Nauty.discreteAtP ctx ptn level = (Hex.GraphIso.Nauty.cellsP ctx ptn level).all fun (p : Nat × Nat) => p.fst.beq p.snd

theorem Hex.GraphIso.Nauty.discreteAtP_eq {ctx : CtxP} {ctxL : CtxL} (h : CtxRep ctx ctxL) {ptnP : Nat} {ptn : List Nat} (hp : Rep ctx.w ctx.n ptnP ptn) (level : Nat) : discreteAtP ctx ptnP level = discreteAtL ptn level ctxL.n

def Hex.GraphIso.Nauty.joinTestP (ctx : CtxP) (lab wset c1 c2 : Nat) : Bool

Equations

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

theorem Hex.GraphIso.Nauty.joinTestP_eq {ctx : CtxP} {ctxL : CtxL} (h : CtxRep ctx ctxL) {labP : Nat} {lab : List Nat} (hl : Rep ctx.w ctx.n labP lab) (wset c1 c2 : Nat) : joinTestP ctx labP wset c1 c2 = joinTestL ctxL lab wset c1 c2

def Hex.GraphIso.Nauty.specBestcellRowP (ctx : CtxP) (lab ptn level : Nat) (startArr : List Nat) (workset v2 : Nat) : List Nat → List Nat → List Nat

Equations

• One or more equations did not get rendered due to their size.
• Hex.GraphIso.Nauty.specBestcellRowP ctx lab ptn level startArr workset v2 [] x✝ = x✝

theorem Hex.GraphIso.Nauty.specBestcellRowP_eq {ctx : CtxP} {ctxL : CtxL} (h : CtxRep ctx ctxL) {labP : Nat} {lab : List Nat} (hl : Rep ctx.w ctx.n labP lab) {ptnP : Nat} {ptn : List Nat} (hp : Rep ctx.w ctx.n ptnP ptn) (level : Nat) (startArr : List Nat) (workset v2 : Nat) (vs bucket : List Nat) : specBestcellRowP ctx labP ptnP level startArr workset v2 vs bucket = specBestcellRowL ctxL lab ptn level startArr workset v2 vs bucket

def Hex.GraphIso.Nauty.specBestcellRowsP (ctx : CtxP) (lab ptn level : Nat) (startArr : List Nat) : List Nat → List Nat → List Nat

Equations

• One or more equations did not get rendered due to their size.
• Hex.GraphIso.Nauty.specBestcellRowsP ctx lab ptn level startArr [] x✝ = x✝

theorem Hex.GraphIso.Nauty.specBestcellRowsP_eq {ctx : CtxP} {ctxL : CtxL} (h : CtxRep ctx ctxL) {labP : Nat} {lab : List Nat} (hl : Rep ctx.w ctx.n labP lab) {ptnP : Nat} {ptn : List Nat} (hp : Rep ctx.w ctx.n ptnP ptn) (level : Nat) (startArr vs bucket : List Nat) : specBestcellRowsP ctx labP ptnP level startArr vs bucket = specBestcellRowsL ctxL lab ptn level startArr vs bucket

def Hex.GraphIso.Nauty.argmaxLoopK (bucket : List Nat) : List Nat → Nat → Nat → Nat

Equations

• One or more equations did not get rendered due to their size.
• Hex.GraphIso.Nauty.argmaxLoopK bucket [] x✝¹ x✝ = x✝¹

theorem Hex.GraphIso.Nauty.argmaxLoopK_eq (bucket vs : List Nat) (v1 v2 : Nat) : argmaxLoopK bucket vs v1 v2 = argmaxLoopL bucket vs v1 v2

def Hex.GraphIso.Nauty.specBestcellP (ctx : CtxP) (lab ptn level : Nat) : Nat

Equations

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

theorem Hex.GraphIso.Nauty.specBestcellP_eq {ctx : CtxP} {ctxL : CtxL} (h : CtxRep ctx ctxL) {labP : Nat} {lab : List Nat} (hl : Rep ctx.w ctx.n labP lab) {ptnP : Nat} {ptn : List Nat} (hp : Rep ctx.w ctx.n ptnP ptn) (level : Nat) : specBestcellP ctx labP ptnP level = specBestcellL ctxL lab ptn level

def Hex.GraphIso.Nauty.firstNontrivialP : List (Nat × Nat) → Nat

The start of the first nontrivial cell, 0 if every cell is a singleton: the target-cell rule below the tcLevel cutoff.

Equations

• Hex.GraphIso.Nauty.firstNontrivialP [] = 0
• Hex.GraphIso.Nauty.firstNontrivialP (p :: rest) = bif p.fst.beq p.snd then Hex.GraphIso.Nauty.firstNontrivialP rest else p.fst

def Hex.GraphIso.Nauty.specTargetcellP (ctx : CtxP) (lab ptn level tcLevel : Nat) : Nat

Equations

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

theorem Hex.GraphIso.Nauty.specTargetcellP_eq {ctx : CtxP} {ctxL : CtxL} (h : CtxRep ctx ctxL) {labP : Nat} {lab : List Nat} (hl : Rep ctx.w ctx.n labP lab) {ptnP : Nat} {ptn : List Nat} (hp : Rep ctx.w ctx.n ptnP ptn) (level tcLevel : Nat) : specTargetcellP ctx labP ptnP level tcLevel = specTargetcellL ctxL lab ptn level tcLevel

def Hex.GraphIso.Nauty.specMaketargetcellP (ctx : CtxP) (lab ptn level tcLevel : Nat) : Nat × Nat × Nat

Equations

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

theorem Hex.GraphIso.Nauty.specMaketargetcellP_eq {ctx : CtxP} {ctxL : CtxL} (h : CtxRep ctx ctxL) {labP : Nat} {lab : List Nat} (hl : Rep ctx.w ctx.n labP lab) {ptnP : Nat} {ptn : List Nat} (hp : Rep ctx.w ctx.n ptnP ptn) (level tcLevel : Nat) : specMaketargetcellP ctx labP ptnP level tcLevel = specMaketargetcellL ctxL lab ptn level tcLevel

def Hex.GraphIso.Nauty.breakoutGoP (ctx : CtxP) (tv fuel : Nat) : Nat → Nat → Nat → Nat

Equations

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

theorem Hex.GraphIso.Nauty.breakoutGoP_succ (ctx : CtxP) (tv fuel lab i prev : Nat) : breakoutGoP ctx tv (fuel + 1) lab i prev = have next := lget ctx lab i; have lab := lset ctx lab i prev; bif next.beq tv then lab else breakoutGoP ctx tv fuel lab (i.add 1) next

theorem Hex.GraphIso.Nauty.breakoutGoP_rep {ctx : CtxP} {ctxL : CtxL} (h : CtxRep ctx ctxL) (tv fuel : Nat) {labP : Nat} {lab : List Nat} : Rep ctx.w ctx.n labP lab → ∀ (i prev : Nat), prev < 2 ^ ctx.w → Rep ctx.w ctx.n (breakoutGoP ctx tv fuel labP i prev) (breakoutGoL tv fuel lab i prev)

def Hex.GraphIso.Nauty.breakoutP (ctx : CtxP) (lab ptn level tc tv : Nat) : Nat × Nat × Nat

Equations

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

theorem Hex.GraphIso.Nauty.breakoutP_eq {ctx : CtxP} {ctxL : CtxL} (h : CtxRep ctx ctxL) {labP : Nat} {lab : List Nat} (hl : Rep ctx.w ctx.n labP lab) {ptnP : Nat} {ptn : List Nat} (hp : Rep ctx.w ctx.n ptnP ptn) {level : Nat} (hlev : level < 2 ^ ctx.w) (tc : Nat) {tv : Nat} (htv : tv < 2 ^ ctx.w) : Rep ctx.w ctx.n (breakoutP ctx labP ptnP level tc tv).fst (breakoutL ctxL.n lab ptn level tc tv).fst ∧ Rep ctx.w ctx.n (breakoutP ctx labP ptnP level tc tv).snd.fst (breakoutL ctxL.n lab ptn level tc tv).snd.fst ∧ (breakoutP ctx labP ptnP level tc tv).snd.snd = (breakoutL ctxL.n lab ptn level tc tv).snd.snd

def Hex.GraphIso.Nauty.segNP (ctx : CtxP) (lab lo len : Nat) : List Nat

Equations

• Hex.GraphIso.Nauty.segNP ctx lab lo len = Hex.GraphIso.Nauty.mapRange len fun (o : Nat) => Hex.GraphIso.Nauty.lget ctx lab (lo.add o)

theorem Hex.GraphIso.Nauty.segNP_eq {ctx : CtxP} {ctxL : CtxL} (h : CtxRep ctx ctxL) {labP : Nat} {lab : List Nat} (hl : Rep ctx.w ctx.n labP lab) (lo len : Nat) : segNP ctx labP lo len = segNL lab lo len

def Hex.GraphIso.Nauty.mapGammaP (ctx : CtxP) (γP lab : Nat) : Nat

The packed image of a packed labelling under a packed permutation.

Equations

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

theorem Hex.GraphIso.Nauty.mapGammaP_rep {ctx : CtxP} {ctxL : CtxL} (h : CtxRep ctx ctxL) {γP : Nat} {γl : List Nat} (hg : Rep ctx.w ctx.n γP γl) {labP : Nat} {lab : List Nat} (hl : Rep ctx.w ctx.n labP lab) : Rep ctx.w ctx.n (mapGammaP ctx γP labP) (List.map (fun (v : Nat) => atD γl v 0) lab)

def Hex.GraphIso.Nauty.checkCellsPermP (ctx : CtxP) (ptn lab₁ lab₂' level : Nat) : Bool

Equations

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

theorem Hex.GraphIso.Nauty.checkCellsPermP_eq {ctx : CtxP} {ctxL : CtxL} (h : CtxRep ctx ctxL) {ptnP : Nat} {ptn : List Nat} (hp : Rep ctx.w ctx.n ptnP ptn) {lab₁P : Nat} {lab₁ : List Nat} (h1 : Rep ctx.w ctx.n lab₁P lab₁) {lab₂P : Nat} {lab₂ : List Nat} (h2 : Rep ctx.w ctx.n lab₂P lab₂) (level : Nat) : checkCellsPermP ctx ptnP lab₁P lab₂P level = checkCellsPermL ptn lab₁ lab₂ level ctxL.n

theorem Hex.GraphIso.Nauty.invPermGoL_eq_foldl (lab idx inv : List Nat) : invPermGoL lab idx inv = List.foldl (fun (inv : List Nat) (i : Nat) => inv.set (atD lab i 0) i) inv idx

theorem Hex.GraphIso.Nauty.invPermFold_rep {ctx : CtxP} {ctxL : CtxL} (h : CtxRep ctx ctxL) {labP : Nat} {lab : List Nat} (hl : Rep ctx.w ctx.n labP lab) (idx : List Nat) : (∀ (i : Nat), i ∈ idx → i < 2 ^ ctx.w) → ∀ {invP : Nat} {inv : List Nat}, Rep ctx.w ctx.n invP inv → Rep ctx.w ctx.n (List.foldl (fun (inv i : Nat) => lset ctx inv (lget ctx labP i) i) invP idx) (List.foldl (fun (inv : List Nat) (i : Nat) => inv.set (atD lab i 0) i) inv idx)

def Hex.GraphIso.Nauty.invPermP (ctx : CtxP) (lab : Nat) : Nat

Equations

• Hex.GraphIso.Nauty.invPermP ctx lab = Hex.GraphIso.Nauty.iterUp ctx.n (fun (i inv : Nat) => Hex.GraphIso.Nauty.lset ctx inv (Hex.GraphIso.Nauty.lget ctx lab i) i) 0

theorem Hex.GraphIso.Nauty.invPermP_rep {ctx : CtxP} {ctxL : CtxL} (h : CtxRep ctx ctxL) {labP : Nat} {lab : List Nat} (hl : Rep ctx.w ctx.n labP lab) : Rep ctx.w ctx.n (invPermP ctx labP) (invPermL lab)

def Hex.GraphIso.Nauty.permsetP (ctx : CtxP) (s perm : Nat) : Nat

Equations

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

theorem Hex.GraphIso.Nauty.permsetP_eq {ctx : CtxP} {ctxL : CtxL} (h : CtxRep ctx ctxL) {permP : Nat} {perm : List Nat} (hp : Rep ctx.w ctx.n permP perm) (s : Nat) : permsetP ctx s permP = permsetL s perm ctxL.n

def Hex.GraphIso.Nauty.leafRowsP (ctx : CtxP) (lab : Nat) : List Nat

Equations

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

theorem Hex.GraphIso.Nauty.leafRowsP_eq {ctx : CtxP} {ctxL : CtxL} (h : CtxRep ctx ctxL) {labP : Nat} {lab : List Nat} (hl : Rep ctx.w ctx.n labP lab) : leafRowsP ctx labP = leafRowsL ctxL lab

def Hex.GraphIso.Nauty.imageP (σ : Nat → Nat) (n s : Nat) : Nat

Equations

• Hex.GraphIso.Nauty.imageP σ n s = Hex.GraphIso.Nauty.iterUp n (fun (v t : Nat) => bif Hex.GraphIso.Nauty.elemK s v then Hex.GraphIso.Nauty.insertK n t (σ v) else t) 0

theorem Hex.GraphIso.Nauty.imageP_eq (σ : Nat → Nat) (n s : Nat) : imageP σ n s = NatSet.image n σ s

def Hex.GraphIso.Nauty.gammaOkP (ctx : CtxP) (γl : List Nat) : Bool

A candidate permutation array has n entries, all vertices.

Equations

• Hex.GraphIso.Nauty.gammaOkP ctx γl = (γl.length.beq ctx.n && γl.all fun (v : Nat) => v.blt ctx.n)

theorem Hex.GraphIso.Nauty.gammaOkP_rep {ctx : CtxP} {ctxL : CtxL} (h : CtxRep ctx ctxL) {γl : List Nat} (hok : gammaOkP ctx γl = true) : Rep ctx.w ctx.n (pack ctx.w γl) γl

def Hex.GraphIso.Nauty.checkAutomP (ctx : CtxP) (γ : Array Nat) : Bool

Equations

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

theorem Hex.GraphIso.Nauty.gammaOkP_of_checkAutom {ctx : CtxP} {nn : Nat} {g : List Nat} (h : CtxRep ctx { n := nn, g := g }) {γ : Array Nat} (hc : checkAutomL g nn γ = true) : gammaOkP ctx γ.toList = true

theorem Hex.GraphIso.Nauty.checkAutomP_eq {ctx : CtxP} {nn : Nat} {g : List Nat} (h : CtxRep ctx { n := nn, g := g }) (γ : Array Nat) : checkAutomP ctx γ = checkAutomL g nn γ

theorem Hex.GraphIso.Nauty.validGammasL_sound {g : List Nat} {nn : Nat} {cert : CertNode} {γ : Array Nat} (h : γ ∈ validGammasL g nn cert) : checkAutomL g nn γ = true

def Hex.GraphIso.Nauty.validGammasP (ctx : CtxP) (cert : CertNode) : List Nat

Equations

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

theorem Hex.GraphIso.Nauty.validGammasP_eq {ctx : CtxP} {nn : Nat} {g : List Nat} (h : CtxRep ctx { n := nn, g := g }) (cert : CertNode) : validGammasP ctx cert = List.map (fun (γ : Array Nat) => pack ctx.w γ.toList) (validGammasL g nn cert)

def Hex.GraphIso.Nauty.containsGammaP (ctx : CtxP) (vgens : List Nat) (γ : Array Nat) : Bool

Membership of a certificate's permutation among the validated generators, on packed numbers: the array must have n vertex entries (so the packing is faithful) and its packing must appear.

Equations

• Hex.GraphIso.Nauty.containsGammaP ctx vgens γ = (Hex.GraphIso.Nauty.gammaOkP ctx γ.toList && vgens.any (Hex.GraphIso.Nauty.pack ctx.w γ.toList).beq)

theorem Hex.GraphIso.Nauty.containsGamma_of_mem {vgens : List (Array Nat)} {γ : Array Nat} : γ ∈ vgens → containsGamma vgens γ = true

theorem Hex.GraphIso.Nauty.containsGammaP_eq {ctx : CtxP} {nn : Nat} {g : List Nat} (h : CtxRep ctx { n := nn, g := g }) (cert : CertNode) (γ : Array Nat) : containsGammaP ctx (validGammasP ctx cert) γ = containsGamma (validGammasL g nn cert) γ

def Hex.GraphIso.Nauty.checkNodeP (ctx : CtxP) (tcLevel : Nat) (brows vgens : List Nat) : Nat → Nat → Nat → Nat → Nat → Nat → CertNode → List Nat → Option Bool

Equations

• One or more equations did not get rendered due to their size.
• Hex.GraphIso.Nauty.checkNodeP ctx tcLevel brows vgens 0 x✝⁶ x✝⁵ x✝⁴ x✝³ x✝² x✝¹ x✝ = none
• Hex.GraphIso.Nauty.checkNodeP ctx tcLevel brows vgens fuel.succ x✝⁵ x✝⁴ x✝³ x✝² x✝¹ x✝ [] = none
• Hex.GraphIso.Nauty.checkNodeP ctx tcLevel brows vgens fuel.succ x✝⁴ x✝³ x✝² x✝¹ x✝ (Hex.GraphIso.Nauty.CertNode.autom o γ) (x_9 :: rest) = none

theorem Hex.GraphIso.Nauty.checkNodeP_eq {ctx : CtxP} {ctxL : CtxL} (h : CtxRep ctx ctxL) (tcLevel : Nat) (brows : List Nat) {vgensP : List Nat} {vgens : List (Array Nat)} (hcont : ∀ (γ : Array Nat), containsGammaP ctx vgensP γ = containsGamma vgens γ) (fuel level : Nat) : level + fuel ≤ ctx.n + 1 → ∀ {labP : Nat} {lab : List Nat}, Rep ctx.w ctx.n labP lab → ∀ {ptnP : Nat} {ptn : List Nat}, Rep ctx.w ctx.n ptnP ptn → ∀ (active numcells : Nat) (cert : CertNode) (bcodes : List Nat), checkNodeP ctx tcLevel brows vgensP fuel level labP ptnP active numcells cert bcodes = checkNodeL ctxL tcLevel brows vgens fuel level lab ptn active numcells cert bcodes

def Hex.GraphIso.initW (n : Nat) : Nat

The field width of the packed replay on n vertices: positions, vertices, the initial partition's infinity n + 2, and every level the replay fuel of n reaches fit a field.

Equations

• Hex.GraphIso.initW n = (n + 2).log2 + 1

def Hex.GraphIso.initCtx (n rows : Nat) : Nauty.CtxP

The packed context of the replay on n vertices with packed rows rows.

Equations

• Hex.GraphIso.initCtx n rows = { n := n, w := Hex.GraphIso.initW n, m := 2 ^ Hex.GraphIso.initW n - 1, g := rows, rm := 2 ^ n - 1 }

def Hex.GraphIso.initLabP {n k : Nat} (G : Colored n k) : Nat

The initial packed labelling of a coloured graph.

Equations

• Hex.GraphIso.initLabP G = Hex.GraphIso.Nauty.pack (Hex.GraphIso.initW n) (Hex.GraphIso.Nauty.initialPartition G).fst.toList

def Hex.GraphIso.initPtnP {n k : Nat} (G : Colored n k) : Nat

The initial packed partition of a coloured graph.

Equations

• Hex.GraphIso.initPtnP G = Hex.GraphIso.Nauty.pack (Hex.GraphIso.initW n) (Hex.GraphIso.Nauty.initPtn n (n + 2) (Hex.GraphIso.Nauty.initialPartition G).snd).toList

theorem Hex.GraphIso.initW_lt (n : Nat) : n + 2 < 2 ^ initW n

theorem Hex.GraphIso.initRep {n k : Nat} (G : Colored n k) (flat : List Bool) (hn0 : 0 < n) : Nauty.CtxRep (initCtx n (Nauty.pack n (flatRows n flat).toList)) { n := n, g := (flatRows n flat).toList } ∧ Nauty.Rep (initW n) n (initLabP G) (Nauty.initialPartition G).fst.toList ∧ Nauty.Rep (initW n) n (initPtnP G) (Nauty.initPtn n (n + 2) (Nauty.initialPartition G).snd).toList

The correspondences of the initial packed state with the list state the internal replay layer uses.

def Hex.GraphIso.Kernel.checkKey {n k : Nat} (G : Colored n k) (rows : Nat) (cert : Nauty.CertNode) (K : Key) : Bool

The proposition the tactic's negative route reduces in the kernel: the certificate replayed over packed state, with the rows packed once from the adjacency matrix (Kernel.packRows) and the labelling and partition packed with the field width initW n.

Equations

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

theorem Hex.GraphIso.Kernel.checkKey_eq {n k : Nat} (G : Colored n k) (cert : Nauty.CertNode) (K : Key) (h : ∀ (r : Nat), r ∈ K.rows → r < 2 ^ n) : checkKey G (packRows n G.graph.adjMatrix.data.toList) cert K = Nauty.checkKey G cert (Key.toKey n K)

Kernel.checkKey agrees with the trusted Nauty.checkKey, for a literal key whose rows are bitsets over n vertices.

def Hex.GraphIso.Kernel.certifyKey? {n k : Nat} (budget : Nat) (G : Colored n k) : Option (Nauty.CertNode × Key)

The tactic-facing certificate producer: budgeted Nauty.certifyKey? with its key read as a literal.

Equations

• Hex.GraphIso.Kernel.certifyKey? budget G = Option.map (fun (p : Hex.GraphIso.Nauty.CertNode × Hex.GraphIso.Nauty.Key n) => (p.fst, p.snd.toL)) (Hex.GraphIso.Nauty.certifyKey? G (some budget))

theorem Hex.GraphIso.Kernel.not_isomorphic_of_checkKeys {n k : Nat} {G H : Colored n k} {certG certH : Nauty.CertNode} {BG BH : Key} {NA NB : Nat} (hA : packRows n G.graph.adjMatrix.data.toList = NA) (hB : packRows n H.graph.adjMatrix.data.toList = NB) (hG : checkKey G NA certG BG = true) (hH : checkKey H NB certH BH = true) (hd : Nauty.checkDiffL BG BH = true) : ¬Isomorphic G H

Equalities identifying each graph's packed rows, plus two key certificates with differing keys, prove non-isomorphism: one kernel evaluation of the rows per graph, then one certificate replay per side.