Aown 130000 135000

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

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

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Aown130000135000.point0 = ([540000000000], [-540000000000])

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

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Aown130000135000.point1 = ([1170000000000], [0])

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

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Aown130000135000.point2 = ([7573500000000], [841500000000])

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

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Aown130000135000.point3 = ([-7830000000000], [0])

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

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Aown130000135000.point4 = ([-2085000000000], [9000000000000])

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

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Aown130000135000.point5 = ([519000000000], [6375000000000])

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

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Aown130000135000.point6 = ([645000000000], [6375000000000])

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

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Aown130000135000.point7 = ([1500000000000], [5745000000000])

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

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Aown130000135000.point8 = ([2820000000000], [4680000000000])

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

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Aown130000135000.point9 = ([4680000000000], [2820000000000])

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

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Aown130000135000.point10 = ([6870000000000], [375000000000])

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

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Aown130000135000.point11 = ([-11106000000000], [8856000000000])

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

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Aown130000135000.point12 = ([-1875000000000], [8220000000000])

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

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Aown130000135000.point13 = ([-900000000000], [120000000000])

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

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Aown130000135000.point14 = ([-900000000000], [1290000000000])

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

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Aown130000135000.point15 = ([-8625000000000], [7245000000000])

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

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Aown130000135000.point16 = ([-674700000000, -5190000000000], [337350000000, 2595000000000])

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

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Aown130000135000.point17 = ([-337350000000, -2595000000000], [-337350000000, -2595000000000])

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

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Aown130000135000.point18 = ([337350000000, 2595000000000], [-674700000000, -5190000000000])

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

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Aown130000135000.point19 = ([674700000000, 5190000000000], [-337350000000, -2595000000000])

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

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Aown130000135000.point20 = ([337350000000, 2595000000000], [337350000000, 2595000000000])

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

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Aown130000135000.point21 = ([-337350000000, -2595000000000], [674700000000, 5190000000000])

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

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Aown130000135000.point22 = ([7830000000000, -9000000000000], [1170000000000, 9000000000000])

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

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Aown130000135000.point23 = ([9000000000000], [-1170000000000, -9000000000000])

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

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Aown130000135000.point24 = ([9000000000000], [4500000000000])

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

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Aown130000135000.point25 = ([-1170000000000, -9000000000000], [9000000000000])

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

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Aown130000135000.point26 = ([1170000000000, 9000000000000], [7830000000000, -9000000000000])

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

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Aown130000135000.point27 = ([0], [9000000000000])

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

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Aown130000135000.point28 = ([-9000000000000], [7830000000000, -9000000000000])

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

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Aown130000135000.point29 = ([-7830000000000, 9000000000000], [9000000000000])

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

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Aown130000135000.point30 = ([-9000000000000], [9000000000000])

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

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Aown130000135000.point31 = ([-9000000000000], [0])

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

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Aown130000135000.point32 = ([-7830000000000, 9000000000000], [-1170000000000, -9000000000000])

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

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Aown130000135000.point33 = ([-9000000000000], [1170000000000, 9000000000000])

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

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Aown130000135000.point34 = ([-1170000000000, -9000000000000], [-7830000000000, 9000000000000])

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

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Aown130000135000.point35 = ([0], [-9000000000000])

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

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Aown130000135000.point36 = ([1170000000000, 9000000000000], [-9000000000000])

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

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Aown130000135000.point37 = ([7830000000000, -9000000000000], [-9000000000000])

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

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

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

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

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Aown130000135000.point39 = ([9000000000000], [-7830000000000, 9000000000000])

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

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

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

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

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Aown130000135000.point41 = ([9000000000000], [9000000000000])

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

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Aown130000135000.point42 = ([7830000000000, -9000000000000], [9000000000000])

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

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Aown130000135000.point43 = ([-18000000000000], [9000000000000])

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

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Aown130000135000.point44 = ([-16830000000000, 9000000000000], [7830000000000, -9000000000000])

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

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Aown130000135000.point45 = ([-16830000000000, 9000000000000], [9000000000000])

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

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Aown130000135000.point46 = ([7830000000000, -9000000000000], [-16830000000000, 9000000000000])

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

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Aown130000135000.point47 = ([9000000000000], [-18000000000000])

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

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

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

def ConwaySoifer.Simplified.Certificates.Aown130000135000.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.Aown130000135000.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.Aown130000135000.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.Aown130000135000.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.Aown130000135000.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.Aown130000135000.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.Aown130000135000.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.Aown130000135000.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.Aown130000135000.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.Aown130000135000.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.Aown130000135000.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.Aown130000135000.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.Aown130000135000.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.Aown130000135000.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.Aown130000135000.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.Aown130000135000.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.Aown130000135000.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.Aown130000135000.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.Aown130000135000.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.Aown130000135000.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.Aown130000135000.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.Aown130000135000.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.Aown130000135000.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.Aown130000135000.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.Aown130000135000.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.Aown130000135000.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.Aown130000135000.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.Aown130000135000.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.Aown130000135000.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.Aown130000135000.step0 : Certificates.Step

The forced-point assignment at trace index 0.

Equations

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

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

The forced-point assignment at trace index 1.

Equations

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

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

The forced-point assignment at trace index 2.

Equations

• ConwaySoifer.Simplified.Certificates.Aown130000135000.step2 = { owner := 2, q := ConwaySoifer.Simplified.Certificates.Aown130000135000.point2 }

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

The forced-point assignment at trace index 3.

Equations

• ConwaySoifer.Simplified.Certificates.Aown130000135000.step3 = { owner := 4, q := ConwaySoifer.Simplified.Certificates.Aown130000135000.point3 }

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

The forced-point assignment at trace index 4.

Equations

• ConwaySoifer.Simplified.Certificates.Aown130000135000.step4 = { owner := 3, q := ConwaySoifer.Simplified.Certificates.Aown130000135000.point4 }

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

The forced-point assignment at trace index 5.

Equations

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

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

The forced-point assignment at trace index 6.

Equations

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

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

The forced-point assignment at trace index 7.

Equations

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

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

The forced-point assignment at trace index 8.

Equations

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

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

The forced-point assignment at trace index 9.

Equations

• ConwaySoifer.Simplified.Certificates.Aown130000135000.step9 = { owner := 0, q := ConwaySoifer.Simplified.Certificates.Aown130000135000.point9 }

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

The forced-point assignment at trace index 10.

Equations

• ConwaySoifer.Simplified.Certificates.Aown130000135000.step10 = { owner := 0, q := ConwaySoifer.Simplified.Certificates.Aown130000135000.point10 }

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

The forced-point assignment at trace index 11.

Equations

• ConwaySoifer.Simplified.Certificates.Aown130000135000.step11 = { owner := 8, q := ConwaySoifer.Simplified.Certificates.Aown130000135000.point11 }

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

The forced-point assignment at trace index 12.

Equations

• ConwaySoifer.Simplified.Certificates.Aown130000135000.step12 = { owner := 3, q := ConwaySoifer.Simplified.Certificates.Aown130000135000.point12 }

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

The forced-point assignment at trace index 13.

Equations

• ConwaySoifer.Simplified.Certificates.Aown130000135000.step13 = { owner := 4, q := ConwaySoifer.Simplified.Certificates.Aown130000135000.point13 }

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

The forced-point assignment at trace index 14.

Equations

• ConwaySoifer.Simplified.Certificates.Aown130000135000.step14 = { owner := 3, q := ConwaySoifer.Simplified.Certificates.Aown130000135000.point14 }

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

The forced-point assignment at trace index 15.

Equations

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

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

Proposed owner constraints after 16 forced-point assignments.

Equations

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

theorem ConwaySoifer.Simplified.Certificates.Aown130000135000.trace_steps : [step0, step1, step2, step3, step4, step5, step6, step7, step8, step9, step10, step11, step12, step13, step14, step15] = Data.Aown130000135000.steps

The shared step constants reproduce the original certificate trace exactly.