Documentation

LeanPool.ConwaySoifer.Simplified.Certificates.Steps.Sext1400001500008

Sext 140000 150000 8 #

Kernel-checked forced assignments and closed-interval exclusions.

source
def ConwaySoifer.Simplified.Certificates.Sext140000150000.fan66Owner3Part0 :
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.Sext140000150000.fan66Owner3Part1 :
    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.Sext140000150000.fan66Owner3Part2 :
      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.Sext140000150000.fan68Owner2Part0 :
        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.Sext140000150000.fan69Owner3Part0 :
          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.Sext140000150000.fan69Owner3Part1 :
            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.Sext140000150000.fan70Owner2Part0 :
              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.Sext140000150000.fan71Owner3Part0 :
                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.Sext140000150000.fan71Owner3Part1 :
                  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.Sext140000150000.excluded64_1 :
                    Certificates.ExcludedOn (model64.B 1 ++ [step64.q]) 9000000000000 (model64.caps 1) (model64.ord 1) 0 1 100
                    source
                    theorem ConwaySoifer.Simplified.Certificates.Sext140000150000.excluded64_2 :
                    Certificates.ExcludedOn (model64.B 2 ++ [step64.q]) 9000000000000 (model64.caps 2) (model64.ord 2) 0 1 100
                    source
                    theorem ConwaySoifer.Simplified.Certificates.Sext140000150000.excluded64_3 :
                    Certificates.ExcludedOn (model64.B 3 ++ [step64.q]) 9000000000000 (model64.caps 3) (model64.ord 3) 0 1 100
                    source
                    theorem ConwaySoifer.Simplified.Certificates.Sext140000150000.excluded64_4 :
                    Certificates.ExcludedOn (model64.B 4 ++ [step64.q]) 9000000000000 (model64.caps 4) (model64.ord 4) 0 1 100
                    source
                    theorem ConwaySoifer.Simplified.Certificates.Sext140000150000.excluded64_5 :
                    Certificates.ExcludedOn (model64.B 5 ++ [step64.q]) 9000000000000 (model64.caps 5) (model64.ord 5) 0 1 100
                    source
                    theorem ConwaySoifer.Simplified.Certificates.Sext140000150000.excluded64_6 :
                    Certificates.ExcludedOn (model64.B 6 ++ [step64.q]) 9000000000000 (model64.caps 6) (model64.ord 6) 0 1 100
                    source
                    theorem ConwaySoifer.Simplified.Certificates.Sext140000150000.excluded64_7 :
                    Certificates.ExcludedOn (model64.B 7 ++ [step64.q]) 9000000000000 (model64.caps 7) (model64.ord 7) 0 1 100
                    source
                    theorem ConwaySoifer.Simplified.Certificates.Sext140000150000.excluded64_8 :
                    Certificates.ExcludedOn (model64.B 8 ++ [step64.q]) 9000000000000 (model64.caps 8) (model64.ord 8) 0 1 100
                    source
                    theorem ConwaySoifer.Simplified.Certificates.Sext140000150000.excluded64_9 :
                    Certificates.ExcludedOn (model64.B 9 ++ [step64.q]) 9000000000000 (model64.caps 9) (model64.ord 9) 0 1 100
                    source
                    theorem ConwaySoifer.Simplified.Certificates.Sext140000150000.checked64 :
                    Certificates.StepValid model64 9000000000000 step64 0 1 100
                    source
                    theorem ConwaySoifer.Simplified.Certificates.Sext140000150000.next64 :
                    model64.insert step64 = model65
                    source
                    theorem ConwaySoifer.Simplified.Certificates.Sext140000150000.excluded65_0 :
                    Certificates.ExcludedOn (model65.B 0 ++ [step65.q]) 9000000000000 (model65.caps 0) (model65.ord 0) 0 1 100
                    source
                    theorem ConwaySoifer.Simplified.Certificates.Sext140000150000.excluded65_1 :
                    Certificates.ExcludedOn (model65.B 1 ++ [step65.q]) 9000000000000 (model65.caps 1) (model65.ord 1) 0 1 100
                    source
                    theorem ConwaySoifer.Simplified.Certificates.Sext140000150000.excluded65_2 :
                    Certificates.ExcludedOn (model65.B 2 ++ [step65.q]) 9000000000000 (model65.caps 2) (model65.ord 2) 0 1 100
                    source
                    theorem ConwaySoifer.Simplified.Certificates.Sext140000150000.excluded65_3 :
                    Certificates.ExcludedOn (model65.B 3 ++ [step65.q]) 9000000000000 (model65.caps 3) (model65.ord 3) 0 1 100
                    source
                    theorem ConwaySoifer.Simplified.Certificates.Sext140000150000.excluded65_4 :
                    Certificates.ExcludedOn (model65.B 4 ++ [step65.q]) 9000000000000 (model65.caps 4) (model65.ord 4) 0 1 100
                    source
                    theorem ConwaySoifer.Simplified.Certificates.Sext140000150000.excluded65_5 :
                    Certificates.ExcludedOn (model65.B 5 ++ [step65.q]) 9000000000000 (model65.caps 5) (model65.ord 5) 0 1 100
                    source
                    theorem ConwaySoifer.Simplified.Certificates.Sext140000150000.excluded65_6 :
                    Certificates.ExcludedOn (model65.B 6 ++ [step65.q]) 9000000000000 (model65.caps 6) (model65.ord 6) 0 1 100
                    source
                    theorem ConwaySoifer.Simplified.Certificates.Sext140000150000.excluded65_8 :
                    Certificates.ExcludedOn (model65.B 8 ++ [step65.q]) 9000000000000 (model65.caps 8) (model65.ord 8) 0 1 100
                    source
                    theorem ConwaySoifer.Simplified.Certificates.Sext140000150000.excluded65_9 :
                    Certificates.ExcludedOn (model65.B 9 ++ [step65.q]) 9000000000000 (model65.caps 9) (model65.ord 9) 0 1 100
                    source
                    theorem ConwaySoifer.Simplified.Certificates.Sext140000150000.checked65 :
                    Certificates.StepValid model65 9000000000000 step65 0 1 100
                    source
                    theorem ConwaySoifer.Simplified.Certificates.Sext140000150000.next65 :
                    model65.insert step65 = model66
                    source
                    theorem ConwaySoifer.Simplified.Certificates.Sext140000150000.excluded66_0 :
                    Certificates.ExcludedOn (model66.B 0 ++ [step66.q]) 9000000000000 (model66.caps 0) (model66.ord 0) 0 1 100
                    source
                    theorem ConwaySoifer.Simplified.Certificates.Sext140000150000.excluded66_1 :
                    Certificates.ExcludedOn (model66.B 1 ++ [step66.q]) 9000000000000 (model66.caps 1) (model66.ord 1) 0 1 100
                    source
                    theorem ConwaySoifer.Simplified.Certificates.Sext140000150000.excluded66_2 :
                    Certificates.ExcludedOn (model66.B 2 ++ [step66.q]) 9000000000000 (model66.caps 2) (model66.ord 2) 0 1 100
                    source
                    theorem ConwaySoifer.Simplified.Certificates.Sext140000150000.excluded66_3 :
                    Certificates.ExcludedOn (model66.B 3 ++ [step66.q]) 9000000000000 (model66.caps 3) (model66.ord 3) 0 1 100
                    source
                    theorem ConwaySoifer.Simplified.Certificates.Sext140000150000.excluded66_4 :
                    Certificates.ExcludedOn (model66.B 4 ++ [step66.q]) 9000000000000 (model66.caps 4) (model66.ord 4) 0 1 100
                    source
                    theorem ConwaySoifer.Simplified.Certificates.Sext140000150000.excluded66_5 :
                    Certificates.ExcludedOn (model66.B 5 ++ [step66.q]) 9000000000000 (model66.caps 5) (model66.ord 5) 0 1 100
                    source
                    theorem ConwaySoifer.Simplified.Certificates.Sext140000150000.excluded66_6 :
                    Certificates.ExcludedOn (model66.B 6 ++ [step66.q]) 9000000000000 (model66.caps 6) (model66.ord 6) 0 1 100
                    source
                    theorem ConwaySoifer.Simplified.Certificates.Sext140000150000.excluded66_7 :
                    Certificates.ExcludedOn (model66.B 7 ++ [step66.q]) 9000000000000 (model66.caps 7) (model66.ord 7) 0 1 100
                    source
                    theorem ConwaySoifer.Simplified.Certificates.Sext140000150000.excluded66_9 :
                    Certificates.ExcludedOn (model66.B 9 ++ [step66.q]) 9000000000000 (model66.caps 9) (model66.ord 9) 0 1 100
                    source
                    theorem ConwaySoifer.Simplified.Certificates.Sext140000150000.checked66 :
                    Certificates.StepValid model66 9000000000000 step66 0 1 100
                    source
                    theorem ConwaySoifer.Simplified.Certificates.Sext140000150000.next66 :
                    model66.insert step66 = model67
                    source
                    theorem ConwaySoifer.Simplified.Certificates.Sext140000150000.excluded67_0 :
                    Certificates.ExcludedOn (model67.B 0 ++ [step67.q]) 9000000000000 (model67.caps 0) (model67.ord 0) 0 1 100
                    source
                    theorem ConwaySoifer.Simplified.Certificates.Sext140000150000.excluded67_1 :
                    Certificates.ExcludedOn (model67.B 1 ++ [step67.q]) 9000000000000 (model67.caps 1) (model67.ord 1) 0 1 100
                    source
                    theorem ConwaySoifer.Simplified.Certificates.Sext140000150000.excluded67_2 :
                    Certificates.ExcludedOn (model67.B 2 ++ [step67.q]) 9000000000000 (model67.caps 2) (model67.ord 2) 0 1 100
                    source
                    theorem ConwaySoifer.Simplified.Certificates.Sext140000150000.excluded67_4 :
                    Certificates.ExcludedOn (model67.B 4 ++ [step67.q]) 9000000000000 (model67.caps 4) (model67.ord 4) 0 1 100
                    source
                    theorem ConwaySoifer.Simplified.Certificates.Sext140000150000.excluded67_5 :
                    Certificates.ExcludedOn (model67.B 5 ++ [step67.q]) 9000000000000 (model67.caps 5) (model67.ord 5) 0 1 100
                    source
                    theorem ConwaySoifer.Simplified.Certificates.Sext140000150000.excluded67_6 :
                    Certificates.ExcludedOn (model67.B 6 ++ [step67.q]) 9000000000000 (model67.caps 6) (model67.ord 6) 0 1 100
                    source
                    theorem ConwaySoifer.Simplified.Certificates.Sext140000150000.excluded67_7 :
                    Certificates.ExcludedOn (model67.B 7 ++ [step67.q]) 9000000000000 (model67.caps 7) (model67.ord 7) 0 1 100
                    source
                    theorem ConwaySoifer.Simplified.Certificates.Sext140000150000.excluded67_8 :
                    Certificates.ExcludedOn (model67.B 8 ++ [step67.q]) 9000000000000 (model67.caps 8) (model67.ord 8) 0 1 100
                    source
                    theorem ConwaySoifer.Simplified.Certificates.Sext140000150000.excluded67_9 :
                    Certificates.ExcludedOn (model67.B 9 ++ [step67.q]) 9000000000000 (model67.caps 9) (model67.ord 9) 0 1 100
                    source
                    theorem ConwaySoifer.Simplified.Certificates.Sext140000150000.checked67 :
                    Certificates.StepValid model67 9000000000000 step67 0 1 100
                    source
                    theorem ConwaySoifer.Simplified.Certificates.Sext140000150000.next67 :
                    model67.insert step67 = model68
                    source
                    theorem ConwaySoifer.Simplified.Certificates.Sext140000150000.excluded68_0 :
                    Certificates.ExcludedOn (model68.B 0 ++ [step68.q]) 9000000000000 (model68.caps 0) (model68.ord 0) 0 1 100
                    source
                    theorem ConwaySoifer.Simplified.Certificates.Sext140000150000.excluded68_1 :
                    Certificates.ExcludedOn (model68.B 1 ++ [step68.q]) 9000000000000 (model68.caps 1) (model68.ord 1) 0 1 100
                    source
                    theorem ConwaySoifer.Simplified.Certificates.Sext140000150000.excluded68_2 :
                    Certificates.ExcludedOn (model68.B 2 ++ [step68.q]) 9000000000000 (model68.caps 2) (model68.ord 2) 0 1 100
                    source
                    theorem ConwaySoifer.Simplified.Certificates.Sext140000150000.excluded68_4 :
                    Certificates.ExcludedOn (model68.B 4 ++ [step68.q]) 9000000000000 (model68.caps 4) (model68.ord 4) 0 1 100
                    source
                    theorem ConwaySoifer.Simplified.Certificates.Sext140000150000.excluded68_5 :
                    Certificates.ExcludedOn (model68.B 5 ++ [step68.q]) 9000000000000 (model68.caps 5) (model68.ord 5) 0 1 100
                    source
                    theorem ConwaySoifer.Simplified.Certificates.Sext140000150000.excluded68_6 :
                    Certificates.ExcludedOn (model68.B 6 ++ [step68.q]) 9000000000000 (model68.caps 6) (model68.ord 6) 0 1 100
                    source
                    theorem ConwaySoifer.Simplified.Certificates.Sext140000150000.excluded68_7 :
                    Certificates.ExcludedOn (model68.B 7 ++ [step68.q]) 9000000000000 (model68.caps 7) (model68.ord 7) 0 1 100
                    source
                    theorem ConwaySoifer.Simplified.Certificates.Sext140000150000.excluded68_8 :
                    Certificates.ExcludedOn (model68.B 8 ++ [step68.q]) 9000000000000 (model68.caps 8) (model68.ord 8) 0 1 100
                    source
                    theorem ConwaySoifer.Simplified.Certificates.Sext140000150000.excluded68_9 :
                    Certificates.ExcludedOn (model68.B 9 ++ [step68.q]) 9000000000000 (model68.caps 9) (model68.ord 9) 0 1 100
                    source
                    theorem ConwaySoifer.Simplified.Certificates.Sext140000150000.checked68 :
                    Certificates.StepValid model68 9000000000000 step68 0 1 100
                    source
                    theorem ConwaySoifer.Simplified.Certificates.Sext140000150000.next68 :
                    model68.insert step68 = model69
                    source
                    theorem ConwaySoifer.Simplified.Certificates.Sext140000150000.excluded69_0 :
                    Certificates.ExcludedOn (model69.B 0 ++ [step69.q]) 9000000000000 (model69.caps 0) (model69.ord 0) 0 1 100
                    source
                    theorem ConwaySoifer.Simplified.Certificates.Sext140000150000.excluded69_1 :
                    Certificates.ExcludedOn (model69.B 1 ++ [step69.q]) 9000000000000 (model69.caps 1) (model69.ord 1) 0 1 100
                    source
                    theorem ConwaySoifer.Simplified.Certificates.Sext140000150000.excluded69_2 :
                    Certificates.ExcludedOn (model69.B 2 ++ [step69.q]) 9000000000000 (model69.caps 2) (model69.ord 2) 0 1 100
                    source
                    theorem ConwaySoifer.Simplified.Certificates.Sext140000150000.excluded69_3 :
                    Certificates.ExcludedOn (model69.B 3 ++ [step69.q]) 9000000000000 (model69.caps 3) (model69.ord 3) 0 1 100
                    source
                    theorem ConwaySoifer.Simplified.Certificates.Sext140000150000.excluded69_5 :
                    Certificates.ExcludedOn (model69.B 5 ++ [step69.q]) 9000000000000 (model69.caps 5) (model69.ord 5) 0 1 100
                    source
                    theorem ConwaySoifer.Simplified.Certificates.Sext140000150000.excluded69_6 :
                    Certificates.ExcludedOn (model69.B 6 ++ [step69.q]) 9000000000000 (model69.caps 6) (model69.ord 6) 0 1 100
                    source
                    theorem ConwaySoifer.Simplified.Certificates.Sext140000150000.excluded69_7 :
                    Certificates.ExcludedOn (model69.B 7 ++ [step69.q]) 9000000000000 (model69.caps 7) (model69.ord 7) 0 1 100
                    source
                    theorem ConwaySoifer.Simplified.Certificates.Sext140000150000.excluded69_8 :
                    Certificates.ExcludedOn (model69.B 8 ++ [step69.q]) 9000000000000 (model69.caps 8) (model69.ord 8) 0 1 100
                    source
                    theorem ConwaySoifer.Simplified.Certificates.Sext140000150000.excluded69_9 :
                    Certificates.ExcludedOn (model69.B 9 ++ [step69.q]) 9000000000000 (model69.caps 9) (model69.ord 9) 0 1 100
                    source
                    theorem ConwaySoifer.Simplified.Certificates.Sext140000150000.checked69 :
                    Certificates.StepValid model69 9000000000000 step69 0 1 100
                    source
                    theorem ConwaySoifer.Simplified.Certificates.Sext140000150000.next69 :
                    model69.insert step69 = model70
                    source
                    theorem ConwaySoifer.Simplified.Certificates.Sext140000150000.excluded70_0 :
                    Certificates.ExcludedOn (model70.B 0 ++ [step70.q]) 9000000000000 (model70.caps 0) (model70.ord 0) 0 1 100
                    source
                    theorem ConwaySoifer.Simplified.Certificates.Sext140000150000.excluded70_1 :
                    Certificates.ExcludedOn (model70.B 1 ++ [step70.q]) 9000000000000 (model70.caps 1) (model70.ord 1) 0 1 100
                    source
                    theorem ConwaySoifer.Simplified.Certificates.Sext140000150000.excluded70_2 :
                    Certificates.ExcludedOn (model70.B 2 ++ [step70.q]) 9000000000000 (model70.caps 2) (model70.ord 2) 0 1 100
                    source
                    theorem ConwaySoifer.Simplified.Certificates.Sext140000150000.excluded70_4 :
                    Certificates.ExcludedOn (model70.B 4 ++ [step70.q]) 9000000000000 (model70.caps 4) (model70.ord 4) 0 1 100
                    source
                    theorem ConwaySoifer.Simplified.Certificates.Sext140000150000.excluded70_5 :
                    Certificates.ExcludedOn (model70.B 5 ++ [step70.q]) 9000000000000 (model70.caps 5) (model70.ord 5) 0 1 100
                    source
                    theorem ConwaySoifer.Simplified.Certificates.Sext140000150000.excluded70_6 :
                    Certificates.ExcludedOn (model70.B 6 ++ [step70.q]) 9000000000000 (model70.caps 6) (model70.ord 6) 0 1 100
                    source
                    theorem ConwaySoifer.Simplified.Certificates.Sext140000150000.excluded70_7 :
                    Certificates.ExcludedOn (model70.B 7 ++ [step70.q]) 9000000000000 (model70.caps 7) (model70.ord 7) 0 1 100
                    source
                    theorem ConwaySoifer.Simplified.Certificates.Sext140000150000.excluded70_8 :
                    Certificates.ExcludedOn (model70.B 8 ++ [step70.q]) 9000000000000 (model70.caps 8) (model70.ord 8) 0 1 100
                    source
                    theorem ConwaySoifer.Simplified.Certificates.Sext140000150000.excluded70_9 :
                    Certificates.ExcludedOn (model70.B 9 ++ [step70.q]) 9000000000000 (model70.caps 9) (model70.ord 9) 0 1 100
                    source
                    theorem ConwaySoifer.Simplified.Certificates.Sext140000150000.checked70 :
                    Certificates.StepValid model70 9000000000000 step70 0 1 100
                    source
                    theorem ConwaySoifer.Simplified.Certificates.Sext140000150000.next70 :
                    model70.insert step70 = model71
                    source
                    theorem ConwaySoifer.Simplified.Certificates.Sext140000150000.excluded71_1 :
                    Certificates.ExcludedOn (model71.B 1 ++ [step71.q]) 9000000000000 (model71.caps 1) (model71.ord 1) 0 1 100
                    source
                    theorem ConwaySoifer.Simplified.Certificates.Sext140000150000.excluded71_2 :
                    Certificates.ExcludedOn (model71.B 2 ++ [step71.q]) 9000000000000 (model71.caps 2) (model71.ord 2) 0 1 100
                    source
                    theorem ConwaySoifer.Simplified.Certificates.Sext140000150000.excluded71_3 :
                    Certificates.ExcludedOn (model71.B 3 ++ [step71.q]) 9000000000000 (model71.caps 3) (model71.ord 3) 0 1 100
                    source
                    theorem ConwaySoifer.Simplified.Certificates.Sext140000150000.excluded71_4 :
                    Certificates.ExcludedOn (model71.B 4 ++ [step71.q]) 9000000000000 (model71.caps 4) (model71.ord 4) 0 1 100
                    source
                    theorem ConwaySoifer.Simplified.Certificates.Sext140000150000.excluded71_5 :
                    Certificates.ExcludedOn (model71.B 5 ++ [step71.q]) 9000000000000 (model71.caps 5) (model71.ord 5) 0 1 100
                    source
                    theorem ConwaySoifer.Simplified.Certificates.Sext140000150000.excluded71_6 :
                    Certificates.ExcludedOn (model71.B 6 ++ [step71.q]) 9000000000000 (model71.caps 6) (model71.ord 6) 0 1 100
                    source
                    theorem ConwaySoifer.Simplified.Certificates.Sext140000150000.excluded71_7 :
                    Certificates.ExcludedOn (model71.B 7 ++ [step71.q]) 9000000000000 (model71.caps 7) (model71.ord 7) 0 1 100
                    source
                    theorem ConwaySoifer.Simplified.Certificates.Sext140000150000.excluded71_8 :
                    Certificates.ExcludedOn (model71.B 8 ++ [step71.q]) 9000000000000 (model71.caps 8) (model71.ord 8) 0 1 100
                    source
                    theorem ConwaySoifer.Simplified.Certificates.Sext140000150000.excluded71_9 :
                    Certificates.ExcludedOn (model71.B 9 ++ [step71.q]) 9000000000000 (model71.caps 9) (model71.ord 9) 0 1 100
                    source
                    theorem ConwaySoifer.Simplified.Certificates.Sext140000150000.checked71 :
                    Certificates.StepValid model71 9000000000000 step71 0 1 100
                    source
                    theorem ConwaySoifer.Simplified.Certificates.Sext140000150000.next71 :
                    model71.insert step71 = model72