Documentation

LeanPool.ConwaySoifer.Simplified.Certificates.Steps.Sext1100001200003

Sext 110000 120000 3 #

Kernel-checked forced assignments and closed-interval exclusions.

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