Gerver sofa: related certificate and semantic modules

• GerverSofa.KernelOnly.PartE.Certificates.Batch036.

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells02f8aca2f2.phiAboveCell1101 : AngleCell

Subcell 1101 of the phi-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.CertificateCells02f8aca2f2.phiAboveCell11011011 : AngleCell

Subcell 11011011 of the phi-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.CertificateCellsca6ca7b54c.phiAboveCell1101 : AngleCell

Subcell 1101 of the phi-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.CertificateCellsca6ca7b54c.phiAboveCell11011011 : AngleCell

Subcell 11011011 of the phi-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.CertificateCells8161bed319.phiAboveCell1101 : AngleCell

Subcell 1101 of the phi-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.CertificateCells8161bed319.phiAboveCell11011011 : AngleCell

Subcell 11011011 of the phi-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.CertificateCells5f2ef3defa.phiAboveCell1101 : AngleCell

Subcell 1101 of the phi-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.CertificateCells5f2ef3defa.phiAboveCell11011011 : AngleCell

Subcell 11011011 of the phi-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.CertificateCellsd4f6865820.phiAboveCell1101 : AngleCell

Subcell 1101 of the phi-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.CertificateCellsd4f6865820.phiAboveCell11011011 : AngleCell

Subcell 11011011 of the phi-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.CertificateCellsaca7f76cfa.phiAboveCell1101 : AngleCell

Subcell 1101 of the phi-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.CertificateCellsaca7f76cfa.phiAboveCell11011011 : AngleCell

Subcell 11011011 of the phi-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.CertificateCellsa7ad4ac263.phiAboveCell1101 : AngleCell

Subcell 1101 of the phi-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.CertificateCellsa7ad4ac263.phiAboveCell11011011 : AngleCell

Subcell 11011011 of the phi-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.CertificateCells53f8862830.phiAboveCell1101 : AngleCell

Subcell 1101 of the phi-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.CertificateCells53f8862830.phiAboveCell11011011 : AngleCell

Subcell 11011011 of the phi-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.CertificateCellsb6a37b0947.phiAboveCell1101 : AngleCell

Subcell 1101 of the phi-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.CertificateCellsb6a37b0947.phiAboveCell11011011 : AngleCell

Subcell 11011011 of the phi-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.CertificateCellsbc3b77fd62.phiAboveCell1101 : AngleCell

Subcell 1101 of the phi-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.CertificateCellsbc3b77fd62.phiAboveCell11011011 : AngleCell

Subcell 11011011 of the phi-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.CertificateCellsec2a80bcb9.phiAboveCell1101 : AngleCell

Subcell 1101 of the phi-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.CertificateCellsec2a80bcb9.phiAboveCell11011011 : AngleCell

Subcell 11011011 of the phi-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.CertificateCells69b4ed96bb.phiAboveCell1101 : AngleCell

Subcell 1101 of the phi-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.CertificateCells69b4ed96bb.phiAboveCell11011011 : AngleCell

Subcell 11011011 of the phi-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.CertificateCells81024818f0.phiAboveCell1101 : AngleCell

Subcell 1101 of the phi-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.CertificateCells81024818f0.phiAboveCell11011011 : AngleCell

Subcell 11011011 of the phi-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.CertificateCellsbaba88fb03.phiAboveCell1101 : AngleCell

Subcell 1101 of the phi-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.CertificateCellsbaba88fb03.phiAboveCell11011011 : AngleCell

Subcell 11011011 of the phi-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.CertificateCells4431add919.phiAboveCell1101 : AngleCell

Subcell 1101 of the phi-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.CertificateCells4431add919.phiAboveCell11011011 : AngleCell

Subcell 11011011 of the phi-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.CertificateCells0c4c476da0.phiAboveCell1101 : AngleCell

Subcell 1101 of the phi-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.CertificateCells0c4c476da0.phiAboveCell11011011 : AngleCell

Subcell 11011011 of the phi-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.CertificateCells4cc4ec35a2.phiAboveCell1101 : AngleCell

Subcell 1101 of the phi-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.CertificateCells4cc4ec35a2.phiAboveCell11011011 : AngleCell

Subcell 11011011 of the phi-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.CertificateCells35cb6fddbf.phiAboveCell1101 : AngleCell

Subcell 1101 of the phi-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.CertificateCells35cb6fddbf.phiAboveCell11011011 : AngleCell

Subcell 11011011 of the phi-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.CertificateCells23ac2ec29f.phiAboveCell1101 : AngleCell

Subcell 1101 of the phi-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.CertificateCells23ac2ec29f.phiAboveCell11011012 : AngleCell

Subcell 11011012 of the phi-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.CertificateCellsfeaf82eaaf.phiAboveCell1101 : AngleCell

Subcell 1101 of the phi-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.CertificateCellsfeaf82eaaf.phiAboveCell11011013 : AngleCell

Subcell 11011013 of the phi-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.CertificateCellsb3a5df470b.phiAboveCell1101 : AngleCell

Subcell 1101 of the phi-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.CertificateCellsb3a5df470b.phiAboveCell11011100 : AngleCell

Subcell 11011100 of the phi-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.CertificateCells347f84d8ab.phiAboveCell1101 : AngleCell

Subcell 1101 of the phi-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.CertificateCells347f84d8ab.phiAboveCell11011100 : AngleCell

Subcell 11011100 of the phi-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.CertificateCells7c0e2d8793.phiAboveCell1101 : AngleCell

Subcell 1101 of the phi-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.CertificateCells7c0e2d8793.phiAboveCell11011100 : AngleCell

Subcell 11011100 of the phi-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.CertificateCells7ce200bf6e.phiAboveCell1101 : AngleCell

Subcell 1101 of the phi-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.CertificateCells7ce200bf6e.phiAboveCell11011100 : AngleCell

Subcell 11011100 of the phi-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.CertificateCells947c600e46.phiAboveCell1101 : AngleCell

Subcell 1101 of the phi-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.CertificateCells947c600e46.phiAboveCell11011100 : AngleCell

Subcell 11011100 of the phi-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.CertificateCells8f0ac2a0b1.phiAboveCell1101 : AngleCell

Subcell 1101 of the phi-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.CertificateCells8f0ac2a0b1.phiAboveCell11011100 : AngleCell

Subcell 11011100 of the phi-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.CertificateCells3019c743c4.phiAboveCell1101 : AngleCell

Subcell 1101 of the phi-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.CertificateCells3019c743c4.phiAboveCell11011100 : AngleCell

Subcell 11011100 of the phi-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.CertificateCellsa28fd06134.phiAboveCell1101 : AngleCell

Subcell 1101 of the phi-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.CertificateCellsa28fd06134.phiAboveCell11011100 : AngleCell

Subcell 11011100 of the phi-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.CertificateCells77eee4a3e4.phiAboveCell1101 : AngleCell

Subcell 1101 of the phi-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.CertificateCells77eee4a3e4.phiAboveCell11011100 : AngleCell

Subcell 11011100 of the phi-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.CertificateCells49eb854006.phiAboveCell1101 : AngleCell

Subcell 1101 of the phi-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.CertificateCells49eb854006.phiAboveCell11011100 : AngleCell

Subcell 11011100 of the phi-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.CertificateCellsfd1ec1f302.phiAboveCell1101 : AngleCell

Subcell 1101 of the phi-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.CertificateCellsfd1ec1f302.phiAboveCell11011100 : AngleCell

Subcell 11011100 of the phi-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.CertificateCellsc041f3b547.phiAboveCell1101 : AngleCell

Subcell 1101 of the phi-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.CertificateCellsc041f3b547.phiAboveCell11011100 : AngleCell

Subcell 11011100 of the phi-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.CertificateCells4859223aba.phiAboveCell1101 : AngleCell

Subcell 1101 of the phi-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.CertificateCells4859223aba.phiAboveCell11011100 : AngleCell

Subcell 11011100 of the phi-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.CertificateCellsfd6149c12c.phiAboveCell1101 : AngleCell

Subcell 1101 of the phi-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.CertificateCellsfd6149c12c.phiAboveCell11011101 : AngleCell

Subcell 11011101 of the phi-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.CertificateCells858f68cb01.phiAboveCell1101 : AngleCell

Subcell 1101 of the phi-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.CertificateCells858f68cb01.phiAboveCell11011101 : AngleCell

Subcell 11011101 of the phi-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.CertificateCellsfd737d0524.phiAboveCell1101 : AngleCell

Subcell 1101 of the phi-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.CertificateCellsfd737d0524.phiAboveCell11011101 : AngleCell

Subcell 11011101 of the phi-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.CertificateCells8872ea9267.phiAboveCell1101 : AngleCell

Subcell 1101 of the phi-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.CertificateCells8872ea9267.phiAboveCell11011101 : AngleCell

Subcell 11011101 of the phi-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.CertificateCells911bdd7a98.phiAboveCell1101 : AngleCell

Subcell 1101 of the phi-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.CertificateCells911bdd7a98.phiAboveCell11011102 : AngleCell

Subcell 11011102 of the phi-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.CertificateCells6b2d569c3f.phiAboveCell1101 : AngleCell

Subcell 1101 of the phi-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.CertificateCells6b2d569c3f.phiAboveCell11011103 : AngleCell

Subcell 11011103 of the phi-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.CertificateCells692b3d6bf8.phiAboveCell1101 : AngleCell

Subcell 1101 of the phi-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.CertificateCells692b3d6bf8.phiAboveCell11011110 : AngleCell

Subcell 11011110 of the phi-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.CertificateCells6503060a21.phiAboveCell1101 : AngleCell

Subcell 1101 of the phi-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.CertificateCells6503060a21.phiAboveCell11011110 : AngleCell

Subcell 11011110 of the phi-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.CertificateCells262d88f1dc.phiAboveCell1101 : AngleCell

Subcell 1101 of the phi-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.CertificateCells262d88f1dc.phiAboveCell11011110 : AngleCell

Subcell 11011110 of the phi-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.CertificateCellse46caf457c.phiAboveCell1101 : AngleCell

Subcell 1101 of the phi-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.CertificateCellse46caf457c.phiAboveCell11011110 : AngleCell

Subcell 11011110 of the phi-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.CertificateCells16ed6aeb9e.phiAboveCell1101 : AngleCell

Subcell 1101 of the phi-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.CertificateCells16ed6aeb9e.phiAboveCell11011110 : AngleCell

Subcell 11011110 of the phi-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.CertificateCellsde6b2a5e55.phiAboveCell1101 : AngleCell

Subcell 1101 of the phi-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.CertificateCellsde6b2a5e55.phiAboveCell11011110 : AngleCell

Subcell 11011110 of the phi-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.CertificateCells522fe632f2.phiAboveCell1101 : AngleCell

Subcell 1101 of the phi-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.CertificateCells522fe632f2.phiAboveCell11011110 : AngleCell

Subcell 11011110 of the phi-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.PhiAbove.Leaf00082.
• KernelOnly.PartE.PhiAbove.Leaf00083.
• KernelOnly.PartE.PhiAbove.Leaf00084.
• KernelOnly.PartE.PhiAbove.Leaf00087.
• KernelOnly.PartE.PhiAbove.Leaf00088.
• KernelOnly.PartE.PhiAbove.Leaf00089.
• KernelOnly.PartE.PhiAbove.Leaf00090.
• KernelOnly.PartE.PhiAbove.Leaf00092.
• KernelOnly.PartE.PhiAbove.Leaf00093.
• KernelOnly.PartE.PhiAbove.Leaf00097.
• KernelOnly.PartE.PhiAbove.Leaf00098.
• KernelOnly.PartE.PhiAbove.Leaf00099.
• KernelOnly.PartE.PhiAbove.Leaf00100.
• KernelOnly.PartE.PhiAbove.Leaf00102.
• KernelOnly.PartE.PhiAbove.Leaf00103.
• KernelOnly.PartE.PhiAbove.Leaf00104.
• KernelOnly.PartE.PhiAbove.Leaf00106.
• KernelOnly.PartE.PhiAbove.Leaf00107.
• KernelOnly.PartE.PhiAbove.Leaf00109.
• KernelOnly.PartE.PhiAbove.Leaf00110.
• KernelOnly.PartE.PhiAbove.Leaf00118.
• KernelOnly.PartE.PhiAbove.Leaf00119.
• KernelOnly.PartE.PhiAbove.Leaf00120.
• KernelOnly.PartE.PhiAbove.Leaf00121.
• KernelOnly.PartE.PhiAbove.Leaf00125.
• KernelOnly.PartE.PhiAbove.Leaf00126.
• KernelOnly.PartE.PhiAbove.Leaf00127.
• KernelOnly.PartE.PhiAbove.Leaf00128.
• KernelOnly.PartE.PhiAbove.Leaf00130.
• KernelOnly.PartE.PhiAbove.Leaf00131.
• KernelOnly.PartE.PhiAbove.Leaf00132.
• KernelOnly.PartE.PhiAbove.Leaf00134.
• KernelOnly.PartE.PhiAbove.Leaf00135.
• KernelOnly.PartE.PhiAbove.Leaf00138.
• KernelOnly.PartE.PhiAbove.Leaf00139.
• KernelOnly.PartE.PhiAbove.Leaf00140.
• KernelOnly.PartE.PhiAbove.Leaf00141.
• KernelOnly.PartE.PhiAbove.Leaf00143.
• KernelOnly.PartE.PhiAbove.Leaf00144.
• KernelOnly.PartE.PhiAbove.Leaf00150.
• KernelOnly.PartE.PhiAbove.Leaf00152.
• KernelOnly.PartE.PhiAbove.Leaf00153.
• KernelOnly.PartE.PhiAbove.Leaf00154.
• KernelOnly.PartE.PhiAbove.Leaf00155.
• KernelOnly.PartE.PhiAbove.Leaf00157.
• KernelOnly.PartE.PhiAbove.Leaf00158.

Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Phi Above Leaf1101101_c1_c0_c0_c1_5_00082

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1101101_c1_c0_c0_c1 : adaptiveCoverCheck 5 (childLH (childLL (childLL CertificateCells02f8aca2f2.phiAboveCell11011011))) = true

Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Phi Above Leaf1101101_c1_c0_c0_c2_5_00083

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1101101_c1_c0_c0_c2 : adaptiveCoverCheck 5 (childHL (childLL (childLL CertificateCellsca6ca7b54c.phiAboveCell11011011))) = true

Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Phi Above Leaf1101101_c1_c0_c0_c3_5_00084

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1101101_c1_c0_c0_c3 : adaptiveCoverCheck 5 (childHH (childLL (childLL CertificateCells8161bed319.phiAboveCell11011011))) = true

Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Phi Above Leaf1101101_c1_c0_c1_c0_5_00087

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1101101_c1_c0_c1_c0 : adaptiveCoverCheck 5 (childLL (childLH (childLL CertificateCells5f2ef3defa.phiAboveCell11011011))) = true

Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Phi Above Leaf1101101_c1_c0_c1_c1_5_00088

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1101101_c1_c0_c1_c1 : adaptiveCoverCheck 5 (childLH (childLH (childLL CertificateCellsd4f6865820.phiAboveCell11011011))) = true

Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Phi Above Leaf1101101_c1_c0_c1_c2_5_00089

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1101101_c1_c0_c1_c2 : adaptiveCoverCheck 5 (childHL (childLH (childLL CertificateCellsaca7f76cfa.phiAboveCell11011011))) = true

Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Phi Above Leaf1101101_c1_c0_c1_c3_5_00090

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1101101_c1_c0_c1_c3 : adaptiveCoverCheck 5 (childHH (childLH (childLL CertificateCellsa7ad4ac263.phiAboveCell11011011))) = true

Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Phi Above Leaf1101101_c1_c0_c2_6_00092

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1101101_c1_c0_c2 : adaptiveCoverCheck 6 (childHL (childLL CertificateCells53f8862830.phiAboveCell11011011)) = true

Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Phi Above Leaf1101101_c1_c0_c3_6_00093

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1101101_c1_c0_c3 : adaptiveCoverCheck 6 (childHH (childLL CertificateCellsb6a37b0947.phiAboveCell11011011)) = true

Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Phi Above Leaf1101101_c1_c1_c0_c0_5_00097

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1101101_c1_c1_c0_c0 : adaptiveCoverCheck 5 (childLL (childLL (childLH CertificateCellsbc3b77fd62.phiAboveCell11011011))) = true

Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Phi Above Leaf1101101_c1_c1_c0_c1_5_00098

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1101101_c1_c1_c0_c1 : adaptiveCoverCheck 5 (childLH (childLL (childLH CertificateCellsec2a80bcb9.phiAboveCell11011011))) = true

Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Phi Above Leaf1101101_c1_c1_c0_c2_5_00099

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1101101_c1_c1_c0_c2 : adaptiveCoverCheck 5 (childHL (childLL (childLH CertificateCells69b4ed96bb.phiAboveCell11011011))) = true

Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Phi Above Leaf1101101_c1_c1_c0_c3_5_00100

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1101101_c1_c1_c0_c3 : adaptiveCoverCheck 5 (childHH (childLL (childLH CertificateCells81024818f0.phiAboveCell11011011))) = true

Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Phi Above Leaf1101101_c1_c1_c1_6_00102

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1101101_c1_c1_c1 : adaptiveCoverCheck 6 (childLH (childLH CertificateCellsbaba88fb03.phiAboveCell11011011)) = true

Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Phi Above Leaf1101101_c1_c1_c2_6_00103

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1101101_c1_c1_c2 : adaptiveCoverCheck 6 (childHL (childLH CertificateCells4431add919.phiAboveCell11011011)) = true

Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Phi Above Leaf1101101_c1_c1_c3_6_00104

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1101101_c1_c1_c3 : adaptiveCoverCheck 6 (childHH (childLH CertificateCells0c4c476da0.phiAboveCell11011011)) = true

Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Phi Above Leaf1101101_c1_c2_7_00106

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1101101_c1_c2 : adaptiveCoverCheck 7 (childHL CertificateCells4cc4ec35a2.phiAboveCell11011011) = true

Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Phi Above Leaf1101101_c1_c3_7_00107

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1101101_c1_c3 : adaptiveCoverCheck 7 (childHH CertificateCells35cb6fddbf.phiAboveCell11011011) = true

Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Phi Above Leaf1101101_c2_8_00109

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1101101_c2 : adaptiveCoverCheck 8 CertificateCells23ac2ec29f.phiAboveCell11011012 = true

Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Phi Above Leaf1101101_c3_8_00110

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1101101_c3 : adaptiveCoverCheck 8 CertificateCellsfeaf82eaaf.phiAboveCell11011013 = true

Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Phi Above Leaf1101110_c0_c0_c0_6_00118

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1101110_c0_c0_c0 : adaptiveCoverCheck 6 (childLL (childLL CertificateCellsb3a5df470b.phiAboveCell11011100)) = true

Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Phi Above Leaf1101110_c0_c0_c1_6_00119

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1101110_c0_c0_c1 : adaptiveCoverCheck 6 (childLH (childLL CertificateCells347f84d8ab.phiAboveCell11011100)) = true

Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Phi Above Leaf1101110_c0_c0_c2_6_00120

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1101110_c0_c0_c2 : adaptiveCoverCheck 6 (childHL (childLL CertificateCells7c0e2d8793.phiAboveCell11011100)) = true

Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Phi Above Leaf1101110_c0_c0_c3_6_00121

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1101110_c0_c0_c3 : adaptiveCoverCheck 6 (childHH (childLL CertificateCells7ce200bf6e.phiAboveCell11011100)) = true

Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Phi Above Leaf1101110_c0_c1_c0_c0_5_00125

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1101110_c0_c1_c0_c0 : adaptiveCoverCheck 5 (childLL (childLL (childLH CertificateCells947c600e46.phiAboveCell11011100))) = true

Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Phi Above Leaf1101110_c0_c1_c0_c1_5_00126

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1101110_c0_c1_c0_c1 : adaptiveCoverCheck 5 (childLH (childLL (childLH CertificateCells8f0ac2a0b1.phiAboveCell11011100))) = true

Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Phi Above Leaf1101110_c0_c1_c0_c2_5_00127

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1101110_c0_c1_c0_c2 : adaptiveCoverCheck 5 (childHL (childLL (childLH CertificateCells3019c743c4.phiAboveCell11011100))) = true

Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Phi Above Leaf1101110_c0_c1_c0_c3_5_00128

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1101110_c0_c1_c0_c3 : adaptiveCoverCheck 5 (childHH (childLL (childLH CertificateCellsa28fd06134.phiAboveCell11011100))) = true

Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Phi Above Leaf1101110_c0_c1_c1_6_00130

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1101110_c0_c1_c1 : adaptiveCoverCheck 6 (childLH (childLH CertificateCells77eee4a3e4.phiAboveCell11011100)) = true

Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Phi Above Leaf1101110_c0_c1_c2_6_00131

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1101110_c0_c1_c2 : adaptiveCoverCheck 6 (childHL (childLH CertificateCells49eb854006.phiAboveCell11011100)) = true

Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Phi Above Leaf1101110_c0_c1_c3_6_00132

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1101110_c0_c1_c3 : adaptiveCoverCheck 6 (childHH (childLH CertificateCellsfd1ec1f302.phiAboveCell11011100)) = true

Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Phi Above Leaf1101110_c0_c2_7_00134

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1101110_c0_c2 : adaptiveCoverCheck 7 (childHL CertificateCellsc041f3b547.phiAboveCell11011100) = true

Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Phi Above Leaf1101110_c0_c3_7_00135

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1101110_c0_c3 : adaptiveCoverCheck 7 (childHH CertificateCells4859223aba.phiAboveCell11011100) = true

Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Phi Above Leaf1101110_c1_c0_7_00138

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1101110_c1_c0 : adaptiveCoverCheck 7 (childLL CertificateCellsfd6149c12c.phiAboveCell11011101) = true

Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Phi Above Leaf1101110_c1_c1_7_00139

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1101110_c1_c1 : adaptiveCoverCheck 7 (childLH CertificateCells858f68cb01.phiAboveCell11011101) = true

Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Phi Above Leaf1101110_c1_c2_7_00140

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1101110_c1_c2 : adaptiveCoverCheck 7 (childHL CertificateCellsfd737d0524.phiAboveCell11011101) = true

Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Phi Above Leaf1101110_c1_c3_7_00141

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1101110_c1_c3 : adaptiveCoverCheck 7 (childHH CertificateCells8872ea9267.phiAboveCell11011101) = true

Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Phi Above Leaf1101110_c2_8_00143

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1101110_c2 : adaptiveCoverCheck 8 CertificateCells911bdd7a98.phiAboveCell11011102 = true

Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Phi Above Leaf1101110_c3_8_00144

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1101110_c3 : adaptiveCoverCheck 8 CertificateCells6b2d569c3f.phiAboveCell11011103 = true

Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Phi Above Leaf1101111_c0_c0_7_00150

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1101111_c0_c0 : adaptiveCoverCheck 7 (childLL CertificateCells692b3d6bf8.phiAboveCell11011110) = true

Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Phi Above Leaf1101111_c0_c1_c0_6_00152

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1101111_c0_c1_c0 : adaptiveCoverCheck 6 (childLL (childLH CertificateCells6503060a21.phiAboveCell11011110)) = true

Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Phi Above Leaf1101111_c0_c1_c1_6_00153

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1101111_c0_c1_c1 : adaptiveCoverCheck 6 (childLH (childLH CertificateCells262d88f1dc.phiAboveCell11011110)) = true

Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Phi Above Leaf1101111_c0_c1_c2_6_00154

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1101111_c0_c1_c2 : adaptiveCoverCheck 6 (childHL (childLH CertificateCellse46caf457c.phiAboveCell11011110)) = true

Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Phi Above Leaf1101111_c0_c1_c3_6_00155

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1101111_c0_c1_c3 : adaptiveCoverCheck 6 (childHH (childLH CertificateCells16ed6aeb9e.phiAboveCell11011110)) = true

Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Phi Above Leaf1101111_c0_c2_7_00157

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1101111_c0_c2 : adaptiveCoverCheck 7 (childHL CertificateCellsde6b2a5e55.phiAboveCell11011110) = true

Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Phi Above Leaf1101111_c0_c3_7_00158

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1101111_c0_c3 : adaptiveCoverCheck 7 (childHH CertificateCells522fe632f2.phiAboveCell11011110) = true