Documentation

LeanPool.ConwaySoifer.Simplified.Certificates.Steps.Sext2500002525001

Sext 250000 252500 1 #

Kernel-checked forced assignments and closed-interval exclusions.

source
def ConwaySoifer.Simplified.Certificates.Sext250000252500.fan12Owner0Part0 :
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.Sext250000252500.fan12Owner0Part1 :
    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.Sext250000252500.fan13Owner0Part0 :
      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.Sext250000252500.fan13Owner0Part1 :
        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.Sext250000252500.fan14Owner0Part0 :
          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.Sext250000252500.fan14Owner0Part1 :
            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.Sext250000252500.excluded8_1 :
              Certificates.ExcludedOn (model8.B 1 ++ [step8.q]) 9000000000000 (model8.caps 1) (model8.ord 1) 0 1 400
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext250000252500.excluded8_2 :
              Certificates.ExcludedOn (model8.B 2 ++ [step8.q]) 9000000000000 (model8.caps 2) (model8.ord 2) 0 1 400
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext250000252500.excluded8_3 :
              Certificates.ExcludedOn (model8.B 3 ++ [step8.q]) 9000000000000 (model8.caps 3) (model8.ord 3) 0 1 400
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext250000252500.excluded8_4 :
              Certificates.ExcludedOn (model8.B 4 ++ [step8.q]) 9000000000000 (model8.caps 4) (model8.ord 4) 0 1 400
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext250000252500.excluded8_5 :
              Certificates.ExcludedOn (model8.B 5 ++ [step8.q]) 9000000000000 (model8.caps 5) (model8.ord 5) 0 1 400
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext250000252500.excluded8_6 :
              Certificates.ExcludedOn (model8.B 6 ++ [step8.q]) 9000000000000 (model8.caps 6) (model8.ord 6) 0 1 400
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext250000252500.excluded8_7 :
              Certificates.ExcludedOn (model8.B 7 ++ [step8.q]) 9000000000000 (model8.caps 7) (model8.ord 7) 0 1 400
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext250000252500.excluded8_8 :
              Certificates.ExcludedOn (model8.B 8 ++ [step8.q]) 9000000000000 (model8.caps 8) (model8.ord 8) 0 1 400
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext250000252500.excluded8_9 :
              Certificates.ExcludedOn (model8.B 9 ++ [step8.q]) 9000000000000 (model8.caps 9) (model8.ord 9) 0 1 400
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext250000252500.checked8 :
              Certificates.StepValid model8 9000000000000 step8 0 1 400
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext250000252500.next8 :
              model8.insert step8 = model9
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext250000252500.excluded9_1 :
              Certificates.ExcludedOn (model9.B 1 ++ [step9.q]) 9000000000000 (model9.caps 1) (model9.ord 1) 0 1 400
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext250000252500.excluded9_2 :
              Certificates.ExcludedOn (model9.B 2 ++ [step9.q]) 9000000000000 (model9.caps 2) (model9.ord 2) 0 1 400
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext250000252500.excluded9_3 :
              Certificates.ExcludedOn (model9.B 3 ++ [step9.q]) 9000000000000 (model9.caps 3) (model9.ord 3) 0 1 400
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext250000252500.excluded9_4 :
              Certificates.ExcludedOn (model9.B 4 ++ [step9.q]) 9000000000000 (model9.caps 4) (model9.ord 4) 0 1 400
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext250000252500.excluded9_5 :
              Certificates.ExcludedOn (model9.B 5 ++ [step9.q]) 9000000000000 (model9.caps 5) (model9.ord 5) 0 1 400
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext250000252500.excluded9_6 :
              Certificates.ExcludedOn (model9.B 6 ++ [step9.q]) 9000000000000 (model9.caps 6) (model9.ord 6) 0 1 400
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext250000252500.excluded9_7 :
              Certificates.ExcludedOn (model9.B 7 ++ [step9.q]) 9000000000000 (model9.caps 7) (model9.ord 7) 0 1 400
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext250000252500.excluded9_8 :
              Certificates.ExcludedOn (model9.B 8 ++ [step9.q]) 9000000000000 (model9.caps 8) (model9.ord 8) 0 1 400
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext250000252500.excluded9_9 :
              Certificates.ExcludedOn (model9.B 9 ++ [step9.q]) 9000000000000 (model9.caps 9) (model9.ord 9) 0 1 400
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext250000252500.checked9 :
              Certificates.StepValid model9 9000000000000 step9 0 1 400
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext250000252500.next9 :
              model9.insert step9 = model10
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext250000252500.excluded10_0 :
              Certificates.ExcludedOn (model10.B 0 ++ [step10.q]) 9000000000000 (model10.caps 0) (model10.ord 0) 0 1 400
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext250000252500.excluded10_1 :
              Certificates.ExcludedOn (model10.B 1 ++ [step10.q]) 9000000000000 (model10.caps 1) (model10.ord 1) 0 1 400
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext250000252500.excluded10_2 :
              Certificates.ExcludedOn (model10.B 2 ++ [step10.q]) 9000000000000 (model10.caps 2) (model10.ord 2) 0 1 400
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext250000252500.excluded10_3 :
              Certificates.ExcludedOn (model10.B 3 ++ [step10.q]) 9000000000000 (model10.caps 3) (model10.ord 3) 0 1 400
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext250000252500.excluded10_4 :
              Certificates.ExcludedOn (model10.B 4 ++ [step10.q]) 9000000000000 (model10.caps 4) (model10.ord 4) 0 1 400
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext250000252500.excluded10_5 :
              Certificates.ExcludedOn (model10.B 5 ++ [step10.q]) 9000000000000 (model10.caps 5) (model10.ord 5) 0 1 400
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext250000252500.excluded10_6 :
              Certificates.ExcludedOn (model10.B 6 ++ [step10.q]) 9000000000000 (model10.caps 6) (model10.ord 6) 0 1 400
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext250000252500.excluded10_7 :
              Certificates.ExcludedOn (model10.B 7 ++ [step10.q]) 9000000000000 (model10.caps 7) (model10.ord 7) 0 1 400
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext250000252500.excluded10_8 :
              Certificates.ExcludedOn (model10.B 8 ++ [step10.q]) 9000000000000 (model10.caps 8) (model10.ord 8) 0 1 400
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext250000252500.checked10 :
              Certificates.StepValid model10 9000000000000 step10 0 1 400
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext250000252500.next10 :
              model10.insert step10 = model11
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext250000252500.excluded11_0 :
              Certificates.ExcludedOn (model11.B 0 ++ [step11.q]) 9000000000000 (model11.caps 0) (model11.ord 0) 0 1 400
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext250000252500.excluded11_1 :
              Certificates.ExcludedOn (model11.B 1 ++ [step11.q]) 9000000000000 (model11.caps 1) (model11.ord 1) 0 1 400
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext250000252500.excluded11_2 :
              Certificates.ExcludedOn (model11.B 2 ++ [step11.q]) 9000000000000 (model11.caps 2) (model11.ord 2) 0 1 400
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext250000252500.excluded11_3 :
              Certificates.ExcludedOn (model11.B 3 ++ [step11.q]) 9000000000000 (model11.caps 3) (model11.ord 3) 0 1 400
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext250000252500.excluded11_4 :
              Certificates.ExcludedOn (model11.B 4 ++ [step11.q]) 9000000000000 (model11.caps 4) (model11.ord 4) 0 1 400
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext250000252500.excluded11_5 :
              Certificates.ExcludedOn (model11.B 5 ++ [step11.q]) 9000000000000 (model11.caps 5) (model11.ord 5) 0 1 400
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext250000252500.excluded11_6 :
              Certificates.ExcludedOn (model11.B 6 ++ [step11.q]) 9000000000000 (model11.caps 6) (model11.ord 6) 0 1 400
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext250000252500.excluded11_7 :
              Certificates.ExcludedOn (model11.B 7 ++ [step11.q]) 9000000000000 (model11.caps 7) (model11.ord 7) 0 1 400
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext250000252500.excluded11_8 :
              Certificates.ExcludedOn (model11.B 8 ++ [step11.q]) 9000000000000 (model11.caps 8) (model11.ord 8) 0 1 400
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext250000252500.checked11 :
              Certificates.StepValid model11 9000000000000 step11 0 1 400
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext250000252500.next11 :
              model11.insert step11 = model12
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext250000252500.excluded12_0 :
              Certificates.ExcludedOn (model12.B 0 ++ [step12.q]) 9000000000000 (model12.caps 0) (model12.ord 0) 0 1 400
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext250000252500.excluded12_1 :
              Certificates.ExcludedOn (model12.B 1 ++ [step12.q]) 9000000000000 (model12.caps 1) (model12.ord 1) 0 1 400
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext250000252500.excluded12_2 :
              Certificates.ExcludedOn (model12.B 2 ++ [step12.q]) 9000000000000 (model12.caps 2) (model12.ord 2) 0 1 400
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext250000252500.excluded12_4 :
              Certificates.ExcludedOn (model12.B 4 ++ [step12.q]) 9000000000000 (model12.caps 4) (model12.ord 4) 0 1 400
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext250000252500.excluded12_5 :
              Certificates.ExcludedOn (model12.B 5 ++ [step12.q]) 9000000000000 (model12.caps 5) (model12.ord 5) 0 1 400
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext250000252500.excluded12_6 :
              Certificates.ExcludedOn (model12.B 6 ++ [step12.q]) 9000000000000 (model12.caps 6) (model12.ord 6) 0 1 400
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext250000252500.excluded12_7 :
              Certificates.ExcludedOn (model12.B 7 ++ [step12.q]) 9000000000000 (model12.caps 7) (model12.ord 7) 0 1 400
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext250000252500.excluded12_8 :
              Certificates.ExcludedOn (model12.B 8 ++ [step12.q]) 9000000000000 (model12.caps 8) (model12.ord 8) 0 1 400
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext250000252500.excluded12_9 :
              Certificates.ExcludedOn (model12.B 9 ++ [step12.q]) 9000000000000 (model12.caps 9) (model12.ord 9) 0 1 400
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext250000252500.checked12 :
              Certificates.StepValid model12 9000000000000 step12 0 1 400
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext250000252500.next12 :
              model12.insert step12 = model13
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext250000252500.excluded13_0 :
              Certificates.ExcludedOn (model13.B 0 ++ [step13.q]) 9000000000000 (model13.caps 0) (model13.ord 0) 0 1 400
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext250000252500.excluded13_1 :
              Certificates.ExcludedOn (model13.B 1 ++ [step13.q]) 9000000000000 (model13.caps 1) (model13.ord 1) 0 1 400
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext250000252500.excluded13_2 :
              Certificates.ExcludedOn (model13.B 2 ++ [step13.q]) 9000000000000 (model13.caps 2) (model13.ord 2) 0 1 400
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext250000252500.excluded13_3 :
              Certificates.ExcludedOn (model13.B 3 ++ [step13.q]) 9000000000000 (model13.caps 3) (model13.ord 3) 0 1 400
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext250000252500.excluded13_4 :
              Certificates.ExcludedOn (model13.B 4 ++ [step13.q]) 9000000000000 (model13.caps 4) (model13.ord 4) 0 1 400
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext250000252500.excluded13_6 :
              Certificates.ExcludedOn (model13.B 6 ++ [step13.q]) 9000000000000 (model13.caps 6) (model13.ord 6) 0 1 400
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext250000252500.excluded13_7 :
              Certificates.ExcludedOn (model13.B 7 ++ [step13.q]) 9000000000000 (model13.caps 7) (model13.ord 7) 0 1 400
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext250000252500.excluded13_8 :
              Certificates.ExcludedOn (model13.B 8 ++ [step13.q]) 9000000000000 (model13.caps 8) (model13.ord 8) 0 1 400
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext250000252500.excluded13_9 :
              Certificates.ExcludedOn (model13.B 9 ++ [step13.q]) 9000000000000 (model13.caps 9) (model13.ord 9) 0 1 400
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext250000252500.checked13 :
              Certificates.StepValid model13 9000000000000 step13 0 1 400
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext250000252500.next13 :
              model13.insert step13 = model14
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext250000252500.excluded14_0 :
              Certificates.ExcludedOn (model14.B 0 ++ [step14.q]) 9000000000000 (model14.caps 0) (model14.ord 0) 0 1 400
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext250000252500.excluded14_1 :
              Certificates.ExcludedOn (model14.B 1 ++ [step14.q]) 9000000000000 (model14.caps 1) (model14.ord 1) 0 1 400
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext250000252500.excluded14_2 :
              Certificates.ExcludedOn (model14.B 2 ++ [step14.q]) 9000000000000 (model14.caps 2) (model14.ord 2) 0 1 400
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext250000252500.excluded14_3 :
              Certificates.ExcludedOn (model14.B 3 ++ [step14.q]) 9000000000000 (model14.caps 3) (model14.ord 3) 0 1 400
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext250000252500.excluded14_4 :
              Certificates.ExcludedOn (model14.B 4 ++ [step14.q]) 9000000000000 (model14.caps 4) (model14.ord 4) 0 1 400
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext250000252500.excluded14_6 :
              Certificates.ExcludedOn (model14.B 6 ++ [step14.q]) 9000000000000 (model14.caps 6) (model14.ord 6) 0 1 400
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext250000252500.excluded14_7 :
              Certificates.ExcludedOn (model14.B 7 ++ [step14.q]) 9000000000000 (model14.caps 7) (model14.ord 7) 0 1 400
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext250000252500.excluded14_8 :
              Certificates.ExcludedOn (model14.B 8 ++ [step14.q]) 9000000000000 (model14.caps 8) (model14.ord 8) 0 1 400
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext250000252500.excluded14_9 :
              Certificates.ExcludedOn (model14.B 9 ++ [step14.q]) 9000000000000 (model14.caps 9) (model14.ord 9) 0 1 400
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext250000252500.checked14 :
              Certificates.StepValid model14 9000000000000 step14 0 1 400
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext250000252500.next14 :
              model14.insert step14 = model15
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext250000252500.excluded15_0 :
              Certificates.ExcludedOn (model15.B 0 ++ [step15.q]) 9000000000000 (model15.caps 0) (model15.ord 0) 0 1 400
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext250000252500.excluded15_1 :
              Certificates.ExcludedOn (model15.B 1 ++ [step15.q]) 9000000000000 (model15.caps 1) (model15.ord 1) 0 1 400
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext250000252500.excluded15_2 :
              Certificates.ExcludedOn (model15.B 2 ++ [step15.q]) 9000000000000 (model15.caps 2) (model15.ord 2) 0 1 400
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext250000252500.excluded15_3 :
              Certificates.ExcludedOn (model15.B 3 ++ [step15.q]) 9000000000000 (model15.caps 3) (model15.ord 3) 0 1 400
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext250000252500.excluded15_4 :
              Certificates.ExcludedOn (model15.B 4 ++ [step15.q]) 9000000000000 (model15.caps 4) (model15.ord 4) 0 1 400
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext250000252500.excluded15_5 :
              Certificates.ExcludedOn (model15.B 5 ++ [step15.q]) 9000000000000 (model15.caps 5) (model15.ord 5) 0 1 400
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext250000252500.excluded15_6 :
              Certificates.ExcludedOn (model15.B 6 ++ [step15.q]) 9000000000000 (model15.caps 6) (model15.ord 6) 0 1 400
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext250000252500.excluded15_7 :
              Certificates.ExcludedOn (model15.B 7 ++ [step15.q]) 9000000000000 (model15.caps 7) (model15.ord 7) 0 1 400
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext250000252500.excluded15_9 :
              Certificates.ExcludedOn (model15.B 9 ++ [step15.q]) 9000000000000 (model15.caps 9) (model15.ord 9) 0 1 400
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext250000252500.checked15 :
              Certificates.StepValid model15 9000000000000 step15 0 1 400
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext250000252500.next15 :
              model15.insert step15 = model16