LeanPool.TwoColoringOneRound.LowerBound.N1000000BCompressionComputeSiIntBlock6Vars8to11

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

theorem Distributed2Coloring.LowerBound.N1000000BCompressionCompute.siIntGoal_block6_var9 (p q : Fin 3) : SiIntGoal ⟨6, siIntGoal_block6_var8._proof_1⟩ ⟨9, siIntGoal_block6_var9._proof_1⟩ p q

theorem Distributed2Coloring.LowerBound.N1000000BCompressionCompute.siIntGoal_block6_var10 (p q : Fin 3) : SiIntGoal ⟨6, siIntGoal_block6_var8._proof_1⟩ ⟨10, siIntGoal_block6_var10._proof_1⟩ p q

theorem Distributed2Coloring.LowerBound.N1000000BCompressionCompute.siIntGoal_block6_var11 (p q : Fin 3) : SiIntGoal ⟨6, siIntGoal_block6_var8._proof_1⟩ ⟨11, siIntGoal_block6_var11._proof_1⟩ p q