Documentation

LeanPool.ConwaySoifer.Simplified.Certificates.Steps.Aown2500002600000

Aown 250000 260000 0 #

Kernel-checked forced assignments and closed-interval exclusions.

source
def ConwaySoifer.Simplified.Certificates.Aown250000260000.fan6Owner0Part0 :
Certificates.FanWitness

Shared exact orientation-fan tail for this local exclusion.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem ConwaySoifer.Simplified.Certificates.Aown250000260000.excluded0_1 :
    Certificates.ExcludedOn (model0.B 1 ++ [step0.q]) 9000000000000 (model0.caps 1) (model0.ord 1) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Aown250000260000.excluded0_2 :
    Certificates.ExcludedOn (model0.B 2 ++ [step0.q]) 9000000000000 (model0.caps 2) (model0.ord 2) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Aown250000260000.excluded0_3 :
    Certificates.ExcludedOn (model0.B 3 ++ [step0.q]) 9000000000000 (model0.caps 3) (model0.ord 3) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Aown250000260000.excluded0_4 :
    Certificates.ExcludedOn (model0.B 4 ++ [step0.q]) 9000000000000 (model0.caps 4) (model0.ord 4) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Aown250000260000.excluded0_5 :
    Certificates.ExcludedOn (model0.B 5 ++ [step0.q]) 9000000000000 (model0.caps 5) (model0.ord 5) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Aown250000260000.excluded0_6 :
    Certificates.ExcludedOn (model0.B 6 ++ [step0.q]) 9000000000000 (model0.caps 6) (model0.ord 6) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Aown250000260000.excluded0_7 :
    Certificates.ExcludedOn (model0.B 7 ++ [step0.q]) 9000000000000 (model0.caps 7) (model0.ord 7) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Aown250000260000.excluded0_8 :
    Certificates.ExcludedOn (model0.B 8 ++ [step0.q]) 9000000000000 (model0.caps 8) (model0.ord 8) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Aown250000260000.excluded0_9 :
    Certificates.ExcludedOn (model0.B 9 ++ [step0.q]) 9000000000000 (model0.caps 9) (model0.ord 9) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Aown250000260000.checked0 :
    Certificates.StepValid model0 9000000000000 step0 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Aown250000260000.next0 :
    model0.insert step0 = model1
    source
    theorem ConwaySoifer.Simplified.Certificates.Aown250000260000.excluded1_1 :
    Certificates.ExcludedOn (model1.B 1 ++ [step1.q]) 9000000000000 (model1.caps 1) (model1.ord 1) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Aown250000260000.excluded1_2 :
    Certificates.ExcludedOn (model1.B 2 ++ [step1.q]) 9000000000000 (model1.caps 2) (model1.ord 2) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Aown250000260000.excluded1_3 :
    Certificates.ExcludedOn (model1.B 3 ++ [step1.q]) 9000000000000 (model1.caps 3) (model1.ord 3) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Aown250000260000.excluded1_4 :
    Certificates.ExcludedOn (model1.B 4 ++ [step1.q]) 9000000000000 (model1.caps 4) (model1.ord 4) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Aown250000260000.excluded1_5 :
    Certificates.ExcludedOn (model1.B 5 ++ [step1.q]) 9000000000000 (model1.caps 5) (model1.ord 5) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Aown250000260000.excluded1_6 :
    Certificates.ExcludedOn (model1.B 6 ++ [step1.q]) 9000000000000 (model1.caps 6) (model1.ord 6) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Aown250000260000.excluded1_7 :
    Certificates.ExcludedOn (model1.B 7 ++ [step1.q]) 9000000000000 (model1.caps 7) (model1.ord 7) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Aown250000260000.excluded1_8 :
    Certificates.ExcludedOn (model1.B 8 ++ [step1.q]) 9000000000000 (model1.caps 8) (model1.ord 8) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Aown250000260000.excluded1_9 :
    Certificates.ExcludedOn (model1.B 9 ++ [step1.q]) 9000000000000 (model1.caps 9) (model1.ord 9) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Aown250000260000.checked1 :
    Certificates.StepValid model1 9000000000000 step1 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Aown250000260000.next1 :
    model1.insert step1 = model2
    source
    theorem ConwaySoifer.Simplified.Certificates.Aown250000260000.excluded2_1 :
    Certificates.ExcludedOn (model2.B 1 ++ [step2.q]) 9000000000000 (model2.caps 1) (model2.ord 1) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Aown250000260000.excluded2_2 :
    Certificates.ExcludedOn (model2.B 2 ++ [step2.q]) 9000000000000 (model2.caps 2) (model2.ord 2) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Aown250000260000.excluded2_3 :
    Certificates.ExcludedOn (model2.B 3 ++ [step2.q]) 9000000000000 (model2.caps 3) (model2.ord 3) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Aown250000260000.excluded2_4 :
    Certificates.ExcludedOn (model2.B 4 ++ [step2.q]) 9000000000000 (model2.caps 4) (model2.ord 4) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Aown250000260000.excluded2_5 :
    Certificates.ExcludedOn (model2.B 5 ++ [step2.q]) 9000000000000 (model2.caps 5) (model2.ord 5) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Aown250000260000.excluded2_6 :
    Certificates.ExcludedOn (model2.B 6 ++ [step2.q]) 9000000000000 (model2.caps 6) (model2.ord 6) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Aown250000260000.excluded2_7 :
    Certificates.ExcludedOn (model2.B 7 ++ [step2.q]) 9000000000000 (model2.caps 7) (model2.ord 7) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Aown250000260000.excluded2_8 :
    Certificates.ExcludedOn (model2.B 8 ++ [step2.q]) 9000000000000 (model2.caps 8) (model2.ord 8) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Aown250000260000.excluded2_9 :
    Certificates.ExcludedOn (model2.B 9 ++ [step2.q]) 9000000000000 (model2.caps 9) (model2.ord 9) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Aown250000260000.checked2 :
    Certificates.StepValid model2 9000000000000 step2 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Aown250000260000.next2 :
    model2.insert step2 = model3
    source
    theorem ConwaySoifer.Simplified.Certificates.Aown250000260000.excluded3_1 :
    Certificates.ExcludedOn (model3.B 1 ++ [step3.q]) 9000000000000 (model3.caps 1) (model3.ord 1) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Aown250000260000.excluded3_2 :
    Certificates.ExcludedOn (model3.B 2 ++ [step3.q]) 9000000000000 (model3.caps 2) (model3.ord 2) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Aown250000260000.excluded3_3 :
    Certificates.ExcludedOn (model3.B 3 ++ [step3.q]) 9000000000000 (model3.caps 3) (model3.ord 3) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Aown250000260000.excluded3_4 :
    Certificates.ExcludedOn (model3.B 4 ++ [step3.q]) 9000000000000 (model3.caps 4) (model3.ord 4) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Aown250000260000.excluded3_5 :
    Certificates.ExcludedOn (model3.B 5 ++ [step3.q]) 9000000000000 (model3.caps 5) (model3.ord 5) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Aown250000260000.excluded3_6 :
    Certificates.ExcludedOn (model3.B 6 ++ [step3.q]) 9000000000000 (model3.caps 6) (model3.ord 6) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Aown250000260000.excluded3_7 :
    Certificates.ExcludedOn (model3.B 7 ++ [step3.q]) 9000000000000 (model3.caps 7) (model3.ord 7) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Aown250000260000.excluded3_8 :
    Certificates.ExcludedOn (model3.B 8 ++ [step3.q]) 9000000000000 (model3.caps 8) (model3.ord 8) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Aown250000260000.excluded3_9 :
    Certificates.ExcludedOn (model3.B 9 ++ [step3.q]) 9000000000000 (model3.caps 9) (model3.ord 9) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Aown250000260000.checked3 :
    Certificates.StepValid model3 9000000000000 step3 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Aown250000260000.next3 :
    model3.insert step3 = model4
    source
    theorem ConwaySoifer.Simplified.Certificates.Aown250000260000.excluded4_1 :
    Certificates.ExcludedOn (model4.B 1 ++ [step4.q]) 9000000000000 (model4.caps 1) (model4.ord 1) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Aown250000260000.excluded4_2 :
    Certificates.ExcludedOn (model4.B 2 ++ [step4.q]) 9000000000000 (model4.caps 2) (model4.ord 2) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Aown250000260000.excluded4_3 :
    Certificates.ExcludedOn (model4.B 3 ++ [step4.q]) 9000000000000 (model4.caps 3) (model4.ord 3) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Aown250000260000.excluded4_4 :
    Certificates.ExcludedOn (model4.B 4 ++ [step4.q]) 9000000000000 (model4.caps 4) (model4.ord 4) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Aown250000260000.excluded4_5 :
    Certificates.ExcludedOn (model4.B 5 ++ [step4.q]) 9000000000000 (model4.caps 5) (model4.ord 5) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Aown250000260000.excluded4_6 :
    Certificates.ExcludedOn (model4.B 6 ++ [step4.q]) 9000000000000 (model4.caps 6) (model4.ord 6) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Aown250000260000.excluded4_7 :
    Certificates.ExcludedOn (model4.B 7 ++ [step4.q]) 9000000000000 (model4.caps 7) (model4.ord 7) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Aown250000260000.excluded4_8 :
    Certificates.ExcludedOn (model4.B 8 ++ [step4.q]) 9000000000000 (model4.caps 8) (model4.ord 8) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Aown250000260000.excluded4_9 :
    Certificates.ExcludedOn (model4.B 9 ++ [step4.q]) 9000000000000 (model4.caps 9) (model4.ord 9) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Aown250000260000.checked4 :
    Certificates.StepValid model4 9000000000000 step4 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Aown250000260000.next4 :
    model4.insert step4 = model5
    source
    theorem ConwaySoifer.Simplified.Certificates.Aown250000260000.excluded5_1 :
    Certificates.ExcludedOn (model5.B 1 ++ [step5.q]) 9000000000000 (model5.caps 1) (model5.ord 1) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Aown250000260000.excluded5_2 :
    Certificates.ExcludedOn (model5.B 2 ++ [step5.q]) 9000000000000 (model5.caps 2) (model5.ord 2) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Aown250000260000.excluded5_3 :
    Certificates.ExcludedOn (model5.B 3 ++ [step5.q]) 9000000000000 (model5.caps 3) (model5.ord 3) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Aown250000260000.excluded5_4 :
    Certificates.ExcludedOn (model5.B 4 ++ [step5.q]) 9000000000000 (model5.caps 4) (model5.ord 4) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Aown250000260000.excluded5_5 :
    Certificates.ExcludedOn (model5.B 5 ++ [step5.q]) 9000000000000 (model5.caps 5) (model5.ord 5) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Aown250000260000.excluded5_6 :
    Certificates.ExcludedOn (model5.B 6 ++ [step5.q]) 9000000000000 (model5.caps 6) (model5.ord 6) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Aown250000260000.excluded5_7 :
    Certificates.ExcludedOn (model5.B 7 ++ [step5.q]) 9000000000000 (model5.caps 7) (model5.ord 7) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Aown250000260000.excluded5_8 :
    Certificates.ExcludedOn (model5.B 8 ++ [step5.q]) 9000000000000 (model5.caps 8) (model5.ord 8) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Aown250000260000.excluded5_9 :
    Certificates.ExcludedOn (model5.B 9 ++ [step5.q]) 9000000000000 (model5.caps 9) (model5.ord 9) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Aown250000260000.checked5 :
    Certificates.StepValid model5 9000000000000 step5 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Aown250000260000.next5 :
    model5.insert step5 = model6
    source
    theorem ConwaySoifer.Simplified.Certificates.Aown250000260000.excluded6_0 :
    Certificates.ExcludedOn (model6.B 0 ++ [step6.q]) 9000000000000 (model6.caps 0) (model6.ord 0) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Aown250000260000.excluded6_1 :
    Certificates.ExcludedOn (model6.B 1 ++ [step6.q]) 9000000000000 (model6.caps 1) (model6.ord 1) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Aown250000260000.excluded6_3 :
    Certificates.ExcludedOn (model6.B 3 ++ [step6.q]) 9000000000000 (model6.caps 3) (model6.ord 3) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Aown250000260000.excluded6_4 :
    Certificates.ExcludedOn (model6.B 4 ++ [step6.q]) 9000000000000 (model6.caps 4) (model6.ord 4) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Aown250000260000.excluded6_5 :
    Certificates.ExcludedOn (model6.B 5 ++ [step6.q]) 9000000000000 (model6.caps 5) (model6.ord 5) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Aown250000260000.excluded6_6 :
    Certificates.ExcludedOn (model6.B 6 ++ [step6.q]) 9000000000000 (model6.caps 6) (model6.ord 6) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Aown250000260000.excluded6_7 :
    Certificates.ExcludedOn (model6.B 7 ++ [step6.q]) 9000000000000 (model6.caps 7) (model6.ord 7) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Aown250000260000.excluded6_8 :
    Certificates.ExcludedOn (model6.B 8 ++ [step6.q]) 9000000000000 (model6.caps 8) (model6.ord 8) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Aown250000260000.excluded6_9 :
    Certificates.ExcludedOn (model6.B 9 ++ [step6.q]) 9000000000000 (model6.caps 9) (model6.ord 9) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Aown250000260000.checked6 :
    Certificates.StepValid model6 9000000000000 step6 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Aown250000260000.next6 :
    model6.insert step6 = model7
    source
    theorem ConwaySoifer.Simplified.Certificates.Aown250000260000.excluded7_1 :
    Certificates.ExcludedOn (model7.B 1 ++ [step7.q]) 9000000000000 (model7.caps 1) (model7.ord 1) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Aown250000260000.excluded7_2 :
    Certificates.ExcludedOn (model7.B 2 ++ [step7.q]) 9000000000000 (model7.caps 2) (model7.ord 2) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Aown250000260000.excluded7_3 :
    Certificates.ExcludedOn (model7.B 3 ++ [step7.q]) 9000000000000 (model7.caps 3) (model7.ord 3) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Aown250000260000.excluded7_4 :
    Certificates.ExcludedOn (model7.B 4 ++ [step7.q]) 9000000000000 (model7.caps 4) (model7.ord 4) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Aown250000260000.excluded7_5 :
    Certificates.ExcludedOn (model7.B 5 ++ [step7.q]) 9000000000000 (model7.caps 5) (model7.ord 5) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Aown250000260000.excluded7_6 :
    Certificates.ExcludedOn (model7.B 6 ++ [step7.q]) 9000000000000 (model7.caps 6) (model7.ord 6) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Aown250000260000.excluded7_7 :
    Certificates.ExcludedOn (model7.B 7 ++ [step7.q]) 9000000000000 (model7.caps 7) (model7.ord 7) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Aown250000260000.excluded7_8 :
    Certificates.ExcludedOn (model7.B 8 ++ [step7.q]) 9000000000000 (model7.caps 8) (model7.ord 8) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Aown250000260000.excluded7_9 :
    Certificates.ExcludedOn (model7.B 9 ++ [step7.q]) 9000000000000 (model7.caps 9) (model7.ord 9) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Aown250000260000.checked7 :
    Certificates.StepValid model7 9000000000000 step7 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Aown250000260000.next7 :
    model7.insert step7 = model8