LeanPool.TwoColoringOneRound.LowerBound.N1000000Witness

@[reducible, inline]

abbrev Distributed2Coloring.LowerBound.N1000000Witness.masks : Array ℕ

Imported auxiliary declaration for the 2-coloring one-round formalization.

Equations

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

@[reducible, inline]

abbrev Distributed2Coloring.LowerBound.N1000000Witness.tTr : Array ℕ

Imported auxiliary declaration for the 2-coloring one-round formalization.

Equations

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

def Distributed2Coloring.LowerBound.N1000000Witness.idIndex : ℕ

Imported auxiliary declaration for the 2-coloring one-round formalization.

Equations

• Distributed2Coloring.LowerBound.N1000000Witness.idIndex = 33

@[reducible, inline]

abbrev Distributed2Coloring.LowerBound.N1000000Witness.varToOrbitRep : Array ℕ

Imported auxiliary declaration for the 2-coloring one-round formalization.

Equations

• Distributed2Coloring.LowerBound.N1000000Witness.varToOrbitRep = #[0, 1, 2, 3, 5, 6, 7, 8, 9, 10, 11, 12, 15, 17, 18, 19, 25, 26, 27, 28, 29, 31, 32]

def Distributed2Coloring.LowerBound.N1000000Witness.edgeVar' : ℕ

Imported auxiliary declaration for the 2-coloring one-round formalization.

Equations

• Distributed2Coloring.LowerBound.N1000000Witness.edgeVar' = 11

@[reducible, inline]

abbrev Distributed2Coloring.LowerBound.N1000000Witness.LabelTriple : Type

Imported auxiliary declaration for the 2-coloring one-round formalization.

Equations

• Distributed2Coloring.LowerBound.N1000000Witness.LabelTriple = (ℕ × ℕ × ℕ)

@[reducible, inline]

abbrev Distributed2Coloring.LowerBound.N1000000Witness.varRepU : Array LabelTriple

Imported auxiliary declaration for the 2-coloring one-round formalization.

Equations

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

@[reducible, inline]

abbrev Distributed2Coloring.LowerBound.N1000000Witness.varRepV : Array LabelTriple

Imported auxiliary declaration for the 2-coloring one-round formalization.

Equations

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