Documentation

LeanPool.ConwaySoifer.Simplified.Certificates.Steps.Sext2550002600004

Sext 255000 260000 4 #

Kernel-checked forced assignments and closed-interval exclusions.

source
def ConwaySoifer.Simplified.Certificates.Sext255000260000.fan33Owner4Part0 :
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.Sext255000260000.fan33Owner4Part1 :
    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.Sext255000260000.fan33Owner5Part0 :
      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.Sext255000260000.excluded32_0 :
        Certificates.ExcludedOn (model32.B 0 ++ [step32.q]) 9000000000000 (model32.caps 0) (model32.ord 0) 0 1 200
        source
        theorem ConwaySoifer.Simplified.Certificates.Sext255000260000.excluded32_1 :
        Certificates.ExcludedOn (model32.B 1 ++ [step32.q]) 9000000000000 (model32.caps 1) (model32.ord 1) 0 1 200
        source
        theorem ConwaySoifer.Simplified.Certificates.Sext255000260000.excluded32_2 :
        Certificates.ExcludedOn (model32.B 2 ++ [step32.q]) 9000000000000 (model32.caps 2) (model32.ord 2) 0 1 200
        source
        theorem ConwaySoifer.Simplified.Certificates.Sext255000260000.excluded32_3 :
        Certificates.ExcludedOn (model32.B 3 ++ [step32.q]) 9000000000000 (model32.caps 3) (model32.ord 3) 0 1 200
        source
        theorem ConwaySoifer.Simplified.Certificates.Sext255000260000.excluded32_5 :
        Certificates.ExcludedOn (model32.B 5 ++ [step32.q]) 9000000000000 (model32.caps 5) (model32.ord 5) 0 1 200
        source
        theorem ConwaySoifer.Simplified.Certificates.Sext255000260000.excluded32_6 :
        Certificates.ExcludedOn (model32.B 6 ++ [step32.q]) 9000000000000 (model32.caps 6) (model32.ord 6) 0 1 200
        source
        theorem ConwaySoifer.Simplified.Certificates.Sext255000260000.excluded32_7 :
        Certificates.ExcludedOn (model32.B 7 ++ [step32.q]) 9000000000000 (model32.caps 7) (model32.ord 7) 0 1 200
        source
        theorem ConwaySoifer.Simplified.Certificates.Sext255000260000.excluded32_8 :
        Certificates.ExcludedOn (model32.B 8 ++ [step32.q]) 9000000000000 (model32.caps 8) (model32.ord 8) 0 1 200
        source
        theorem ConwaySoifer.Simplified.Certificates.Sext255000260000.excluded32_9 :
        Certificates.ExcludedOn (model32.B 9 ++ [step32.q]) 9000000000000 (model32.caps 9) (model32.ord 9) 0 1 200
        source
        theorem ConwaySoifer.Simplified.Certificates.Sext255000260000.checked32 :
        Certificates.StepValid model32 9000000000000 step32 0 1 200
        source
        theorem ConwaySoifer.Simplified.Certificates.Sext255000260000.next32 :
        model32.insert step32 = model33
        source
        theorem ConwaySoifer.Simplified.Certificates.Sext255000260000.excluded33_1 :
        Certificates.ExcludedOn (model33.B 1 ++ [step33.q]) 9000000000000 (model33.caps 1) (model33.ord 1) 0 1 200
        source
        theorem ConwaySoifer.Simplified.Certificates.Sext255000260000.excluded33_2 :
        Certificates.ExcludedOn (model33.B 2 ++ [step33.q]) 9000000000000 (model33.caps 2) (model33.ord 2) 0 1 200
        source
        theorem ConwaySoifer.Simplified.Certificates.Sext255000260000.excluded33_3 :
        Certificates.ExcludedOn (model33.B 3 ++ [step33.q]) 9000000000000 (model33.caps 3) (model33.ord 3) 0 1 200
        source
        theorem ConwaySoifer.Simplified.Certificates.Sext255000260000.excluded33_4 :
        Certificates.ExcludedOn (model33.B 4 ++ [step33.q]) 9000000000000 (model33.caps 4) (model33.ord 4) 0 1 200
        source
        theorem ConwaySoifer.Simplified.Certificates.Sext255000260000.excluded33_5 :
        Certificates.ExcludedOn (model33.B 5 ++ [step33.q]) 9000000000000 (model33.caps 5) (model33.ord 5) 0 1 200
        source
        theorem ConwaySoifer.Simplified.Certificates.Sext255000260000.excluded33_6 :
        Certificates.ExcludedOn (model33.B 6 ++ [step33.q]) 9000000000000 (model33.caps 6) (model33.ord 6) 0 1 200
        source
        theorem ConwaySoifer.Simplified.Certificates.Sext255000260000.excluded33_7 :
        Certificates.ExcludedOn (model33.B 7 ++ [step33.q]) 9000000000000 (model33.caps 7) (model33.ord 7) 0 1 200
        source
        theorem ConwaySoifer.Simplified.Certificates.Sext255000260000.excluded33_8 :
        Certificates.ExcludedOn (model33.B 8 ++ [step33.q]) 9000000000000 (model33.caps 8) (model33.ord 8) 0 1 200
        source
        theorem ConwaySoifer.Simplified.Certificates.Sext255000260000.excluded33_9 :
        Certificates.ExcludedOn (model33.B 9 ++ [step33.q]) 9000000000000 (model33.caps 9) (model33.ord 9) 0 1 200
        source
        theorem ConwaySoifer.Simplified.Certificates.Sext255000260000.checked33 :
        Certificates.StepValid model33 9000000000000 step33 0 1 200
        source
        theorem ConwaySoifer.Simplified.Certificates.Sext255000260000.next33 :
        model33.insert step33 = model34
        source
        theorem ConwaySoifer.Simplified.Certificates.Sext255000260000.excluded34_1 :
        Certificates.ExcludedOn (model34.B 1 ++ [step34.q]) 9000000000000 (model34.caps 1) (model34.ord 1) 0 1 200
        source
        theorem ConwaySoifer.Simplified.Certificates.Sext255000260000.excluded34_2 :
        Certificates.ExcludedOn (model34.B 2 ++ [step34.q]) 9000000000000 (model34.caps 2) (model34.ord 2) 0 1 200
        source
        theorem ConwaySoifer.Simplified.Certificates.Sext255000260000.excluded34_3 :
        Certificates.ExcludedOn (model34.B 3 ++ [step34.q]) 9000000000000 (model34.caps 3) (model34.ord 3) 0 1 200
        source
        theorem ConwaySoifer.Simplified.Certificates.Sext255000260000.excluded34_4 :
        Certificates.ExcludedOn (model34.B 4 ++ [step34.q]) 9000000000000 (model34.caps 4) (model34.ord 4) 0 1 200
        source
        theorem ConwaySoifer.Simplified.Certificates.Sext255000260000.excluded34_5 :
        Certificates.ExcludedOn (model34.B 5 ++ [step34.q]) 9000000000000 (model34.caps 5) (model34.ord 5) 0 1 200
        source
        theorem ConwaySoifer.Simplified.Certificates.Sext255000260000.excluded34_6 :
        Certificates.ExcludedOn (model34.B 6 ++ [step34.q]) 9000000000000 (model34.caps 6) (model34.ord 6) 0 1 200
        source
        theorem ConwaySoifer.Simplified.Certificates.Sext255000260000.excluded34_7 :
        Certificates.ExcludedOn (model34.B 7 ++ [step34.q]) 9000000000000 (model34.caps 7) (model34.ord 7) 0 1 200
        source
        theorem ConwaySoifer.Simplified.Certificates.Sext255000260000.excluded34_8 :
        Certificates.ExcludedOn (model34.B 8 ++ [step34.q]) 9000000000000 (model34.caps 8) (model34.ord 8) 0 1 200
        source
        theorem ConwaySoifer.Simplified.Certificates.Sext255000260000.excluded34_9 :
        Certificates.ExcludedOn (model34.B 9 ++ [step34.q]) 9000000000000 (model34.caps 9) (model34.ord 9) 0 1 200
        source
        theorem ConwaySoifer.Simplified.Certificates.Sext255000260000.checked34 :
        Certificates.StepValid model34 9000000000000 step34 0 1 200
        source
        theorem ConwaySoifer.Simplified.Certificates.Sext255000260000.next34 :
        model34.insert step34 = model35