Gerver sofa: related certificate and semantic modules

• GerverSofa.KernelOnly.PartE.Certificates.Batch041.

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCellsd112ae8b34.phiBelowCell3323 : AngleCell

Subcell 3323 of the phi-below root; digits 0–3 mean LL, LH, HL, HH.

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCellsd112ae8b34.phiBelowCell33233223 : AngleCell

Subcell 33233223 of the phi-below root; digits 0–3 mean LL, LH, HL, HH.

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells005204f093.phiBelowCell3323 : AngleCell

Subcell 3323 of the phi-below root; digits 0–3 mean LL, LH, HL, HH.

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells005204f093.phiBelowCell33233230 : AngleCell

Subcell 33233230 of the phi-below root; digits 0–3 mean LL, LH, HL, HH.

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells1db372ce58.phiBelowCell3323 : AngleCell

Subcell 3323 of the phi-below root; digits 0–3 mean LL, LH, HL, HH.

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells1db372ce58.phiBelowCell33233231 : AngleCell

Subcell 33233231 of the phi-below root; digits 0–3 mean LL, LH, HL, HH.

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells747d0e3511.phiBelowCell3323 : AngleCell

Subcell 3323 of the phi-below root; digits 0–3 mean LL, LH, HL, HH.

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells747d0e3511.phiBelowCell33233232 : AngleCell

Subcell 33233232 of the phi-below root; digits 0–3 mean LL, LH, HL, HH.

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2c20a17ff6.phiBelowCell3323 : AngleCell

Subcell 3323 of the phi-below root; digits 0–3 mean LL, LH, HL, HH.

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells2c20a17ff6.phiBelowCell33233232 : AngleCell

Subcell 33233232 of the phi-below root; digits 0–3 mean LL, LH, HL, HH.

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells6d9a408f54.phiBelowCell3323 : AngleCell

Subcell 3323 of the phi-below root; digits 0–3 mean LL, LH, HL, HH.

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells6d9a408f54.phiBelowCell33233232 : AngleCell

Subcell 33233232 of the phi-below root; digits 0–3 mean LL, LH, HL, HH.

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells26c5fe31ab.phiBelowCell3323 : AngleCell

Subcell 3323 of the phi-below root; digits 0–3 mean LL, LH, HL, HH.

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells26c5fe31ab.phiBelowCell33233232 : AngleCell

Subcell 33233232 of the phi-below root; digits 0–3 mean LL, LH, HL, HH.

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells8faba9c99a.phiBelowCell3323 : AngleCell

Subcell 3323 of the phi-below root; digits 0–3 mean LL, LH, HL, HH.

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells8faba9c99a.phiBelowCell33233233 : AngleCell

Subcell 33233233 of the phi-below root; digits 0–3 mean LL, LH, HL, HH.

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCellsd0acf0005e.phiBelowCell3323 : AngleCell

Subcell 3323 of the phi-below root; digits 0–3 mean LL, LH, HL, HH.

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCellsd9f8181f0f.thetaAboveCell0000 : AngleCell

Subcell 0000 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCellsd9f8181f0f.thetaAboveCell00002200 : AngleCell

Subcell 00002200 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCellsd9f8181f0f.thetaAboveCell000022002011 : AngleCell

Subcell 000022002011 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCellsc3ac49754f.thetaAboveCell0000 : AngleCell

Subcell 0000 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCellsc3ac49754f.thetaAboveCell00002200 : AngleCell

Subcell 00002200 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCellsc3ac49754f.thetaAboveCell000022002011 : AngleCell

Subcell 000022002011 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCellsa708f81b81.thetaAboveCell0000 : AngleCell

Subcell 0000 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCellsa708f81b81.thetaAboveCell00002200 : AngleCell

Subcell 00002200 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCellsa708f81b81.thetaAboveCell000022002011 : AngleCell

Subcell 000022002011 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCellsa708f81b81.thetaAboveCell0000220020113120 : AngleCell

Subcell 0000220020113120 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCellsd0cc56b48c.thetaAboveCell0000 : AngleCell

Subcell 0000 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCellsd0cc56b48c.thetaAboveCell00002200 : AngleCell

Subcell 00002200 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCellsd0cc56b48c.thetaAboveCell000022002011 : AngleCell

Subcell 000022002011 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCellsd0cc56b48c.thetaAboveCell0000220020113121 : AngleCell

Subcell 0000220020113121 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCellsecda937af3.thetaAboveCell0000 : AngleCell

Subcell 0000 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCellsecda937af3.thetaAboveCell00002200 : AngleCell

Subcell 00002200 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCellsecda937af3.thetaAboveCell000022002011 : AngleCell

Subcell 000022002011 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCellsecda937af3.thetaAboveCell0000220020113122 : AngleCell

Subcell 0000220020113122 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCellsefa0cf83b9.thetaAboveCell0000 : AngleCell

Subcell 0000 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCellsefa0cf83b9.thetaAboveCell00002200 : AngleCell

Subcell 00002200 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCellsefa0cf83b9.thetaAboveCell000022002011 : AngleCell

Subcell 000022002011 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCellsefa0cf83b9.thetaAboveCell0000220020113123 : AngleCell

Subcell 0000220020113123 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells38fe0cae80.thetaAboveCell0000 : AngleCell

Subcell 0000 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells38fe0cae80.thetaAboveCell00002200 : AngleCell

Subcell 00002200 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells38fe0cae80.thetaAboveCell000022002011 : AngleCell

Subcell 000022002011 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells38fe0cae80.thetaAboveCell0000220020113130 : AngleCell

Subcell 0000220020113130 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells32c7b8b1fa.thetaAboveCell0000 : AngleCell

Subcell 0000 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells32c7b8b1fa.thetaAboveCell00002200 : AngleCell

Subcell 00002200 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells32c7b8b1fa.thetaAboveCell000022002011 : AngleCell

Subcell 000022002011 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells32c7b8b1fa.thetaAboveCell0000220020113131 : AngleCell

Subcell 0000220020113131 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCellsb136ba3941.thetaAboveCell0000 : AngleCell

Subcell 0000 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCellsb136ba3941.thetaAboveCell00002200 : AngleCell

Subcell 00002200 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCellsb136ba3941.thetaAboveCell000022002011 : AngleCell

Subcell 000022002011 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCellsb136ba3941.thetaAboveCell0000220020113132 : AngleCell

Subcell 0000220020113132 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells8ac48dda13.thetaAboveCell0000 : AngleCell

Subcell 0000 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells8ac48dda13.thetaAboveCell00002200 : AngleCell

Subcell 00002200 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells8ac48dda13.thetaAboveCell000022002011 : AngleCell

Subcell 000022002011 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells8ac48dda13.thetaAboveCell0000220020113133 : AngleCell

Subcell 0000220020113133 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCellsde5c2f11fb.thetaAboveCell0000 : AngleCell

Subcell 0000 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCellsde5c2f11fb.thetaAboveCell00002200 : AngleCell

Subcell 00002200 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCellsde5c2f11fb.thetaAboveCell000022002011 : AngleCell

Subcell 000022002011 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCellsc44d408296.thetaAboveCell0000 : AngleCell

Subcell 0000 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCellsc44d408296.thetaAboveCell00002200 : AngleCell

Subcell 00002200 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCellsc44d408296.thetaAboveCell000022002011 : AngleCell

Subcell 000022002011 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells057d5ed82d.thetaAboveCell0000 : AngleCell

Subcell 0000 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells057d5ed82d.thetaAboveCell00002200 : AngleCell

Subcell 00002200 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells057d5ed82d.thetaAboveCell000022002012 : AngleCell

Subcell 000022002012 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCellsc56edf0af2.thetaAboveCell0000 : AngleCell

Subcell 0000 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCellsc56edf0af2.thetaAboveCell00002200 : AngleCell

Subcell 00002200 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCellsc56edf0af2.thetaAboveCell000022002013 : AngleCell

Subcell 000022002013 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells38f587bebf.thetaAboveCell0000 : AngleCell

Subcell 0000 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells38f587bebf.thetaAboveCell00002200 : AngleCell

Subcell 00002200 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells38f587bebf.thetaAboveCell000022002000 : AngleCell

Subcell 000022002000 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCellsc330c6667b.thetaAboveCell0000 : AngleCell

Subcell 0000 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCellsc330c6667b.thetaAboveCell00002200 : AngleCell

Subcell 00002200 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCellsc330c6667b.thetaAboveCell000022002000 : AngleCell

Subcell 000022002000 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells8addf3ec0f.thetaAboveCell0000 : AngleCell

Subcell 0000 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells8addf3ec0f.thetaAboveCell00002200 : AngleCell

Subcell 00002200 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells8addf3ec0f.thetaAboveCell000022002000 : AngleCell

Subcell 000022002000 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells8addf3ec0f.thetaAboveCell0000220020002000 : AngleCell

Subcell 0000220020002000 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells06b0cdd59e.thetaAboveCell0000 : AngleCell

Subcell 0000 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells06b0cdd59e.thetaAboveCell00002200 : AngleCell

Subcell 00002200 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells06b0cdd59e.thetaAboveCell000022002000 : AngleCell

Subcell 000022002000 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells06b0cdd59e.thetaAboveCell0000220020002001 : AngleCell

Subcell 0000220020002001 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCellsf1a599f1e1.thetaAboveCell0000 : AngleCell

Subcell 0000 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCellsf1a599f1e1.thetaAboveCell00002200 : AngleCell

Subcell 00002200 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCellsf1a599f1e1.thetaAboveCell000022002000 : AngleCell

Subcell 000022002000 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCellsf1a599f1e1.thetaAboveCell0000220020002002 : AngleCell

Subcell 0000220020002002 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells260222ce28.thetaAboveCell0000 : AngleCell

Subcell 0000 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells260222ce28.thetaAboveCell00002200 : AngleCell

Subcell 00002200 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells260222ce28.thetaAboveCell000022002000 : AngleCell

Subcell 000022002000 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells260222ce28.thetaAboveCell0000220020002003 : AngleCell

Subcell 0000220020002003 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells5c03b20b81.thetaAboveCell0000 : AngleCell

Subcell 0000 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells5c03b20b81.thetaAboveCell00002200 : AngleCell

Subcell 00002200 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells5c03b20b81.thetaAboveCell000022002000 : AngleCell

Subcell 000022002000 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells5c03b20b81.thetaAboveCell0000220020002010 : AngleCell

Subcell 0000220020002010 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells36e0f7722b.thetaAboveCell0000 : AngleCell

Subcell 0000 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells36e0f7722b.thetaAboveCell00002200 : AngleCell

Subcell 00002200 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells36e0f7722b.thetaAboveCell000022002000 : AngleCell

Subcell 000022002000 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells36e0f7722b.thetaAboveCell0000220020002011 : AngleCell

Subcell 0000220020002011 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCellsb7dd59a80a.thetaAboveCell0000 : AngleCell

Subcell 0000 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCellsb7dd59a80a.thetaAboveCell00002200 : AngleCell

Subcell 00002200 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCellsb7dd59a80a.thetaAboveCell000022002000 : AngleCell

Subcell 000022002000 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCellsb7dd59a80a.thetaAboveCell0000220020002012 : AngleCell

Subcell 0000220020002012 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCellsef0079dc28.thetaAboveCell0000 : AngleCell

Subcell 0000 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCellsef0079dc28.thetaAboveCell00002200 : AngleCell

Subcell 00002200 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCellsef0079dc28.thetaAboveCell000022002000 : AngleCell

Subcell 000022002000 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCellsef0079dc28.thetaAboveCell0000220020002013 : AngleCell

Subcell 0000220020002013 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells58fa53de1e.thetaAboveCell0000 : AngleCell

Subcell 0000 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells58fa53de1e.thetaAboveCell00002200 : AngleCell

Subcell 00002200 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells58fa53de1e.thetaAboveCell000022002000 : AngleCell

Subcell 000022002000 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells5c48ba0580.thetaAboveCell0000 : AngleCell

Subcell 0000 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells5c48ba0580.thetaAboveCell00002200 : AngleCell

Subcell 00002200 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells5c48ba0580.thetaAboveCell000022002000 : AngleCell

Subcell 000022002000 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells35af4df13c.thetaAboveCell0000 : AngleCell

Subcell 0000 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells35af4df13c.thetaAboveCell00002200 : AngleCell

Subcell 00002200 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells35af4df13c.thetaAboveCell000022002000 : AngleCell

Subcell 000022002000 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells35af4df13c.thetaAboveCell0000220020002100 : AngleCell

Subcell 0000220020002100 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCellsbb596d2a3e.thetaAboveCell0000 : AngleCell

Subcell 0000 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCellsbb596d2a3e.thetaAboveCell00002200 : AngleCell

Subcell 00002200 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCellsbb596d2a3e.thetaAboveCell000022002000 : AngleCell

Subcell 000022002000 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCellsbb596d2a3e.thetaAboveCell0000220020002101 : AngleCell

Subcell 0000220020002101 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells8645eca0c5.thetaAboveCell0000 : AngleCell

Subcell 0000 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells8645eca0c5.thetaAboveCell00002200 : AngleCell

Subcell 00002200 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells8645eca0c5.thetaAboveCell000022002000 : AngleCell

Subcell 000022002000 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells8645eca0c5.thetaAboveCell0000220020002102 : AngleCell

Subcell 0000220020002102 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCellsbe94e44cff.thetaAboveCell0000 : AngleCell

Subcell 0000 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCellsbe94e44cff.thetaAboveCell00002200 : AngleCell

Subcell 00002200 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCellsbe94e44cff.thetaAboveCell000022002000 : AngleCell

Subcell 000022002000 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCellsbe94e44cff.thetaAboveCell0000220020002103 : AngleCell

Subcell 0000220020002103 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCellsd01cbbb894.thetaAboveCell0000 : AngleCell

Subcell 0000 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCellsd01cbbb894.thetaAboveCell00002200 : AngleCell

Subcell 00002200 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCellsd01cbbb894.thetaAboveCell000022002000 : AngleCell

Subcell 000022002000 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCellsd01cbbb894.thetaAboveCell0000220020002110 : AngleCell

Subcell 0000220020002110 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells768f9f5a16.thetaAboveCell0000 : AngleCell

Subcell 0000 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells768f9f5a16.thetaAboveCell00002200 : AngleCell

Subcell 00002200 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells768f9f5a16.thetaAboveCell000022002000 : AngleCell

Subcell 000022002000 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

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

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells768f9f5a16.thetaAboveCell0000220020002111 : AngleCell

Subcell 0000220020002111 of the theta-above root; digits 0–3 mean LL, LH, HL, HH.

Equations

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

Gerver sofa dependency batch

• KernelOnly.PartE.PhiBelow.Leaf00445.
• KernelOnly.PartE.PhiBelow.Leaf00450.
• KernelOnly.PartE.PhiBelow.Leaf00451.
• KernelOnly.PartE.PhiBelow.Leaf00453.
• KernelOnly.PartE.PhiBelow.Leaf00454.
• KernelOnly.PartE.PhiBelow.Leaf00455.
• KernelOnly.PartE.PhiBelow.Leaf00456.
• KernelOnly.PartE.PhiBelow.Leaf00458.
• KernelOnly.PartE.PhiBelow.Leaf00461.
• KernelOnly.PartE.ThetaAbove.Leaf00009.
• KernelOnly.PartE.ThetaAbove.Leaf00010.
• KernelOnly.PartE.ThetaAbove.Leaf00012.
• KernelOnly.PartE.ThetaAbove.Leaf00013.
• KernelOnly.PartE.ThetaAbove.Leaf00014.
• KernelOnly.PartE.ThetaAbove.Leaf00015.
• KernelOnly.PartE.ThetaAbove.Leaf00018.
• KernelOnly.PartE.ThetaAbove.Leaf00019.
• KernelOnly.PartE.ThetaAbove.Leaf00020.
• KernelOnly.PartE.ThetaAbove.Leaf00021.
• KernelOnly.PartE.ThetaAbove.Leaf00024.
• KernelOnly.PartE.ThetaAbove.Leaf00025.
• KernelOnly.PartE.ThetaAbove.Leaf00028.
• KernelOnly.PartE.ThetaAbove.Leaf00029.
• KernelOnly.PartE.ThetaAbove.Leaf00475.
• KernelOnly.PartE.ThetaAbove.Leaf00476.
• KernelOnly.PartE.ThetaAbove.Leaf00480.
• KernelOnly.PartE.ThetaAbove.Leaf00481.
• KernelOnly.PartE.ThetaAbove.Leaf00482.
• KernelOnly.PartE.ThetaAbove.Leaf00483.
• KernelOnly.PartE.ThetaAbove.Leaf00486.
• KernelOnly.PartE.ThetaAbove.Leaf00487.
• KernelOnly.PartE.ThetaAbove.Leaf00488.
• KernelOnly.PartE.ThetaAbove.Leaf00489.
• KernelOnly.PartE.ThetaAbove.Leaf00491.
• KernelOnly.PartE.ThetaAbove.Leaf00492.
• KernelOnly.PartE.ThetaAbove.Leaf00496.
• KernelOnly.PartE.ThetaAbove.Leaf00497.
• KernelOnly.PartE.ThetaAbove.Leaf00498.
• KernelOnly.PartE.ThetaAbove.Leaf00499.
• KernelOnly.PartE.ThetaAbove.Leaf00502.
• KernelOnly.PartE.ThetaAbove.Leaf00503.

Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Phi Below Leaf33233_c2_c2_c3_c3_c3_4_00445

theorem GerverSofa.PartE.e24KC2PhiBelowLeaf33233_c2_c2_c3_c3_c3 : adaptiveCoverCheck 4 (childHH (childHH CertificateCellsd112ae8b34.phiBelowCell33233223)) = true

Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Phi Below Leaf33233_c2_c3_c0_6_00450

theorem GerverSofa.PartE.e24KC2PhiBelowLeaf33233_c2_c3_c0 : adaptiveCoverCheck 6 CertificateCells005204f093.phiBelowCell33233230 = true

Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Phi Below Leaf33233_c2_c3_c1_6_00451

theorem GerverSofa.PartE.e24KC2PhiBelowLeaf33233_c2_c3_c1 : adaptiveCoverCheck 6 CertificateCells1db372ce58.phiBelowCell33233231 = true

Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Phi Below Leaf33233_c2_c3_c2_c0_5_00453

theorem GerverSofa.PartE.e24KC2PhiBelowLeaf33233_c2_c3_c2_c0 : adaptiveCoverCheck 5 (childLL CertificateCells747d0e3511.phiBelowCell33233232) = true

Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Phi Below Leaf33233_c2_c3_c2_c1_5_00454

theorem GerverSofa.PartE.e24KC2PhiBelowLeaf33233_c2_c3_c2_c1 : adaptiveCoverCheck 5 (childLH CertificateCells2c20a17ff6.phiBelowCell33233232) = true

Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Phi Below Leaf33233_c2_c3_c2_c2_5_00455

theorem GerverSofa.PartE.e24KC2PhiBelowLeaf33233_c2_c3_c2_c2 : adaptiveCoverCheck 5 (childHL CertificateCells6d9a408f54.phiBelowCell33233232) = true

Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Phi Below Leaf33233_c2_c3_c2_c3_5_00456

theorem GerverSofa.PartE.e24KC2PhiBelowLeaf33233_c2_c3_c2_c3 : adaptiveCoverCheck 5 (childHH CertificateCells26c5fe31ab.phiBelowCell33233232) = true

Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Phi Below Leaf33233_c2_c3_c3_6_00458

theorem GerverSofa.PartE.e24KC2PhiBelowLeaf33233_c2_c3_c3 : adaptiveCoverCheck 6 CertificateCells8faba9c99a.phiBelowCell33233233 = true

Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Phi Below Leaf33233_c3_8_00461

theorem GerverSofa.PartE.e24KC2PhiBelowLeaf33233_c3 : adaptiveCoverCheck 8 (childHH (childHH CertificateCellsd0acf0005e.phiBelowCell3323)) = true

Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Theta Above

Leaf0000220020_c1_c1_c3_c1_c0_4_00009

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000220020_c1_c1_c3_c1_c0 : adaptiveCoverCheck 4 (childLL (childLH (childHH CertificateCellsd9f8181f0f.thetaAboveCell000022002011))) = true

Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Theta Above

Leaf0000220020_c1_c1_c3_c1_c1_4_00010

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000220020_c1_c1_c3_c1_c1 : adaptiveCoverCheck 4 (childLH (childLH (childHH CertificateCellsc3ac49754f.thetaAboveCell000022002011))) = true

Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Theta Above

Leaf0000220020_c1_c1_c3_c1_c2_c0_3_00012

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000220020_c1_c1_c3_c1_c2_c0 : adaptiveCoverCheck 3 CertificateCellsa708f81b81.thetaAboveCell0000220020113120 = true

Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Theta Above

Leaf0000220020_c1_c1_c3_c1_c2_c1_3_00013

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000220020_c1_c1_c3_c1_c2_c1 : adaptiveCoverCheck 3 CertificateCellsd0cc56b48c.thetaAboveCell0000220020113121 = true

Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Theta Above

Leaf0000220020_c1_c1_c3_c1_c2_c2_3_00014

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000220020_c1_c1_c3_c1_c2_c2 : adaptiveCoverCheck 3 CertificateCellsecda937af3.thetaAboveCell0000220020113122 = true

Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Theta Above

Leaf0000220020_c1_c1_c3_c1_c2_c3_3_00015

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000220020_c1_c1_c3_c1_c2_c3 : adaptiveCoverCheck 3 CertificateCellsefa0cf83b9.thetaAboveCell0000220020113123 = true

Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Theta Above

Leaf0000220020_c1_c1_c3_c1_c3_c0_3_00018

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000220020_c1_c1_c3_c1_c3_c0 : adaptiveCoverCheck 3 CertificateCells38fe0cae80.thetaAboveCell0000220020113130 = true

Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Theta Above

Leaf0000220020_c1_c1_c3_c1_c3_c1_3_00019

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000220020_c1_c1_c3_c1_c3_c1 : adaptiveCoverCheck 3 CertificateCells32c7b8b1fa.thetaAboveCell0000220020113131 = true

Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Theta Above

Leaf0000220020_c1_c1_c3_c1_c3_c2_3_00020

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000220020_c1_c1_c3_c1_c3_c2 : adaptiveCoverCheck 3 CertificateCellsb136ba3941.thetaAboveCell0000220020113132 = true

Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Theta Above

Leaf0000220020_c1_c1_c3_c1_c3_c3_3_00021

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000220020_c1_c1_c3_c1_c3_c3 : adaptiveCoverCheck 3 CertificateCells8ac48dda13.thetaAboveCell0000220020113133 = true

Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Theta Above

Leaf0000220020_c1_c1_c3_c2_5_00024

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000220020_c1_c1_c3_c2 : adaptiveCoverCheck 5 (childHL (childHH CertificateCellsde5c2f11fb.thetaAboveCell000022002011)) = true

Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Theta Above

Leaf0000220020_c1_c1_c3_c3_5_00025

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000220020_c1_c1_c3_c3 : adaptiveCoverCheck 5 (childHH (childHH CertificateCellsc44d408296.thetaAboveCell000022002011)) = true

Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Theta Above Leaf0000220020_c1_c2_7_00028

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000220020_c1_c2 : adaptiveCoverCheck 7 CertificateCells057d5ed82d.thetaAboveCell000022002012 = true

Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Theta Above Leaf0000220020_c1_c3_7_00029

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000220020_c1_c3 : adaptiveCoverCheck 7 CertificateCellsc56edf0af2.thetaAboveCell000022002013 = true

Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Theta Above

Leaf0000220020_c0_c0_c0_6_00475

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000220020_c0_c0_c0 : adaptiveCoverCheck 6 (childLL CertificateCells38f587bebf.thetaAboveCell000022002000) = true

Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Theta Above

Leaf0000220020_c0_c0_c1_6_00476

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000220020_c0_c0_c1 : adaptiveCoverCheck 6 (childLH CertificateCellsc330c6667b.thetaAboveCell000022002000) = true

Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Theta Above

Leaf0000220020_c0_c0_c2_c0_c0_c0_3_00480

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000220020_c0_c0_c2_c0_c0_c0 : adaptiveCoverCheck 3 CertificateCells8addf3ec0f.thetaAboveCell0000220020002000 = true

Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Theta Above

Leaf0000220020_c0_c0_c2_c0_c0_c1_3_00481

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000220020_c0_c0_c2_c0_c0_c1 : adaptiveCoverCheck 3 CertificateCells06b0cdd59e.thetaAboveCell0000220020002001 = true

Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Theta Above

Leaf0000220020_c0_c0_c2_c0_c0_c2_3_00482

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000220020_c0_c0_c2_c0_c0_c2 : adaptiveCoverCheck 3 CertificateCellsf1a599f1e1.thetaAboveCell0000220020002002 = true

Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Theta Above

Leaf0000220020_c0_c0_c2_c0_c0_c3_3_00483

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000220020_c0_c0_c2_c0_c0_c3 : adaptiveCoverCheck 3 CertificateCells260222ce28.thetaAboveCell0000220020002003 = true

Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Theta Above

Leaf0000220020_c0_c0_c2_c0_c1_c0_3_00486

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000220020_c0_c0_c2_c0_c1_c0 : adaptiveCoverCheck 3 CertificateCells5c03b20b81.thetaAboveCell0000220020002010 = true

Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Theta Above

Leaf0000220020_c0_c0_c2_c0_c1_c1_3_00487

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000220020_c0_c0_c2_c0_c1_c1 : adaptiveCoverCheck 3 CertificateCells36e0f7722b.thetaAboveCell0000220020002011 = true

Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Theta Above

Leaf0000220020_c0_c0_c2_c0_c1_c2_3_00488

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000220020_c0_c0_c2_c0_c1_c2 : adaptiveCoverCheck 3 CertificateCellsb7dd59a80a.thetaAboveCell0000220020002012 = true

Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Theta Above

Leaf0000220020_c0_c0_c2_c0_c1_c3_3_00489

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000220020_c0_c0_c2_c0_c1_c3 : adaptiveCoverCheck 3 CertificateCellsef0079dc28.thetaAboveCell0000220020002013 = true

Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Theta Above

Leaf0000220020_c0_c0_c2_c0_c2_4_00491

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000220020_c0_c0_c2_c0_c2 : adaptiveCoverCheck 4 (childHL (childLL (childHL CertificateCells58fa53de1e.thetaAboveCell000022002000))) = true

Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Theta Above

Leaf0000220020_c0_c0_c2_c0_c3_4_00492

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000220020_c0_c0_c2_c0_c3 : adaptiveCoverCheck 4 (childHH (childLL (childHL CertificateCells5c48ba0580.thetaAboveCell000022002000))) = true

Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Theta Above

Leaf0000220020_c0_c0_c2_c1_c0_c0_3_00496

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000220020_c0_c0_c2_c1_c0_c0 : adaptiveCoverCheck 3 CertificateCells35af4df13c.thetaAboveCell0000220020002100 = true

Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Theta Above

Leaf0000220020_c0_c0_c2_c1_c0_c1_3_00497

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000220020_c0_c0_c2_c1_c0_c1 : adaptiveCoverCheck 3 CertificateCellsbb596d2a3e.thetaAboveCell0000220020002101 = true

Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Theta Above

Leaf0000220020_c0_c0_c2_c1_c0_c2_3_00498

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000220020_c0_c0_c2_c1_c0_c2 : adaptiveCoverCheck 3 CertificateCells8645eca0c5.thetaAboveCell0000220020002102 = true

Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Theta Above

Leaf0000220020_c0_c0_c2_c1_c0_c3_3_00499

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000220020_c0_c0_c2_c1_c0_c3 : adaptiveCoverCheck 3 CertificateCellsbe94e44cff.thetaAboveCell0000220020002103 = true

Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Theta Above

Leaf0000220020_c0_c0_c2_c1_c1_c0_3_00502

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000220020_c0_c0_c2_c1_c1_c0 : adaptiveCoverCheck 3 CertificateCellsd01cbbb894.thetaAboveCell0000220020002110 = true

Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Theta Above

Leaf0000220020_c0_c0_c2_c1_c1_c1_3_00503

theorem GerverSofa.PartE.e24KC2ThetaAboveLeaf0000220020_c0_c0_c2_c1_c1_c1 : adaptiveCoverCheck 3 CertificateCells768f9f5a16.thetaAboveCell0000220020002111 = true