Documentation

LeanPool.ConwaySoifer.Simplified.Certificates.Steps.Sext2300002400007

Sext 230000 240000 7 #

Kernel-checked forced assignments and closed-interval exclusions.

source
def ConwaySoifer.Simplified.Certificates.Sext230000240000.fan56Owner5Part0 :
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.Sext230000240000.fan57Owner1Part0 :
    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.Sext230000240000.excluded56_1 :
      Certificates.ExcludedOn (model56.B 1 ++ [step56.q]) 9000000000000 (model56.caps 1) (model56.ord 1) 0 1 100
      source
      theorem ConwaySoifer.Simplified.Certificates.Sext230000240000.excluded56_2 :
      Certificates.ExcludedOn (model56.B 2 ++ [step56.q]) 9000000000000 (model56.caps 2) (model56.ord 2) 0 1 100
      source
      theorem ConwaySoifer.Simplified.Certificates.Sext230000240000.excluded56_3 :
      Certificates.ExcludedOn (model56.B 3 ++ [step56.q]) 9000000000000 (model56.caps 3) (model56.ord 3) 0 1 100
      source
      theorem ConwaySoifer.Simplified.Certificates.Sext230000240000.excluded56_4 :
      Certificates.ExcludedOn (model56.B 4 ++ [step56.q]) 9000000000000 (model56.caps 4) (model56.ord 4) 0 1 100
      source
      theorem ConwaySoifer.Simplified.Certificates.Sext230000240000.excluded56_5 :
      Certificates.ExcludedOn (model56.B 5 ++ [step56.q]) 9000000000000 (model56.caps 5) (model56.ord 5) 0 1 100
      source
      theorem ConwaySoifer.Simplified.Certificates.Sext230000240000.excluded56_6 :
      Certificates.ExcludedOn (model56.B 6 ++ [step56.q]) 9000000000000 (model56.caps 6) (model56.ord 6) 0 1 100
      source
      theorem ConwaySoifer.Simplified.Certificates.Sext230000240000.excluded56_7 :
      Certificates.ExcludedOn (model56.B 7 ++ [step56.q]) 9000000000000 (model56.caps 7) (model56.ord 7) 0 1 100
      source
      theorem ConwaySoifer.Simplified.Certificates.Sext230000240000.excluded56_8 :
      Certificates.ExcludedOn (model56.B 8 ++ [step56.q]) 9000000000000 (model56.caps 8) (model56.ord 8) 0 1 100
      source
      theorem ConwaySoifer.Simplified.Certificates.Sext230000240000.excluded56_9 :
      Certificates.ExcludedOn (model56.B 9 ++ [step56.q]) 9000000000000 (model56.caps 9) (model56.ord 9) 0 1 100
      source
      theorem ConwaySoifer.Simplified.Certificates.Sext230000240000.checked56 :
      Certificates.StepValid model56 9000000000000 step56 0 1 100
      source
      theorem ConwaySoifer.Simplified.Certificates.Sext230000240000.next56 :
      model56.insert step56 = model57
      source
      theorem ConwaySoifer.Simplified.Certificates.Sext230000240000.excluded57_1 :
      Certificates.ExcludedOn (model57.B 1 ++ [step57.q]) 9000000000000 (model57.caps 1) (model57.ord 1) 0 1 100
      source
      theorem ConwaySoifer.Simplified.Certificates.Sext230000240000.excluded57_2 :
      Certificates.ExcludedOn (model57.B 2 ++ [step57.q]) 9000000000000 (model57.caps 2) (model57.ord 2) 0 1 100
      source
      theorem ConwaySoifer.Simplified.Certificates.Sext230000240000.excluded57_3 :
      Certificates.ExcludedOn (model57.B 3 ++ [step57.q]) 9000000000000 (model57.caps 3) (model57.ord 3) 0 1 100
      source
      theorem ConwaySoifer.Simplified.Certificates.Sext230000240000.excluded57_4 :
      Certificates.ExcludedOn (model57.B 4 ++ [step57.q]) 9000000000000 (model57.caps 4) (model57.ord 4) 0 1 100
      source
      theorem ConwaySoifer.Simplified.Certificates.Sext230000240000.excluded57_5 :
      Certificates.ExcludedOn (model57.B 5 ++ [step57.q]) 9000000000000 (model57.caps 5) (model57.ord 5) 0 1 100
      source
      theorem ConwaySoifer.Simplified.Certificates.Sext230000240000.excluded57_6 :
      Certificates.ExcludedOn (model57.B 6 ++ [step57.q]) 9000000000000 (model57.caps 6) (model57.ord 6) 0 1 100
      source
      theorem ConwaySoifer.Simplified.Certificates.Sext230000240000.excluded57_7 :
      Certificates.ExcludedOn (model57.B 7 ++ [step57.q]) 9000000000000 (model57.caps 7) (model57.ord 7) 0 1 100
      source
      theorem ConwaySoifer.Simplified.Certificates.Sext230000240000.excluded57_8 :
      Certificates.ExcludedOn (model57.B 8 ++ [step57.q]) 9000000000000 (model57.caps 8) (model57.ord 8) 0 1 100
      source
      theorem ConwaySoifer.Simplified.Certificates.Sext230000240000.excluded57_9 :
      Certificates.ExcludedOn (model57.B 9 ++ [step57.q]) 9000000000000 (model57.caps 9) (model57.ord 9) 0 1 100
      source
      theorem ConwaySoifer.Simplified.Certificates.Sext230000240000.checked57 :
      Certificates.StepValid model57 9000000000000 step57 0 1 100
      source
      theorem ConwaySoifer.Simplified.Certificates.Sext230000240000.next57 :
      model57.insert step57 = model58