Gerver sofa: related certificate and semantic modules

• GerverSofa.KernelOnly.PartE.Certificates.Batch039.

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells88f33db9e4.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.CertificateCells88f33db9e4.phiBelowCell33232311 : AngleCell

Subcell 33232311 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.CertificateCellsbe3ab504ac.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.CertificateCellsbe3ab504ac.phiBelowCell33232311 : AngleCell

Subcell 33232311 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.CertificateCellsc46bd88a54.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.CertificateCellsc46bd88a54.phiBelowCell33232312 : AngleCell

Subcell 33232312 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.CertificateCellse089a8f9ae.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.CertificateCellse089a8f9ae.phiBelowCell33232313 : AngleCell

Subcell 33232313 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.CertificateCellsf5ba6a429c.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.CertificateCellsf5ba6a429c.phiBelowCell33232313 : AngleCell

Subcell 33232313 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.CertificateCellsff1f5625e7.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.CertificateCellsff1f5625e7.phiBelowCell33232313 : AngleCell

Subcell 33232313 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.CertificateCells2a20ecd725.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.CertificateCells2a20ecd725.phiBelowCell33232313 : AngleCell

Subcell 33232313 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.CertificateCellsa4ad8d7233.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.CertificateCells6d4400643e.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.CertificateCells6d4400643e.phiBelowCell33232330 : AngleCell

Subcell 33232330 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.CertificateCellsa7c3c8a0e8.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.CertificateCellsa7c3c8a0e8.phiBelowCell33232331 : AngleCell

Subcell 33232331 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.CertificateCellsee53a497bf.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.CertificateCellsee53a497bf.phiBelowCell33232331 : AngleCell

Subcell 33232331 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.CertificateCells672c985771.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.CertificateCells672c985771.phiBelowCell33232331 : AngleCell

Subcell 33232331 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.CertificateCellsbdc9b1cb1f.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.CertificateCellsbdc9b1cb1f.phiBelowCell33232331 : AngleCell

Subcell 33232331 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.CertificateCells6f8943a51a.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.CertificateCells6f8943a51a.phiBelowCell33232332 : AngleCell

Subcell 33232332 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.CertificateCells3c06cca83d.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.CertificateCells3c06cca83d.phiBelowCell33232333 : AngleCell

Subcell 33232333 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.CertificateCells9a18487959.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.CertificateCells5679b6d0b8.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.CertificateCells94565979ef.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.CertificateCells1a32aff68c.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.CertificateCells170ce03ef2.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.CertificateCells8706070b49.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.CertificateCells8706070b49.phiBelowCell33233200 : AngleCell

Subcell 33233200 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.CertificateCells29218b6dfb.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.CertificateCells29218b6dfb.phiBelowCell33233201 : AngleCell

Subcell 33233201 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.CertificateCellscd85cede4b.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.CertificateCellscd85cede4b.phiBelowCell33233202 : AngleCell

Subcell 33233202 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.CertificateCells14bc720168.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.CertificateCells14bc720168.phiBelowCell33233202 : AngleCell

Subcell 33233202 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.CertificateCellsc20163bbb0.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.CertificateCellsc20163bbb0.phiBelowCell33233202 : AngleCell

Subcell 33233202 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.CertificateCellsfb4e8d760d.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.CertificateCellsfb4e8d760d.phiBelowCell33233202 : AngleCell

Subcell 33233202 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.CertificateCells1167e65ac9.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.CertificateCells1167e65ac9.phiBelowCell33233203 : AngleCell

Subcell 33233203 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.CertificateCellsa97cd5b1f9.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.CertificateCells33181810b4.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.CertificateCells33181810b4.phiBelowCell33233220 : AngleCell

Subcell 33233220 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.CertificateCellseb15d79203.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.CertificateCellseb15d79203.phiBelowCell33233220 : AngleCell

Subcell 33233220 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.CertificateCellse0133145f0.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.CertificateCellse0133145f0.phiBelowCell33233220 : AngleCell

Subcell 33233220 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.CertificateCellsdabae3eeeb.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.CertificateCellsdabae3eeeb.phiBelowCell33233220 : AngleCell

Subcell 33233220 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.CertificateCells18d43d056c.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.CertificateCells18d43d056c.phiBelowCell33233220 : AngleCell

Subcell 33233220 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.CertificateCellse49667421f.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.CertificateCellse49667421f.phiBelowCell33233220 : AngleCell

Subcell 33233220 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.CertificateCellsd4600f4c86.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.CertificateCellsd4600f4c86.phiBelowCell33233220 : AngleCell

Subcell 33233220 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.CertificateCells368be09a97.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.CertificateCells368be09a97.phiBelowCell33233221 : AngleCell

Subcell 33233221 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.CertificateCells1f54f397e7.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.CertificateCells1f54f397e7.phiBelowCell33233221 : AngleCell

Subcell 33233221 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.

Gerver sofa dependency batch

• KernelOnly.PartE.PhiBelow.Leaf00324.
• KernelOnly.PartE.PhiBelow.Leaf00325.
• KernelOnly.PartE.PhiBelow.Leaf00327.
• KernelOnly.PartE.PhiBelow.Leaf00329.
• KernelOnly.PartE.PhiBelow.Leaf00330.
• KernelOnly.PartE.PhiBelow.Leaf00331.
• KernelOnly.PartE.PhiBelow.Leaf00332.
• KernelOnly.PartE.PhiBelow.Leaf00335.
• KernelOnly.PartE.PhiBelow.Leaf00337.
• KernelOnly.PartE.PhiBelow.Leaf00339.
• KernelOnly.PartE.PhiBelow.Leaf00340.
• KernelOnly.PartE.PhiBelow.Leaf00341.
• KernelOnly.PartE.PhiBelow.Leaf00342.
• KernelOnly.PartE.PhiBelow.Leaf00344.
• KernelOnly.PartE.PhiBelow.Leaf00345.
• KernelOnly.PartE.PhiBelow.Leaf00354.
• KernelOnly.PartE.PhiBelow.Leaf00355.
• KernelOnly.PartE.PhiBelow.Leaf00356.
• KernelOnly.PartE.PhiBelow.Leaf00357.
• KernelOnly.PartE.PhiBelow.Leaf00359.
• KernelOnly.PartE.PhiBelow.Leaf00362.
• KernelOnly.PartE.PhiBelow.Leaf00363.
• KernelOnly.PartE.PhiBelow.Leaf00365.
• KernelOnly.PartE.PhiBelow.Leaf00366.
• KernelOnly.PartE.PhiBelow.Leaf00367.
• KernelOnly.PartE.PhiBelow.Leaf00368.
• KernelOnly.PartE.PhiBelow.Leaf00370.
• KernelOnly.PartE.PhiBelow.Leaf00372.
• KernelOnly.PartE.PhiBelow.Leaf00375.
• KernelOnly.PartE.PhiBelow.Leaf00376.
• KernelOnly.PartE.PhiBelow.Leaf00377.
• KernelOnly.PartE.PhiBelow.Leaf00379.
• KernelOnly.PartE.PhiBelow.Leaf00380.
• KernelOnly.PartE.PhiBelow.Leaf00381.
• KernelOnly.PartE.PhiBelow.Leaf00382.
• KernelOnly.PartE.PhiBelow.Leaf00386.
• KernelOnly.PartE.PhiBelow.Leaf00387.

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

theorem GerverSofa.PartE.e24KC2PhiBelowLeaf33232_c3_c1_c1_c2 : adaptiveCoverCheck 5 (childHL CertificateCells88f33db9e4.phiBelowCell33232311) = true

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

theorem GerverSofa.PartE.e24KC2PhiBelowLeaf33232_c3_c1_c1_c3 : adaptiveCoverCheck 5 (childHH CertificateCellsbe3ab504ac.phiBelowCell33232311) = true

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

theorem GerverSofa.PartE.e24KC2PhiBelowLeaf33232_c3_c1_c2 : adaptiveCoverCheck 6 CertificateCellsc46bd88a54.phiBelowCell33232312 = true

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

theorem GerverSofa.PartE.e24KC2PhiBelowLeaf33232_c3_c1_c3_c0 : adaptiveCoverCheck 5 (childLL CertificateCellse089a8f9ae.phiBelowCell33232313) = true

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

theorem GerverSofa.PartE.e24KC2PhiBelowLeaf33232_c3_c1_c3_c1 : adaptiveCoverCheck 5 (childLH CertificateCellsf5ba6a429c.phiBelowCell33232313) = true

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

theorem GerverSofa.PartE.e24KC2PhiBelowLeaf33232_c3_c1_c3_c2 : adaptiveCoverCheck 5 (childHL CertificateCellsff1f5625e7.phiBelowCell33232313) = true

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

theorem GerverSofa.PartE.e24KC2PhiBelowLeaf33232_c3_c1_c3_c3 : adaptiveCoverCheck 5 (childHH CertificateCells2a20ecd725.phiBelowCell33232313) = true

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

theorem GerverSofa.PartE.e24KC2PhiBelowLeaf33232_c3_c2 : adaptiveCoverCheck 7 (childHL (childHH (childHL CertificateCellsa4ad8d7233.phiBelowCell3323))) = true

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

theorem GerverSofa.PartE.e24KC2PhiBelowLeaf33232_c3_c3_c0 : adaptiveCoverCheck 6 CertificateCells6d4400643e.phiBelowCell33232330 = true

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

theorem GerverSofa.PartE.e24KC2PhiBelowLeaf33232_c3_c3_c1_c0 : adaptiveCoverCheck 5 (childLL CertificateCellsa7c3c8a0e8.phiBelowCell33232331) = true

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

theorem GerverSofa.PartE.e24KC2PhiBelowLeaf33232_c3_c3_c1_c1 : adaptiveCoverCheck 5 (childLH CertificateCellsee53a497bf.phiBelowCell33232331) = true

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

theorem GerverSofa.PartE.e24KC2PhiBelowLeaf33232_c3_c3_c1_c2 : adaptiveCoverCheck 5 (childHL CertificateCells672c985771.phiBelowCell33232331) = true

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

theorem GerverSofa.PartE.e24KC2PhiBelowLeaf33232_c3_c3_c1_c3 : adaptiveCoverCheck 5 (childHH CertificateCellsbdc9b1cb1f.phiBelowCell33232331) = true

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

theorem GerverSofa.PartE.e24KC2PhiBelowLeaf33232_c3_c3_c2 : adaptiveCoverCheck 6 CertificateCells6f8943a51a.phiBelowCell33232332 = true

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

theorem GerverSofa.PartE.e24KC2PhiBelowLeaf33232_c3_c3_c3 : adaptiveCoverCheck 6 CertificateCells3c06cca83d.phiBelowCell33232333 = true

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

theorem GerverSofa.PartE.e24KC2PhiBelowLeaf33233_c0_c0 : adaptiveCoverCheck 7 (childLL (childLL (childHH CertificateCells9a18487959.phiBelowCell3323))) = true

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

theorem GerverSofa.PartE.e24KC2PhiBelowLeaf33233_c0_c1 : adaptiveCoverCheck 7 (childLH (childLL (childHH CertificateCells5679b6d0b8.phiBelowCell3323))) = true

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

theorem GerverSofa.PartE.e24KC2PhiBelowLeaf33233_c0_c2 : adaptiveCoverCheck 7 (childHL (childLL (childHH CertificateCells94565979ef.phiBelowCell3323))) = true

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

theorem GerverSofa.PartE.e24KC2PhiBelowLeaf33233_c0_c3 : adaptiveCoverCheck 7 (childHH (childLL (childHH CertificateCells1a32aff68c.phiBelowCell3323))) = true

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

theorem GerverSofa.PartE.e24KC2PhiBelowLeaf33233_c1 : adaptiveCoverCheck 8 (childLH (childHH CertificateCells170ce03ef2.phiBelowCell3323)) = true

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

theorem GerverSofa.PartE.e24KC2PhiBelowLeaf33233_c2_c0_c0 : adaptiveCoverCheck 6 CertificateCells8706070b49.phiBelowCell33233200 = true

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

theorem GerverSofa.PartE.e24KC2PhiBelowLeaf33233_c2_c0_c1 : adaptiveCoverCheck 6 CertificateCells29218b6dfb.phiBelowCell33233201 = true

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

theorem GerverSofa.PartE.e24KC2PhiBelowLeaf33233_c2_c0_c2_c0 : adaptiveCoverCheck 5 (childLL CertificateCellscd85cede4b.phiBelowCell33233202) = true

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

theorem GerverSofa.PartE.e24KC2PhiBelowLeaf33233_c2_c0_c2_c1 : adaptiveCoverCheck 5 (childLH CertificateCells14bc720168.phiBelowCell33233202) = true

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

theorem GerverSofa.PartE.e24KC2PhiBelowLeaf33233_c2_c0_c2_c2 : adaptiveCoverCheck 5 (childHL CertificateCellsc20163bbb0.phiBelowCell33233202) = true

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

theorem GerverSofa.PartE.e24KC2PhiBelowLeaf33233_c2_c0_c2_c3 : adaptiveCoverCheck 5 (childHH CertificateCellsfb4e8d760d.phiBelowCell33233202) = true

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

theorem GerverSofa.PartE.e24KC2PhiBelowLeaf33233_c2_c0_c3 : adaptiveCoverCheck 6 CertificateCells1167e65ac9.phiBelowCell33233203 = true

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

theorem GerverSofa.PartE.e24KC2PhiBelowLeaf33233_c2_c1 : adaptiveCoverCheck 7 (childLH (childHL (childHH CertificateCellsa97cd5b1f9.phiBelowCell3323))) = true

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

theorem GerverSofa.PartE.e24KC2PhiBelowLeaf33233_c2_c2_c0_c0 : adaptiveCoverCheck 5 (childLL CertificateCells33181810b4.phiBelowCell33233220) = true

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

theorem GerverSofa.PartE.e24KC2PhiBelowLeaf33233_c2_c2_c0_c1 : adaptiveCoverCheck 5 (childLH CertificateCellseb15d79203.phiBelowCell33233220) = true

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

theorem GerverSofa.PartE.e24KC2PhiBelowLeaf33233_c2_c2_c0_c2 : adaptiveCoverCheck 5 (childHL CertificateCellse0133145f0.phiBelowCell33233220) = true

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

theorem GerverSofa.PartE.e24KC2PhiBelowLeaf33233_c2_c2_c0_c3_c0 : adaptiveCoverCheck 4 (childLL (childHH CertificateCellsdabae3eeeb.phiBelowCell33233220)) = true

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

theorem GerverSofa.PartE.e24KC2PhiBelowLeaf33233_c2_c2_c0_c3_c1 : adaptiveCoverCheck 4 (childLH (childHH CertificateCells18d43d056c.phiBelowCell33233220)) = true

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

theorem GerverSofa.PartE.e24KC2PhiBelowLeaf33233_c2_c2_c0_c3_c2 : adaptiveCoverCheck 4 (childHL (childHH CertificateCellse49667421f.phiBelowCell33233220)) = true

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

theorem GerverSofa.PartE.e24KC2PhiBelowLeaf33233_c2_c2_c0_c3_c3 : adaptiveCoverCheck 4 (childHH (childHH CertificateCellsd4600f4c86.phiBelowCell33233220)) = true

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

theorem GerverSofa.PartE.e24KC2PhiBelowLeaf33233_c2_c2_c1_c0 : adaptiveCoverCheck 5 (childLL CertificateCells368be09a97.phiBelowCell33233221) = true

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

theorem GerverSofa.PartE.e24KC2PhiBelowLeaf33233_c2_c2_c1_c1 : adaptiveCoverCheck 5 (childLH CertificateCells1f54f397e7.phiBelowCell33233221) = true