LeanPool.TwoColoringOneRound.LowerBound.N1000000BCompressionComputeSiIntBlock6Vars0to3

theorem Distributed2Coloring.LowerBound.N1000000BCompressionCompute.siIntGoal_block6_var0 (p q : Fin 3) : SiIntGoal ⟨6, siIntGoal_block6_var0._proof_1⟩ ⟨0, siIntGoal_block6_var0._proof_2⟩ p q

theorem Distributed2Coloring.LowerBound.N1000000BCompressionCompute.siIntGoal_block6_var1 (p q : Fin 3) : SiIntGoal ⟨6, siIntGoal_block6_var0._proof_1⟩ ⟨1, siIntGoal_block6_var1._proof_1⟩ p q

theorem Distributed2Coloring.LowerBound.N1000000BCompressionCompute.siIntGoal_block6_var2 (p q : Fin 3) : SiIntGoal ⟨6, siIntGoal_block6_var0._proof_1⟩ ⟨2, siIntGoal_block6_var2._proof_1⟩ p q

theorem Distributed2Coloring.LowerBound.N1000000BCompressionCompute.siIntGoal_block6_var3 (p q : Fin 3) : SiIntGoal ⟨6, siIntGoal_block6_var0._proof_1⟩ ⟨3, siIntGoal_block6_var3._proof_1⟩ p q