Documentation

LeanPool.ConwaySoifer.Simplified.Certificates.Steps.Sext1000001100003

Sext 100000 110000 3 #

Kernel-checked forced assignments and closed-interval exclusions.

source
def ConwaySoifer.Simplified.Certificates.Sext100000110000.fan31Owner2Part0 :
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.Sext100000110000.excluded24_0 :
    Certificates.ExcludedOn (model24.B 0 ++ [step24.q]) 9000000000000 (model24.caps 0) (model24.ord 0) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Sext100000110000.excluded24_1 :
    Certificates.ExcludedOn (model24.B 1 ++ [step24.q]) 9000000000000 (model24.caps 1) (model24.ord 1) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Sext100000110000.excluded24_2 :
    Certificates.ExcludedOn (model24.B 2 ++ [step24.q]) 9000000000000 (model24.caps 2) (model24.ord 2) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Sext100000110000.excluded24_4 :
    Certificates.ExcludedOn (model24.B 4 ++ [step24.q]) 9000000000000 (model24.caps 4) (model24.ord 4) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Sext100000110000.excluded24_5 :
    Certificates.ExcludedOn (model24.B 5 ++ [step24.q]) 9000000000000 (model24.caps 5) (model24.ord 5) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Sext100000110000.excluded24_6 :
    Certificates.ExcludedOn (model24.B 6 ++ [step24.q]) 9000000000000 (model24.caps 6) (model24.ord 6) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Sext100000110000.excluded24_7 :
    Certificates.ExcludedOn (model24.B 7 ++ [step24.q]) 9000000000000 (model24.caps 7) (model24.ord 7) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Sext100000110000.excluded24_8 :
    Certificates.ExcludedOn (model24.B 8 ++ [step24.q]) 9000000000000 (model24.caps 8) (model24.ord 8) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Sext100000110000.excluded24_9 :
    Certificates.ExcludedOn (model24.B 9 ++ [step24.q]) 9000000000000 (model24.caps 9) (model24.ord 9) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Sext100000110000.checked24 :
    Certificates.StepValid model24 9000000000000 step24 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Sext100000110000.next24 :
    model24.insert step24 = model25
    source
    theorem ConwaySoifer.Simplified.Certificates.Sext100000110000.excluded25_0 :
    Certificates.ExcludedOn (model25.B 0 ++ [step25.q]) 9000000000000 (model25.caps 0) (model25.ord 0) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Sext100000110000.excluded25_1 :
    Certificates.ExcludedOn (model25.B 1 ++ [step25.q]) 9000000000000 (model25.caps 1) (model25.ord 1) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Sext100000110000.excluded25_3 :
    Certificates.ExcludedOn (model25.B 3 ++ [step25.q]) 9000000000000 (model25.caps 3) (model25.ord 3) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Sext100000110000.excluded25_4 :
    Certificates.ExcludedOn (model25.B 4 ++ [step25.q]) 9000000000000 (model25.caps 4) (model25.ord 4) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Sext100000110000.excluded25_5 :
    Certificates.ExcludedOn (model25.B 5 ++ [step25.q]) 9000000000000 (model25.caps 5) (model25.ord 5) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Sext100000110000.excluded25_6 :
    Certificates.ExcludedOn (model25.B 6 ++ [step25.q]) 9000000000000 (model25.caps 6) (model25.ord 6) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Sext100000110000.excluded25_7 :
    Certificates.ExcludedOn (model25.B 7 ++ [step25.q]) 9000000000000 (model25.caps 7) (model25.ord 7) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Sext100000110000.excluded25_8 :
    Certificates.ExcludedOn (model25.B 8 ++ [step25.q]) 9000000000000 (model25.caps 8) (model25.ord 8) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Sext100000110000.excluded25_9 :
    Certificates.ExcludedOn (model25.B 9 ++ [step25.q]) 9000000000000 (model25.caps 9) (model25.ord 9) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Sext100000110000.checked25 :
    Certificates.StepValid model25 9000000000000 step25 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Sext100000110000.next25 :
    model25.insert step25 = model26
    source
    theorem ConwaySoifer.Simplified.Certificates.Sext100000110000.excluded26_0 :
    Certificates.ExcludedOn (model26.B 0 ++ [step26.q]) 9000000000000 (model26.caps 0) (model26.ord 0) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Sext100000110000.excluded26_1 :
    Certificates.ExcludedOn (model26.B 1 ++ [step26.q]) 9000000000000 (model26.caps 1) (model26.ord 1) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Sext100000110000.excluded26_2 :
    Certificates.ExcludedOn (model26.B 2 ++ [step26.q]) 9000000000000 (model26.caps 2) (model26.ord 2) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Sext100000110000.excluded26_4 :
    Certificates.ExcludedOn (model26.B 4 ++ [step26.q]) 9000000000000 (model26.caps 4) (model26.ord 4) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Sext100000110000.excluded26_5 :
    Certificates.ExcludedOn (model26.B 5 ++ [step26.q]) 9000000000000 (model26.caps 5) (model26.ord 5) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Sext100000110000.excluded26_6 :
    Certificates.ExcludedOn (model26.B 6 ++ [step26.q]) 9000000000000 (model26.caps 6) (model26.ord 6) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Sext100000110000.excluded26_7 :
    Certificates.ExcludedOn (model26.B 7 ++ [step26.q]) 9000000000000 (model26.caps 7) (model26.ord 7) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Sext100000110000.excluded26_8 :
    Certificates.ExcludedOn (model26.B 8 ++ [step26.q]) 9000000000000 (model26.caps 8) (model26.ord 8) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Sext100000110000.excluded26_9 :
    Certificates.ExcludedOn (model26.B 9 ++ [step26.q]) 9000000000000 (model26.caps 9) (model26.ord 9) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Sext100000110000.checked26 :
    Certificates.StepValid model26 9000000000000 step26 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Sext100000110000.next26 :
    model26.insert step26 = model27
    source
    theorem ConwaySoifer.Simplified.Certificates.Sext100000110000.excluded27_0 :
    Certificates.ExcludedOn (model27.B 0 ++ [step27.q]) 9000000000000 (model27.caps 0) (model27.ord 0) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Sext100000110000.excluded27_1 :
    Certificates.ExcludedOn (model27.B 1 ++ [step27.q]) 9000000000000 (model27.caps 1) (model27.ord 1) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Sext100000110000.excluded27_2 :
    Certificates.ExcludedOn (model27.B 2 ++ [step27.q]) 9000000000000 (model27.caps 2) (model27.ord 2) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Sext100000110000.excluded27_3 :
    Certificates.ExcludedOn (model27.B 3 ++ [step27.q]) 9000000000000 (model27.caps 3) (model27.ord 3) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Sext100000110000.excluded27_4 :
    Certificates.ExcludedOn (model27.B 4 ++ [step27.q]) 9000000000000 (model27.caps 4) (model27.ord 4) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Sext100000110000.excluded27_5 :
    Certificates.ExcludedOn (model27.B 5 ++ [step27.q]) 9000000000000 (model27.caps 5) (model27.ord 5) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Sext100000110000.excluded27_6 :
    Certificates.ExcludedOn (model27.B 6 ++ [step27.q]) 9000000000000 (model27.caps 6) (model27.ord 6) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Sext100000110000.excluded27_8 :
    Certificates.ExcludedOn (model27.B 8 ++ [step27.q]) 9000000000000 (model27.caps 8) (model27.ord 8) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Sext100000110000.excluded27_9 :
    Certificates.ExcludedOn (model27.B 9 ++ [step27.q]) 9000000000000 (model27.caps 9) (model27.ord 9) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Sext100000110000.checked27 :
    Certificates.StepValid model27 9000000000000 step27 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Sext100000110000.next27 :
    model27.insert step27 = model28
    source
    theorem ConwaySoifer.Simplified.Certificates.Sext100000110000.excluded28_0 :
    Certificates.ExcludedOn (model28.B 0 ++ [step28.q]) 9000000000000 (model28.caps 0) (model28.ord 0) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Sext100000110000.excluded28_1 :
    Certificates.ExcludedOn (model28.B 1 ++ [step28.q]) 9000000000000 (model28.caps 1) (model28.ord 1) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Sext100000110000.excluded28_3 :
    Certificates.ExcludedOn (model28.B 3 ++ [step28.q]) 9000000000000 (model28.caps 3) (model28.ord 3) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Sext100000110000.excluded28_4 :
    Certificates.ExcludedOn (model28.B 4 ++ [step28.q]) 9000000000000 (model28.caps 4) (model28.ord 4) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Sext100000110000.excluded28_5 :
    Certificates.ExcludedOn (model28.B 5 ++ [step28.q]) 9000000000000 (model28.caps 5) (model28.ord 5) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Sext100000110000.excluded28_6 :
    Certificates.ExcludedOn (model28.B 6 ++ [step28.q]) 9000000000000 (model28.caps 6) (model28.ord 6) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Sext100000110000.excluded28_7 :
    Certificates.ExcludedOn (model28.B 7 ++ [step28.q]) 9000000000000 (model28.caps 7) (model28.ord 7) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Sext100000110000.excluded28_8 :
    Certificates.ExcludedOn (model28.B 8 ++ [step28.q]) 9000000000000 (model28.caps 8) (model28.ord 8) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Sext100000110000.excluded28_9 :
    Certificates.ExcludedOn (model28.B 9 ++ [step28.q]) 9000000000000 (model28.caps 9) (model28.ord 9) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Sext100000110000.checked28 :
    Certificates.StepValid model28 9000000000000 step28 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Sext100000110000.next28 :
    model28.insert step28 = model29
    source
    theorem ConwaySoifer.Simplified.Certificates.Sext100000110000.excluded29_0 :
    Certificates.ExcludedOn (model29.B 0 ++ [step29.q]) 9000000000000 (model29.caps 0) (model29.ord 0) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Sext100000110000.excluded29_1 :
    Certificates.ExcludedOn (model29.B 1 ++ [step29.q]) 9000000000000 (model29.caps 1) (model29.ord 1) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Sext100000110000.excluded29_3 :
    Certificates.ExcludedOn (model29.B 3 ++ [step29.q]) 9000000000000 (model29.caps 3) (model29.ord 3) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Sext100000110000.excluded29_4 :
    Certificates.ExcludedOn (model29.B 4 ++ [step29.q]) 9000000000000 (model29.caps 4) (model29.ord 4) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Sext100000110000.excluded29_5 :
    Certificates.ExcludedOn (model29.B 5 ++ [step29.q]) 9000000000000 (model29.caps 5) (model29.ord 5) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Sext100000110000.excluded29_6 :
    Certificates.ExcludedOn (model29.B 6 ++ [step29.q]) 9000000000000 (model29.caps 6) (model29.ord 6) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Sext100000110000.excluded29_7 :
    Certificates.ExcludedOn (model29.B 7 ++ [step29.q]) 9000000000000 (model29.caps 7) (model29.ord 7) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Sext100000110000.excluded29_8 :
    Certificates.ExcludedOn (model29.B 8 ++ [step29.q]) 9000000000000 (model29.caps 8) (model29.ord 8) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Sext100000110000.excluded29_9 :
    Certificates.ExcludedOn (model29.B 9 ++ [step29.q]) 9000000000000 (model29.caps 9) (model29.ord 9) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Sext100000110000.checked29 :
    Certificates.StepValid model29 9000000000000 step29 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Sext100000110000.next29 :
    model29.insert step29 = model30
    source
    theorem ConwaySoifer.Simplified.Certificates.Sext100000110000.excluded30_0 :
    Certificates.ExcludedOn (model30.B 0 ++ [step30.q]) 9000000000000 (model30.caps 0) (model30.ord 0) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Sext100000110000.excluded30_1 :
    Certificates.ExcludedOn (model30.B 1 ++ [step30.q]) 9000000000000 (model30.caps 1) (model30.ord 1) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Sext100000110000.excluded30_3 :
    Certificates.ExcludedOn (model30.B 3 ++ [step30.q]) 9000000000000 (model30.caps 3) (model30.ord 3) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Sext100000110000.excluded30_4 :
    Certificates.ExcludedOn (model30.B 4 ++ [step30.q]) 9000000000000 (model30.caps 4) (model30.ord 4) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Sext100000110000.excluded30_5 :
    Certificates.ExcludedOn (model30.B 5 ++ [step30.q]) 9000000000000 (model30.caps 5) (model30.ord 5) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Sext100000110000.excluded30_6 :
    Certificates.ExcludedOn (model30.B 6 ++ [step30.q]) 9000000000000 (model30.caps 6) (model30.ord 6) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Sext100000110000.excluded30_7 :
    Certificates.ExcludedOn (model30.B 7 ++ [step30.q]) 9000000000000 (model30.caps 7) (model30.ord 7) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Sext100000110000.excluded30_8 :
    Certificates.ExcludedOn (model30.B 8 ++ [step30.q]) 9000000000000 (model30.caps 8) (model30.ord 8) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Sext100000110000.excluded30_9 :
    Certificates.ExcludedOn (model30.B 9 ++ [step30.q]) 9000000000000 (model30.caps 9) (model30.ord 9) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Sext100000110000.checked30 :
    Certificates.StepValid model30 9000000000000 step30 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Sext100000110000.next30 :
    model30.insert step30 = model31
    source
    theorem ConwaySoifer.Simplified.Certificates.Sext100000110000.excluded31_0 :
    Certificates.ExcludedOn (model31.B 0 ++ [step31.q]) 9000000000000 (model31.caps 0) (model31.ord 0) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Sext100000110000.excluded31_2 :
    Certificates.ExcludedOn (model31.B 2 ++ [step31.q]) 9000000000000 (model31.caps 2) (model31.ord 2) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Sext100000110000.excluded31_3 :
    Certificates.ExcludedOn (model31.B 3 ++ [step31.q]) 9000000000000 (model31.caps 3) (model31.ord 3) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Sext100000110000.excluded31_4 :
    Certificates.ExcludedOn (model31.B 4 ++ [step31.q]) 9000000000000 (model31.caps 4) (model31.ord 4) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Sext100000110000.excluded31_5 :
    Certificates.ExcludedOn (model31.B 5 ++ [step31.q]) 9000000000000 (model31.caps 5) (model31.ord 5) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Sext100000110000.excluded31_6 :
    Certificates.ExcludedOn (model31.B 6 ++ [step31.q]) 9000000000000 (model31.caps 6) (model31.ord 6) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Sext100000110000.excluded31_7 :
    Certificates.ExcludedOn (model31.B 7 ++ [step31.q]) 9000000000000 (model31.caps 7) (model31.ord 7) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Sext100000110000.excluded31_8 :
    Certificates.ExcludedOn (model31.B 8 ++ [step31.q]) 9000000000000 (model31.caps 8) (model31.ord 8) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Sext100000110000.excluded31_9 :
    Certificates.ExcludedOn (model31.B 9 ++ [step31.q]) 9000000000000 (model31.caps 9) (model31.ord 9) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Sext100000110000.checked31 :
    Certificates.StepValid model31 9000000000000 step31 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Sext100000110000.next31 :
    model31.insert step31 = model32