Documentation

LeanPool.ConwaySoifer.Simplified.Certificates.Steps.Sext1800001900008

Sext 180000 190000 8 #

Kernel-checked forced assignments and closed-interval exclusions.

source
def ConwaySoifer.Simplified.Certificates.Sext180000190000.fan64Owner3Part0 :
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.Sext180000190000.fan64Owner4Part0 :
    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.Sext180000190000.fan65Owner0Part0 :
      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.Sext180000190000.fan65Owner0Part1 :
        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.Sext180000190000.fan65Owner0Part2 :
          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.Sext180000190000.fan65Owner0Part3 :
            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.Sext180000190000.fan66Owner2Part0 :
              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.Sext180000190000.fan67Owner0Part0 :
                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.Sext180000190000.fan67Owner0Part1 :
                  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.Sext180000190000.fan67Owner0Part2 :
                    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.Sext180000190000.fan67Owner0Part3 :
                      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.Sext180000190000.excluded64_1 :
                        Certificates.ExcludedOn (model64.B 1 ++ [step64.q]) 9000000000000 (model64.caps 1) (model64.ord 1) 0 1 100
                        source
                        theorem ConwaySoifer.Simplified.Certificates.Sext180000190000.excluded64_2 :
                        Certificates.ExcludedOn (model64.B 2 ++ [step64.q]) 9000000000000 (model64.caps 2) (model64.ord 2) 0 1 100
                        source
                        theorem ConwaySoifer.Simplified.Certificates.Sext180000190000.excluded64_3 :
                        Certificates.ExcludedOn (model64.B 3 ++ [step64.q]) 9000000000000 (model64.caps 3) (model64.ord 3) 0 1 100
                        source
                        theorem ConwaySoifer.Simplified.Certificates.Sext180000190000.excluded64_4 :
                        Certificates.ExcludedOn (model64.B 4 ++ [step64.q]) 9000000000000 (model64.caps 4) (model64.ord 4) 0 1 100
                        source
                        theorem ConwaySoifer.Simplified.Certificates.Sext180000190000.excluded64_5 :
                        Certificates.ExcludedOn (model64.B 5 ++ [step64.q]) 9000000000000 (model64.caps 5) (model64.ord 5) 0 1 100
                        source
                        theorem ConwaySoifer.Simplified.Certificates.Sext180000190000.excluded64_6 :
                        Certificates.ExcludedOn (model64.B 6 ++ [step64.q]) 9000000000000 (model64.caps 6) (model64.ord 6) 0 1 100
                        source
                        theorem ConwaySoifer.Simplified.Certificates.Sext180000190000.excluded64_7 :
                        Certificates.ExcludedOn (model64.B 7 ++ [step64.q]) 9000000000000 (model64.caps 7) (model64.ord 7) 0 1 100
                        source
                        theorem ConwaySoifer.Simplified.Certificates.Sext180000190000.excluded64_8 :
                        Certificates.ExcludedOn (model64.B 8 ++ [step64.q]) 9000000000000 (model64.caps 8) (model64.ord 8) 0 1 100
                        source
                        theorem ConwaySoifer.Simplified.Certificates.Sext180000190000.excluded64_9 :
                        Certificates.ExcludedOn (model64.B 9 ++ [step64.q]) 9000000000000 (model64.caps 9) (model64.ord 9) 0 1 100
                        source
                        theorem ConwaySoifer.Simplified.Certificates.Sext180000190000.checked64 :
                        Certificates.StepValid model64 9000000000000 step64 0 1 100
                        source
                        theorem ConwaySoifer.Simplified.Certificates.Sext180000190000.next64 :
                        model64.insert step64 = model65
                        source
                        theorem ConwaySoifer.Simplified.Certificates.Sext180000190000.excluded65_0 :
                        Certificates.ExcludedOn (model65.B 0 ++ [step65.q]) 9000000000000 (model65.caps 0) (model65.ord 0) 0 1 100
                        source
                        theorem ConwaySoifer.Simplified.Certificates.Sext180000190000.excluded65_2 :
                        Certificates.ExcludedOn (model65.B 2 ++ [step65.q]) 9000000000000 (model65.caps 2) (model65.ord 2) 0 1 100
                        source
                        theorem ConwaySoifer.Simplified.Certificates.Sext180000190000.excluded65_3 :
                        Certificates.ExcludedOn (model65.B 3 ++ [step65.q]) 9000000000000 (model65.caps 3) (model65.ord 3) 0 1 100
                        source
                        theorem ConwaySoifer.Simplified.Certificates.Sext180000190000.excluded65_4 :
                        Certificates.ExcludedOn (model65.B 4 ++ [step65.q]) 9000000000000 (model65.caps 4) (model65.ord 4) 0 1 100
                        source
                        theorem ConwaySoifer.Simplified.Certificates.Sext180000190000.excluded65_5 :
                        Certificates.ExcludedOn (model65.B 5 ++ [step65.q]) 9000000000000 (model65.caps 5) (model65.ord 5) 0 1 100
                        source
                        theorem ConwaySoifer.Simplified.Certificates.Sext180000190000.excluded65_6 :
                        Certificates.ExcludedOn (model65.B 6 ++ [step65.q]) 9000000000000 (model65.caps 6) (model65.ord 6) 0 1 100
                        source
                        theorem ConwaySoifer.Simplified.Certificates.Sext180000190000.excluded65_7 :
                        Certificates.ExcludedOn (model65.B 7 ++ [step65.q]) 9000000000000 (model65.caps 7) (model65.ord 7) 0 1 100
                        source
                        theorem ConwaySoifer.Simplified.Certificates.Sext180000190000.excluded65_8 :
                        Certificates.ExcludedOn (model65.B 8 ++ [step65.q]) 9000000000000 (model65.caps 8) (model65.ord 8) 0 1 100
                        source
                        theorem ConwaySoifer.Simplified.Certificates.Sext180000190000.excluded65_9 :
                        Certificates.ExcludedOn (model65.B 9 ++ [step65.q]) 9000000000000 (model65.caps 9) (model65.ord 9) 0 1 100
                        source
                        theorem ConwaySoifer.Simplified.Certificates.Sext180000190000.checked65 :
                        Certificates.StepValid model65 9000000000000 step65 0 1 100
                        source
                        theorem ConwaySoifer.Simplified.Certificates.Sext180000190000.next65 :
                        model65.insert step65 = model66
                        source
                        theorem ConwaySoifer.Simplified.Certificates.Sext180000190000.excluded66_0 :
                        Certificates.ExcludedOn (model66.B 0 ++ [step66.q]) 9000000000000 (model66.caps 0) (model66.ord 0) 0 1 100
                        source
                        theorem ConwaySoifer.Simplified.Certificates.Sext180000190000.excluded66_2 :
                        Certificates.ExcludedOn (model66.B 2 ++ [step66.q]) 9000000000000 (model66.caps 2) (model66.ord 2) 0 1 100
                        source
                        theorem ConwaySoifer.Simplified.Certificates.Sext180000190000.excluded66_3 :
                        Certificates.ExcludedOn (model66.B 3 ++ [step66.q]) 9000000000000 (model66.caps 3) (model66.ord 3) 0 1 100
                        source
                        theorem ConwaySoifer.Simplified.Certificates.Sext180000190000.excluded66_4 :
                        Certificates.ExcludedOn (model66.B 4 ++ [step66.q]) 9000000000000 (model66.caps 4) (model66.ord 4) 0 1 100
                        source
                        theorem ConwaySoifer.Simplified.Certificates.Sext180000190000.excluded66_5 :
                        Certificates.ExcludedOn (model66.B 5 ++ [step66.q]) 9000000000000 (model66.caps 5) (model66.ord 5) 0 1 100
                        source
                        theorem ConwaySoifer.Simplified.Certificates.Sext180000190000.excluded66_6 :
                        Certificates.ExcludedOn (model66.B 6 ++ [step66.q]) 9000000000000 (model66.caps 6) (model66.ord 6) 0 1 100
                        source
                        theorem ConwaySoifer.Simplified.Certificates.Sext180000190000.excluded66_7 :
                        Certificates.ExcludedOn (model66.B 7 ++ [step66.q]) 9000000000000 (model66.caps 7) (model66.ord 7) 0 1 100
                        source
                        theorem ConwaySoifer.Simplified.Certificates.Sext180000190000.excluded66_8 :
                        Certificates.ExcludedOn (model66.B 8 ++ [step66.q]) 9000000000000 (model66.caps 8) (model66.ord 8) 0 1 100
                        source
                        theorem ConwaySoifer.Simplified.Certificates.Sext180000190000.excluded66_9 :
                        Certificates.ExcludedOn (model66.B 9 ++ [step66.q]) 9000000000000 (model66.caps 9) (model66.ord 9) 0 1 100
                        source
                        theorem ConwaySoifer.Simplified.Certificates.Sext180000190000.checked66 :
                        Certificates.StepValid model66 9000000000000 step66 0 1 100
                        source
                        theorem ConwaySoifer.Simplified.Certificates.Sext180000190000.next66 :
                        model66.insert step66 = model67
                        source
                        theorem ConwaySoifer.Simplified.Certificates.Sext180000190000.excluded67_0 :
                        Certificates.ExcludedOn (model67.B 0 ++ [step67.q]) 9000000000000 (model67.caps 0) (model67.ord 0) 0 1 100
                        source
                        theorem ConwaySoifer.Simplified.Certificates.Sext180000190000.excluded67_2 :
                        Certificates.ExcludedOn (model67.B 2 ++ [step67.q]) 9000000000000 (model67.caps 2) (model67.ord 2) 0 1 100
                        source
                        theorem ConwaySoifer.Simplified.Certificates.Sext180000190000.excluded67_3 :
                        Certificates.ExcludedOn (model67.B 3 ++ [step67.q]) 9000000000000 (model67.caps 3) (model67.ord 3) 0 1 100
                        source
                        theorem ConwaySoifer.Simplified.Certificates.Sext180000190000.excluded67_4 :
                        Certificates.ExcludedOn (model67.B 4 ++ [step67.q]) 9000000000000 (model67.caps 4) (model67.ord 4) 0 1 100
                        source
                        theorem ConwaySoifer.Simplified.Certificates.Sext180000190000.excluded67_5 :
                        Certificates.ExcludedOn (model67.B 5 ++ [step67.q]) 9000000000000 (model67.caps 5) (model67.ord 5) 0 1 100
                        source
                        theorem ConwaySoifer.Simplified.Certificates.Sext180000190000.excluded67_6 :
                        Certificates.ExcludedOn (model67.B 6 ++ [step67.q]) 9000000000000 (model67.caps 6) (model67.ord 6) 0 1 100
                        source
                        theorem ConwaySoifer.Simplified.Certificates.Sext180000190000.excluded67_7 :
                        Certificates.ExcludedOn (model67.B 7 ++ [step67.q]) 9000000000000 (model67.caps 7) (model67.ord 7) 0 1 100
                        source
                        theorem ConwaySoifer.Simplified.Certificates.Sext180000190000.excluded67_8 :
                        Certificates.ExcludedOn (model67.B 8 ++ [step67.q]) 9000000000000 (model67.caps 8) (model67.ord 8) 0 1 100
                        source
                        theorem ConwaySoifer.Simplified.Certificates.Sext180000190000.excluded67_9 :
                        Certificates.ExcludedOn (model67.B 9 ++ [step67.q]) 9000000000000 (model67.caps 9) (model67.ord 9) 0 1 100
                        source
                        theorem ConwaySoifer.Simplified.Certificates.Sext180000190000.checked67 :
                        Certificates.StepValid model67 9000000000000 step67 0 1 100
                        source
                        theorem ConwaySoifer.Simplified.Certificates.Sext180000190000.next67 :
                        model67.insert step67 = model68