Documentation

LeanPool.ConwaySoifer.Simplified.Certificates.Steps.Sint2300002400006

Sint 230000 240000 6 #

Kernel-checked forced assignments and closed-interval exclusions.

source
def ConwaySoifer.Simplified.Certificates.Sint230000240000.fan48Owner6Part0 :
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.Sint230000240000.fan48Owner6Part1 :
    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.Sint230000240000.excluded48_0 :
      Certificates.ExcludedOn (model48.B 0 ++ [step48.q]) 9000000000000 (model48.caps 0) (model48.ord 0) 0 1 100
      source
      theorem ConwaySoifer.Simplified.Certificates.Sint230000240000.excluded48_2 :
      Certificates.ExcludedOn (model48.B 2 ++ [step48.q]) 9000000000000 (model48.caps 2) (model48.ord 2) 0 1 100
      source
      theorem ConwaySoifer.Simplified.Certificates.Sint230000240000.excluded48_3 :
      Certificates.ExcludedOn (model48.B 3 ++ [step48.q]) 9000000000000 (model48.caps 3) (model48.ord 3) 0 1 100
      source
      theorem ConwaySoifer.Simplified.Certificates.Sint230000240000.excluded48_4 :
      Certificates.ExcludedOn (model48.B 4 ++ [step48.q]) 9000000000000 (model48.caps 4) (model48.ord 4) 0 1 100
      source
      theorem ConwaySoifer.Simplified.Certificates.Sint230000240000.excluded48_5 :
      Certificates.ExcludedOn (model48.B 5 ++ [step48.q]) 9000000000000 (model48.caps 5) (model48.ord 5) 0 1 100
      source
      theorem ConwaySoifer.Simplified.Certificates.Sint230000240000.excluded48_6 :
      Certificates.ExcludedOn (model48.B 6 ++ [step48.q]) 9000000000000 (model48.caps 6) (model48.ord 6) 0 1 100
      source
      theorem ConwaySoifer.Simplified.Certificates.Sint230000240000.excluded48_7 :
      Certificates.ExcludedOn (model48.B 7 ++ [step48.q]) 9000000000000 (model48.caps 7) (model48.ord 7) 0 1 100
      source
      theorem ConwaySoifer.Simplified.Certificates.Sint230000240000.excluded48_8 :
      Certificates.ExcludedOn (model48.B 8 ++ [step48.q]) 9000000000000 (model48.caps 8) (model48.ord 8) 0 1 100
      source
      theorem ConwaySoifer.Simplified.Certificates.Sint230000240000.excluded48_9 :
      Certificates.ExcludedOn (model48.B 9 ++ [step48.q]) 9000000000000 (model48.caps 9) (model48.ord 9) 0 1 100
      source
      theorem ConwaySoifer.Simplified.Certificates.Sint230000240000.checked48 :
      Certificates.StepValid model48 9000000000000 step48 0 1 100
      source
      theorem ConwaySoifer.Simplified.Certificates.Sint230000240000.next48 :
      model48.insert step48 = model49
      source
      theorem ConwaySoifer.Simplified.Certificates.Sint230000240000.excluded49_1 :
      Certificates.ExcludedOn (model49.B 1 ++ [step49.q]) 9000000000000 (model49.caps 1) (model49.ord 1) 0 1 100
      source
      theorem ConwaySoifer.Simplified.Certificates.Sint230000240000.excluded49_2 :
      Certificates.ExcludedOn (model49.B 2 ++ [step49.q]) 9000000000000 (model49.caps 2) (model49.ord 2) 0 1 100
      source
      theorem ConwaySoifer.Simplified.Certificates.Sint230000240000.excluded49_3 :
      Certificates.ExcludedOn (model49.B 3 ++ [step49.q]) 9000000000000 (model49.caps 3) (model49.ord 3) 0 1 100
      source
      theorem ConwaySoifer.Simplified.Certificates.Sint230000240000.excluded49_4 :
      Certificates.ExcludedOn (model49.B 4 ++ [step49.q]) 9000000000000 (model49.caps 4) (model49.ord 4) 0 1 100
      source
      theorem ConwaySoifer.Simplified.Certificates.Sint230000240000.excluded49_5 :
      Certificates.ExcludedOn (model49.B 5 ++ [step49.q]) 9000000000000 (model49.caps 5) (model49.ord 5) 0 1 100
      source
      theorem ConwaySoifer.Simplified.Certificates.Sint230000240000.excluded49_6 :
      Certificates.ExcludedOn (model49.B 6 ++ [step49.q]) 9000000000000 (model49.caps 6) (model49.ord 6) 0 1 100
      source
      theorem ConwaySoifer.Simplified.Certificates.Sint230000240000.excluded49_7 :
      Certificates.ExcludedOn (model49.B 7 ++ [step49.q]) 9000000000000 (model49.caps 7) (model49.ord 7) 0 1 100
      source
      theorem ConwaySoifer.Simplified.Certificates.Sint230000240000.excluded49_8 :
      Certificates.ExcludedOn (model49.B 8 ++ [step49.q]) 9000000000000 (model49.caps 8) (model49.ord 8) 0 1 100
      source
      theorem ConwaySoifer.Simplified.Certificates.Sint230000240000.excluded49_9 :
      Certificates.ExcludedOn (model49.B 9 ++ [step49.q]) 9000000000000 (model49.caps 9) (model49.ord 9) 0 1 100
      source
      theorem ConwaySoifer.Simplified.Certificates.Sint230000240000.checked49 :
      Certificates.StepValid model49 9000000000000 step49 0 1 100
      source
      theorem ConwaySoifer.Simplified.Certificates.Sint230000240000.next49 :
      model49.insert step49 = model50