Across 017500 022500 0

Kernel-checked forced assignments and closed-interval exclusions.

theorem ConwaySoifer.Simplified.Certificates.Across017500022500.excluded0_0 : Certificates.ExcludedOn (model0.B 0 ++ [step0.q]) 9000000000000 (model0.caps 0) (model0.ord 0) 0 1 200

theorem ConwaySoifer.Simplified.Certificates.Across017500022500.excluded0_1 : Certificates.ExcludedOn (model0.B 1 ++ [step0.q]) 9000000000000 (model0.caps 1) (model0.ord 1) 0 1 200

theorem ConwaySoifer.Simplified.Certificates.Across017500022500.excluded0_2 : Certificates.ExcludedOn (model0.B 2 ++ [step0.q]) 9000000000000 (model0.caps 2) (model0.ord 2) 0 1 200

theorem ConwaySoifer.Simplified.Certificates.Across017500022500.excluded0_3 : Certificates.ExcludedOn (model0.B 3 ++ [step0.q]) 9000000000000 (model0.caps 3) (model0.ord 3) 0 1 200

theorem ConwaySoifer.Simplified.Certificates.Across017500022500.excluded0_4 : Certificates.ExcludedOn (model0.B 4 ++ [step0.q]) 9000000000000 (model0.caps 4) (model0.ord 4) 0 1 200

theorem ConwaySoifer.Simplified.Certificates.Across017500022500.excluded0_5 : Certificates.ExcludedOn (model0.B 5 ++ [step0.q]) 9000000000000 (model0.caps 5) (model0.ord 5) 0 1 200

theorem ConwaySoifer.Simplified.Certificates.Across017500022500.excluded0_6 : Certificates.ExcludedOn (model0.B 6 ++ [step0.q]) 9000000000000 (model0.caps 6) (model0.ord 6) 0 1 200

theorem ConwaySoifer.Simplified.Certificates.Across017500022500.excluded0_8 : Certificates.ExcludedOn (model0.B 8 ++ [step0.q]) 9000000000000 (model0.caps 8) (model0.ord 8) 0 1 200

theorem ConwaySoifer.Simplified.Certificates.Across017500022500.excluded0_9 : Certificates.ExcludedOn (model0.B 9 ++ [step0.q]) 9000000000000 (model0.caps 9) (model0.ord 9) 0 1 200

theorem ConwaySoifer.Simplified.Certificates.Across017500022500.checked0 : Certificates.StepValid model0 9000000000000 step0 0 1 200

theorem ConwaySoifer.Simplified.Certificates.Across017500022500.next0 : model0.insert step0 = model1

theorem ConwaySoifer.Simplified.Certificates.Across017500022500.excluded1_0 : Certificates.ExcludedOn (model1.B 0 ++ [step1.q]) 9000000000000 (model1.caps 0) (model1.ord 0) 0 1 200

theorem ConwaySoifer.Simplified.Certificates.Across017500022500.excluded1_2 : Certificates.ExcludedOn (model1.B 2 ++ [step1.q]) 9000000000000 (model1.caps 2) (model1.ord 2) 0 1 200

theorem ConwaySoifer.Simplified.Certificates.Across017500022500.excluded1_3 : Certificates.ExcludedOn (model1.B 3 ++ [step1.q]) 9000000000000 (model1.caps 3) (model1.ord 3) 0 1 200

theorem ConwaySoifer.Simplified.Certificates.Across017500022500.excluded1_4 : Certificates.ExcludedOn (model1.B 4 ++ [step1.q]) 9000000000000 (model1.caps 4) (model1.ord 4) 0 1 200

theorem ConwaySoifer.Simplified.Certificates.Across017500022500.excluded1_5 : Certificates.ExcludedOn (model1.B 5 ++ [step1.q]) 9000000000000 (model1.caps 5) (model1.ord 5) 0 1 200

theorem ConwaySoifer.Simplified.Certificates.Across017500022500.excluded1_6 : Certificates.ExcludedOn (model1.B 6 ++ [step1.q]) 9000000000000 (model1.caps 6) (model1.ord 6) 0 1 200

theorem ConwaySoifer.Simplified.Certificates.Across017500022500.excluded1_7 : Certificates.ExcludedOn (model1.B 7 ++ [step1.q]) 9000000000000 (model1.caps 7) (model1.ord 7) 0 1 200

theorem ConwaySoifer.Simplified.Certificates.Across017500022500.excluded1_8 : Certificates.ExcludedOn (model1.B 8 ++ [step1.q]) 9000000000000 (model1.caps 8) (model1.ord 8) 0 1 200

theorem ConwaySoifer.Simplified.Certificates.Across017500022500.excluded1_9 : Certificates.ExcludedOn (model1.B 9 ++ [step1.q]) 9000000000000 (model1.caps 9) (model1.ord 9) 0 1 200

theorem ConwaySoifer.Simplified.Certificates.Across017500022500.checked1 : Certificates.StepValid model1 9000000000000 step1 0 1 200

theorem ConwaySoifer.Simplified.Certificates.Across017500022500.next1 : model1.insert step1 = model2

theorem ConwaySoifer.Simplified.Certificates.Across017500022500.excluded2_1 : Certificates.ExcludedOn (model2.B 1 ++ [step2.q]) 9000000000000 (model2.caps 1) (model2.ord 1) 0 1 200

theorem ConwaySoifer.Simplified.Certificates.Across017500022500.excluded2_2 : Certificates.ExcludedOn (model2.B 2 ++ [step2.q]) 9000000000000 (model2.caps 2) (model2.ord 2) 0 1 200

theorem ConwaySoifer.Simplified.Certificates.Across017500022500.excluded2_3 : Certificates.ExcludedOn (model2.B 3 ++ [step2.q]) 9000000000000 (model2.caps 3) (model2.ord 3) 0 1 200

theorem ConwaySoifer.Simplified.Certificates.Across017500022500.excluded2_4 : Certificates.ExcludedOn (model2.B 4 ++ [step2.q]) 9000000000000 (model2.caps 4) (model2.ord 4) 0 1 200

theorem ConwaySoifer.Simplified.Certificates.Across017500022500.excluded2_5 : Certificates.ExcludedOn (model2.B 5 ++ [step2.q]) 9000000000000 (model2.caps 5) (model2.ord 5) 0 1 200

theorem ConwaySoifer.Simplified.Certificates.Across017500022500.excluded2_6 : Certificates.ExcludedOn (model2.B 6 ++ [step2.q]) 9000000000000 (model2.caps 6) (model2.ord 6) 0 1 200

theorem ConwaySoifer.Simplified.Certificates.Across017500022500.excluded2_7 : Certificates.ExcludedOn (model2.B 7 ++ [step2.q]) 9000000000000 (model2.caps 7) (model2.ord 7) 0 1 200

theorem ConwaySoifer.Simplified.Certificates.Across017500022500.excluded2_8 : Certificates.ExcludedOn (model2.B 8 ++ [step2.q]) 9000000000000 (model2.caps 8) (model2.ord 8) 0 1 200

theorem ConwaySoifer.Simplified.Certificates.Across017500022500.excluded2_9 : Certificates.ExcludedOn (model2.B 9 ++ [step2.q]) 9000000000000 (model2.caps 9) (model2.ord 9) 0 1 200

theorem ConwaySoifer.Simplified.Certificates.Across017500022500.checked2 : Certificates.StepValid model2 9000000000000 step2 0 1 200

theorem ConwaySoifer.Simplified.Certificates.Across017500022500.next2 : model2.insert step2 = model3

theorem ConwaySoifer.Simplified.Certificates.Across017500022500.excluded3_1 : Certificates.ExcludedOn (model3.B 1 ++ [step3.q]) 9000000000000 (model3.caps 1) (model3.ord 1) 0 1 200

theorem ConwaySoifer.Simplified.Certificates.Across017500022500.excluded3_2 : Certificates.ExcludedOn (model3.B 2 ++ [step3.q]) 9000000000000 (model3.caps 2) (model3.ord 2) 0 1 200

theorem ConwaySoifer.Simplified.Certificates.Across017500022500.excluded3_3 : Certificates.ExcludedOn (model3.B 3 ++ [step3.q]) 9000000000000 (model3.caps 3) (model3.ord 3) 0 1 200

theorem ConwaySoifer.Simplified.Certificates.Across017500022500.excluded3_4 : Certificates.ExcludedOn (model3.B 4 ++ [step3.q]) 9000000000000 (model3.caps 4) (model3.ord 4) 0 1 200

theorem ConwaySoifer.Simplified.Certificates.Across017500022500.excluded3_5 : Certificates.ExcludedOn (model3.B 5 ++ [step3.q]) 9000000000000 (model3.caps 5) (model3.ord 5) 0 1 200

theorem ConwaySoifer.Simplified.Certificates.Across017500022500.excluded3_6 : Certificates.ExcludedOn (model3.B 6 ++ [step3.q]) 9000000000000 (model3.caps 6) (model3.ord 6) 0 1 200

theorem ConwaySoifer.Simplified.Certificates.Across017500022500.excluded3_7 : Certificates.ExcludedOn (model3.B 7 ++ [step3.q]) 9000000000000 (model3.caps 7) (model3.ord 7) 0 1 200

theorem ConwaySoifer.Simplified.Certificates.Across017500022500.excluded3_8 : Certificates.ExcludedOn (model3.B 8 ++ [step3.q]) 9000000000000 (model3.caps 8) (model3.ord 8) 0 1 200

theorem ConwaySoifer.Simplified.Certificates.Across017500022500.excluded3_9 : Certificates.ExcludedOn (model3.B 9 ++ [step3.q]) 9000000000000 (model3.caps 9) (model3.ord 9) 0 1 200

theorem ConwaySoifer.Simplified.Certificates.Across017500022500.checked3 : Certificates.StepValid model3 9000000000000 step3 0 1 200

theorem ConwaySoifer.Simplified.Certificates.Across017500022500.next3 : model3.insert step3 = model4