Documentation

LeanPool.ConwaySoifer.Simplified.Certificates.Steps.Sext1700001800002

Sext 170000 180000 2 #

Kernel-checked forced assignments and closed-interval exclusions.

source
def ConwaySoifer.Simplified.Certificates.Sext170000180000.fan16Owner4Part0 :
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.Sext170000180000.fan17Owner4Part0 :
    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.Sext170000180000.fan18Owner0Part0 :
      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.Sext170000180000.fan18Owner4Part0 :
        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.Sext170000180000.fan19Owner3Part0 :
          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.Sext170000180000.fan19Owner4Part0 :
            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.Sext170000180000.fan20Owner3Part0 :
              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.Sext170000180000.fan21Owner3Part0 :
                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.Sext170000180000.fan22Owner3Part0 :
                  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.Sext170000180000.fan23Owner3Part0 :
                    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.Sext170000180000.excluded16_0 :
                      Certificates.ExcludedOn (model16.B 0 ++ [step16.q]) 9000000000000 (model16.caps 0) (model16.ord 0) 0 1 100
                      source
                      theorem ConwaySoifer.Simplified.Certificates.Sext170000180000.excluded16_1 :
                      Certificates.ExcludedOn (model16.B 1 ++ [step16.q]) 9000000000000 (model16.caps 1) (model16.ord 1) 0 1 100
                      source
                      theorem ConwaySoifer.Simplified.Certificates.Sext170000180000.excluded16_2 :
                      Certificates.ExcludedOn (model16.B 2 ++ [step16.q]) 9000000000000 (model16.caps 2) (model16.ord 2) 0 1 100
                      source
                      theorem ConwaySoifer.Simplified.Certificates.Sext170000180000.excluded16_4 :
                      Certificates.ExcludedOn (model16.B 4 ++ [step16.q]) 9000000000000 (model16.caps 4) (model16.ord 4) 0 1 100
                      source
                      theorem ConwaySoifer.Simplified.Certificates.Sext170000180000.excluded16_5 :
                      Certificates.ExcludedOn (model16.B 5 ++ [step16.q]) 9000000000000 (model16.caps 5) (model16.ord 5) 0 1 100
                      source
                      theorem ConwaySoifer.Simplified.Certificates.Sext170000180000.excluded16_6 :
                      Certificates.ExcludedOn (model16.B 6 ++ [step16.q]) 9000000000000 (model16.caps 6) (model16.ord 6) 0 1 100
                      source
                      theorem ConwaySoifer.Simplified.Certificates.Sext170000180000.excluded16_7 :
                      Certificates.ExcludedOn (model16.B 7 ++ [step16.q]) 9000000000000 (model16.caps 7) (model16.ord 7) 0 1 100
                      source
                      theorem ConwaySoifer.Simplified.Certificates.Sext170000180000.excluded16_8 :
                      Certificates.ExcludedOn (model16.B 8 ++ [step16.q]) 9000000000000 (model16.caps 8) (model16.ord 8) 0 1 100
                      source
                      theorem ConwaySoifer.Simplified.Certificates.Sext170000180000.excluded16_9 :
                      Certificates.ExcludedOn (model16.B 9 ++ [step16.q]) 9000000000000 (model16.caps 9) (model16.ord 9) 0 1 100
                      source
                      theorem ConwaySoifer.Simplified.Certificates.Sext170000180000.checked16 :
                      Certificates.StepValid model16 9000000000000 step16 0 1 100
                      source
                      theorem ConwaySoifer.Simplified.Certificates.Sext170000180000.next16 :
                      model16.insert step16 = model17
                      source
                      theorem ConwaySoifer.Simplified.Certificates.Sext170000180000.excluded17_0 :
                      Certificates.ExcludedOn (model17.B 0 ++ [step17.q]) 9000000000000 (model17.caps 0) (model17.ord 0) 0 1 100
                      source
                      theorem ConwaySoifer.Simplified.Certificates.Sext170000180000.excluded17_1 :
                      Certificates.ExcludedOn (model17.B 1 ++ [step17.q]) 9000000000000 (model17.caps 1) (model17.ord 1) 0 1 100
                      source
                      theorem ConwaySoifer.Simplified.Certificates.Sext170000180000.excluded17_2 :
                      Certificates.ExcludedOn (model17.B 2 ++ [step17.q]) 9000000000000 (model17.caps 2) (model17.ord 2) 0 1 100
                      source
                      theorem ConwaySoifer.Simplified.Certificates.Sext170000180000.excluded17_4 :
                      Certificates.ExcludedOn (model17.B 4 ++ [step17.q]) 9000000000000 (model17.caps 4) (model17.ord 4) 0 1 100
                      source
                      theorem ConwaySoifer.Simplified.Certificates.Sext170000180000.excluded17_5 :
                      Certificates.ExcludedOn (model17.B 5 ++ [step17.q]) 9000000000000 (model17.caps 5) (model17.ord 5) 0 1 100
                      source
                      theorem ConwaySoifer.Simplified.Certificates.Sext170000180000.excluded17_6 :
                      Certificates.ExcludedOn (model17.B 6 ++ [step17.q]) 9000000000000 (model17.caps 6) (model17.ord 6) 0 1 100
                      source
                      theorem ConwaySoifer.Simplified.Certificates.Sext170000180000.excluded17_7 :
                      Certificates.ExcludedOn (model17.B 7 ++ [step17.q]) 9000000000000 (model17.caps 7) (model17.ord 7) 0 1 100
                      source
                      theorem ConwaySoifer.Simplified.Certificates.Sext170000180000.excluded17_8 :
                      Certificates.ExcludedOn (model17.B 8 ++ [step17.q]) 9000000000000 (model17.caps 8) (model17.ord 8) 0 1 100
                      source
                      theorem ConwaySoifer.Simplified.Certificates.Sext170000180000.excluded17_9 :
                      Certificates.ExcludedOn (model17.B 9 ++ [step17.q]) 9000000000000 (model17.caps 9) (model17.ord 9) 0 1 100
                      source
                      theorem ConwaySoifer.Simplified.Certificates.Sext170000180000.checked17 :
                      Certificates.StepValid model17 9000000000000 step17 0 1 100
                      source
                      theorem ConwaySoifer.Simplified.Certificates.Sext170000180000.next17 :
                      model17.insert step17 = model18
                      source
                      theorem ConwaySoifer.Simplified.Certificates.Sext170000180000.excluded18_0 :
                      Certificates.ExcludedOn (model18.B 0 ++ [step18.q]) 9000000000000 (model18.caps 0) (model18.ord 0) 0 1 100
                      source
                      theorem ConwaySoifer.Simplified.Certificates.Sext170000180000.excluded18_1 :
                      Certificates.ExcludedOn (model18.B 1 ++ [step18.q]) 9000000000000 (model18.caps 1) (model18.ord 1) 0 1 100
                      source
                      theorem ConwaySoifer.Simplified.Certificates.Sext170000180000.excluded18_2 :
                      Certificates.ExcludedOn (model18.B 2 ++ [step18.q]) 9000000000000 (model18.caps 2) (model18.ord 2) 0 1 100
                      source
                      theorem ConwaySoifer.Simplified.Certificates.Sext170000180000.excluded18_3 :
                      Certificates.ExcludedOn (model18.B 3 ++ [step18.q]) 9000000000000 (model18.caps 3) (model18.ord 3) 0 1 100
                      source
                      theorem ConwaySoifer.Simplified.Certificates.Sext170000180000.excluded18_4 :
                      Certificates.ExcludedOn (model18.B 4 ++ [step18.q]) 9000000000000 (model18.caps 4) (model18.ord 4) 0 1 100
                      source
                      theorem ConwaySoifer.Simplified.Certificates.Sext170000180000.excluded18_6 :
                      Certificates.ExcludedOn (model18.B 6 ++ [step18.q]) 9000000000000 (model18.caps 6) (model18.ord 6) 0 1 100
                      source
                      theorem ConwaySoifer.Simplified.Certificates.Sext170000180000.excluded18_7 :
                      Certificates.ExcludedOn (model18.B 7 ++ [step18.q]) 9000000000000 (model18.caps 7) (model18.ord 7) 0 1 100
                      source
                      theorem ConwaySoifer.Simplified.Certificates.Sext170000180000.excluded18_8 :
                      Certificates.ExcludedOn (model18.B 8 ++ [step18.q]) 9000000000000 (model18.caps 8) (model18.ord 8) 0 1 100
                      source
                      theorem ConwaySoifer.Simplified.Certificates.Sext170000180000.excluded18_9 :
                      Certificates.ExcludedOn (model18.B 9 ++ [step18.q]) 9000000000000 (model18.caps 9) (model18.ord 9) 0 1 100
                      source
                      theorem ConwaySoifer.Simplified.Certificates.Sext170000180000.checked18 :
                      Certificates.StepValid model18 9000000000000 step18 0 1 100
                      source
                      theorem ConwaySoifer.Simplified.Certificates.Sext170000180000.next18 :
                      model18.insert step18 = model19
                      source
                      theorem ConwaySoifer.Simplified.Certificates.Sext170000180000.excluded19_1 :
                      Certificates.ExcludedOn (model19.B 1 ++ [step19.q]) 9000000000000 (model19.caps 1) (model19.ord 1) 0 1 100
                      source
                      theorem ConwaySoifer.Simplified.Certificates.Sext170000180000.excluded19_2 :
                      Certificates.ExcludedOn (model19.B 2 ++ [step19.q]) 9000000000000 (model19.caps 2) (model19.ord 2) 0 1 100
                      source
                      theorem ConwaySoifer.Simplified.Certificates.Sext170000180000.excluded19_3 :
                      Certificates.ExcludedOn (model19.B 3 ++ [step19.q]) 9000000000000 (model19.caps 3) (model19.ord 3) 0 1 100
                      source
                      theorem ConwaySoifer.Simplified.Certificates.Sext170000180000.excluded19_4 :
                      Certificates.ExcludedOn (model19.B 4 ++ [step19.q]) 9000000000000 (model19.caps 4) (model19.ord 4) 0 1 100
                      source
                      theorem ConwaySoifer.Simplified.Certificates.Sext170000180000.excluded19_5 :
                      Certificates.ExcludedOn (model19.B 5 ++ [step19.q]) 9000000000000 (model19.caps 5) (model19.ord 5) 0 1 100
                      source
                      theorem ConwaySoifer.Simplified.Certificates.Sext170000180000.excluded19_6 :
                      Certificates.ExcludedOn (model19.B 6 ++ [step19.q]) 9000000000000 (model19.caps 6) (model19.ord 6) 0 1 100
                      source
                      theorem ConwaySoifer.Simplified.Certificates.Sext170000180000.excluded19_7 :
                      Certificates.ExcludedOn (model19.B 7 ++ [step19.q]) 9000000000000 (model19.caps 7) (model19.ord 7) 0 1 100
                      source
                      theorem ConwaySoifer.Simplified.Certificates.Sext170000180000.excluded19_8 :
                      Certificates.ExcludedOn (model19.B 8 ++ [step19.q]) 9000000000000 (model19.caps 8) (model19.ord 8) 0 1 100
                      source
                      theorem ConwaySoifer.Simplified.Certificates.Sext170000180000.excluded19_9 :
                      Certificates.ExcludedOn (model19.B 9 ++ [step19.q]) 9000000000000 (model19.caps 9) (model19.ord 9) 0 1 100
                      source
                      theorem ConwaySoifer.Simplified.Certificates.Sext170000180000.checked19 :
                      Certificates.StepValid model19 9000000000000 step19 0 1 100
                      source
                      theorem ConwaySoifer.Simplified.Certificates.Sext170000180000.next19 :
                      model19.insert step19 = model20
                      source
                      theorem ConwaySoifer.Simplified.Certificates.Sext170000180000.excluded20_0 :
                      Certificates.ExcludedOn (model20.B 0 ++ [step20.q]) 9000000000000 (model20.caps 0) (model20.ord 0) 0 1 100
                      source
                      theorem ConwaySoifer.Simplified.Certificates.Sext170000180000.excluded20_1 :
                      Certificates.ExcludedOn (model20.B 1 ++ [step20.q]) 9000000000000 (model20.caps 1) (model20.ord 1) 0 1 100
                      source
                      theorem ConwaySoifer.Simplified.Certificates.Sext170000180000.excluded20_2 :
                      Certificates.ExcludedOn (model20.B 2 ++ [step20.q]) 9000000000000 (model20.caps 2) (model20.ord 2) 0 1 100
                      source
                      theorem ConwaySoifer.Simplified.Certificates.Sext170000180000.excluded20_3 :
                      Certificates.ExcludedOn (model20.B 3 ++ [step20.q]) 9000000000000 (model20.caps 3) (model20.ord 3) 0 1 100
                      source
                      theorem ConwaySoifer.Simplified.Certificates.Sext170000180000.excluded20_4 :
                      Certificates.ExcludedOn (model20.B 4 ++ [step20.q]) 9000000000000 (model20.caps 4) (model20.ord 4) 0 1 100
                      source
                      theorem ConwaySoifer.Simplified.Certificates.Sext170000180000.excluded20_5 :
                      Certificates.ExcludedOn (model20.B 5 ++ [step20.q]) 9000000000000 (model20.caps 5) (model20.ord 5) 0 1 100
                      source
                      theorem ConwaySoifer.Simplified.Certificates.Sext170000180000.excluded20_6 :
                      Certificates.ExcludedOn (model20.B 6 ++ [step20.q]) 9000000000000 (model20.caps 6) (model20.ord 6) 0 1 100
                      source
                      theorem ConwaySoifer.Simplified.Certificates.Sext170000180000.excluded20_7 :
                      Certificates.ExcludedOn (model20.B 7 ++ [step20.q]) 9000000000000 (model20.caps 7) (model20.ord 7) 0 1 100
                      source
                      theorem ConwaySoifer.Simplified.Certificates.Sext170000180000.excluded20_9 :
                      Certificates.ExcludedOn (model20.B 9 ++ [step20.q]) 9000000000000 (model20.caps 9) (model20.ord 9) 0 1 100
                      source
                      theorem ConwaySoifer.Simplified.Certificates.Sext170000180000.checked20 :
                      Certificates.StepValid model20 9000000000000 step20 0 1 100
                      source
                      theorem ConwaySoifer.Simplified.Certificates.Sext170000180000.next20 :
                      model20.insert step20 = model21
                      source
                      theorem ConwaySoifer.Simplified.Certificates.Sext170000180000.excluded21_0 :
                      Certificates.ExcludedOn (model21.B 0 ++ [step21.q]) 9000000000000 (model21.caps 0) (model21.ord 0) 0 1 100
                      source
                      theorem ConwaySoifer.Simplified.Certificates.Sext170000180000.excluded21_1 :
                      Certificates.ExcludedOn (model21.B 1 ++ [step21.q]) 9000000000000 (model21.caps 1) (model21.ord 1) 0 1 100
                      source
                      theorem ConwaySoifer.Simplified.Certificates.Sext170000180000.excluded21_2 :
                      Certificates.ExcludedOn (model21.B 2 ++ [step21.q]) 9000000000000 (model21.caps 2) (model21.ord 2) 0 1 100
                      source
                      theorem ConwaySoifer.Simplified.Certificates.Sext170000180000.excluded21_3 :
                      Certificates.ExcludedOn (model21.B 3 ++ [step21.q]) 9000000000000 (model21.caps 3) (model21.ord 3) 0 1 100
                      source
                      theorem ConwaySoifer.Simplified.Certificates.Sext170000180000.excluded21_5 :
                      Certificates.ExcludedOn (model21.B 5 ++ [step21.q]) 9000000000000 (model21.caps 5) (model21.ord 5) 0 1 100
                      source
                      theorem ConwaySoifer.Simplified.Certificates.Sext170000180000.excluded21_6 :
                      Certificates.ExcludedOn (model21.B 6 ++ [step21.q]) 9000000000000 (model21.caps 6) (model21.ord 6) 0 1 100
                      source
                      theorem ConwaySoifer.Simplified.Certificates.Sext170000180000.excluded21_7 :
                      Certificates.ExcludedOn (model21.B 7 ++ [step21.q]) 9000000000000 (model21.caps 7) (model21.ord 7) 0 1 100
                      source
                      theorem ConwaySoifer.Simplified.Certificates.Sext170000180000.excluded21_8 :
                      Certificates.ExcludedOn (model21.B 8 ++ [step21.q]) 9000000000000 (model21.caps 8) (model21.ord 8) 0 1 100
                      source
                      theorem ConwaySoifer.Simplified.Certificates.Sext170000180000.excluded21_9 :
                      Certificates.ExcludedOn (model21.B 9 ++ [step21.q]) 9000000000000 (model21.caps 9) (model21.ord 9) 0 1 100
                      source
                      theorem ConwaySoifer.Simplified.Certificates.Sext170000180000.checked21 :
                      Certificates.StepValid model21 9000000000000 step21 0 1 100
                      source
                      theorem ConwaySoifer.Simplified.Certificates.Sext170000180000.next21 :
                      model21.insert step21 = model22
                      source
                      theorem ConwaySoifer.Simplified.Certificates.Sext170000180000.excluded22_0 :
                      Certificates.ExcludedOn (model22.B 0 ++ [step22.q]) 9000000000000 (model22.caps 0) (model22.ord 0) 0 1 100
                      source
                      theorem ConwaySoifer.Simplified.Certificates.Sext170000180000.excluded22_1 :
                      Certificates.ExcludedOn (model22.B 1 ++ [step22.q]) 9000000000000 (model22.caps 1) (model22.ord 1) 0 1 100
                      source
                      theorem ConwaySoifer.Simplified.Certificates.Sext170000180000.excluded22_2 :
                      Certificates.ExcludedOn (model22.B 2 ++ [step22.q]) 9000000000000 (model22.caps 2) (model22.ord 2) 0 1 100
                      source
                      theorem ConwaySoifer.Simplified.Certificates.Sext170000180000.excluded22_3 :
                      Certificates.ExcludedOn (model22.B 3 ++ [step22.q]) 9000000000000 (model22.caps 3) (model22.ord 3) 0 1 100
                      source
                      theorem ConwaySoifer.Simplified.Certificates.Sext170000180000.excluded22_5 :
                      Certificates.ExcludedOn (model22.B 5 ++ [step22.q]) 9000000000000 (model22.caps 5) (model22.ord 5) 0 1 100
                      source
                      theorem ConwaySoifer.Simplified.Certificates.Sext170000180000.excluded22_6 :
                      Certificates.ExcludedOn (model22.B 6 ++ [step22.q]) 9000000000000 (model22.caps 6) (model22.ord 6) 0 1 100
                      source
                      theorem ConwaySoifer.Simplified.Certificates.Sext170000180000.excluded22_7 :
                      Certificates.ExcludedOn (model22.B 7 ++ [step22.q]) 9000000000000 (model22.caps 7) (model22.ord 7) 0 1 100
                      source
                      theorem ConwaySoifer.Simplified.Certificates.Sext170000180000.excluded22_8 :
                      Certificates.ExcludedOn (model22.B 8 ++ [step22.q]) 9000000000000 (model22.caps 8) (model22.ord 8) 0 1 100
                      source
                      theorem ConwaySoifer.Simplified.Certificates.Sext170000180000.excluded22_9 :
                      Certificates.ExcludedOn (model22.B 9 ++ [step22.q]) 9000000000000 (model22.caps 9) (model22.ord 9) 0 1 100
                      source
                      theorem ConwaySoifer.Simplified.Certificates.Sext170000180000.checked22 :
                      Certificates.StepValid model22 9000000000000 step22 0 1 100
                      source
                      theorem ConwaySoifer.Simplified.Certificates.Sext170000180000.next22 :
                      model22.insert step22 = model23
                      source
                      theorem ConwaySoifer.Simplified.Certificates.Sext170000180000.excluded23_0 :
                      Certificates.ExcludedOn (model23.B 0 ++ [step23.q]) 9000000000000 (model23.caps 0) (model23.ord 0) 0 1 100
                      source
                      theorem ConwaySoifer.Simplified.Certificates.Sext170000180000.excluded23_1 :
                      Certificates.ExcludedOn (model23.B 1 ++ [step23.q]) 9000000000000 (model23.caps 1) (model23.ord 1) 0 1 100
                      source
                      theorem ConwaySoifer.Simplified.Certificates.Sext170000180000.excluded23_3 :
                      Certificates.ExcludedOn (model23.B 3 ++ [step23.q]) 9000000000000 (model23.caps 3) (model23.ord 3) 0 1 100
                      source
                      theorem ConwaySoifer.Simplified.Certificates.Sext170000180000.excluded23_4 :
                      Certificates.ExcludedOn (model23.B 4 ++ [step23.q]) 9000000000000 (model23.caps 4) (model23.ord 4) 0 1 100
                      source
                      theorem ConwaySoifer.Simplified.Certificates.Sext170000180000.excluded23_5 :
                      Certificates.ExcludedOn (model23.B 5 ++ [step23.q]) 9000000000000 (model23.caps 5) (model23.ord 5) 0 1 100
                      source
                      theorem ConwaySoifer.Simplified.Certificates.Sext170000180000.excluded23_6 :
                      Certificates.ExcludedOn (model23.B 6 ++ [step23.q]) 9000000000000 (model23.caps 6) (model23.ord 6) 0 1 100
                      source
                      theorem ConwaySoifer.Simplified.Certificates.Sext170000180000.excluded23_7 :
                      Certificates.ExcludedOn (model23.B 7 ++ [step23.q]) 9000000000000 (model23.caps 7) (model23.ord 7) 0 1 100
                      source
                      theorem ConwaySoifer.Simplified.Certificates.Sext170000180000.excluded23_8 :
                      Certificates.ExcludedOn (model23.B 8 ++ [step23.q]) 9000000000000 (model23.caps 8) (model23.ord 8) 0 1 100
                      source
                      theorem ConwaySoifer.Simplified.Certificates.Sext170000180000.excluded23_9 :
                      Certificates.ExcludedOn (model23.B 9 ++ [step23.q]) 9000000000000 (model23.caps 9) (model23.ord 9) 0 1 100
                      source
                      theorem ConwaySoifer.Simplified.Certificates.Sext170000180000.checked23 :
                      Certificates.StepValid model23 9000000000000 step23 0 1 100
                      source
                      theorem ConwaySoifer.Simplified.Certificates.Sext170000180000.next23 :
                      model23.insert step23 = model24