Documentation

LeanPool.ConwaySoifer.Simplified.Certificates.Steps.Sext2800002900005

Sext 280000 290000 5 #

Kernel-checked forced assignments and closed-interval exclusions.

source
def ConwaySoifer.Simplified.Certificates.Sext280000290000.fan40Owner4Part0 :
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.Sext280000290000.fan41Owner3Part0 :
    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.Sext280000290000.fan41Owner4Part0 :
      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.Sext280000290000.fan42Owner2Part0 :
        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.Sext280000290000.fan42Owner3Part0 :
          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.Sext280000290000.excluded40_1 :
            Certificates.ExcludedOn (model40.B 1 ++ [step40.q]) 9000000000000 (model40.caps 1) (model40.ord 1) 0 1 100
            source
            theorem ConwaySoifer.Simplified.Certificates.Sext280000290000.excluded40_2 :
            Certificates.ExcludedOn (model40.B 2 ++ [step40.q]) 9000000000000 (model40.caps 2) (model40.ord 2) 0 1 100
            source
            theorem ConwaySoifer.Simplified.Certificates.Sext280000290000.excluded40_3 :
            Certificates.ExcludedOn (model40.B 3 ++ [step40.q]) 9000000000000 (model40.caps 3) (model40.ord 3) 0 1 100
            source
            theorem ConwaySoifer.Simplified.Certificates.Sext280000290000.excluded40_4 :
            Certificates.ExcludedOn (model40.B 4 ++ [step40.q]) 9000000000000 (model40.caps 4) (model40.ord 4) 0 1 100
            source
            theorem ConwaySoifer.Simplified.Certificates.Sext280000290000.excluded40_5 :
            Certificates.ExcludedOn (model40.B 5 ++ [step40.q]) 9000000000000 (model40.caps 5) (model40.ord 5) 0 1 100
            source
            theorem ConwaySoifer.Simplified.Certificates.Sext280000290000.excluded40_6 :
            Certificates.ExcludedOn (model40.B 6 ++ [step40.q]) 9000000000000 (model40.caps 6) (model40.ord 6) 0 1 100
            source
            theorem ConwaySoifer.Simplified.Certificates.Sext280000290000.excluded40_7 :
            Certificates.ExcludedOn (model40.B 7 ++ [step40.q]) 9000000000000 (model40.caps 7) (model40.ord 7) 0 1 100
            source
            theorem ConwaySoifer.Simplified.Certificates.Sext280000290000.excluded40_8 :
            Certificates.ExcludedOn (model40.B 8 ++ [step40.q]) 9000000000000 (model40.caps 8) (model40.ord 8) 0 1 100
            source
            theorem ConwaySoifer.Simplified.Certificates.Sext280000290000.excluded40_9 :
            Certificates.ExcludedOn (model40.B 9 ++ [step40.q]) 9000000000000 (model40.caps 9) (model40.ord 9) 0 1 100
            source
            theorem ConwaySoifer.Simplified.Certificates.Sext280000290000.checked40 :
            Certificates.StepValid model40 9000000000000 step40 0 1 100
            source
            theorem ConwaySoifer.Simplified.Certificates.Sext280000290000.next40 :
            model40.insert step40 = model41
            source
            theorem ConwaySoifer.Simplified.Certificates.Sext280000290000.excluded41_1 :
            Certificates.ExcludedOn (model41.B 1 ++ [step41.q]) 9000000000000 (model41.caps 1) (model41.ord 1) 0 1 100
            source
            theorem ConwaySoifer.Simplified.Certificates.Sext280000290000.excluded41_2 :
            Certificates.ExcludedOn (model41.B 2 ++ [step41.q]) 9000000000000 (model41.caps 2) (model41.ord 2) 0 1 100
            source
            theorem ConwaySoifer.Simplified.Certificates.Sext280000290000.excluded41_3 :
            Certificates.ExcludedOn (model41.B 3 ++ [step41.q]) 9000000000000 (model41.caps 3) (model41.ord 3) 0 1 100
            source
            theorem ConwaySoifer.Simplified.Certificates.Sext280000290000.excluded41_4 :
            Certificates.ExcludedOn (model41.B 4 ++ [step41.q]) 9000000000000 (model41.caps 4) (model41.ord 4) 0 1 100
            source
            theorem ConwaySoifer.Simplified.Certificates.Sext280000290000.excluded41_5 :
            Certificates.ExcludedOn (model41.B 5 ++ [step41.q]) 9000000000000 (model41.caps 5) (model41.ord 5) 0 1 100
            source
            theorem ConwaySoifer.Simplified.Certificates.Sext280000290000.excluded41_6 :
            Certificates.ExcludedOn (model41.B 6 ++ [step41.q]) 9000000000000 (model41.caps 6) (model41.ord 6) 0 1 100
            source
            theorem ConwaySoifer.Simplified.Certificates.Sext280000290000.excluded41_7 :
            Certificates.ExcludedOn (model41.B 7 ++ [step41.q]) 9000000000000 (model41.caps 7) (model41.ord 7) 0 1 100
            source
            theorem ConwaySoifer.Simplified.Certificates.Sext280000290000.excluded41_8 :
            Certificates.ExcludedOn (model41.B 8 ++ [step41.q]) 9000000000000 (model41.caps 8) (model41.ord 8) 0 1 100
            source
            theorem ConwaySoifer.Simplified.Certificates.Sext280000290000.excluded41_9 :
            Certificates.ExcludedOn (model41.B 9 ++ [step41.q]) 9000000000000 (model41.caps 9) (model41.ord 9) 0 1 100
            source
            theorem ConwaySoifer.Simplified.Certificates.Sext280000290000.checked41 :
            Certificates.StepValid model41 9000000000000 step41 0 1 100
            source
            theorem ConwaySoifer.Simplified.Certificates.Sext280000290000.next41 :
            model41.insert step41 = model42
            source
            theorem ConwaySoifer.Simplified.Certificates.Sext280000290000.excluded42_1 :
            Certificates.ExcludedOn (model42.B 1 ++ [step42.q]) 9000000000000 (model42.caps 1) (model42.ord 1) 0 1 100
            source
            theorem ConwaySoifer.Simplified.Certificates.Sext280000290000.excluded42_2 :
            Certificates.ExcludedOn (model42.B 2 ++ [step42.q]) 9000000000000 (model42.caps 2) (model42.ord 2) 0 1 100
            source
            theorem ConwaySoifer.Simplified.Certificates.Sext280000290000.excluded42_3 :
            Certificates.ExcludedOn (model42.B 3 ++ [step42.q]) 9000000000000 (model42.caps 3) (model42.ord 3) 0 1 100
            source
            theorem ConwaySoifer.Simplified.Certificates.Sext280000290000.excluded42_4 :
            Certificates.ExcludedOn (model42.B 4 ++ [step42.q]) 9000000000000 (model42.caps 4) (model42.ord 4) 0 1 100
            source
            theorem ConwaySoifer.Simplified.Certificates.Sext280000290000.excluded42_5 :
            Certificates.ExcludedOn (model42.B 5 ++ [step42.q]) 9000000000000 (model42.caps 5) (model42.ord 5) 0 1 100
            source
            theorem ConwaySoifer.Simplified.Certificates.Sext280000290000.excluded42_6 :
            Certificates.ExcludedOn (model42.B 6 ++ [step42.q]) 9000000000000 (model42.caps 6) (model42.ord 6) 0 1 100
            source
            theorem ConwaySoifer.Simplified.Certificates.Sext280000290000.excluded42_7 :
            Certificates.ExcludedOn (model42.B 7 ++ [step42.q]) 9000000000000 (model42.caps 7) (model42.ord 7) 0 1 100
            source
            theorem ConwaySoifer.Simplified.Certificates.Sext280000290000.excluded42_8 :
            Certificates.ExcludedOn (model42.B 8 ++ [step42.q]) 9000000000000 (model42.caps 8) (model42.ord 8) 0 1 100
            source
            theorem ConwaySoifer.Simplified.Certificates.Sext280000290000.excluded42_9 :
            Certificates.ExcludedOn (model42.B 9 ++ [step42.q]) 9000000000000 (model42.caps 9) (model42.ord 9) 0 1 100
            source
            theorem ConwaySoifer.Simplified.Certificates.Sext280000290000.checked42 :
            Certificates.StepValid model42 9000000000000 step42 0 1 100
            source
            theorem ConwaySoifer.Simplified.Certificates.Sext280000290000.next42 :
            model42.insert step42 = model43