Documentation

LeanPool.ConwaySoifer.Simplified.Certificates.Steps.Sext1200001300006

Sext 120000 130000 6 #

Kernel-checked forced assignments and closed-interval exclusions.

source
def ConwaySoifer.Simplified.Certificates.Sext120000130000.fan48Owner2Part0 :
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.Sext120000130000.fan49Owner3Part0 :
    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.Sext120000130000.fan50Owner3Part0 :
      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.Sext120000130000.fan50Owner4Part0 :
        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.Sext120000130000.fan51Owner2Part0 :
          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.Sext120000130000.excluded48_0 :
            Certificates.ExcludedOn (model48.B 0 ++ [step48.q]) 9000000000000 (model48.caps 0) (model48.ord 0) 0 1 100
            source
            theorem ConwaySoifer.Simplified.Certificates.Sext120000130000.excluded48_1 :
            Certificates.ExcludedOn (model48.B 1 ++ [step48.q]) 9000000000000 (model48.caps 1) (model48.ord 1) 0 1 100
            source
            theorem ConwaySoifer.Simplified.Certificates.Sext120000130000.excluded48_2 :
            Certificates.ExcludedOn (model48.B 2 ++ [step48.q]) 9000000000000 (model48.caps 2) (model48.ord 2) 0 1 100
            source
            theorem ConwaySoifer.Simplified.Certificates.Sext120000130000.excluded48_4 :
            Certificates.ExcludedOn (model48.B 4 ++ [step48.q]) 9000000000000 (model48.caps 4) (model48.ord 4) 0 1 100
            source
            theorem ConwaySoifer.Simplified.Certificates.Sext120000130000.excluded48_5 :
            Certificates.ExcludedOn (model48.B 5 ++ [step48.q]) 9000000000000 (model48.caps 5) (model48.ord 5) 0 1 100
            source
            theorem ConwaySoifer.Simplified.Certificates.Sext120000130000.excluded48_6 :
            Certificates.ExcludedOn (model48.B 6 ++ [step48.q]) 9000000000000 (model48.caps 6) (model48.ord 6) 0 1 100
            source
            theorem ConwaySoifer.Simplified.Certificates.Sext120000130000.excluded48_7 :
            Certificates.ExcludedOn (model48.B 7 ++ [step48.q]) 9000000000000 (model48.caps 7) (model48.ord 7) 0 1 100
            source
            theorem ConwaySoifer.Simplified.Certificates.Sext120000130000.excluded48_8 :
            Certificates.ExcludedOn (model48.B 8 ++ [step48.q]) 9000000000000 (model48.caps 8) (model48.ord 8) 0 1 100
            source
            theorem ConwaySoifer.Simplified.Certificates.Sext120000130000.excluded48_9 :
            Certificates.ExcludedOn (model48.B 9 ++ [step48.q]) 9000000000000 (model48.caps 9) (model48.ord 9) 0 1 100
            source
            theorem ConwaySoifer.Simplified.Certificates.Sext120000130000.checked48 :
            Certificates.StepValid model48 9000000000000 step48 0 1 100
            source
            theorem ConwaySoifer.Simplified.Certificates.Sext120000130000.next48 :
            model48.insert step48 = model49
            source
            theorem ConwaySoifer.Simplified.Certificates.Sext120000130000.excluded49_0 :
            Certificates.ExcludedOn (model49.B 0 ++ [step49.q]) 9000000000000 (model49.caps 0) (model49.ord 0) 0 1 100
            source
            theorem ConwaySoifer.Simplified.Certificates.Sext120000130000.excluded49_1 :
            Certificates.ExcludedOn (model49.B 1 ++ [step49.q]) 9000000000000 (model49.caps 1) (model49.ord 1) 0 1 100
            source
            theorem ConwaySoifer.Simplified.Certificates.Sext120000130000.excluded49_2 :
            Certificates.ExcludedOn (model49.B 2 ++ [step49.q]) 9000000000000 (model49.caps 2) (model49.ord 2) 0 1 100
            source
            theorem ConwaySoifer.Simplified.Certificates.Sext120000130000.excluded49_3 :
            Certificates.ExcludedOn (model49.B 3 ++ [step49.q]) 9000000000000 (model49.caps 3) (model49.ord 3) 0 1 100
            source
            theorem ConwaySoifer.Simplified.Certificates.Sext120000130000.excluded49_5 :
            Certificates.ExcludedOn (model49.B 5 ++ [step49.q]) 9000000000000 (model49.caps 5) (model49.ord 5) 0 1 100
            source
            theorem ConwaySoifer.Simplified.Certificates.Sext120000130000.excluded49_6 :
            Certificates.ExcludedOn (model49.B 6 ++ [step49.q]) 9000000000000 (model49.caps 6) (model49.ord 6) 0 1 100
            source
            theorem ConwaySoifer.Simplified.Certificates.Sext120000130000.excluded49_7 :
            Certificates.ExcludedOn (model49.B 7 ++ [step49.q]) 9000000000000 (model49.caps 7) (model49.ord 7) 0 1 100
            source
            theorem ConwaySoifer.Simplified.Certificates.Sext120000130000.excluded49_8 :
            Certificates.ExcludedOn (model49.B 8 ++ [step49.q]) 9000000000000 (model49.caps 8) (model49.ord 8) 0 1 100
            source
            theorem ConwaySoifer.Simplified.Certificates.Sext120000130000.excluded49_9 :
            Certificates.ExcludedOn (model49.B 9 ++ [step49.q]) 9000000000000 (model49.caps 9) (model49.ord 9) 0 1 100
            source
            theorem ConwaySoifer.Simplified.Certificates.Sext120000130000.checked49 :
            Certificates.StepValid model49 9000000000000 step49 0 1 100
            source
            theorem ConwaySoifer.Simplified.Certificates.Sext120000130000.next49 :
            model49.insert step49 = model50
            source
            theorem ConwaySoifer.Simplified.Certificates.Sext120000130000.excluded50_1 :
            Certificates.ExcludedOn (model50.B 1 ++ [step50.q]) 9000000000000 (model50.caps 1) (model50.ord 1) 0 1 100
            source
            theorem ConwaySoifer.Simplified.Certificates.Sext120000130000.excluded50_2 :
            Certificates.ExcludedOn (model50.B 2 ++ [step50.q]) 9000000000000 (model50.caps 2) (model50.ord 2) 0 1 100
            source
            theorem ConwaySoifer.Simplified.Certificates.Sext120000130000.excluded50_3 :
            Certificates.ExcludedOn (model50.B 3 ++ [step50.q]) 9000000000000 (model50.caps 3) (model50.ord 3) 0 1 100
            source
            theorem ConwaySoifer.Simplified.Certificates.Sext120000130000.excluded50_4 :
            Certificates.ExcludedOn (model50.B 4 ++ [step50.q]) 9000000000000 (model50.caps 4) (model50.ord 4) 0 1 100
            source
            theorem ConwaySoifer.Simplified.Certificates.Sext120000130000.excluded50_5 :
            Certificates.ExcludedOn (model50.B 5 ++ [step50.q]) 9000000000000 (model50.caps 5) (model50.ord 5) 0 1 100
            source
            theorem ConwaySoifer.Simplified.Certificates.Sext120000130000.excluded50_6 :
            Certificates.ExcludedOn (model50.B 6 ++ [step50.q]) 9000000000000 (model50.caps 6) (model50.ord 6) 0 1 100
            source
            theorem ConwaySoifer.Simplified.Certificates.Sext120000130000.excluded50_7 :
            Certificates.ExcludedOn (model50.B 7 ++ [step50.q]) 9000000000000 (model50.caps 7) (model50.ord 7) 0 1 100
            source
            theorem ConwaySoifer.Simplified.Certificates.Sext120000130000.excluded50_8 :
            Certificates.ExcludedOn (model50.B 8 ++ [step50.q]) 9000000000000 (model50.caps 8) (model50.ord 8) 0 1 100
            source
            theorem ConwaySoifer.Simplified.Certificates.Sext120000130000.excluded50_9 :
            Certificates.ExcludedOn (model50.B 9 ++ [step50.q]) 9000000000000 (model50.caps 9) (model50.ord 9) 0 1 100
            source
            theorem ConwaySoifer.Simplified.Certificates.Sext120000130000.checked50 :
            Certificates.StepValid model50 9000000000000 step50 0 1 100
            source
            theorem ConwaySoifer.Simplified.Certificates.Sext120000130000.next50 :
            model50.insert step50 = model51
            source
            theorem ConwaySoifer.Simplified.Certificates.Sext120000130000.excluded51_0 :
            Certificates.ExcludedOn (model51.B 0 ++ [step51.q]) 9000000000000 (model51.caps 0) (model51.ord 0) 0 1 100
            source
            theorem ConwaySoifer.Simplified.Certificates.Sext120000130000.excluded51_2 :
            Certificates.ExcludedOn (model51.B 2 ++ [step51.q]) 9000000000000 (model51.caps 2) (model51.ord 2) 0 1 100
            source
            theorem ConwaySoifer.Simplified.Certificates.Sext120000130000.excluded51_3 :
            Certificates.ExcludedOn (model51.B 3 ++ [step51.q]) 9000000000000 (model51.caps 3) (model51.ord 3) 0 1 100
            source
            theorem ConwaySoifer.Simplified.Certificates.Sext120000130000.excluded51_4 :
            Certificates.ExcludedOn (model51.B 4 ++ [step51.q]) 9000000000000 (model51.caps 4) (model51.ord 4) 0 1 100
            source
            theorem ConwaySoifer.Simplified.Certificates.Sext120000130000.excluded51_5 :
            Certificates.ExcludedOn (model51.B 5 ++ [step51.q]) 9000000000000 (model51.caps 5) (model51.ord 5) 0 1 100
            source
            theorem ConwaySoifer.Simplified.Certificates.Sext120000130000.excluded51_6 :
            Certificates.ExcludedOn (model51.B 6 ++ [step51.q]) 9000000000000 (model51.caps 6) (model51.ord 6) 0 1 100
            source
            theorem ConwaySoifer.Simplified.Certificates.Sext120000130000.excluded51_7 :
            Certificates.ExcludedOn (model51.B 7 ++ [step51.q]) 9000000000000 (model51.caps 7) (model51.ord 7) 0 1 100
            source
            theorem ConwaySoifer.Simplified.Certificates.Sext120000130000.excluded51_8 :
            Certificates.ExcludedOn (model51.B 8 ++ [step51.q]) 9000000000000 (model51.caps 8) (model51.ord 8) 0 1 100
            source
            theorem ConwaySoifer.Simplified.Certificates.Sext120000130000.excluded51_9 :
            Certificates.ExcludedOn (model51.B 9 ++ [step51.q]) 9000000000000 (model51.caps 9) (model51.ord 9) 0 1 100
            source
            theorem ConwaySoifer.Simplified.Certificates.Sext120000130000.checked51 :
            Certificates.StepValid model51 9000000000000 step51 0 1 100
            source
            theorem ConwaySoifer.Simplified.Certificates.Sext120000130000.next51 :
            model51.insert step51 = model52
            source
            theorem ConwaySoifer.Simplified.Certificates.Sext120000130000.excluded52_1 :
            Certificates.ExcludedOn (model52.B 1 ++ [step52.q]) 9000000000000 (model52.caps 1) (model52.ord 1) 0 1 100
            source
            theorem ConwaySoifer.Simplified.Certificates.Sext120000130000.excluded52_2 :
            Certificates.ExcludedOn (model52.B 2 ++ [step52.q]) 9000000000000 (model52.caps 2) (model52.ord 2) 0 1 100
            source
            theorem ConwaySoifer.Simplified.Certificates.Sext120000130000.excluded52_3 :
            Certificates.ExcludedOn (model52.B 3 ++ [step52.q]) 9000000000000 (model52.caps 3) (model52.ord 3) 0 1 100
            source
            theorem ConwaySoifer.Simplified.Certificates.Sext120000130000.excluded52_4 :
            Certificates.ExcludedOn (model52.B 4 ++ [step52.q]) 9000000000000 (model52.caps 4) (model52.ord 4) 0 1 100
            source
            theorem ConwaySoifer.Simplified.Certificates.Sext120000130000.excluded52_5 :
            Certificates.ExcludedOn (model52.B 5 ++ [step52.q]) 9000000000000 (model52.caps 5) (model52.ord 5) 0 1 100
            source
            theorem ConwaySoifer.Simplified.Certificates.Sext120000130000.excluded52_6 :
            Certificates.ExcludedOn (model52.B 6 ++ [step52.q]) 9000000000000 (model52.caps 6) (model52.ord 6) 0 1 100
            source
            theorem ConwaySoifer.Simplified.Certificates.Sext120000130000.excluded52_7 :
            Certificates.ExcludedOn (model52.B 7 ++ [step52.q]) 9000000000000 (model52.caps 7) (model52.ord 7) 0 1 100
            source
            theorem ConwaySoifer.Simplified.Certificates.Sext120000130000.excluded52_8 :
            Certificates.ExcludedOn (model52.B 8 ++ [step52.q]) 9000000000000 (model52.caps 8) (model52.ord 8) 0 1 100
            source
            theorem ConwaySoifer.Simplified.Certificates.Sext120000130000.excluded52_9 :
            Certificates.ExcludedOn (model52.B 9 ++ [step52.q]) 9000000000000 (model52.caps 9) (model52.ord 9) 0 1 100
            source
            theorem ConwaySoifer.Simplified.Certificates.Sext120000130000.checked52 :
            Certificates.StepValid model52 9000000000000 step52 0 1 100
            source
            theorem ConwaySoifer.Simplified.Certificates.Sext120000130000.next52 :
            model52.insert step52 = model53