Documentation

LeanPool.ConwaySoifer.Simplified.Certificates.Steps.Aown1100001200002

Aown 110000 120000 2 #

Kernel-checked forced assignments and closed-interval exclusions.

source
def ConwaySoifer.Simplified.Certificates.Aown110000120000.fan16Owner3Part0 :
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.Aown110000120000.excluded16_1 :
    Certificates.ExcludedOn (model16.B 1 ++ [step16.q]) 9000000000000 (model16.caps 1) (model16.ord 1) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Aown110000120000.excluded16_2 :
    Certificates.ExcludedOn (model16.B 2 ++ [step16.q]) 9000000000000 (model16.caps 2) (model16.ord 2) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Aown110000120000.excluded16_3 :
    Certificates.ExcludedOn (model16.B 3 ++ [step16.q]) 9000000000000 (model16.caps 3) (model16.ord 3) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Aown110000120000.excluded16_4 :
    Certificates.ExcludedOn (model16.B 4 ++ [step16.q]) 9000000000000 (model16.caps 4) (model16.ord 4) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Aown110000120000.excluded16_5 :
    Certificates.ExcludedOn (model16.B 5 ++ [step16.q]) 9000000000000 (model16.caps 5) (model16.ord 5) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Aown110000120000.excluded16_6 :
    Certificates.ExcludedOn (model16.B 6 ++ [step16.q]) 9000000000000 (model16.caps 6) (model16.ord 6) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Aown110000120000.excluded16_7 :
    Certificates.ExcludedOn (model16.B 7 ++ [step16.q]) 9000000000000 (model16.caps 7) (model16.ord 7) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Aown110000120000.excluded16_8 :
    Certificates.ExcludedOn (model16.B 8 ++ [step16.q]) 9000000000000 (model16.caps 8) (model16.ord 8) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Aown110000120000.excluded16_9 :
    Certificates.ExcludedOn (model16.B 9 ++ [step16.q]) 9000000000000 (model16.caps 9) (model16.ord 9) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Aown110000120000.checked16 :
    Certificates.StepValid model16 9000000000000 step16 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Aown110000120000.next16 :
    model16.insert step16 = model17