Documentation

LeanPool.ConwaySoifer.Simplified.Certificates.Steps.Sext1400001500009

Sext 140000 150000 9 #

Kernel-checked forced assignments and closed-interval exclusions.

source
def ConwaySoifer.Simplified.Certificates.Sext140000150000.fan72Owner2Part0 :
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.fan72Owner3Part0 :
    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.fan72Owner3Part1 :
      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.fan73Owner0Part0 :
        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.fan73Owner0Part1 :
          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.fan73Owner2Part0 :
            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.fan74Owner2Part0 :
              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.fan75Owner0Part0 :
                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.fan75Owner0Part1 :
                  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.excluded72_1 :
                    Certificates.ExcludedOn (model72.B 1 ++ [step72.q]) 9000000000000 (model72.caps 1) (model72.ord 1) 0 1 100
                    source
                    theorem ConwaySoifer.Simplified.Certificates.Sext140000150000.excluded72_2 :
                    Certificates.ExcludedOn (model72.B 2 ++ [step72.q]) 9000000000000 (model72.caps 2) (model72.ord 2) 0 1 100
                    source
                    theorem ConwaySoifer.Simplified.Certificates.Sext140000150000.excluded72_3 :
                    Certificates.ExcludedOn (model72.B 3 ++ [step72.q]) 9000000000000 (model72.caps 3) (model72.ord 3) 0 1 100
                    source
                    theorem ConwaySoifer.Simplified.Certificates.Sext140000150000.excluded72_4 :
                    Certificates.ExcludedOn (model72.B 4 ++ [step72.q]) 9000000000000 (model72.caps 4) (model72.ord 4) 0 1 100
                    source
                    theorem ConwaySoifer.Simplified.Certificates.Sext140000150000.excluded72_5 :
                    Certificates.ExcludedOn (model72.B 5 ++ [step72.q]) 9000000000000 (model72.caps 5) (model72.ord 5) 0 1 100
                    source
                    theorem ConwaySoifer.Simplified.Certificates.Sext140000150000.excluded72_6 :
                    Certificates.ExcludedOn (model72.B 6 ++ [step72.q]) 9000000000000 (model72.caps 6) (model72.ord 6) 0 1 100
                    source
                    theorem ConwaySoifer.Simplified.Certificates.Sext140000150000.excluded72_7 :
                    Certificates.ExcludedOn (model72.B 7 ++ [step72.q]) 9000000000000 (model72.caps 7) (model72.ord 7) 0 1 100
                    source
                    theorem ConwaySoifer.Simplified.Certificates.Sext140000150000.excluded72_8 :
                    Certificates.ExcludedOn (model72.B 8 ++ [step72.q]) 9000000000000 (model72.caps 8) (model72.ord 8) 0 1 100
                    source
                    theorem ConwaySoifer.Simplified.Certificates.Sext140000150000.excluded72_9 :
                    Certificates.ExcludedOn (model72.B 9 ++ [step72.q]) 9000000000000 (model72.caps 9) (model72.ord 9) 0 1 100
                    source
                    theorem ConwaySoifer.Simplified.Certificates.Sext140000150000.checked72 :
                    Certificates.StepValid model72 9000000000000 step72 0 1 100
                    source
                    theorem ConwaySoifer.Simplified.Certificates.Sext140000150000.next72 :
                    model72.insert step72 = model73
                    source
                    theorem ConwaySoifer.Simplified.Certificates.Sext140000150000.excluded73_0 :
                    Certificates.ExcludedOn (model73.B 0 ++ [step73.q]) 9000000000000 (model73.caps 0) (model73.ord 0) 0 1 100
                    source
                    theorem ConwaySoifer.Simplified.Certificates.Sext140000150000.excluded73_2 :
                    Certificates.ExcludedOn (model73.B 2 ++ [step73.q]) 9000000000000 (model73.caps 2) (model73.ord 2) 0 1 100
                    source
                    theorem ConwaySoifer.Simplified.Certificates.Sext140000150000.excluded73_3 :
                    Certificates.ExcludedOn (model73.B 3 ++ [step73.q]) 9000000000000 (model73.caps 3) (model73.ord 3) 0 1 100
                    source
                    theorem ConwaySoifer.Simplified.Certificates.Sext140000150000.excluded73_4 :
                    Certificates.ExcludedOn (model73.B 4 ++ [step73.q]) 9000000000000 (model73.caps 4) (model73.ord 4) 0 1 100
                    source
                    theorem ConwaySoifer.Simplified.Certificates.Sext140000150000.excluded73_5 :
                    Certificates.ExcludedOn (model73.B 5 ++ [step73.q]) 9000000000000 (model73.caps 5) (model73.ord 5) 0 1 100
                    source
                    theorem ConwaySoifer.Simplified.Certificates.Sext140000150000.excluded73_6 :
                    Certificates.ExcludedOn (model73.B 6 ++ [step73.q]) 9000000000000 (model73.caps 6) (model73.ord 6) 0 1 100
                    source
                    theorem ConwaySoifer.Simplified.Certificates.Sext140000150000.excluded73_7 :
                    Certificates.ExcludedOn (model73.B 7 ++ [step73.q]) 9000000000000 (model73.caps 7) (model73.ord 7) 0 1 100
                    source
                    theorem ConwaySoifer.Simplified.Certificates.Sext140000150000.excluded73_8 :
                    Certificates.ExcludedOn (model73.B 8 ++ [step73.q]) 9000000000000 (model73.caps 8) (model73.ord 8) 0 1 100
                    source
                    theorem ConwaySoifer.Simplified.Certificates.Sext140000150000.excluded73_9 :
                    Certificates.ExcludedOn (model73.B 9 ++ [step73.q]) 9000000000000 (model73.caps 9) (model73.ord 9) 0 1 100
                    source
                    theorem ConwaySoifer.Simplified.Certificates.Sext140000150000.checked73 :
                    Certificates.StepValid model73 9000000000000 step73 0 1 100
                    source
                    theorem ConwaySoifer.Simplified.Certificates.Sext140000150000.next73 :
                    model73.insert step73 = model74
                    source
                    theorem ConwaySoifer.Simplified.Certificates.Sext140000150000.excluded74_0 :
                    Certificates.ExcludedOn (model74.B 0 ++ [step74.q]) 9000000000000 (model74.caps 0) (model74.ord 0) 0 1 100
                    source
                    theorem ConwaySoifer.Simplified.Certificates.Sext140000150000.excluded74_2 :
                    Certificates.ExcludedOn (model74.B 2 ++ [step74.q]) 9000000000000 (model74.caps 2) (model74.ord 2) 0 1 100
                    source
                    theorem ConwaySoifer.Simplified.Certificates.Sext140000150000.excluded74_3 :
                    Certificates.ExcludedOn (model74.B 3 ++ [step74.q]) 9000000000000 (model74.caps 3) (model74.ord 3) 0 1 100
                    source
                    theorem ConwaySoifer.Simplified.Certificates.Sext140000150000.excluded74_4 :
                    Certificates.ExcludedOn (model74.B 4 ++ [step74.q]) 9000000000000 (model74.caps 4) (model74.ord 4) 0 1 100
                    source
                    theorem ConwaySoifer.Simplified.Certificates.Sext140000150000.excluded74_5 :
                    Certificates.ExcludedOn (model74.B 5 ++ [step74.q]) 9000000000000 (model74.caps 5) (model74.ord 5) 0 1 100
                    source
                    theorem ConwaySoifer.Simplified.Certificates.Sext140000150000.excluded74_6 :
                    Certificates.ExcludedOn (model74.B 6 ++ [step74.q]) 9000000000000 (model74.caps 6) (model74.ord 6) 0 1 100
                    source
                    theorem ConwaySoifer.Simplified.Certificates.Sext140000150000.excluded74_7 :
                    Certificates.ExcludedOn (model74.B 7 ++ [step74.q]) 9000000000000 (model74.caps 7) (model74.ord 7) 0 1 100
                    source
                    theorem ConwaySoifer.Simplified.Certificates.Sext140000150000.excluded74_8 :
                    Certificates.ExcludedOn (model74.B 8 ++ [step74.q]) 9000000000000 (model74.caps 8) (model74.ord 8) 0 1 100
                    source
                    theorem ConwaySoifer.Simplified.Certificates.Sext140000150000.excluded74_9 :
                    Certificates.ExcludedOn (model74.B 9 ++ [step74.q]) 9000000000000 (model74.caps 9) (model74.ord 9) 0 1 100
                    source
                    theorem ConwaySoifer.Simplified.Certificates.Sext140000150000.checked74 :
                    Certificates.StepValid model74 9000000000000 step74 0 1 100
                    source
                    theorem ConwaySoifer.Simplified.Certificates.Sext140000150000.next74 :
                    model74.insert step74 = model75
                    source
                    theorem ConwaySoifer.Simplified.Certificates.Sext140000150000.excluded75_0 :
                    Certificates.ExcludedOn (model75.B 0 ++ [step75.q]) 9000000000000 (model75.caps 0) (model75.ord 0) 0 1 100
                    source
                    theorem ConwaySoifer.Simplified.Certificates.Sext140000150000.excluded75_2 :
                    Certificates.ExcludedOn (model75.B 2 ++ [step75.q]) 9000000000000 (model75.caps 2) (model75.ord 2) 0 1 100
                    source
                    theorem ConwaySoifer.Simplified.Certificates.Sext140000150000.excluded75_3 :
                    Certificates.ExcludedOn (model75.B 3 ++ [step75.q]) 9000000000000 (model75.caps 3) (model75.ord 3) 0 1 100
                    source
                    theorem ConwaySoifer.Simplified.Certificates.Sext140000150000.excluded75_4 :
                    Certificates.ExcludedOn (model75.B 4 ++ [step75.q]) 9000000000000 (model75.caps 4) (model75.ord 4) 0 1 100
                    source
                    theorem ConwaySoifer.Simplified.Certificates.Sext140000150000.excluded75_5 :
                    Certificates.ExcludedOn (model75.B 5 ++ [step75.q]) 9000000000000 (model75.caps 5) (model75.ord 5) 0 1 100
                    source
                    theorem ConwaySoifer.Simplified.Certificates.Sext140000150000.excluded75_6 :
                    Certificates.ExcludedOn (model75.B 6 ++ [step75.q]) 9000000000000 (model75.caps 6) (model75.ord 6) 0 1 100
                    source
                    theorem ConwaySoifer.Simplified.Certificates.Sext140000150000.excluded75_7 :
                    Certificates.ExcludedOn (model75.B 7 ++ [step75.q]) 9000000000000 (model75.caps 7) (model75.ord 7) 0 1 100
                    source
                    theorem ConwaySoifer.Simplified.Certificates.Sext140000150000.excluded75_8 :
                    Certificates.ExcludedOn (model75.B 8 ++ [step75.q]) 9000000000000 (model75.caps 8) (model75.ord 8) 0 1 100
                    source
                    theorem ConwaySoifer.Simplified.Certificates.Sext140000150000.excluded75_9 :
                    Certificates.ExcludedOn (model75.B 9 ++ [step75.q]) 9000000000000 (model75.caps 9) (model75.ord 9) 0 1 100
                    source
                    theorem ConwaySoifer.Simplified.Certificates.Sext140000150000.checked75 :
                    Certificates.StepValid model75 9000000000000 step75 0 1 100
                    source
                    theorem ConwaySoifer.Simplified.Certificates.Sext140000150000.next75 :
                    model75.insert step75 = model76