Documentation

LeanPool.ConwaySoifer.Simplified.Certificates.Steps.Sext1100001200004

Sext 110000 120000 4 #

Kernel-checked forced assignments and closed-interval exclusions.

source
def ConwaySoifer.Simplified.Certificates.Sext110000120000.fan33Owner0Part0 :
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.Sext110000120000.fan33Owner0Part1 :
    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.Sext110000120000.fan33Owner3Part0 :
      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.Sext110000120000.fan37Owner3Part0 :
        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.Sext110000120000.fan38Owner3Part0 :
          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.Sext110000120000.fan39Owner2Part0 :
            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.Sext110000120000.excluded32_0 :
              Certificates.ExcludedOn (model32.B 0 ++ [step32.q]) 9000000000000 (model32.caps 0) (model32.ord 0) 0 1 100
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext110000120000.excluded32_1 :
              Certificates.ExcludedOn (model32.B 1 ++ [step32.q]) 9000000000000 (model32.caps 1) (model32.ord 1) 0 1 100
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext110000120000.excluded32_2 :
              Certificates.ExcludedOn (model32.B 2 ++ [step32.q]) 9000000000000 (model32.caps 2) (model32.ord 2) 0 1 100
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext110000120000.excluded32_4 :
              Certificates.ExcludedOn (model32.B 4 ++ [step32.q]) 9000000000000 (model32.caps 4) (model32.ord 4) 0 1 100
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext110000120000.excluded32_5 :
              Certificates.ExcludedOn (model32.B 5 ++ [step32.q]) 9000000000000 (model32.caps 5) (model32.ord 5) 0 1 100
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext110000120000.excluded32_6 :
              Certificates.ExcludedOn (model32.B 6 ++ [step32.q]) 9000000000000 (model32.caps 6) (model32.ord 6) 0 1 100
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext110000120000.excluded32_7 :
              Certificates.ExcludedOn (model32.B 7 ++ [step32.q]) 9000000000000 (model32.caps 7) (model32.ord 7) 0 1 100
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext110000120000.excluded32_8 :
              Certificates.ExcludedOn (model32.B 8 ++ [step32.q]) 9000000000000 (model32.caps 8) (model32.ord 8) 0 1 100
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext110000120000.excluded32_9 :
              Certificates.ExcludedOn (model32.B 9 ++ [step32.q]) 9000000000000 (model32.caps 9) (model32.ord 9) 0 1 100
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext110000120000.checked32 :
              Certificates.StepValid model32 9000000000000 step32 0 1 100
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext110000120000.next32 :
              model32.insert step32 = model33
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext110000120000.excluded33_0 :
              Certificates.ExcludedOn (model33.B 0 ++ [step33.q]) 9000000000000 (model33.caps 0) (model33.ord 0) 0 1 100
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext110000120000.excluded33_1 :
              Certificates.ExcludedOn (model33.B 1 ++ [step33.q]) 9000000000000 (model33.caps 1) (model33.ord 1) 0 1 100
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext110000120000.excluded33_2 :
              Certificates.ExcludedOn (model33.B 2 ++ [step33.q]) 9000000000000 (model33.caps 2) (model33.ord 2) 0 1 100
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext110000120000.excluded33_3 :
              Certificates.ExcludedOn (model33.B 3 ++ [step33.q]) 9000000000000 (model33.caps 3) (model33.ord 3) 0 1 100
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext110000120000.excluded33_5 :
              Certificates.ExcludedOn (model33.B 5 ++ [step33.q]) 9000000000000 (model33.caps 5) (model33.ord 5) 0 1 100
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext110000120000.excluded33_6 :
              Certificates.ExcludedOn (model33.B 6 ++ [step33.q]) 9000000000000 (model33.caps 6) (model33.ord 6) 0 1 100
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext110000120000.excluded33_7 :
              Certificates.ExcludedOn (model33.B 7 ++ [step33.q]) 9000000000000 (model33.caps 7) (model33.ord 7) 0 1 100
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext110000120000.excluded33_8 :
              Certificates.ExcludedOn (model33.B 8 ++ [step33.q]) 9000000000000 (model33.caps 8) (model33.ord 8) 0 1 100
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext110000120000.excluded33_9 :
              Certificates.ExcludedOn (model33.B 9 ++ [step33.q]) 9000000000000 (model33.caps 9) (model33.ord 9) 0 1 100
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext110000120000.checked33 :
              Certificates.StepValid model33 9000000000000 step33 0 1 100
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext110000120000.next33 :
              model33.insert step33 = model34
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext110000120000.excluded34_0 :
              Certificates.ExcludedOn (model34.B 0 ++ [step34.q]) 9000000000000 (model34.caps 0) (model34.ord 0) 0 1 100
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext110000120000.excluded34_1 :
              Certificates.ExcludedOn (model34.B 1 ++ [step34.q]) 9000000000000 (model34.caps 1) (model34.ord 1) 0 1 100
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext110000120000.excluded34_3 :
              Certificates.ExcludedOn (model34.B 3 ++ [step34.q]) 9000000000000 (model34.caps 3) (model34.ord 3) 0 1 100
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext110000120000.excluded34_4 :
              Certificates.ExcludedOn (model34.B 4 ++ [step34.q]) 9000000000000 (model34.caps 4) (model34.ord 4) 0 1 100
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext110000120000.excluded34_5 :
              Certificates.ExcludedOn (model34.B 5 ++ [step34.q]) 9000000000000 (model34.caps 5) (model34.ord 5) 0 1 100
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext110000120000.excluded34_6 :
              Certificates.ExcludedOn (model34.B 6 ++ [step34.q]) 9000000000000 (model34.caps 6) (model34.ord 6) 0 1 100
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext110000120000.excluded34_7 :
              Certificates.ExcludedOn (model34.B 7 ++ [step34.q]) 9000000000000 (model34.caps 7) (model34.ord 7) 0 1 100
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext110000120000.excluded34_8 :
              Certificates.ExcludedOn (model34.B 8 ++ [step34.q]) 9000000000000 (model34.caps 8) (model34.ord 8) 0 1 100
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext110000120000.excluded34_9 :
              Certificates.ExcludedOn (model34.B 9 ++ [step34.q]) 9000000000000 (model34.caps 9) (model34.ord 9) 0 1 100
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext110000120000.checked34 :
              Certificates.StepValid model34 9000000000000 step34 0 1 100
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext110000120000.next34 :
              model34.insert step34 = model35
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext110000120000.excluded35_0 :
              Certificates.ExcludedOn (model35.B 0 ++ [step35.q]) 9000000000000 (model35.caps 0) (model35.ord 0) 0 1 100
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext110000120000.excluded35_1 :
              Certificates.ExcludedOn (model35.B 1 ++ [step35.q]) 9000000000000 (model35.caps 1) (model35.ord 1) 0 1 100
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext110000120000.excluded35_2 :
              Certificates.ExcludedOn (model35.B 2 ++ [step35.q]) 9000000000000 (model35.caps 2) (model35.ord 2) 0 1 100
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext110000120000.excluded35_3 :
              Certificates.ExcludedOn (model35.B 3 ++ [step35.q]) 9000000000000 (model35.caps 3) (model35.ord 3) 0 1 100
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext110000120000.excluded35_4 :
              Certificates.ExcludedOn (model35.B 4 ++ [step35.q]) 9000000000000 (model35.caps 4) (model35.ord 4) 0 1 100
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext110000120000.excluded35_5 :
              Certificates.ExcludedOn (model35.B 5 ++ [step35.q]) 9000000000000 (model35.caps 5) (model35.ord 5) 0 1 100
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext110000120000.excluded35_6 :
              Certificates.ExcludedOn (model35.B 6 ++ [step35.q]) 9000000000000 (model35.caps 6) (model35.ord 6) 0 1 100
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext110000120000.excluded35_7 :
              Certificates.ExcludedOn (model35.B 7 ++ [step35.q]) 9000000000000 (model35.caps 7) (model35.ord 7) 0 1 100
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext110000120000.excluded35_9 :
              Certificates.ExcludedOn (model35.B 9 ++ [step35.q]) 9000000000000 (model35.caps 9) (model35.ord 9) 0 1 100
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext110000120000.checked35 :
              Certificates.StepValid model35 9000000000000 step35 0 1 100
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext110000120000.next35 :
              model35.insert step35 = model36
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext110000120000.excluded36_0 :
              Certificates.ExcludedOn (model36.B 0 ++ [step36.q]) 9000000000000 (model36.caps 0) (model36.ord 0) 0 1 100
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext110000120000.excluded36_1 :
              Certificates.ExcludedOn (model36.B 1 ++ [step36.q]) 9000000000000 (model36.caps 1) (model36.ord 1) 0 1 100
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext110000120000.excluded36_2 :
              Certificates.ExcludedOn (model36.B 2 ++ [step36.q]) 9000000000000 (model36.caps 2) (model36.ord 2) 0 1 100
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext110000120000.excluded36_4 :
              Certificates.ExcludedOn (model36.B 4 ++ [step36.q]) 9000000000000 (model36.caps 4) (model36.ord 4) 0 1 100
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext110000120000.excluded36_5 :
              Certificates.ExcludedOn (model36.B 5 ++ [step36.q]) 9000000000000 (model36.caps 5) (model36.ord 5) 0 1 100
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext110000120000.excluded36_6 :
              Certificates.ExcludedOn (model36.B 6 ++ [step36.q]) 9000000000000 (model36.caps 6) (model36.ord 6) 0 1 100
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext110000120000.excluded36_7 :
              Certificates.ExcludedOn (model36.B 7 ++ [step36.q]) 9000000000000 (model36.caps 7) (model36.ord 7) 0 1 100
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext110000120000.excluded36_8 :
              Certificates.ExcludedOn (model36.B 8 ++ [step36.q]) 9000000000000 (model36.caps 8) (model36.ord 8) 0 1 100
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext110000120000.excluded36_9 :
              Certificates.ExcludedOn (model36.B 9 ++ [step36.q]) 9000000000000 (model36.caps 9) (model36.ord 9) 0 1 100
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext110000120000.checked36 :
              Certificates.StepValid model36 9000000000000 step36 0 1 100
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext110000120000.next36 :
              model36.insert step36 = model37
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext110000120000.excluded37_0 :
              Certificates.ExcludedOn (model37.B 0 ++ [step37.q]) 9000000000000 (model37.caps 0) (model37.ord 0) 0 1 100
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext110000120000.excluded37_1 :
              Certificates.ExcludedOn (model37.B 1 ++ [step37.q]) 9000000000000 (model37.caps 1) (model37.ord 1) 0 1 100
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext110000120000.excluded37_3 :
              Certificates.ExcludedOn (model37.B 3 ++ [step37.q]) 9000000000000 (model37.caps 3) (model37.ord 3) 0 1 100
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext110000120000.excluded37_4 :
              Certificates.ExcludedOn (model37.B 4 ++ [step37.q]) 9000000000000 (model37.caps 4) (model37.ord 4) 0 1 100
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext110000120000.excluded37_5 :
              Certificates.ExcludedOn (model37.B 5 ++ [step37.q]) 9000000000000 (model37.caps 5) (model37.ord 5) 0 1 100
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext110000120000.excluded37_6 :
              Certificates.ExcludedOn (model37.B 6 ++ [step37.q]) 9000000000000 (model37.caps 6) (model37.ord 6) 0 1 100
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext110000120000.excluded37_7 :
              Certificates.ExcludedOn (model37.B 7 ++ [step37.q]) 9000000000000 (model37.caps 7) (model37.ord 7) 0 1 100
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext110000120000.excluded37_8 :
              Certificates.ExcludedOn (model37.B 8 ++ [step37.q]) 9000000000000 (model37.caps 8) (model37.ord 8) 0 1 100
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext110000120000.excluded37_9 :
              Certificates.ExcludedOn (model37.B 9 ++ [step37.q]) 9000000000000 (model37.caps 9) (model37.ord 9) 0 1 100
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext110000120000.checked37 :
              Certificates.StepValid model37 9000000000000 step37 0 1 100
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext110000120000.next37 :
              model37.insert step37 = model38
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext110000120000.excluded38_0 :
              Certificates.ExcludedOn (model38.B 0 ++ [step38.q]) 9000000000000 (model38.caps 0) (model38.ord 0) 0 1 100
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext110000120000.excluded38_1 :
              Certificates.ExcludedOn (model38.B 1 ++ [step38.q]) 9000000000000 (model38.caps 1) (model38.ord 1) 0 1 100
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext110000120000.excluded38_3 :
              Certificates.ExcludedOn (model38.B 3 ++ [step38.q]) 9000000000000 (model38.caps 3) (model38.ord 3) 0 1 100
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext110000120000.excluded38_4 :
              Certificates.ExcludedOn (model38.B 4 ++ [step38.q]) 9000000000000 (model38.caps 4) (model38.ord 4) 0 1 100
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext110000120000.excluded38_5 :
              Certificates.ExcludedOn (model38.B 5 ++ [step38.q]) 9000000000000 (model38.caps 5) (model38.ord 5) 0 1 100
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext110000120000.excluded38_6 :
              Certificates.ExcludedOn (model38.B 6 ++ [step38.q]) 9000000000000 (model38.caps 6) (model38.ord 6) 0 1 100
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext110000120000.excluded38_7 :
              Certificates.ExcludedOn (model38.B 7 ++ [step38.q]) 9000000000000 (model38.caps 7) (model38.ord 7) 0 1 100
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext110000120000.excluded38_8 :
              Certificates.ExcludedOn (model38.B 8 ++ [step38.q]) 9000000000000 (model38.caps 8) (model38.ord 8) 0 1 100
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext110000120000.excluded38_9 :
              Certificates.ExcludedOn (model38.B 9 ++ [step38.q]) 9000000000000 (model38.caps 9) (model38.ord 9) 0 1 100
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext110000120000.checked38 :
              Certificates.StepValid model38 9000000000000 step38 0 1 100
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext110000120000.next38 :
              model38.insert step38 = model39
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext110000120000.excluded39_0 :
              Certificates.ExcludedOn (model39.B 0 ++ [step39.q]) 9000000000000 (model39.caps 0) (model39.ord 0) 0 1 100
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext110000120000.excluded39_1 :
              Certificates.ExcludedOn (model39.B 1 ++ [step39.q]) 9000000000000 (model39.caps 1) (model39.ord 1) 0 1 100
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext110000120000.excluded39_2 :
              Certificates.ExcludedOn (model39.B 2 ++ [step39.q]) 9000000000000 (model39.caps 2) (model39.ord 2) 0 1 100
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext110000120000.excluded39_4 :
              Certificates.ExcludedOn (model39.B 4 ++ [step39.q]) 9000000000000 (model39.caps 4) (model39.ord 4) 0 1 100
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext110000120000.excluded39_5 :
              Certificates.ExcludedOn (model39.B 5 ++ [step39.q]) 9000000000000 (model39.caps 5) (model39.ord 5) 0 1 100
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext110000120000.excluded39_6 :
              Certificates.ExcludedOn (model39.B 6 ++ [step39.q]) 9000000000000 (model39.caps 6) (model39.ord 6) 0 1 100
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext110000120000.excluded39_7 :
              Certificates.ExcludedOn (model39.B 7 ++ [step39.q]) 9000000000000 (model39.caps 7) (model39.ord 7) 0 1 100
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext110000120000.excluded39_8 :
              Certificates.ExcludedOn (model39.B 8 ++ [step39.q]) 9000000000000 (model39.caps 8) (model39.ord 8) 0 1 100
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext110000120000.excluded39_9 :
              Certificates.ExcludedOn (model39.B 9 ++ [step39.q]) 9000000000000 (model39.caps 9) (model39.ord 9) 0 1 100
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext110000120000.checked39 :
              Certificates.StepValid model39 9000000000000 step39 0 1 100
              source
              theorem ConwaySoifer.Simplified.Certificates.Sext110000120000.next39 :
              model39.insert step39 = model40