Aown 190000 200000

Shared exact checkpoint data; all transitions are verified by kernel proofs.

def ConwaySoifer.Simplified.Certificates.Aown190000200000.point0 : Certificates.IPoint

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Aown190000200000.point0 = ([-945000000000], [375000000000])

def ConwaySoifer.Simplified.Certificates.Aown190000200000.point1 : Certificates.IPoint

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Aown190000200000.point1 = ([-945000000000], [570000000000])

def ConwaySoifer.Simplified.Certificates.Aown190000200000.point2 : Certificates.IPoint

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Aown190000200000.point2 = ([-765000000000], [765000000000])

def ConwaySoifer.Simplified.Certificates.Aown190000200000.point3 : Certificates.IPoint

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Aown190000200000.point3 = ([-570000000000], [-375000000000])

def ConwaySoifer.Simplified.Certificates.Aown190000200000.point4 : Certificates.IPoint

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Aown190000200000.point4 = ([-375000000000], [-570000000000])

def ConwaySoifer.Simplified.Certificates.Aown190000200000.point5 : Certificates.IPoint

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Aown190000200000.point5 = ([0], [-765000000000])

def ConwaySoifer.Simplified.Certificates.Aown190000200000.point6 : Certificates.IPoint

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Aown190000200000.point6 = ([375000000000], [-945000000000])

def ConwaySoifer.Simplified.Certificates.Aown190000200000.point7 : Certificates.IPoint

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Aown190000200000.point7 = ([570000000000], [-945000000000])

def ConwaySoifer.Simplified.Certificates.Aown190000200000.point8 : Certificates.IPoint

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Aown190000200000.point8 = ([1710000000000], [0])

def ConwaySoifer.Simplified.Certificates.Aown190000200000.point9 : Certificates.IPoint

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Aown190000200000.point9 = ([5310000000000], [3690000000000])

def ConwaySoifer.Simplified.Certificates.Aown190000200000.point10 : Certificates.IPoint

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Aown190000200000.point10 = ([6930000000000], [1500000000000])

def ConwaySoifer.Simplified.Certificates.Aown190000200000.point11 : Certificates.IPoint

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Aown190000200000.point11 = ([9000000000000], [4755000000000])

def ConwaySoifer.Simplified.Certificates.Aown190000200000.point12 : Certificates.IPoint

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Aown190000200000.point12 = ([9000000000000], [6435000000000])

def ConwaySoifer.Simplified.Certificates.Aown190000200000.point13 : Certificates.IPoint

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Aown190000200000.point13 = ([-3060000000000], [9000000000000])

def ConwaySoifer.Simplified.Certificates.Aown190000200000.point14 : Certificates.IPoint

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Aown190000200000.point14 = ([420000000000], [5580000000000])

def ConwaySoifer.Simplified.Certificates.Aown190000200000.point15 : Certificates.IPoint

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Aown190000200000.point15 = ([2625000000000], [4275000000000])

def ConwaySoifer.Simplified.Certificates.Aown190000200000.point16 : Certificates.IPoint

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Aown190000200000.point16 = ([3840000000000], [3000000000000])

def ConwaySoifer.Simplified.Certificates.Aown190000200000.point17 : Certificates.IPoint

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Aown190000200000.point17 = ([5250000000000], [1470000000000])

def ConwaySoifer.Simplified.Certificates.Aown190000200000.point18 : Certificates.IPoint

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Aown190000200000.point18 = ([6060000000000], [375000000000])

def ConwaySoifer.Simplified.Certificates.Aown190000200000.point19 : Certificates.IPoint

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Aown190000200000.point19 = ([6840000000000], [1410000000000])

def ConwaySoifer.Simplified.Certificates.Aown190000200000.point20 : Certificates.IPoint

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Aown190000200000.point20 = ([6915000000000], [1710000000000])

def ConwaySoifer.Simplified.Certificates.Aown190000200000.point21 : Certificates.IPoint

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Aown190000200000.point21 = ([-12078000000000], [9000000000000])

def ConwaySoifer.Simplified.Certificates.Aown190000200000.point22 : Certificates.IPoint

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Aown190000200000.point22 = ([-2895000000000], [9000000000000])

def ConwaySoifer.Simplified.Certificates.Aown190000200000.point23 : Certificates.IPoint

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Aown190000200000.point23 = ([-1335000000000], [1710000000000])

def ConwaySoifer.Simplified.Certificates.Aown190000200000.point24 : Certificates.IPoint

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Aown190000200000.point24 = ([-1260000000000], [0])

def ConwaySoifer.Simplified.Certificates.Aown190000200000.point25 : Certificates.IPoint

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Aown190000200000.point25 = ([-8625000000000], [6465000000000])

def ConwaySoifer.Simplified.Certificates.Aown190000200000.point26 : Certificates.IPoint

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Aown190000200000.point26 = ([-912000000000, -4800000000000], [456000000000, 2400000000000])

def ConwaySoifer.Simplified.Certificates.Aown190000200000.point27 : Certificates.IPoint

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Aown190000200000.point27 = ([-456000000000, -2400000000000], [-456000000000, -2400000000000])

def ConwaySoifer.Simplified.Certificates.Aown190000200000.point28 : Certificates.IPoint

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Aown190000200000.point28 = ([456000000000, 2400000000000], [-912000000000, -4800000000000])

def ConwaySoifer.Simplified.Certificates.Aown190000200000.point29 : Certificates.IPoint

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Aown190000200000.point29 = ([912000000000, 4800000000000], [-456000000000, -2400000000000])

def ConwaySoifer.Simplified.Certificates.Aown190000200000.point30 : Certificates.IPoint

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Aown190000200000.point30 = ([456000000000, 2400000000000], [456000000000, 2400000000000])

def ConwaySoifer.Simplified.Certificates.Aown190000200000.point31 : Certificates.IPoint

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Aown190000200000.point31 = ([-456000000000, -2400000000000], [912000000000, 4800000000000])

def ConwaySoifer.Simplified.Certificates.Aown190000200000.point32 : Certificates.IPoint

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Aown190000200000.point32 = ([7290000000000, -9000000000000], [1710000000000, 9000000000000])

def ConwaySoifer.Simplified.Certificates.Aown190000200000.point33 : Certificates.IPoint

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Aown190000200000.point33 = ([9000000000000], [-1710000000000, -9000000000000])

def ConwaySoifer.Simplified.Certificates.Aown190000200000.point34 : Certificates.IPoint

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Aown190000200000.point34 = ([9000000000000], [4500000000000])

def ConwaySoifer.Simplified.Certificates.Aown190000200000.point35 : Certificates.IPoint

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Aown190000200000.point35 = ([-1710000000000, -9000000000000], [9000000000000])

def ConwaySoifer.Simplified.Certificates.Aown190000200000.point36 : Certificates.IPoint

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Aown190000200000.point36 = ([1710000000000, 9000000000000], [7290000000000, -9000000000000])

def ConwaySoifer.Simplified.Certificates.Aown190000200000.point37 : Certificates.IPoint

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Aown190000200000.point37 = ([0], [9000000000000])

def ConwaySoifer.Simplified.Certificates.Aown190000200000.point38 : Certificates.IPoint

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Aown190000200000.point38 = ([-9000000000000], [7290000000000, -9000000000000])

def ConwaySoifer.Simplified.Certificates.Aown190000200000.point39 : Certificates.IPoint

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Aown190000200000.point39 = ([-7290000000000, 9000000000000], [9000000000000])

def ConwaySoifer.Simplified.Certificates.Aown190000200000.point40 : Certificates.IPoint

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Aown190000200000.point40 = ([-9000000000000], [9000000000000])

def ConwaySoifer.Simplified.Certificates.Aown190000200000.point41 : Certificates.IPoint

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Aown190000200000.point41 = ([-9000000000000], [0])

def ConwaySoifer.Simplified.Certificates.Aown190000200000.point42 : Certificates.IPoint

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Aown190000200000.point42 = ([-7290000000000, 9000000000000], [-1710000000000, -9000000000000])

def ConwaySoifer.Simplified.Certificates.Aown190000200000.point43 : Certificates.IPoint

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Aown190000200000.point43 = ([-9000000000000], [1710000000000, 9000000000000])

def ConwaySoifer.Simplified.Certificates.Aown190000200000.point44 : Certificates.IPoint

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Aown190000200000.point44 = ([-1710000000000, -9000000000000], [-7290000000000, 9000000000000])

def ConwaySoifer.Simplified.Certificates.Aown190000200000.point45 : Certificates.IPoint

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Aown190000200000.point45 = ([0], [-9000000000000])

def ConwaySoifer.Simplified.Certificates.Aown190000200000.point46 : Certificates.IPoint

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Aown190000200000.point46 = ([1710000000000, 9000000000000], [-9000000000000])

def ConwaySoifer.Simplified.Certificates.Aown190000200000.point47 : Certificates.IPoint

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Aown190000200000.point47 = ([7290000000000, -9000000000000], [-9000000000000])

def ConwaySoifer.Simplified.Certificates.Aown190000200000.point48 : Certificates.IPoint

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Aown190000200000.point48 = ([9000000000000], [-9000000000000])

def ConwaySoifer.Simplified.Certificates.Aown190000200000.point49 : Certificates.IPoint

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Aown190000200000.point49 = ([9000000000000], [-7290000000000, 9000000000000])

def ConwaySoifer.Simplified.Certificates.Aown190000200000.point50 : Certificates.IPoint

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Aown190000200000.point50 = ([9000000000000], [7290000000000, -9000000000000])

def ConwaySoifer.Simplified.Certificates.Aown190000200000.point51 : Certificates.IPoint

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Aown190000200000.point51 = ([9000000000000], [9000000000000])

def ConwaySoifer.Simplified.Certificates.Aown190000200000.point52 : Certificates.IPoint

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Aown190000200000.point52 = ([7290000000000, -9000000000000], [9000000000000])

def ConwaySoifer.Simplified.Certificates.Aown190000200000.point53 : Certificates.IPoint

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Aown190000200000.point53 = ([-18000000000000], [9000000000000])

def ConwaySoifer.Simplified.Certificates.Aown190000200000.point54 : Certificates.IPoint

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Aown190000200000.point54 = ([-16290000000000, 9000000000000], [7290000000000, -9000000000000])

def ConwaySoifer.Simplified.Certificates.Aown190000200000.point55 : Certificates.IPoint

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Aown190000200000.point55 = ([-16290000000000, 9000000000000], [9000000000000])

def ConwaySoifer.Simplified.Certificates.Aown190000200000.point56 : Certificates.IPoint

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Aown190000200000.point56 = ([7290000000000, -9000000000000], [-16290000000000, 9000000000000])

def ConwaySoifer.Simplified.Certificates.Aown190000200000.point57 : Certificates.IPoint

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Aown190000200000.point57 = ([9000000000000], [-18000000000000])

def ConwaySoifer.Simplified.Certificates.Aown190000200000.point58 : Certificates.IPoint

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Aown190000200000.point58 = ([9000000000000], [-16290000000000, 9000000000000])

def ConwaySoifer.Simplified.Certificates.Aown190000200000.pointSet0 : List Certificates.IPoint

Shared mandatory-point list for one proposed owner state.

Equations

• One or more equations did not get rendered due to their size.

def ConwaySoifer.Simplified.Certificates.Aown190000200000.pointSet1 : List Certificates.IPoint

Shared mandatory-point list for one proposed owner state.

Equations

• One or more equations did not get rendered due to their size.

def ConwaySoifer.Simplified.Certificates.Aown190000200000.pointSet2 : List Certificates.IPoint

Shared mandatory-point list for one proposed owner state.

Equations

• One or more equations did not get rendered due to their size.

def ConwaySoifer.Simplified.Certificates.Aown190000200000.pointSet3 : List Certificates.IPoint

Shared mandatory-point list for one proposed owner state.

Equations

• One or more equations did not get rendered due to their size.

def ConwaySoifer.Simplified.Certificates.Aown190000200000.pointSet4 : List Certificates.IPoint

Shared mandatory-point list for one proposed owner state.

Equations

• One or more equations did not get rendered due to their size.

def ConwaySoifer.Simplified.Certificates.Aown190000200000.pointSet5 : List Certificates.IPoint

Shared mandatory-point list for one proposed owner state.

Equations

• One or more equations did not get rendered due to their size.

def ConwaySoifer.Simplified.Certificates.Aown190000200000.pointSet6 : List Certificates.IPoint

Shared mandatory-point list for one proposed owner state.

Equations

• One or more equations did not get rendered due to their size.

def ConwaySoifer.Simplified.Certificates.Aown190000200000.pointSet7 : List Certificates.IPoint

Shared mandatory-point list for one proposed owner state.

Equations

• One or more equations did not get rendered due to their size.

def ConwaySoifer.Simplified.Certificates.Aown190000200000.pointSet8 : List Certificates.IPoint

Shared mandatory-point list for one proposed owner state.

Equations

• One or more equations did not get rendered due to their size.

def ConwaySoifer.Simplified.Certificates.Aown190000200000.pointSet9 : List Certificates.IPoint

Shared mandatory-point list for one proposed owner state.

Equations

• One or more equations did not get rendered due to their size.

def ConwaySoifer.Simplified.Certificates.Aown190000200000.pointSet10 : List Certificates.IPoint

Shared mandatory-point list for one proposed owner state.

Equations

• One or more equations did not get rendered due to their size.

def ConwaySoifer.Simplified.Certificates.Aown190000200000.pointSet11 : List Certificates.IPoint

Shared mandatory-point list for one proposed owner state.

Equations

• One or more equations did not get rendered due to their size.

def ConwaySoifer.Simplified.Certificates.Aown190000200000.pointSet12 : List Certificates.IPoint

Shared mandatory-point list for one proposed owner state.

Equations

• One or more equations did not get rendered due to their size.

def ConwaySoifer.Simplified.Certificates.Aown190000200000.pointSet13 : List Certificates.IPoint

Shared mandatory-point list for one proposed owner state.

Equations

• One or more equations did not get rendered due to their size.

def ConwaySoifer.Simplified.Certificates.Aown190000200000.pointSet14 : List Certificates.IPoint

Shared mandatory-point list for one proposed owner state.

Equations

• One or more equations did not get rendered due to their size.

def ConwaySoifer.Simplified.Certificates.Aown190000200000.pointSet15 : List Certificates.IPoint

Shared mandatory-point list for one proposed owner state.

Equations

• One or more equations did not get rendered due to their size.

def ConwaySoifer.Simplified.Certificates.Aown190000200000.pointSet16 : List Certificates.IPoint

Shared mandatory-point list for one proposed owner state.

Equations

• One or more equations did not get rendered due to their size.

def ConwaySoifer.Simplified.Certificates.Aown190000200000.pointSet17 : List Certificates.IPoint

Shared mandatory-point list for one proposed owner state.

Equations

• One or more equations did not get rendered due to their size.

def ConwaySoifer.Simplified.Certificates.Aown190000200000.pointSet18 : List Certificates.IPoint

Shared mandatory-point list for one proposed owner state.

Equations

• One or more equations did not get rendered due to their size.

def ConwaySoifer.Simplified.Certificates.Aown190000200000.pointSet19 : List Certificates.IPoint

Shared mandatory-point list for one proposed owner state.

Equations

• One or more equations did not get rendered due to their size.

def ConwaySoifer.Simplified.Certificates.Aown190000200000.pointSet20 : List Certificates.IPoint

Shared mandatory-point list for one proposed owner state.

Equations

• One or more equations did not get rendered due to their size.

def ConwaySoifer.Simplified.Certificates.Aown190000200000.pointSet21 : List Certificates.IPoint

Shared mandatory-point list for one proposed owner state.

Equations

• One or more equations did not get rendered due to their size.

def ConwaySoifer.Simplified.Certificates.Aown190000200000.pointSet22 : List Certificates.IPoint

Shared mandatory-point list for one proposed owner state.

Equations

• One or more equations did not get rendered due to their size.

def ConwaySoifer.Simplified.Certificates.Aown190000200000.pointSet23 : List Certificates.IPoint

Shared mandatory-point list for one proposed owner state.

Equations

• One or more equations did not get rendered due to their size.

def ConwaySoifer.Simplified.Certificates.Aown190000200000.pointSet24 : List Certificates.IPoint

Shared mandatory-point list for one proposed owner state.

Equations

• One or more equations did not get rendered due to their size.

def ConwaySoifer.Simplified.Certificates.Aown190000200000.pointSet25 : List Certificates.IPoint

Shared mandatory-point list for one proposed owner state.

Equations

• One or more equations did not get rendered due to their size.

def ConwaySoifer.Simplified.Certificates.Aown190000200000.pointSet26 : List Certificates.IPoint

Shared mandatory-point list for one proposed owner state.

Equations

• One or more equations did not get rendered due to their size.

def ConwaySoifer.Simplified.Certificates.Aown190000200000.pointSet27 : List Certificates.IPoint

Shared mandatory-point list for one proposed owner state.

Equations

• One or more equations did not get rendered due to their size.

def ConwaySoifer.Simplified.Certificates.Aown190000200000.pointSet28 : List Certificates.IPoint

Shared mandatory-point list for one proposed owner state.

Equations

• One or more equations did not get rendered due to their size.

def ConwaySoifer.Simplified.Certificates.Aown190000200000.pointSet29 : List Certificates.IPoint

Shared mandatory-point list for one proposed owner state.

Equations

• One or more equations did not get rendered due to their size.

def ConwaySoifer.Simplified.Certificates.Aown190000200000.pointSet30 : List Certificates.IPoint

Shared mandatory-point list for one proposed owner state.

Equations

• One or more equations did not get rendered due to their size.

def ConwaySoifer.Simplified.Certificates.Aown190000200000.pointSet31 : List Certificates.IPoint

Shared mandatory-point list for one proposed owner state.

Equations

• One or more equations did not get rendered due to their size.

def ConwaySoifer.Simplified.Certificates.Aown190000200000.pointSet32 : List Certificates.IPoint

Shared mandatory-point list for one proposed owner state.

Equations

• One or more equations did not get rendered due to their size.

def ConwaySoifer.Simplified.Certificates.Aown190000200000.pointSet33 : List Certificates.IPoint

Shared mandatory-point list for one proposed owner state.

Equations

• One or more equations did not get rendered due to their size.

def ConwaySoifer.Simplified.Certificates.Aown190000200000.pointSet34 : List Certificates.IPoint

Shared mandatory-point list for one proposed owner state.

Equations

• One or more equations did not get rendered due to their size.

def ConwaySoifer.Simplified.Certificates.Aown190000200000.pointSet35 : List Certificates.IPoint

Shared mandatory-point list for one proposed owner state.

Equations

• One or more equations did not get rendered due to their size.

def ConwaySoifer.Simplified.Certificates.Aown190000200000.capsConstraints : Fin 10 → List Certificates.Cap

Contact constraints shared by every state in this certificate trace.

Equations

• One or more equations did not get rendered due to their size.

def ConwaySoifer.Simplified.Certificates.Aown190000200000.ownerFlags : Fin 10 → Option (Fin 6)

Side-owner restrictions shared by every state in this certificate trace.

Equations

• One or more equations did not get rendered due to their size.

def ConwaySoifer.Simplified.Certificates.Aown190000200000.model0 : Certificates.Model

Proposed owner constraints after 0 forced-point assignments.

Equations

• One or more equations did not get rendered due to their size.

def ConwaySoifer.Simplified.Certificates.Aown190000200000.step0 : Certificates.Step

The forced-point assignment at trace index 0.

Equations

• ConwaySoifer.Simplified.Certificates.Aown190000200000.step0 = { owner := 0, q := ConwaySoifer.Simplified.Certificates.Aown190000200000.point0 }

def ConwaySoifer.Simplified.Certificates.Aown190000200000.model1 : Certificates.Model

Proposed owner constraints after 1 forced-point assignments.

Equations

• One or more equations did not get rendered due to their size.

def ConwaySoifer.Simplified.Certificates.Aown190000200000.step1 : Certificates.Step

The forced-point assignment at trace index 1.

Equations

• ConwaySoifer.Simplified.Certificates.Aown190000200000.step1 = { owner := 0, q := ConwaySoifer.Simplified.Certificates.Aown190000200000.point1 }

def ConwaySoifer.Simplified.Certificates.Aown190000200000.model2 : Certificates.Model

Proposed owner constraints after 2 forced-point assignments.

Equations

• One or more equations did not get rendered due to their size.

def ConwaySoifer.Simplified.Certificates.Aown190000200000.step2 : Certificates.Step

The forced-point assignment at trace index 2.

Equations

• ConwaySoifer.Simplified.Certificates.Aown190000200000.step2 = { owner := 0, q := ConwaySoifer.Simplified.Certificates.Aown190000200000.point2 }

def ConwaySoifer.Simplified.Certificates.Aown190000200000.model3 : Certificates.Model

Proposed owner constraints after 3 forced-point assignments.

Equations

• One or more equations did not get rendered due to their size.

def ConwaySoifer.Simplified.Certificates.Aown190000200000.step3 : Certificates.Step

The forced-point assignment at trace index 3.

Equations

• ConwaySoifer.Simplified.Certificates.Aown190000200000.step3 = { owner := 0, q := ConwaySoifer.Simplified.Certificates.Aown190000200000.point3 }

def ConwaySoifer.Simplified.Certificates.Aown190000200000.model4 : Certificates.Model

Proposed owner constraints after 4 forced-point assignments.

Equations

• One or more equations did not get rendered due to their size.

def ConwaySoifer.Simplified.Certificates.Aown190000200000.step4 : Certificates.Step

The forced-point assignment at trace index 4.

Equations

• ConwaySoifer.Simplified.Certificates.Aown190000200000.step4 = { owner := 0, q := ConwaySoifer.Simplified.Certificates.Aown190000200000.point4 }

def ConwaySoifer.Simplified.Certificates.Aown190000200000.model5 : Certificates.Model

Proposed owner constraints after 5 forced-point assignments.

Equations

• One or more equations did not get rendered due to their size.

def ConwaySoifer.Simplified.Certificates.Aown190000200000.step5 : Certificates.Step

The forced-point assignment at trace index 5.

Equations

• ConwaySoifer.Simplified.Certificates.Aown190000200000.step5 = { owner := 0, q := ConwaySoifer.Simplified.Certificates.Aown190000200000.point5 }

def ConwaySoifer.Simplified.Certificates.Aown190000200000.model6 : Certificates.Model

Proposed owner constraints after 6 forced-point assignments.

Equations

• One or more equations did not get rendered due to their size.

def ConwaySoifer.Simplified.Certificates.Aown190000200000.step6 : Certificates.Step

The forced-point assignment at trace index 6.

Equations

• ConwaySoifer.Simplified.Certificates.Aown190000200000.step6 = { owner := 0, q := ConwaySoifer.Simplified.Certificates.Aown190000200000.point6 }

def ConwaySoifer.Simplified.Certificates.Aown190000200000.model7 : Certificates.Model

Proposed owner constraints after 7 forced-point assignments.

Equations

• One or more equations did not get rendered due to their size.

def ConwaySoifer.Simplified.Certificates.Aown190000200000.step7 : Certificates.Step

The forced-point assignment at trace index 7.

Equations

• ConwaySoifer.Simplified.Certificates.Aown190000200000.step7 = { owner := 0, q := ConwaySoifer.Simplified.Certificates.Aown190000200000.point7 }

def ConwaySoifer.Simplified.Certificates.Aown190000200000.model8 : Certificates.Model

Proposed owner constraints after 8 forced-point assignments.

Equations

• One or more equations did not get rendered due to their size.

def ConwaySoifer.Simplified.Certificates.Aown190000200000.step8 : Certificates.Step

The forced-point assignment at trace index 8.

Equations

• ConwaySoifer.Simplified.Certificates.Aown190000200000.step8 = { owner := 0, q := ConwaySoifer.Simplified.Certificates.Aown190000200000.point8 }

def ConwaySoifer.Simplified.Certificates.Aown190000200000.model9 : Certificates.Model

Proposed owner constraints after 9 forced-point assignments.

Equations

• One or more equations did not get rendered due to their size.

def ConwaySoifer.Simplified.Certificates.Aown190000200000.step9 : Certificates.Step

The forced-point assignment at trace index 9.

Equations

• ConwaySoifer.Simplified.Certificates.Aown190000200000.step9 = { owner := 2, q := ConwaySoifer.Simplified.Certificates.Aown190000200000.point9 }

def ConwaySoifer.Simplified.Certificates.Aown190000200000.model10 : Certificates.Model

Proposed owner constraints after 10 forced-point assignments.

Equations

• One or more equations did not get rendered due to their size.

def ConwaySoifer.Simplified.Certificates.Aown190000200000.step10 : Certificates.Step

The forced-point assignment at trace index 10.

Equations

• ConwaySoifer.Simplified.Certificates.Aown190000200000.step10 = { owner := 2, q := ConwaySoifer.Simplified.Certificates.Aown190000200000.point10 }

def ConwaySoifer.Simplified.Certificates.Aown190000200000.model11 : Certificates.Model

Proposed owner constraints after 11 forced-point assignments.

Equations

• One or more equations did not get rendered due to their size.

def ConwaySoifer.Simplified.Certificates.Aown190000200000.step11 : Certificates.Step

The forced-point assignment at trace index 11.

Equations

• ConwaySoifer.Simplified.Certificates.Aown190000200000.step11 = { owner := 1, q := ConwaySoifer.Simplified.Certificates.Aown190000200000.point11 }

def ConwaySoifer.Simplified.Certificates.Aown190000200000.model12 : Certificates.Model

Proposed owner constraints after 12 forced-point assignments.

Equations

• One or more equations did not get rendered due to their size.

def ConwaySoifer.Simplified.Certificates.Aown190000200000.step12 : Certificates.Step

The forced-point assignment at trace index 12.

Equations

• ConwaySoifer.Simplified.Certificates.Aown190000200000.step12 = { owner := 7, q := ConwaySoifer.Simplified.Certificates.Aown190000200000.point12 }

def ConwaySoifer.Simplified.Certificates.Aown190000200000.model13 : Certificates.Model

Proposed owner constraints after 13 forced-point assignments.

Equations

• One or more equations did not get rendered due to their size.

def ConwaySoifer.Simplified.Certificates.Aown190000200000.step13 : Certificates.Step

The forced-point assignment at trace index 13.

Equations

• ConwaySoifer.Simplified.Certificates.Aown190000200000.step13 = { owner := 3, q := ConwaySoifer.Simplified.Certificates.Aown190000200000.point13 }

def ConwaySoifer.Simplified.Certificates.Aown190000200000.model14 : Certificates.Model

Proposed owner constraints after 14 forced-point assignments.

Equations

• One or more equations did not get rendered due to their size.

def ConwaySoifer.Simplified.Certificates.Aown190000200000.step14 : Certificates.Step

The forced-point assignment at trace index 14.

Equations

• ConwaySoifer.Simplified.Certificates.Aown190000200000.step14 = { owner := 0, q := ConwaySoifer.Simplified.Certificates.Aown190000200000.point14 }

def ConwaySoifer.Simplified.Certificates.Aown190000200000.model15 : Certificates.Model

Proposed owner constraints after 15 forced-point assignments.

Equations

• One or more equations did not get rendered due to their size.

def ConwaySoifer.Simplified.Certificates.Aown190000200000.step15 : Certificates.Step

The forced-point assignment at trace index 15.

Equations

• ConwaySoifer.Simplified.Certificates.Aown190000200000.step15 = { owner := 0, q := ConwaySoifer.Simplified.Certificates.Aown190000200000.point15 }

def ConwaySoifer.Simplified.Certificates.Aown190000200000.model16 : Certificates.Model

Proposed owner constraints after 16 forced-point assignments.

Equations

• One or more equations did not get rendered due to their size.

def ConwaySoifer.Simplified.Certificates.Aown190000200000.step16 : Certificates.Step

The forced-point assignment at trace index 16.

Equations

• ConwaySoifer.Simplified.Certificates.Aown190000200000.step16 = { owner := 0, q := ConwaySoifer.Simplified.Certificates.Aown190000200000.point16 }

def ConwaySoifer.Simplified.Certificates.Aown190000200000.model17 : Certificates.Model

Proposed owner constraints after 17 forced-point assignments.

Equations

• One or more equations did not get rendered due to their size.

def ConwaySoifer.Simplified.Certificates.Aown190000200000.step17 : Certificates.Step

The forced-point assignment at trace index 17.

Equations

• ConwaySoifer.Simplified.Certificates.Aown190000200000.step17 = { owner := 0, q := ConwaySoifer.Simplified.Certificates.Aown190000200000.point17 }

def ConwaySoifer.Simplified.Certificates.Aown190000200000.model18 : Certificates.Model

Proposed owner constraints after 18 forced-point assignments.

Equations

• One or more equations did not get rendered due to their size.

def ConwaySoifer.Simplified.Certificates.Aown190000200000.step18 : Certificates.Step

The forced-point assignment at trace index 18.

Equations

• ConwaySoifer.Simplified.Certificates.Aown190000200000.step18 = { owner := 0, q := ConwaySoifer.Simplified.Certificates.Aown190000200000.point18 }

def ConwaySoifer.Simplified.Certificates.Aown190000200000.model19 : Certificates.Model

Proposed owner constraints after 19 forced-point assignments.

Equations

• One or more equations did not get rendered due to their size.

def ConwaySoifer.Simplified.Certificates.Aown190000200000.step19 : Certificates.Step

The forced-point assignment at trace index 19.

Equations

• ConwaySoifer.Simplified.Certificates.Aown190000200000.step19 = { owner := 2, q := ConwaySoifer.Simplified.Certificates.Aown190000200000.point19 }

def ConwaySoifer.Simplified.Certificates.Aown190000200000.model20 : Certificates.Model

Proposed owner constraints after 20 forced-point assignments.

Equations

• One or more equations did not get rendered due to their size.

def ConwaySoifer.Simplified.Certificates.Aown190000200000.step20 : Certificates.Step

The forced-point assignment at trace index 20.

Equations

• ConwaySoifer.Simplified.Certificates.Aown190000200000.step20 = { owner := 2, q := ConwaySoifer.Simplified.Certificates.Aown190000200000.point20 }

def ConwaySoifer.Simplified.Certificates.Aown190000200000.model21 : Certificates.Model

Proposed owner constraints after 21 forced-point assignments.

Equations

• One or more equations did not get rendered due to their size.

def ConwaySoifer.Simplified.Certificates.Aown190000200000.step21 : Certificates.Step

The forced-point assignment at trace index 21.

Equations

• ConwaySoifer.Simplified.Certificates.Aown190000200000.step21 = { owner := 8, q := ConwaySoifer.Simplified.Certificates.Aown190000200000.point21 }

def ConwaySoifer.Simplified.Certificates.Aown190000200000.model22 : Certificates.Model

Proposed owner constraints after 22 forced-point assignments.

Equations

• One or more equations did not get rendered due to their size.

def ConwaySoifer.Simplified.Certificates.Aown190000200000.step22 : Certificates.Step

The forced-point assignment at trace index 22.

Equations

• ConwaySoifer.Simplified.Certificates.Aown190000200000.step22 = { owner := 3, q := ConwaySoifer.Simplified.Certificates.Aown190000200000.point22 }

def ConwaySoifer.Simplified.Certificates.Aown190000200000.model23 : Certificates.Model

Proposed owner constraints after 23 forced-point assignments.

Equations

• One or more equations did not get rendered due to their size.

def ConwaySoifer.Simplified.Certificates.Aown190000200000.step23 : Certificates.Step

The forced-point assignment at trace index 23.

Equations

• ConwaySoifer.Simplified.Certificates.Aown190000200000.step23 = { owner := 3, q := ConwaySoifer.Simplified.Certificates.Aown190000200000.point23 }

def ConwaySoifer.Simplified.Certificates.Aown190000200000.model24 : Certificates.Model

Proposed owner constraints after 24 forced-point assignments.

Equations

• One or more equations did not get rendered due to their size.

def ConwaySoifer.Simplified.Certificates.Aown190000200000.step24 : Certificates.Step

The forced-point assignment at trace index 24.

Equations

• ConwaySoifer.Simplified.Certificates.Aown190000200000.step24 = { owner := 4, q := ConwaySoifer.Simplified.Certificates.Aown190000200000.point24 }

def ConwaySoifer.Simplified.Certificates.Aown190000200000.model25 : Certificates.Model

Proposed owner constraints after 25 forced-point assignments.

Equations

• One or more equations did not get rendered due to their size.

def ConwaySoifer.Simplified.Certificates.Aown190000200000.step25 : Certificates.Step

The forced-point assignment at trace index 25.

Equations

• ConwaySoifer.Simplified.Certificates.Aown190000200000.step25 = { owner := 0, q := ConwaySoifer.Simplified.Certificates.Aown190000200000.point25 }

def ConwaySoifer.Simplified.Certificates.Aown190000200000.model26 : Certificates.Model

Proposed owner constraints after 26 forced-point assignments.

Equations

• One or more equations did not get rendered due to their size.

theorem ConwaySoifer.Simplified.Certificates.Aown190000200000.trace_steps : [step0, step1, step2, step3, step4, step5, step6, step7, step8, step9, step10, step11, step12, step13, step14, step15, step16, step17, step18, step19, step20, step21, step22, step23, step24, step25] = Data.Aown190000200000.steps

The shared step constants reproduce the original certificate trace exactly.