Aown 220000 230000 3 #

Kernel-checked forced assignments and closed-interval exclusions.

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.Aown220000230000.fan24Owner0Part1 :

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.Aown220000230000.fan24Owner0Part2 :

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.Aown220000230000.fan24Owner0Part3 :

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.Aown220000230000.fan24Owner0Part4 :

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.Aown220000230000.fan25Owner0Part0 :

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.Aown220000230000.fan25Owner0Part1 :

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.Aown220000230000.fan25Owner0Part2 :

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.Aown220000230000.fan25Owner0Part3 :

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.Aown220000230000.fan25Owner0Part4 :

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.Aown220000230000.fan27Owner0Part0 :

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.Aown220000230000.fan27Owner0Part1 :

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.Aown220000230000.fan27Owner0Part2 :

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.Aown220000230000.fan27Owner0Part3 :

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.Aown220000230000.fan27Owner0Part4 :

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.Aown220000230000.fan28Owner0Part0 :

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.Aown220000230000.fan28Owner0Part1 :

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.Aown220000230000.fan28Owner0Part2 :

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.Aown220000230000.fan28Owner0Part3 :

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.Aown220000230000.fan28Owner0Part4 :

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.Aown220000230000.fan29Owner2Part0 :

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.Aown220000230000.fan31Owner2Part0 :

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.Aown220000230000.excluded24_0 :

Certificates.ExcludedOn (model24.B 0 ++ [step24.q]) 9000000000000 (model24.caps 0) (model24.ord 0) 0 1 100

source

theorem ConwaySoifer.Simplified.Certificates.Aown220000230000.excluded24_1 :

Certificates.ExcludedOn (model24.B 1 ++ [step24.q]) 9000000000000 (model24.caps 1) (model24.ord 1) 0 1 100

source

theorem ConwaySoifer.Simplified.Certificates.Aown220000230000.excluded24_3 :

Certificates.ExcludedOn (model24.B 3 ++ [step24.q]) 9000000000000 (model24.caps 3) (model24.ord 3) 0 1 100

source

theorem ConwaySoifer.Simplified.Certificates.Aown220000230000.excluded24_4 :

Certificates.ExcludedOn (model24.B 4 ++ [step24.q]) 9000000000000 (model24.caps 4) (model24.ord 4) 0 1 100

source

theorem ConwaySoifer.Simplified.Certificates.Aown220000230000.excluded24_5 :

Certificates.ExcludedOn (model24.B 5 ++ [step24.q]) 9000000000000 (model24.caps 5) (model24.ord 5) 0 1 100

source

theorem ConwaySoifer.Simplified.Certificates.Aown220000230000.excluded24_6 :

Certificates.ExcludedOn (model24.B 6 ++ [step24.q]) 9000000000000 (model24.caps 6) (model24.ord 6) 0 1 100

source

theorem ConwaySoifer.Simplified.Certificates.Aown220000230000.excluded24_7 :

Certificates.ExcludedOn (model24.B 7 ++ [step24.q]) 9000000000000 (model24.caps 7) (model24.ord 7) 0 1 100

source

theorem ConwaySoifer.Simplified.Certificates.Aown220000230000.excluded24_8 :

Certificates.ExcludedOn (model24.B 8 ++ [step24.q]) 9000000000000 (model24.caps 8) (model24.ord 8) 0 1 100

source

theorem ConwaySoifer.Simplified.Certificates.Aown220000230000.excluded24_9 :

Certificates.ExcludedOn (model24.B 9 ++ [step24.q]) 9000000000000 (model24.caps 9) (model24.ord 9) 0 1 100

source

theorem ConwaySoifer.Simplified.Certificates.Aown220000230000.checked24 :

Certificates.StepValid model24 9000000000000 step24 0 1 100

source

theorem ConwaySoifer.Simplified.Certificates.Aown220000230000.next24 :

model24.insert step24 = model25

source

theorem ConwaySoifer.Simplified.Certificates.Aown220000230000.excluded25_0 :

Certificates.ExcludedOn (model25.B 0 ++ [step25.q]) 9000000000000 (model25.caps 0) (model25.ord 0) 0 1 100

source

theorem ConwaySoifer.Simplified.Certificates.Aown220000230000.excluded25_1 :

Certificates.ExcludedOn (model25.B 1 ++ [step25.q]) 9000000000000 (model25.caps 1) (model25.ord 1) 0 1 100

source

theorem ConwaySoifer.Simplified.Certificates.Aown220000230000.excluded25_3 :

Certificates.ExcludedOn (model25.B 3 ++ [step25.q]) 9000000000000 (model25.caps 3) (model25.ord 3) 0 1 100

source

theorem ConwaySoifer.Simplified.Certificates.Aown220000230000.excluded25_4 :

Certificates.ExcludedOn (model25.B 4 ++ [step25.q]) 9000000000000 (model25.caps 4) (model25.ord 4) 0 1 100

source

theorem ConwaySoifer.Simplified.Certificates.Aown220000230000.excluded25_5 :

Certificates.ExcludedOn (model25.B 5 ++ [step25.q]) 9000000000000 (model25.caps 5) (model25.ord 5) 0 1 100

source

theorem ConwaySoifer.Simplified.Certificates.Aown220000230000.excluded25_6 :

Certificates.ExcludedOn (model25.B 6 ++ [step25.q]) 9000000000000 (model25.caps 6) (model25.ord 6) 0 1 100

source

theorem ConwaySoifer.Simplified.Certificates.Aown220000230000.excluded25_7 :

Certificates.ExcludedOn (model25.B 7 ++ [step25.q]) 9000000000000 (model25.caps 7) (model25.ord 7) 0 1 100

source

theorem ConwaySoifer.Simplified.Certificates.Aown220000230000.excluded25_8 :

Certificates.ExcludedOn (model25.B 8 ++ [step25.q]) 9000000000000 (model25.caps 8) (model25.ord 8) 0 1 100

source

theorem ConwaySoifer.Simplified.Certificates.Aown220000230000.excluded25_9 :

Certificates.ExcludedOn (model25.B 9 ++ [step25.q]) 9000000000000 (model25.caps 9) (model25.ord 9) 0 1 100

source

theorem ConwaySoifer.Simplified.Certificates.Aown220000230000.checked25 :

Certificates.StepValid model25 9000000000000 step25 0 1 100

source

theorem ConwaySoifer.Simplified.Certificates.Aown220000230000.next25 :

model25.insert step25 = model26

source

theorem ConwaySoifer.Simplified.Certificates.Aown220000230000.excluded26_0 :

Certificates.ExcludedOn (model26.B 0 ++ [step26.q]) 9000000000000 (model26.caps 0) (model26.ord 0) 0 1 100

source

theorem ConwaySoifer.Simplified.Certificates.Aown220000230000.excluded26_1 :

Certificates.ExcludedOn (model26.B 1 ++ [step26.q]) 9000000000000 (model26.caps 1) (model26.ord 1) 0 1 100

source

theorem ConwaySoifer.Simplified.Certificates.Aown220000230000.excluded26_2 :

Certificates.ExcludedOn (model26.B 2 ++ [step26.q]) 9000000000000 (model26.caps 2) (model26.ord 2) 0 1 100

source

theorem ConwaySoifer.Simplified.Certificates.Aown220000230000.excluded26_3 :

Certificates.ExcludedOn (model26.B 3 ++ [step26.q]) 9000000000000 (model26.caps 3) (model26.ord 3) 0 1 100

source

theorem ConwaySoifer.Simplified.Certificates.Aown220000230000.excluded26_4 :

Certificates.ExcludedOn (model26.B 4 ++ [step26.q]) 9000000000000 (model26.caps 4) (model26.ord 4) 0 1 100

source

theorem ConwaySoifer.Simplified.Certificates.Aown220000230000.excluded26_5 :

Certificates.ExcludedOn (model26.B 5 ++ [step26.q]) 9000000000000 (model26.caps 5) (model26.ord 5) 0 1 100

source

theorem ConwaySoifer.Simplified.Certificates.Aown220000230000.excluded26_6 :

Certificates.ExcludedOn (model26.B 6 ++ [step26.q]) 9000000000000 (model26.caps 6) (model26.ord 6) 0 1 100

source

theorem ConwaySoifer.Simplified.Certificates.Aown220000230000.excluded26_7 :

Certificates.ExcludedOn (model26.B 7 ++ [step26.q]) 9000000000000 (model26.caps 7) (model26.ord 7) 0 1 100

source

theorem ConwaySoifer.Simplified.Certificates.Aown220000230000.excluded26_8 :

Certificates.ExcludedOn (model26.B 8 ++ [step26.q]) 9000000000000 (model26.caps 8) (model26.ord 8) 0 1 100

source

theorem ConwaySoifer.Simplified.Certificates.Aown220000230000.checked26 :

Certificates.StepValid model26 9000000000000 step26 0 1 100

source

theorem ConwaySoifer.Simplified.Certificates.Aown220000230000.next26 :

model26.insert step26 = model27

source

theorem ConwaySoifer.Simplified.Certificates.Aown220000230000.excluded27_0 :

Certificates.ExcludedOn (model27.B 0 ++ [step27.q]) 9000000000000 (model27.caps 0) (model27.ord 0) 0 1 100

source

theorem ConwaySoifer.Simplified.Certificates.Aown220000230000.excluded27_1 :

Certificates.ExcludedOn (model27.B 1 ++ [step27.q]) 9000000000000 (model27.caps 1) (model27.ord 1) 0 1 100

source

theorem ConwaySoifer.Simplified.Certificates.Aown220000230000.excluded27_2 :

Certificates.ExcludedOn (model27.B 2 ++ [step27.q]) 9000000000000 (model27.caps 2) (model27.ord 2) 0 1 100

source

theorem ConwaySoifer.Simplified.Certificates.Aown220000230000.excluded27_3 :

Certificates.ExcludedOn (model27.B 3 ++ [step27.q]) 9000000000000 (model27.caps 3) (model27.ord 3) 0 1 100

source

theorem ConwaySoifer.Simplified.Certificates.Aown220000230000.excluded27_4 :

Certificates.ExcludedOn (model27.B 4 ++ [step27.q]) 9000000000000 (model27.caps 4) (model27.ord 4) 0 1 100

source

theorem ConwaySoifer.Simplified.Certificates.Aown220000230000.excluded27_5 :

Certificates.ExcludedOn (model27.B 5 ++ [step27.q]) 9000000000000 (model27.caps 5) (model27.ord 5) 0 1 100

source

theorem ConwaySoifer.Simplified.Certificates.Aown220000230000.excluded27_7 :

Certificates.ExcludedOn (model27.B 7 ++ [step27.q]) 9000000000000 (model27.caps 7) (model27.ord 7) 0 1 100

source

theorem ConwaySoifer.Simplified.Certificates.Aown220000230000.excluded27_8 :

Certificates.ExcludedOn (model27.B 8 ++ [step27.q]) 9000000000000 (model27.caps 8) (model27.ord 8) 0 1 100

source

theorem ConwaySoifer.Simplified.Certificates.Aown220000230000.excluded27_9 :

Certificates.ExcludedOn (model27.B 9 ++ [step27.q]) 9000000000000 (model27.caps 9) (model27.ord 9) 0 1 100

source

theorem ConwaySoifer.Simplified.Certificates.Aown220000230000.checked27 :

Certificates.StepValid model27 9000000000000 step27 0 1 100

source

theorem ConwaySoifer.Simplified.Certificates.Aown220000230000.next27 :

model27.insert step27 = model28

source

theorem ConwaySoifer.Simplified.Certificates.Aown220000230000.excluded28_0 :

Certificates.ExcludedOn (model28.B 0 ++ [step28.q]) 9000000000000 (model28.caps 0) (model28.ord 0) 0 1 100

source

theorem ConwaySoifer.Simplified.Certificates.Aown220000230000.excluded28_1 :

Certificates.ExcludedOn (model28.B 1 ++ [step28.q]) 9000000000000 (model28.caps 1) (model28.ord 1) 0 1 100

source

theorem ConwaySoifer.Simplified.Certificates.Aown220000230000.excluded28_2 :

Certificates.ExcludedOn (model28.B 2 ++ [step28.q]) 9000000000000 (model28.caps 2) (model28.ord 2) 0 1 100

source

theorem ConwaySoifer.Simplified.Certificates.Aown220000230000.excluded28_3 :

Certificates.ExcludedOn (model28.B 3 ++ [step28.q]) 9000000000000 (model28.caps 3) (model28.ord 3) 0 1 100

source

theorem ConwaySoifer.Simplified.Certificates.Aown220000230000.excluded28_4 :

Certificates.ExcludedOn (model28.B 4 ++ [step28.q]) 9000000000000 (model28.caps 4) (model28.ord 4) 0 1 100

source

theorem ConwaySoifer.Simplified.Certificates.Aown220000230000.excluded28_5 :

Certificates.ExcludedOn (model28.B 5 ++ [step28.q]) 9000000000000 (model28.caps 5) (model28.ord 5) 0 1 100

source

theorem ConwaySoifer.Simplified.Certificates.Aown220000230000.excluded28_7 :

Certificates.ExcludedOn (model28.B 7 ++ [step28.q]) 9000000000000 (model28.caps 7) (model28.ord 7) 0 1 100

source

theorem ConwaySoifer.Simplified.Certificates.Aown220000230000.excluded28_8 :

Certificates.ExcludedOn (model28.B 8 ++ [step28.q]) 9000000000000 (model28.caps 8) (model28.ord 8) 0 1 100

source

theorem ConwaySoifer.Simplified.Certificates.Aown220000230000.excluded28_9 :

Certificates.ExcludedOn (model28.B 9 ++ [step28.q]) 9000000000000 (model28.caps 9) (model28.ord 9) 0 1 100

source

theorem ConwaySoifer.Simplified.Certificates.Aown220000230000.checked28 :

Certificates.StepValid model28 9000000000000 step28 0 1 100

source

theorem ConwaySoifer.Simplified.Certificates.Aown220000230000.next28 :

model28.insert step28 = model29

source

theorem ConwaySoifer.Simplified.Certificates.Aown220000230000.excluded29_1 :

Certificates.ExcludedOn (model29.B 1 ++ [step29.q]) 9000000000000 (model29.caps 1) (model29.ord 1) 0 1 100

source

theorem ConwaySoifer.Simplified.Certificates.Aown220000230000.excluded29_2 :

Certificates.ExcludedOn (model29.B 2 ++ [step29.q]) 9000000000000 (model29.caps 2) (model29.ord 2) 0 1 100

source

theorem ConwaySoifer.Simplified.Certificates.Aown220000230000.excluded29_3 :

Certificates.ExcludedOn (model29.B 3 ++ [step29.q]) 9000000000000 (model29.caps 3) (model29.ord 3) 0 1 100

source

theorem ConwaySoifer.Simplified.Certificates.Aown220000230000.excluded29_4 :

Certificates.ExcludedOn (model29.B 4 ++ [step29.q]) 9000000000000 (model29.caps 4) (model29.ord 4) 0 1 100

source

theorem ConwaySoifer.Simplified.Certificates.Aown220000230000.excluded29_5 :

Certificates.ExcludedOn (model29.B 5 ++ [step29.q]) 9000000000000 (model29.caps 5) (model29.ord 5) 0 1 100

source

theorem ConwaySoifer.Simplified.Certificates.Aown220000230000.excluded29_6 :

Certificates.ExcludedOn (model29.B 6 ++ [step29.q]) 9000000000000 (model29.caps 6) (model29.ord 6) 0 1 100

source

theorem ConwaySoifer.Simplified.Certificates.Aown220000230000.excluded29_7 :

Certificates.ExcludedOn (model29.B 7 ++ [step29.q]) 9000000000000 (model29.caps 7) (model29.ord 7) 0 1 100

source

theorem ConwaySoifer.Simplified.Certificates.Aown220000230000.excluded29_8 :

Certificates.ExcludedOn (model29.B 8 ++ [step29.q]) 9000000000000 (model29.caps 8) (model29.ord 8) 0 1 100

source

theorem ConwaySoifer.Simplified.Certificates.Aown220000230000.excluded29_9 :

Certificates.ExcludedOn (model29.B 9 ++ [step29.q]) 9000000000000 (model29.caps 9) (model29.ord 9) 0 1 100

source

theorem ConwaySoifer.Simplified.Certificates.Aown220000230000.checked29 :

Certificates.StepValid model29 9000000000000 step29 0 1 100

source

theorem ConwaySoifer.Simplified.Certificates.Aown220000230000.next29 :

model29.insert step29 = model30

source

theorem ConwaySoifer.Simplified.Certificates.Aown220000230000.excluded30_0 :

Certificates.ExcludedOn (model30.B 0 ++ [step30.q]) 9000000000000 (model30.caps 0) (model30.ord 0) 0 1 100

source

theorem ConwaySoifer.Simplified.Certificates.Aown220000230000.excluded30_1 :

Certificates.ExcludedOn (model30.B 1 ++ [step30.q]) 9000000000000 (model30.caps 1) (model30.ord 1) 0 1 100

source

theorem ConwaySoifer.Simplified.Certificates.Aown220000230000.excluded30_2 :

Certificates.ExcludedOn (model30.B 2 ++ [step30.q]) 9000000000000 (model30.caps 2) (model30.ord 2) 0 1 100

source

theorem ConwaySoifer.Simplified.Certificates.Aown220000230000.excluded30_3 :

Certificates.ExcludedOn (model30.B 3 ++ [step30.q]) 9000000000000 (model30.caps 3) (model30.ord 3) 0 1 100

source

theorem ConwaySoifer.Simplified.Certificates.Aown220000230000.excluded30_4 :

Certificates.ExcludedOn (model30.B 4 ++ [step30.q]) 9000000000000 (model30.caps 4) (model30.ord 4) 0 1 100

source

theorem ConwaySoifer.Simplified.Certificates.Aown220000230000.excluded30_6 :

Certificates.ExcludedOn (model30.B 6 ++ [step30.q]) 9000000000000 (model30.caps 6) (model30.ord 6) 0 1 100

source

theorem ConwaySoifer.Simplified.Certificates.Aown220000230000.excluded30_7 :

Certificates.ExcludedOn (model30.B 7 ++ [step30.q]) 9000000000000 (model30.caps 7) (model30.ord 7) 0 1 100

source

theorem ConwaySoifer.Simplified.Certificates.Aown220000230000.excluded30_8 :

Certificates.ExcludedOn (model30.B 8 ++ [step30.q]) 9000000000000 (model30.caps 8) (model30.ord 8) 0 1 100

source

theorem ConwaySoifer.Simplified.Certificates.Aown220000230000.excluded30_9 :

Certificates.ExcludedOn (model30.B 9 ++ [step30.q]) 9000000000000 (model30.caps 9) (model30.ord 9) 0 1 100

source

theorem ConwaySoifer.Simplified.Certificates.Aown220000230000.checked30 :

Certificates.StepValid model30 9000000000000 step30 0 1 100

source

theorem ConwaySoifer.Simplified.Certificates.Aown220000230000.next30 :

model30.insert step30 = model31

source

theorem ConwaySoifer.Simplified.Certificates.Aown220000230000.excluded31_1 :

Certificates.ExcludedOn (model31.B 1 ++ [step31.q]) 9000000000000 (model31.caps 1) (model31.ord 1) 0 1 100

source

theorem ConwaySoifer.Simplified.Certificates.Aown220000230000.excluded31_2 :

Certificates.ExcludedOn (model31.B 2 ++ [step31.q]) 9000000000000 (model31.caps 2) (model31.ord 2) 0 1 100

source

theorem ConwaySoifer.Simplified.Certificates.Aown220000230000.excluded31_3 :

Certificates.ExcludedOn (model31.B 3 ++ [step31.q]) 9000000000000 (model31.caps 3) (model31.ord 3) 0 1 100

source

theorem ConwaySoifer.Simplified.Certificates.Aown220000230000.excluded31_4 :

Certificates.ExcludedOn (model31.B 4 ++ [step31.q]) 9000000000000 (model31.caps 4) (model31.ord 4) 0 1 100

source

theorem ConwaySoifer.Simplified.Certificates.Aown220000230000.excluded31_5 :

Certificates.ExcludedOn (model31.B 5 ++ [step31.q]) 9000000000000 (model31.caps 5) (model31.ord 5) 0 1 100

source

theorem ConwaySoifer.Simplified.Certificates.Aown220000230000.excluded31_6 :

Certificates.ExcludedOn (model31.B 6 ++ [step31.q]) 9000000000000 (model31.caps 6) (model31.ord 6) 0 1 100

source

theorem ConwaySoifer.Simplified.Certificates.Aown220000230000.excluded31_7 :

Certificates.ExcludedOn (model31.B 7 ++ [step31.q]) 9000000000000 (model31.caps 7) (model31.ord 7) 0 1 100

source

theorem ConwaySoifer.Simplified.Certificates.Aown220000230000.excluded31_8 :

Certificates.ExcludedOn (model31.B 8 ++ [step31.q]) 9000000000000 (model31.caps 8) (model31.ord 8) 0 1 100

source

theorem ConwaySoifer.Simplified.Certificates.Aown220000230000.excluded31_9 :

Certificates.ExcludedOn (model31.B 9 ++ [step31.q]) 9000000000000 (model31.caps 9) (model31.ord 9) 0 1 100

source

theorem ConwaySoifer.Simplified.Certificates.Aown220000230000.checked31 :

Certificates.StepValid model31 9000000000000 step31 0 1 100

source

theorem ConwaySoifer.Simplified.Certificates.Aown220000230000.next31 :

model31.insert step31 = model32

Documentation

LeanPool.ConwaySoifer.Simplified.Certificates.Steps.Aown2200002300003

Aown 220000 230000 3 #