Documentation

LeanPool.ConwaySoifer.Simplified.Certificates.Steps.Aown2800002900002

Aown 280000 290000 2 #

Kernel-checked forced assignments and closed-interval exclusions.

source
def ConwaySoifer.Simplified.Certificates.Aown280000290000.fan16Owner2Part0 :
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.Aown280000290000.fan17Owner0Part0 :
    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.Aown280000290000.fan17Owner0Part1 :
      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.Aown280000290000.fan17Owner0Part2 :
        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.Aown280000290000.excluded16_1 :
          Certificates.ExcludedOn (model16.B 1 ++ [step16.q]) 9000000000000 (model16.caps 1) (model16.ord 1) 0 1 100
          source
          theorem ConwaySoifer.Simplified.Certificates.Aown280000290000.excluded16_2 :
          Certificates.ExcludedOn (model16.B 2 ++ [step16.q]) 9000000000000 (model16.caps 2) (model16.ord 2) 0 1 100
          source
          theorem ConwaySoifer.Simplified.Certificates.Aown280000290000.excluded16_3 :
          Certificates.ExcludedOn (model16.B 3 ++ [step16.q]) 9000000000000 (model16.caps 3) (model16.ord 3) 0 1 100
          source
          theorem ConwaySoifer.Simplified.Certificates.Aown280000290000.excluded16_4 :
          Certificates.ExcludedOn (model16.B 4 ++ [step16.q]) 9000000000000 (model16.caps 4) (model16.ord 4) 0 1 100
          source
          theorem ConwaySoifer.Simplified.Certificates.Aown280000290000.excluded16_5 :
          Certificates.ExcludedOn (model16.B 5 ++ [step16.q]) 9000000000000 (model16.caps 5) (model16.ord 5) 0 1 100
          source
          theorem ConwaySoifer.Simplified.Certificates.Aown280000290000.excluded16_6 :
          Certificates.ExcludedOn (model16.B 6 ++ [step16.q]) 9000000000000 (model16.caps 6) (model16.ord 6) 0 1 100
          source
          theorem ConwaySoifer.Simplified.Certificates.Aown280000290000.excluded16_7 :
          Certificates.ExcludedOn (model16.B 7 ++ [step16.q]) 9000000000000 (model16.caps 7) (model16.ord 7) 0 1 100
          source
          theorem ConwaySoifer.Simplified.Certificates.Aown280000290000.excluded16_8 :
          Certificates.ExcludedOn (model16.B 8 ++ [step16.q]) 9000000000000 (model16.caps 8) (model16.ord 8) 0 1 100
          source
          theorem ConwaySoifer.Simplified.Certificates.Aown280000290000.excluded16_9 :
          Certificates.ExcludedOn (model16.B 9 ++ [step16.q]) 9000000000000 (model16.caps 9) (model16.ord 9) 0 1 100
          source
          theorem ConwaySoifer.Simplified.Certificates.Aown280000290000.checked16 :
          Certificates.StepValid model16 9000000000000 step16 0 1 100
          source
          theorem ConwaySoifer.Simplified.Certificates.Aown280000290000.next16 :
          model16.insert step16 = model17
          source
          theorem ConwaySoifer.Simplified.Certificates.Aown280000290000.excluded17_0 :
          Certificates.ExcludedOn (model17.B 0 ++ [step17.q]) 9000000000000 (model17.caps 0) (model17.ord 0) 0 1 100
          source
          theorem ConwaySoifer.Simplified.Certificates.Aown280000290000.excluded17_1 :
          Certificates.ExcludedOn (model17.B 1 ++ [step17.q]) 9000000000000 (model17.caps 1) (model17.ord 1) 0 1 100
          source
          theorem ConwaySoifer.Simplified.Certificates.Aown280000290000.excluded17_2 :
          Certificates.ExcludedOn (model17.B 2 ++ [step17.q]) 9000000000000 (model17.caps 2) (model17.ord 2) 0 1 100
          source
          theorem ConwaySoifer.Simplified.Certificates.Aown280000290000.excluded17_3 :
          Certificates.ExcludedOn (model17.B 3 ++ [step17.q]) 9000000000000 (model17.caps 3) (model17.ord 3) 0 1 100
          source
          theorem ConwaySoifer.Simplified.Certificates.Aown280000290000.excluded17_4 :
          Certificates.ExcludedOn (model17.B 4 ++ [step17.q]) 9000000000000 (model17.caps 4) (model17.ord 4) 0 1 100
          source
          theorem ConwaySoifer.Simplified.Certificates.Aown280000290000.excluded17_5 :
          Certificates.ExcludedOn (model17.B 5 ++ [step17.q]) 9000000000000 (model17.caps 5) (model17.ord 5) 0 1 100
          source
          theorem ConwaySoifer.Simplified.Certificates.Aown280000290000.excluded17_7 :
          Certificates.ExcludedOn (model17.B 7 ++ [step17.q]) 9000000000000 (model17.caps 7) (model17.ord 7) 0 1 100
          source
          theorem ConwaySoifer.Simplified.Certificates.Aown280000290000.excluded17_8 :
          Certificates.ExcludedOn (model17.B 8 ++ [step17.q]) 9000000000000 (model17.caps 8) (model17.ord 8) 0 1 100
          source
          theorem ConwaySoifer.Simplified.Certificates.Aown280000290000.excluded17_9 :
          Certificates.ExcludedOn (model17.B 9 ++ [step17.q]) 9000000000000 (model17.caps 9) (model17.ord 9) 0 1 100
          source
          theorem ConwaySoifer.Simplified.Certificates.Aown280000290000.checked17 :
          Certificates.StepValid model17 9000000000000 step17 0 1 100
          source
          theorem ConwaySoifer.Simplified.Certificates.Aown280000290000.next17 :
          model17.insert step17 = model18
          source
          theorem ConwaySoifer.Simplified.Certificates.Aown280000290000.excluded18_1 :
          Certificates.ExcludedOn (model18.B 1 ++ [step18.q]) 9000000000000 (model18.caps 1) (model18.ord 1) 0 1 100
          source
          theorem ConwaySoifer.Simplified.Certificates.Aown280000290000.excluded18_2 :
          Certificates.ExcludedOn (model18.B 2 ++ [step18.q]) 9000000000000 (model18.caps 2) (model18.ord 2) 0 1 100
          source
          theorem ConwaySoifer.Simplified.Certificates.Aown280000290000.excluded18_3 :
          Certificates.ExcludedOn (model18.B 3 ++ [step18.q]) 9000000000000 (model18.caps 3) (model18.ord 3) 0 1 100
          source
          theorem ConwaySoifer.Simplified.Certificates.Aown280000290000.excluded18_4 :
          Certificates.ExcludedOn (model18.B 4 ++ [step18.q]) 9000000000000 (model18.caps 4) (model18.ord 4) 0 1 100
          source
          theorem ConwaySoifer.Simplified.Certificates.Aown280000290000.excluded18_5 :
          Certificates.ExcludedOn (model18.B 5 ++ [step18.q]) 9000000000000 (model18.caps 5) (model18.ord 5) 0 1 100
          source
          theorem ConwaySoifer.Simplified.Certificates.Aown280000290000.excluded18_6 :
          Certificates.ExcludedOn (model18.B 6 ++ [step18.q]) 9000000000000 (model18.caps 6) (model18.ord 6) 0 1 100
          source
          theorem ConwaySoifer.Simplified.Certificates.Aown280000290000.excluded18_7 :
          Certificates.ExcludedOn (model18.B 7 ++ [step18.q]) 9000000000000 (model18.caps 7) (model18.ord 7) 0 1 100
          source
          theorem ConwaySoifer.Simplified.Certificates.Aown280000290000.excluded18_8 :
          Certificates.ExcludedOn (model18.B 8 ++ [step18.q]) 9000000000000 (model18.caps 8) (model18.ord 8) 0 1 100
          source
          theorem ConwaySoifer.Simplified.Certificates.Aown280000290000.excluded18_9 :
          Certificates.ExcludedOn (model18.B 9 ++ [step18.q]) 9000000000000 (model18.caps 9) (model18.ord 9) 0 1 100
          source
          theorem ConwaySoifer.Simplified.Certificates.Aown280000290000.checked18 :
          Certificates.StepValid model18 9000000000000 step18 0 1 100
          source
          theorem ConwaySoifer.Simplified.Certificates.Aown280000290000.next18 :
          model18.insert step18 = model19