Sint 200000 210000

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

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

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Sint200000210000.point0 = ([-3240000000000], [8865000000000])

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

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Sint200000210000.point1 = ([-3075000000000], [9000000000000])

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

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Sint200000210000.point2 = ([-975000000000], [375000000000])

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

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Sint200000210000.point3 = ([300000000000], [6000000000000])

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

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Sint200000210000.point4 = ([375000000000], [-975000000000])

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

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Sint200000210000.point5 = ([600000000000], [-975000000000])

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

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Sint200000210000.point6 = ([600000000000], [5775000000000])

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

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Sint200000210000.point7 = ([975000000000], [-600000000000])

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

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Sint200000210000.point8 = ([-12075000000000], [9000000000000])

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

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Sint200000210000.point9 = ([-8100000000000], [3600000000000])

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

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Sint200000210000.point10 = ([-5175000000000], [1200000000000])

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

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Sint200000210000.point11 = ([-4500000000000], [600000000000])

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

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Sint200000210000.point12 = ([-13800000000000], [4800000000000])

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

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Sint200000210000.point13 = ([-3450000000000], [-5550000000000])

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

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Sint200000210000.point14 = ([-576000000000], [-5184000000000])

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

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Sint200000210000.point15 = ([-9000000000000], [4500000000000])

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

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Sint200000210000.point16 = ([-4500000000000], [375000000000])

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

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Sint200000210000.point17 = ([5325000000000], [-14325000000000])

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

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Sint200000210000.point18 = ([5400000000000], [-6000000000000])

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

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Sint200000210000.point19 = ([5760000000000], [-8100000000000])

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

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Sint200000210000.point20 = ([-11775000000000], [2775000000000])

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

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Sint200000210000.point21 = ([-8250000000000], [6600000000000])

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

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Sint200000210000.point22 = ([-4500000000000], [-4500000000000])

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

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Sint200000210000.point23 = ([-4500000000000], [-3900000000000])

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

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Sint200000210000.point24 = ([-600000000000], [-4125000000000])

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

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Sint200000210000.point25 = ([9000000000000], [-15150000000000])

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

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Sint200000210000.point26 = ([9000000000000], [-2025000000000])

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

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Sint200000210000.point27 = ([-4875000000000], [-1800000000000])

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

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Sint200000210000.point28 = ([-1275000000000], [4875000000000])

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

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Sint200000210000.point29 = ([750000000000], [5550000000000])

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

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Sint200000210000.point30 = ([3900000000000], [-12900000000000])

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

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Sint200000210000.point31 = ([4275000000000], [-8400000000000])

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

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Sint200000210000.point32 = ([4275000000000], [-4875000000000])

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

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Sint200000210000.point33 = ([-4125000000000], [525000000000])

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

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Sint200000210000.point34 = ([-1200000000000], [300000000000])

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

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Sint200000210000.point35 = ([-750000000000], [-450000000000])

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

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Sint200000210000.point36 = ([-375000000000], [-4125000000000])

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

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Sint200000210000.point37 = ([0], [-4875000000000])

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

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Sint200000210000.point38 = ([7500000000000], [-2400000000000])

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

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Sint200000210000.point39 = ([9000000000000], [-3990000000000])

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

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Sint200000210000.point40 = ([-5175000000000], [-3825000000000])

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

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Sint200000210000.point41 = ([-4500000000000], [-1800000000000])

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

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Sint200000210000.point42 = ([-3375000000000], [0])

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

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Sint200000210000.point43 = ([-2400000000000], [6900000000000])

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

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Sint200000210000.point44 = ([1800000000000], [4950000000000])

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

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Sint200000210000.point45 = ([1875000000000], [4500000000000])

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

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Sint200000210000.point46 = ([3240000000000], [3750000000000])

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

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Sint200000210000.point47 = ([-11400000000000], [9000000000000])

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

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Sint200000210000.point48 = ([-10800000000000], [1800000000000])

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

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Sint200000210000.point49 = ([-9000000000000], [5550000000000])

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

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Sint200000210000.point50 = ([-5250000000000], [-3750000000000])

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

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Sint200000210000.point51 = ([-4425000000000], [2625000000000])

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

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Sint200000210000.point52 = ([-1800000000000], [8550000000000])

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

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Sint200000210000.point53 = ([1725000000000], [-1725000000000])

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

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Sint200000210000.point54 = ([2400000000000], [4725000000000])

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

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Sint200000210000.point55 = ([4050000000000], [0])

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

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Sint200000210000.point56 = ([-948000000000, -4740000000000], [474000000000, 2370000000000])

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

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Sint200000210000.point57 = ([-474000000000, -2370000000000], [-474000000000, -2370000000000])

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

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Sint200000210000.point58 = ([474000000000, 2370000000000], [-948000000000, -4740000000000])

def ConwaySoifer.Simplified.Certificates.Sint200000210000.point59 : Certificates.IPoint

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Sint200000210000.point59 = ([948000000000, 4740000000000], [-474000000000, -2370000000000])

def ConwaySoifer.Simplified.Certificates.Sint200000210000.point60 : Certificates.IPoint

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Sint200000210000.point60 = ([474000000000, 2370000000000], [474000000000, 2370000000000])

def ConwaySoifer.Simplified.Certificates.Sint200000210000.point61 : Certificates.IPoint

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Sint200000210000.point61 = ([-474000000000, -2370000000000], [948000000000, 4740000000000])

def ConwaySoifer.Simplified.Certificates.Sint200000210000.point62 : Certificates.IPoint

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Sint200000210000.point62 = ([7200000000000, -9000000000000], [1800000000000, 9000000000000])

def ConwaySoifer.Simplified.Certificates.Sint200000210000.point63 : Certificates.IPoint

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Sint200000210000.point63 = ([9000000000000], [-1800000000000, -9000000000000])

def ConwaySoifer.Simplified.Certificates.Sint200000210000.point64 : Certificates.IPoint

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Sint200000210000.point64 = ([9000000000000], [0])

def ConwaySoifer.Simplified.Certificates.Sint200000210000.point65 : Certificates.IPoint

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Sint200000210000.point65 = ([-1800000000000, -9000000000000], [9000000000000])

def ConwaySoifer.Simplified.Certificates.Sint200000210000.point66 : Certificates.IPoint

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Sint200000210000.point66 = ([0], [9000000000000])

def ConwaySoifer.Simplified.Certificates.Sint200000210000.point67 : Certificates.IPoint

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Sint200000210000.point67 = ([-9000000000000], [7200000000000, -9000000000000])

def ConwaySoifer.Simplified.Certificates.Sint200000210000.point68 : Certificates.IPoint

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Sint200000210000.point68 = ([-7200000000000, 9000000000000], [9000000000000])

def ConwaySoifer.Simplified.Certificates.Sint200000210000.point69 : Certificates.IPoint

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Sint200000210000.point69 = ([-9000000000000], [9000000000000])

def ConwaySoifer.Simplified.Certificates.Sint200000210000.point70 : Certificates.IPoint

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Sint200000210000.point70 = ([-9000000000000], [0])

def ConwaySoifer.Simplified.Certificates.Sint200000210000.point71 : Certificates.IPoint

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Sint200000210000.point71 = ([-7200000000000, 9000000000000], [-1800000000000, -9000000000000])

def ConwaySoifer.Simplified.Certificates.Sint200000210000.point72 : Certificates.IPoint

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Sint200000210000.point72 = ([-9000000000000], [1800000000000, 9000000000000])

def ConwaySoifer.Simplified.Certificates.Sint200000210000.point73 : Certificates.IPoint

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Sint200000210000.point73 = ([-1800000000000, -9000000000000], [-7200000000000, 9000000000000])

def ConwaySoifer.Simplified.Certificates.Sint200000210000.point74 : Certificates.IPoint

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Sint200000210000.point74 = ([0], [-9000000000000])

def ConwaySoifer.Simplified.Certificates.Sint200000210000.point75 : Certificates.IPoint

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Sint200000210000.point75 = ([1800000000000, 9000000000000], [-9000000000000])

def ConwaySoifer.Simplified.Certificates.Sint200000210000.point76 : Certificates.IPoint

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Sint200000210000.point76 = ([7200000000000, -9000000000000], [-9000000000000])

def ConwaySoifer.Simplified.Certificates.Sint200000210000.point77 : Certificates.IPoint

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Sint200000210000.point77 = ([9000000000000], [-9000000000000])

def ConwaySoifer.Simplified.Certificates.Sint200000210000.point78 : Certificates.IPoint

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Sint200000210000.point78 = ([9000000000000], [-7200000000000, 9000000000000])

def ConwaySoifer.Simplified.Certificates.Sint200000210000.point79 : Certificates.IPoint

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Sint200000210000.point79 = ([7200000000000, -9000000000000], [9000000000000])

def ConwaySoifer.Simplified.Certificates.Sint200000210000.point80 : Certificates.IPoint

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Sint200000210000.point80 = ([9000000000000], [7200000000000, -9000000000000])

def ConwaySoifer.Simplified.Certificates.Sint200000210000.point81 : Certificates.IPoint

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Sint200000210000.point81 = ([9000000000000], [9000000000000])

def ConwaySoifer.Simplified.Certificates.Sint200000210000.point82 : Certificates.IPoint

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Sint200000210000.point82 = ([-18000000000000], [9000000000000])

def ConwaySoifer.Simplified.Certificates.Sint200000210000.point83 : Certificates.IPoint

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Sint200000210000.point83 = ([-16200000000000, 9000000000000], [7200000000000, -9000000000000])

def ConwaySoifer.Simplified.Certificates.Sint200000210000.point84 : Certificates.IPoint

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Sint200000210000.point84 = ([-16200000000000, 9000000000000], [9000000000000])

def ConwaySoifer.Simplified.Certificates.Sint200000210000.point85 : Certificates.IPoint

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Sint200000210000.point85 = ([7200000000000, -9000000000000], [-16200000000000, 9000000000000])

def ConwaySoifer.Simplified.Certificates.Sint200000210000.point86 : Certificates.IPoint

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Sint200000210000.point86 = ([9000000000000], [-18000000000000])

def ConwaySoifer.Simplified.Certificates.Sint200000210000.point87 : Certificates.IPoint

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Sint200000210000.point87 = ([9000000000000], [-16200000000000, 9000000000000])

def ConwaySoifer.Simplified.Certificates.Sint200000210000.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.Sint200000210000.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.Sint200000210000.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.Sint200000210000.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.Sint200000210000.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.Sint200000210000.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.Sint200000210000.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.Sint200000210000.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.Sint200000210000.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.Sint200000210000.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.Sint200000210000.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.Sint200000210000.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.Sint200000210000.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.Sint200000210000.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.Sint200000210000.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.Sint200000210000.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.Sint200000210000.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.Sint200000210000.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.Sint200000210000.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.Sint200000210000.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.Sint200000210000.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.Sint200000210000.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.Sint200000210000.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.Sint200000210000.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.Sint200000210000.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.Sint200000210000.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.Sint200000210000.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.Sint200000210000.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.Sint200000210000.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.Sint200000210000.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.Sint200000210000.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.Sint200000210000.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.Sint200000210000.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.Sint200000210000.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.Sint200000210000.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.Sint200000210000.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.Sint200000210000.pointSet36 : 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.Sint200000210000.pointSet37 : 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.Sint200000210000.pointSet38 : 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.Sint200000210000.pointSet39 : 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.Sint200000210000.pointSet40 : 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.Sint200000210000.pointSet41 : 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.Sint200000210000.pointSet42 : 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.Sint200000210000.pointSet43 : 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.Sint200000210000.pointSet44 : 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.Sint200000210000.pointSet45 : 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.Sint200000210000.pointSet46 : 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.Sint200000210000.pointSet47 : 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.Sint200000210000.pointSet48 : 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.Sint200000210000.pointSet49 : 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.Sint200000210000.pointSet50 : 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.Sint200000210000.pointSet51 : 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.Sint200000210000.pointSet52 : 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.Sint200000210000.pointSet53 : 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.Sint200000210000.pointSet54 : 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.Sint200000210000.pointSet55 : 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.Sint200000210000.pointSet56 : 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.Sint200000210000.pointSet57 : 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.Sint200000210000.pointSet58 : 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.Sint200000210000.pointSet59 : 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.Sint200000210000.pointSet60 : 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.Sint200000210000.pointSet61 : 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.Sint200000210000.pointSet62 : 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.Sint200000210000.pointSet63 : 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.Sint200000210000.pointSet64 : 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.Sint200000210000.pointSet65 : 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.Sint200000210000.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.Sint200000210000.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.Sint200000210000.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.Sint200000210000.step0 : Certificates.Step

The forced-point assignment at trace index 0.

Equations

• ConwaySoifer.Simplified.Certificates.Sint200000210000.step0 = { owner := 3, q := ConwaySoifer.Simplified.Certificates.Sint200000210000.point0 }

def ConwaySoifer.Simplified.Certificates.Sint200000210000.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.Sint200000210000.step1 : Certificates.Step

The forced-point assignment at trace index 1.

Equations

• ConwaySoifer.Simplified.Certificates.Sint200000210000.step1 = { owner := 3, q := ConwaySoifer.Simplified.Certificates.Sint200000210000.point1 }

def ConwaySoifer.Simplified.Certificates.Sint200000210000.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.Sint200000210000.step2 : Certificates.Step

The forced-point assignment at trace index 2.

Equations

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

def ConwaySoifer.Simplified.Certificates.Sint200000210000.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.Sint200000210000.step3 : Certificates.Step

The forced-point assignment at trace index 3.

Equations

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

def ConwaySoifer.Simplified.Certificates.Sint200000210000.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.Sint200000210000.step4 : Certificates.Step

The forced-point assignment at trace index 4.

Equations

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

def ConwaySoifer.Simplified.Certificates.Sint200000210000.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.Sint200000210000.step5 : Certificates.Step

The forced-point assignment at trace index 5.

Equations

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

def ConwaySoifer.Simplified.Certificates.Sint200000210000.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.Sint200000210000.step6 : Certificates.Step

The forced-point assignment at trace index 6.

Equations

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

def ConwaySoifer.Simplified.Certificates.Sint200000210000.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.Sint200000210000.step7 : Certificates.Step

The forced-point assignment at trace index 7.

Equations

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

def ConwaySoifer.Simplified.Certificates.Sint200000210000.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.Sint200000210000.step8 : Certificates.Step

The forced-point assignment at trace index 8.

Equations

• ConwaySoifer.Simplified.Certificates.Sint200000210000.step8 = { owner := 8, q := ConwaySoifer.Simplified.Certificates.Sint200000210000.point8 }

def ConwaySoifer.Simplified.Certificates.Sint200000210000.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.Sint200000210000.step9 : Certificates.Step

The forced-point assignment at trace index 9.

Equations

• ConwaySoifer.Simplified.Certificates.Sint200000210000.step9 = { owner := 4, q := ConwaySoifer.Simplified.Certificates.Sint200000210000.point9 }

def ConwaySoifer.Simplified.Certificates.Sint200000210000.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.Sint200000210000.step10 : Certificates.Step

The forced-point assignment at trace index 10.

Equations

• ConwaySoifer.Simplified.Certificates.Sint200000210000.step10 = { owner := 4, q := ConwaySoifer.Simplified.Certificates.Sint200000210000.point10 }

def ConwaySoifer.Simplified.Certificates.Sint200000210000.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.Sint200000210000.step11 : Certificates.Step

The forced-point assignment at trace index 11.

Equations

• ConwaySoifer.Simplified.Certificates.Sint200000210000.step11 = { owner := 4, q := ConwaySoifer.Simplified.Certificates.Sint200000210000.point11 }

def ConwaySoifer.Simplified.Certificates.Sint200000210000.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.Sint200000210000.step12 : Certificates.Step

The forced-point assignment at trace index 12.

Equations

• ConwaySoifer.Simplified.Certificates.Sint200000210000.step12 = { owner := 8, q := ConwaySoifer.Simplified.Certificates.Sint200000210000.point12 }

def ConwaySoifer.Simplified.Certificates.Sint200000210000.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.Sint200000210000.step13 : Certificates.Step

The forced-point assignment at trace index 13.

Equations

• ConwaySoifer.Simplified.Certificates.Sint200000210000.step13 = { owner := 5, q := ConwaySoifer.Simplified.Certificates.Sint200000210000.point13 }

def ConwaySoifer.Simplified.Certificates.Sint200000210000.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.Sint200000210000.step14 : Certificates.Step

The forced-point assignment at trace index 14.

Equations

• ConwaySoifer.Simplified.Certificates.Sint200000210000.step14 = { owner := 5, q := ConwaySoifer.Simplified.Certificates.Sint200000210000.point14 }

def ConwaySoifer.Simplified.Certificates.Sint200000210000.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.Sint200000210000.step15 : Certificates.Step

The forced-point assignment at trace index 15.

Equations

• ConwaySoifer.Simplified.Certificates.Sint200000210000.step15 = { owner := 4, q := ConwaySoifer.Simplified.Certificates.Sint200000210000.point15 }

def ConwaySoifer.Simplified.Certificates.Sint200000210000.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.Sint200000210000.step16 : Certificates.Step

The forced-point assignment at trace index 16.

Equations

• ConwaySoifer.Simplified.Certificates.Sint200000210000.step16 = { owner := 4, q := ConwaySoifer.Simplified.Certificates.Sint200000210000.point16 }

def ConwaySoifer.Simplified.Certificates.Sint200000210000.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.Sint200000210000.step17 : Certificates.Step

The forced-point assignment at trace index 17.

Equations

• ConwaySoifer.Simplified.Certificates.Sint200000210000.step17 = { owner := 9, q := ConwaySoifer.Simplified.Certificates.Sint200000210000.point17 }

def ConwaySoifer.Simplified.Certificates.Sint200000210000.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.Sint200000210000.step18 : Certificates.Step

The forced-point assignment at trace index 18.

Equations

• ConwaySoifer.Simplified.Certificates.Sint200000210000.step18 = { owner := 6, q := ConwaySoifer.Simplified.Certificates.Sint200000210000.point18 }

def ConwaySoifer.Simplified.Certificates.Sint200000210000.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.Sint200000210000.step19 : Certificates.Step

The forced-point assignment at trace index 19.

Equations

• ConwaySoifer.Simplified.Certificates.Sint200000210000.step19 = { owner := 6, q := ConwaySoifer.Simplified.Certificates.Sint200000210000.point19 }

def ConwaySoifer.Simplified.Certificates.Sint200000210000.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.Sint200000210000.step20 : Certificates.Step

The forced-point assignment at trace index 20.

Equations

• ConwaySoifer.Simplified.Certificates.Sint200000210000.step20 = { owner := 8, q := ConwaySoifer.Simplified.Certificates.Sint200000210000.point20 }

def ConwaySoifer.Simplified.Certificates.Sint200000210000.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.Sint200000210000.step21 : Certificates.Step

The forced-point assignment at trace index 21.

Equations

• ConwaySoifer.Simplified.Certificates.Sint200000210000.step21 = { owner := 3, q := ConwaySoifer.Simplified.Certificates.Sint200000210000.point21 }

def ConwaySoifer.Simplified.Certificates.Sint200000210000.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.Sint200000210000.step22 : Certificates.Step

The forced-point assignment at trace index 22.

Equations

• ConwaySoifer.Simplified.Certificates.Sint200000210000.step22 = { owner := 5, q := ConwaySoifer.Simplified.Certificates.Sint200000210000.point22 }

def ConwaySoifer.Simplified.Certificates.Sint200000210000.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.Sint200000210000.step23 : Certificates.Step

The forced-point assignment at trace index 23.

Equations

• ConwaySoifer.Simplified.Certificates.Sint200000210000.step23 = { owner := 5, q := ConwaySoifer.Simplified.Certificates.Sint200000210000.point23 }

def ConwaySoifer.Simplified.Certificates.Sint200000210000.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.Sint200000210000.step24 : Certificates.Step

The forced-point assignment at trace index 24.

Equations

• ConwaySoifer.Simplified.Certificates.Sint200000210000.step24 = { owner := 5, q := ConwaySoifer.Simplified.Certificates.Sint200000210000.point24 }

def ConwaySoifer.Simplified.Certificates.Sint200000210000.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.Sint200000210000.step25 : Certificates.Step

The forced-point assignment at trace index 25.

Equations

• ConwaySoifer.Simplified.Certificates.Sint200000210000.step25 = { owner := 9, q := ConwaySoifer.Simplified.Certificates.Sint200000210000.point25 }

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

Proposed owner constraints after 26 forced-point assignments.

Equations

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

def ConwaySoifer.Simplified.Certificates.Sint200000210000.step26 : Certificates.Step

The forced-point assignment at trace index 26.

Equations

• ConwaySoifer.Simplified.Certificates.Sint200000210000.step26 = { owner := 1, q := ConwaySoifer.Simplified.Certificates.Sint200000210000.point26 }

def ConwaySoifer.Simplified.Certificates.Sint200000210000.model27 : Certificates.Model

Proposed owner constraints after 27 forced-point assignments.

Equations

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

def ConwaySoifer.Simplified.Certificates.Sint200000210000.step27 : Certificates.Step

The forced-point assignment at trace index 27.

Equations

• ConwaySoifer.Simplified.Certificates.Sint200000210000.step27 = { owner := 4, q := ConwaySoifer.Simplified.Certificates.Sint200000210000.point27 }

def ConwaySoifer.Simplified.Certificates.Sint200000210000.model28 : Certificates.Model

Proposed owner constraints after 28 forced-point assignments.

Equations

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

def ConwaySoifer.Simplified.Certificates.Sint200000210000.step28 : Certificates.Step

The forced-point assignment at trace index 28.

Equations

• ConwaySoifer.Simplified.Certificates.Sint200000210000.step28 = { owner := 0, q := ConwaySoifer.Simplified.Certificates.Sint200000210000.point28 }

def ConwaySoifer.Simplified.Certificates.Sint200000210000.model29 : Certificates.Model

Proposed owner constraints after 29 forced-point assignments.

Equations

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

def ConwaySoifer.Simplified.Certificates.Sint200000210000.step29 : Certificates.Step

The forced-point assignment at trace index 29.

Equations

• ConwaySoifer.Simplified.Certificates.Sint200000210000.step29 = { owner := 0, q := ConwaySoifer.Simplified.Certificates.Sint200000210000.point29 }

def ConwaySoifer.Simplified.Certificates.Sint200000210000.model30 : Certificates.Model

Proposed owner constraints after 30 forced-point assignments.

Equations

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

def ConwaySoifer.Simplified.Certificates.Sint200000210000.step30 : Certificates.Step

The forced-point assignment at trace index 30.

Equations

• ConwaySoifer.Simplified.Certificates.Sint200000210000.step30 = { owner := 9, q := ConwaySoifer.Simplified.Certificates.Sint200000210000.point30 }

def ConwaySoifer.Simplified.Certificates.Sint200000210000.model31 : Certificates.Model

Proposed owner constraints after 31 forced-point assignments.

Equations

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

def ConwaySoifer.Simplified.Certificates.Sint200000210000.step31 : Certificates.Step

The forced-point assignment at trace index 31.

Equations

• ConwaySoifer.Simplified.Certificates.Sint200000210000.step31 = { owner := 6, q := ConwaySoifer.Simplified.Certificates.Sint200000210000.point31 }

def ConwaySoifer.Simplified.Certificates.Sint200000210000.model32 : Certificates.Model

Proposed owner constraints after 32 forced-point assignments.

Equations

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

def ConwaySoifer.Simplified.Certificates.Sint200000210000.step32 : Certificates.Step

The forced-point assignment at trace index 32.

Equations

• ConwaySoifer.Simplified.Certificates.Sint200000210000.step32 = { owner := 6, q := ConwaySoifer.Simplified.Certificates.Sint200000210000.point32 }

def ConwaySoifer.Simplified.Certificates.Sint200000210000.model33 : Certificates.Model

Proposed owner constraints after 33 forced-point assignments.

Equations

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

def ConwaySoifer.Simplified.Certificates.Sint200000210000.step33 : Certificates.Step

The forced-point assignment at trace index 33.

Equations

• ConwaySoifer.Simplified.Certificates.Sint200000210000.step33 = { owner := 4, q := ConwaySoifer.Simplified.Certificates.Sint200000210000.point33 }

def ConwaySoifer.Simplified.Certificates.Sint200000210000.model34 : Certificates.Model

Proposed owner constraints after 34 forced-point assignments.

Equations

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

def ConwaySoifer.Simplified.Certificates.Sint200000210000.step34 : Certificates.Step

The forced-point assignment at trace index 34.

Equations

• ConwaySoifer.Simplified.Certificates.Sint200000210000.step34 = { owner := 0, q := ConwaySoifer.Simplified.Certificates.Sint200000210000.point34 }

def ConwaySoifer.Simplified.Certificates.Sint200000210000.model35 : Certificates.Model

Proposed owner constraints after 35 forced-point assignments.

Equations

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

def ConwaySoifer.Simplified.Certificates.Sint200000210000.step35 : Certificates.Step

The forced-point assignment at trace index 35.

Equations

• ConwaySoifer.Simplified.Certificates.Sint200000210000.step35 = { owner := 0, q := ConwaySoifer.Simplified.Certificates.Sint200000210000.point35 }

def ConwaySoifer.Simplified.Certificates.Sint200000210000.model36 : Certificates.Model

Proposed owner constraints after 36 forced-point assignments.

Equations

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

def ConwaySoifer.Simplified.Certificates.Sint200000210000.step36 : Certificates.Step

The forced-point assignment at trace index 36.

Equations

• ConwaySoifer.Simplified.Certificates.Sint200000210000.step36 = { owner := 5, q := ConwaySoifer.Simplified.Certificates.Sint200000210000.point36 }

def ConwaySoifer.Simplified.Certificates.Sint200000210000.model37 : Certificates.Model

Proposed owner constraints after 37 forced-point assignments.

Equations

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

def ConwaySoifer.Simplified.Certificates.Sint200000210000.step37 : Certificates.Step

The forced-point assignment at trace index 37.

Equations

• ConwaySoifer.Simplified.Certificates.Sint200000210000.step37 = { owner := 5, q := ConwaySoifer.Simplified.Certificates.Sint200000210000.point37 }

def ConwaySoifer.Simplified.Certificates.Sint200000210000.model38 : Certificates.Model

Proposed owner constraints after 38 forced-point assignments.

Equations

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

def ConwaySoifer.Simplified.Certificates.Sint200000210000.step38 : Certificates.Step

The forced-point assignment at trace index 38.

Equations

• ConwaySoifer.Simplified.Certificates.Sint200000210000.step38 = { owner := 1, q := ConwaySoifer.Simplified.Certificates.Sint200000210000.point38 }

def ConwaySoifer.Simplified.Certificates.Sint200000210000.model39 : Certificates.Model

Proposed owner constraints after 39 forced-point assignments.

Equations

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

def ConwaySoifer.Simplified.Certificates.Sint200000210000.step39 : Certificates.Step

The forced-point assignment at trace index 39.

Equations

• ConwaySoifer.Simplified.Certificates.Sint200000210000.step39 = { owner := 1, q := ConwaySoifer.Simplified.Certificates.Sint200000210000.point39 }

def ConwaySoifer.Simplified.Certificates.Sint200000210000.model40 : Certificates.Model

Proposed owner constraints after 40 forced-point assignments.

Equations

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

def ConwaySoifer.Simplified.Certificates.Sint200000210000.step40 : Certificates.Step

The forced-point assignment at trace index 40.

Equations

• ConwaySoifer.Simplified.Certificates.Sint200000210000.step40 = { owner := 5, q := ConwaySoifer.Simplified.Certificates.Sint200000210000.point40 }

def ConwaySoifer.Simplified.Certificates.Sint200000210000.model41 : Certificates.Model

Proposed owner constraints after 41 forced-point assignments.

Equations

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

def ConwaySoifer.Simplified.Certificates.Sint200000210000.step41 : Certificates.Step

The forced-point assignment at trace index 41.

Equations

• ConwaySoifer.Simplified.Certificates.Sint200000210000.step41 = { owner := 4, q := ConwaySoifer.Simplified.Certificates.Sint200000210000.point41 }

def ConwaySoifer.Simplified.Certificates.Sint200000210000.model42 : Certificates.Model

Proposed owner constraints after 42 forced-point assignments.

Equations

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

def ConwaySoifer.Simplified.Certificates.Sint200000210000.step42 : Certificates.Step

The forced-point assignment at trace index 42.

Equations

• ConwaySoifer.Simplified.Certificates.Sint200000210000.step42 = { owner := 4, q := ConwaySoifer.Simplified.Certificates.Sint200000210000.point42 }

def ConwaySoifer.Simplified.Certificates.Sint200000210000.model43 : Certificates.Model

Proposed owner constraints after 43 forced-point assignments.

Equations

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

def ConwaySoifer.Simplified.Certificates.Sint200000210000.step43 : Certificates.Step

The forced-point assignment at trace index 43.

Equations

• ConwaySoifer.Simplified.Certificates.Sint200000210000.step43 = { owner := 3, q := ConwaySoifer.Simplified.Certificates.Sint200000210000.point43 }

def ConwaySoifer.Simplified.Certificates.Sint200000210000.model44 : Certificates.Model

Proposed owner constraints after 44 forced-point assignments.

Equations

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

def ConwaySoifer.Simplified.Certificates.Sint200000210000.step44 : Certificates.Step

The forced-point assignment at trace index 44.

Equations

• ConwaySoifer.Simplified.Certificates.Sint200000210000.step44 = { owner := 0, q := ConwaySoifer.Simplified.Certificates.Sint200000210000.point44 }

def ConwaySoifer.Simplified.Certificates.Sint200000210000.model45 : Certificates.Model

Proposed owner constraints after 45 forced-point assignments.

Equations

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

def ConwaySoifer.Simplified.Certificates.Sint200000210000.step45 : Certificates.Step

The forced-point assignment at trace index 45.

Equations

• ConwaySoifer.Simplified.Certificates.Sint200000210000.step45 = { owner := 0, q := ConwaySoifer.Simplified.Certificates.Sint200000210000.point45 }

def ConwaySoifer.Simplified.Certificates.Sint200000210000.model46 : Certificates.Model

Proposed owner constraints after 46 forced-point assignments.

Equations

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

def ConwaySoifer.Simplified.Certificates.Sint200000210000.step46 : Certificates.Step

The forced-point assignment at trace index 46.

Equations

• ConwaySoifer.Simplified.Certificates.Sint200000210000.step46 = { owner := 1, q := ConwaySoifer.Simplified.Certificates.Sint200000210000.point46 }

def ConwaySoifer.Simplified.Certificates.Sint200000210000.model47 : Certificates.Model

Proposed owner constraints after 47 forced-point assignments.

Equations

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

def ConwaySoifer.Simplified.Certificates.Sint200000210000.step47 : Certificates.Step

The forced-point assignment at trace index 47.

Equations

• ConwaySoifer.Simplified.Certificates.Sint200000210000.step47 = { owner := 8, q := ConwaySoifer.Simplified.Certificates.Sint200000210000.point47 }

def ConwaySoifer.Simplified.Certificates.Sint200000210000.model48 : Certificates.Model

Proposed owner constraints after 48 forced-point assignments.

Equations

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

def ConwaySoifer.Simplified.Certificates.Sint200000210000.step48 : Certificates.Step

The forced-point assignment at trace index 48.

Equations

• ConwaySoifer.Simplified.Certificates.Sint200000210000.step48 = { owner := 8, q := ConwaySoifer.Simplified.Certificates.Sint200000210000.point48 }

def ConwaySoifer.Simplified.Certificates.Sint200000210000.model49 : Certificates.Model

Proposed owner constraints after 49 forced-point assignments.

Equations

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

def ConwaySoifer.Simplified.Certificates.Sint200000210000.step49 : Certificates.Step

The forced-point assignment at trace index 49.

Equations

• ConwaySoifer.Simplified.Certificates.Sint200000210000.step49 = { owner := 4, q := ConwaySoifer.Simplified.Certificates.Sint200000210000.point49 }

def ConwaySoifer.Simplified.Certificates.Sint200000210000.model50 : Certificates.Model

Proposed owner constraints after 50 forced-point assignments.

Equations

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

def ConwaySoifer.Simplified.Certificates.Sint200000210000.step50 : Certificates.Step

The forced-point assignment at trace index 50.

Equations

• ConwaySoifer.Simplified.Certificates.Sint200000210000.step50 = { owner := 5, q := ConwaySoifer.Simplified.Certificates.Sint200000210000.point50 }

def ConwaySoifer.Simplified.Certificates.Sint200000210000.model51 : Certificates.Model

Proposed owner constraints after 51 forced-point assignments.

Equations

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

def ConwaySoifer.Simplified.Certificates.Sint200000210000.step51 : Certificates.Step

The forced-point assignment at trace index 51.

Equations

• ConwaySoifer.Simplified.Certificates.Sint200000210000.step51 = { owner := 3, q := ConwaySoifer.Simplified.Certificates.Sint200000210000.point51 }

def ConwaySoifer.Simplified.Certificates.Sint200000210000.model52 : Certificates.Model

Proposed owner constraints after 52 forced-point assignments.

Equations

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

def ConwaySoifer.Simplified.Certificates.Sint200000210000.step52 : Certificates.Step

The forced-point assignment at trace index 52.

Equations

• ConwaySoifer.Simplified.Certificates.Sint200000210000.step52 = { owner := 2, q := ConwaySoifer.Simplified.Certificates.Sint200000210000.point52 }

def ConwaySoifer.Simplified.Certificates.Sint200000210000.model53 : Certificates.Model

Proposed owner constraints after 53 forced-point assignments.

Equations

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

def ConwaySoifer.Simplified.Certificates.Sint200000210000.step53 : Certificates.Step

The forced-point assignment at trace index 53.

Equations

• ConwaySoifer.Simplified.Certificates.Sint200000210000.step53 = { owner := 6, q := ConwaySoifer.Simplified.Certificates.Sint200000210000.point53 }

def ConwaySoifer.Simplified.Certificates.Sint200000210000.model54 : Certificates.Model

Proposed owner constraints after 54 forced-point assignments.

Equations

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

def ConwaySoifer.Simplified.Certificates.Sint200000210000.step54 : Certificates.Step

The forced-point assignment at trace index 54.

Equations

• ConwaySoifer.Simplified.Certificates.Sint200000210000.step54 = { owner := 0, q := ConwaySoifer.Simplified.Certificates.Sint200000210000.point54 }

def ConwaySoifer.Simplified.Certificates.Sint200000210000.model55 : Certificates.Model

Proposed owner constraints after 55 forced-point assignments.

Equations

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

def ConwaySoifer.Simplified.Certificates.Sint200000210000.step55 : Certificates.Step

The forced-point assignment at trace index 55.

Equations

• ConwaySoifer.Simplified.Certificates.Sint200000210000.step55 = { owner := 0, q := ConwaySoifer.Simplified.Certificates.Sint200000210000.point55 }

def ConwaySoifer.Simplified.Certificates.Sint200000210000.model56 : Certificates.Model

Proposed owner constraints after 56 forced-point assignments.

Equations

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

theorem ConwaySoifer.Simplified.Certificates.Sint200000210000.trace_steps : (have y := have y := have y := [step49, step50, step51, step52, step53, step54, step55]; step42 :: step43 :: step44 :: step45 :: step46 :: step47 :: step48 :: y; have y := step35 :: step36 :: step37 :: step38 :: step39 :: step40 :: step41 :: y; step28 :: step29 :: step30 :: step31 :: step32 :: step33 :: step34 :: y; have y := have y := step21 :: step22 :: step23 :: step24 :: step25 :: step26 :: step27 :: y; step14 :: step15 :: step16 :: step17 :: step18 :: step19 :: step20 :: y; have y := step7 :: step8 :: step9 :: step10 :: step11 :: step12 :: step13 :: y; step0 :: step1 :: step2 :: step3 :: step4 :: step5 :: step6 :: y) = Data.Sint200000210000.steps

The shared step constants reproduce the original certificate trace exactly.