Gerver sofa: related certificate and semantic modules

• GerverSofa.KernelOnly.PartE.Certificates.Batch037.

@[reducible, inline]

abbrev GerverSofa.PartE.CertificateCells018fd5e668.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.CertificateCells018fd5e668.phiAboveCell11011111 : AngleCell

Subcell 11011111 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.CertificateCells63f0679649.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.CertificateCells63f0679649.phiAboveCell11011111 : AngleCell

Subcell 11011111 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.CertificateCellsa5edf5ee06.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.CertificateCellsa5edf5ee06.phiAboveCell11011111 : AngleCell

Subcell 11011111 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.CertificateCellsd0bb651e18.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.CertificateCellsd0bb651e18.phiAboveCell11011111 : AngleCell

Subcell 11011111 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.CertificateCells347e84a45d.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.CertificateCells347e84a45d.phiAboveCell11011112 : AngleCell

Subcell 11011112 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.CertificateCells06372696b5.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.CertificateCells06372696b5.phiAboveCell11011113 : AngleCell

Subcell 11011113 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.CertificateCellsdc3bb009fb.phiAboveCell1110 : AngleCell

Subcell 1110 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.CertificateCellsdc3bb009fb.phiAboveCell11100000 : AngleCell

Subcell 11100000 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.CertificateCellsa17c45a931.phiAboveCell1110 : AngleCell

Subcell 1110 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.CertificateCellsa17c45a931.phiAboveCell11100000 : AngleCell

Subcell 11100000 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.CertificateCells11ac46d6b2.phiAboveCell1110 : AngleCell

Subcell 1110 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.CertificateCells11ac46d6b2.phiAboveCell11100000 : AngleCell

Subcell 11100000 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.CertificateCells4bb3cae3bb.phiAboveCell1110 : AngleCell

Subcell 1110 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.CertificateCells4bb3cae3bb.phiAboveCell11100000 : AngleCell

Subcell 11100000 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.CertificateCells517a8caf86.phiAboveCell1110 : AngleCell

Subcell 1110 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.CertificateCells517a8caf86.phiAboveCell11100001 : AngleCell

Subcell 11100001 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.CertificateCells5795a3d5ea.phiAboveCell1110 : AngleCell

Subcell 1110 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.CertificateCells5795a3d5ea.phiAboveCell11100002 : AngleCell

Subcell 11100002 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.CertificateCellsa32d189193.phiAboveCell1110 : AngleCell

Subcell 1110 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.CertificateCellsa32d189193.phiAboveCell11100003 : AngleCell

Subcell 11100003 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.CertificateCellsf628113fc1.phiAboveCell1110 : AngleCell

Subcell 1110 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.CertificateCellsf628113fc1.phiAboveCell11100010 : AngleCell

Subcell 11100010 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.CertificateCells740eeaba32.phiAboveCell1110 : AngleCell

Subcell 1110 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.CertificateCells740eeaba32.phiAboveCell11100011 : AngleCell

Subcell 11100011 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.CertificateCells626f3fc028.phiAboveCell1110 : AngleCell

Subcell 1110 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.CertificateCells626f3fc028.phiAboveCell11100012 : AngleCell

Subcell 11100012 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.CertificateCells15f9582e4b.phiAboveCell1110 : AngleCell

Subcell 1110 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.CertificateCells15f9582e4b.phiAboveCell11100013 : AngleCell

Subcell 11100013 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.CertificateCellsc156062d1b.phiAboveCell1110 : AngleCell

Subcell 1110 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.CertificateCellsc156062d1b.phiAboveCell11100100 : AngleCell

Subcell 11100100 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.CertificateCellsdb4a23ce5a.phiAboveCell1110 : AngleCell

Subcell 1110 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.CertificateCellsdb4a23ce5a.phiAboveCell11100101 : AngleCell

Subcell 11100101 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.CertificateCells8ced9a3143.phiAboveCell1110 : AngleCell

Subcell 1110 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.CertificateCells8ced9a3143.phiAboveCell11100102 : AngleCell

Subcell 11100102 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.CertificateCells1c46ec9a00.phiAboveCell1110 : AngleCell

Subcell 1110 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.CertificateCells1c46ec9a00.phiAboveCell11100103 : AngleCell

Subcell 11100103 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.CertificateCellsc9ea34c02b.phiAboveCell1110 : AngleCell

Subcell 1110 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.CertificateCellsc9ea34c02b.phiAboveCell11100110 : AngleCell

Subcell 11100110 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.CertificateCells7575776df3.phiAboveCell1110 : AngleCell

Subcell 1110 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.CertificateCells7575776df3.phiAboveCell11100111 : AngleCell

Subcell 11100111 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.CertificateCells8b638b7054.phiAboveCell1110 : AngleCell

Subcell 1110 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.CertificateCells8b638b7054.phiAboveCell11100112 : AngleCell

Subcell 11100112 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.CertificateCells3bd9cbb8df.phiAboveCell1110 : AngleCell

Subcell 1110 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.CertificateCells3bd9cbb8df.phiAboveCell11100113 : AngleCell

Subcell 11100113 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.CertificateCells41c704a1f1.phiBelowCell3320 : AngleCell

Subcell 3320 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.CertificateCells67d940c92a.phiBelowCell3320 : AngleCell

Subcell 3320 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.CertificateCells8d68909634.phiBelowCell3320 : AngleCell

Subcell 3320 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.CertificateCellsc208943a95.phiBelowCell3320 : AngleCell

Subcell 3320 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.CertificateCells42a66228ec.phiBelowCell3322 : AngleCell

Subcell 3322 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.CertificateCells67af310b24.phiBelowCell3322 : AngleCell

Subcell 3322 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.CertificateCells9b91503b21.phiBelowCell3322 : AngleCell

Subcell 3322 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.CertificateCellsb36cfca8f0.phiBelowCell3322 : AngleCell

Subcell 3322 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.PhiAbove.Leaf00161.
• KernelOnly.PartE.PhiAbove.Leaf00162.
• KernelOnly.PartE.PhiAbove.Leaf00163.
• KernelOnly.PartE.PhiAbove.Leaf00164.
• KernelOnly.PartE.PhiAbove.Leaf00166.
• KernelOnly.PartE.PhiAbove.Leaf00167.
• KernelOnly.PartE.PhiAbove.Leaf00174.
• KernelOnly.PartE.PhiAbove.Leaf00175.
• KernelOnly.PartE.PhiAbove.Leaf00176.
• KernelOnly.PartE.PhiAbove.Leaf00177.
• KernelOnly.PartE.PhiAbove.Leaf00179.
• KernelOnly.PartE.PhiAbove.Leaf00180.
• KernelOnly.PartE.PhiAbove.Leaf00181.
• KernelOnly.PartE.PhiAbove.Leaf00187.
• KernelOnly.PartE.PhiAbove.Leaf00188.
• KernelOnly.PartE.PhiAbove.Leaf00189.
• KernelOnly.PartE.PhiAbove.Leaf00190.
• KernelOnly.PartE.PhiAbove.Leaf00196.
• KernelOnly.PartE.PhiAbove.Leaf00197.
• KernelOnly.PartE.PhiAbove.Leaf00198.
• KernelOnly.PartE.PhiAbove.Leaf00199.
• KernelOnly.PartE.PhiAbove.Leaf00204.
• KernelOnly.PartE.PhiAbove.Leaf00205.
• KernelOnly.PartE.PhiAbove.Leaf00206.
• KernelOnly.PartE.PhiAbove.Leaf00207.
• KernelOnly.PartE.PhiBelow.Leaf00242.
• KernelOnly.PartE.PhiBelow.Leaf00243.
• KernelOnly.PartE.PhiBelow.Leaf00244.
• KernelOnly.PartE.PhiBelow.Leaf00245.
• KernelOnly.PartE.PhiBelow.Leaf00256.
• KernelOnly.PartE.PhiBelow.Leaf00257.
• KernelOnly.PartE.PhiBelow.Leaf00258.
• KernelOnly.PartE.PhiBelow.Leaf00259.

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

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1101111_c1_c0 : adaptiveCoverCheck 7 (childLL CertificateCells018fd5e668.phiAboveCell11011111) = true

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

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1101111_c1_c1 : adaptiveCoverCheck 7 (childLH CertificateCells63f0679649.phiAboveCell11011111) = true

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

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1101111_c1_c2 : adaptiveCoverCheck 7 (childHL CertificateCellsa5edf5ee06.phiAboveCell11011111) = true

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

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1101111_c1_c3 : adaptiveCoverCheck 7 (childHH CertificateCellsd0bb651e18.phiAboveCell11011111) = true

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

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1101111_c2 : adaptiveCoverCheck 8 CertificateCells347e84a45d.phiAboveCell11011112 = true

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

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1101111_c3 : adaptiveCoverCheck 8 CertificateCells06372696b5.phiAboveCell11011113 = true

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

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1110000_c0_c0 : adaptiveCoverCheck 7 (childLL CertificateCellsdc3bb009fb.phiAboveCell11100000) = true

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

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1110000_c0_c1 : adaptiveCoverCheck 7 (childLH CertificateCellsa17c45a931.phiAboveCell11100000) = true

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

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1110000_c0_c2 : adaptiveCoverCheck 7 (childHL CertificateCells11ac46d6b2.phiAboveCell11100000) = true

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

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1110000_c0_c3 : adaptiveCoverCheck 7 (childHH CertificateCells4bb3cae3bb.phiAboveCell11100000) = true

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

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1110000_c1 : adaptiveCoverCheck 8 CertificateCells517a8caf86.phiAboveCell11100001 = true

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

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1110000_c2 : adaptiveCoverCheck 8 CertificateCells5795a3d5ea.phiAboveCell11100002 = true

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

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1110000_c3 : adaptiveCoverCheck 8 CertificateCellsa32d189193.phiAboveCell11100003 = true

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

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1110001_c0 : adaptiveCoverCheck 8 CertificateCellsf628113fc1.phiAboveCell11100010 = true

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

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1110001_c1 : adaptiveCoverCheck 8 CertificateCells740eeaba32.phiAboveCell11100011 = true

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

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1110001_c2 : adaptiveCoverCheck 8 CertificateCells626f3fc028.phiAboveCell11100012 = true

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

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1110001_c3 : adaptiveCoverCheck 8 CertificateCells15f9582e4b.phiAboveCell11100013 = true

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

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1110010_c0 : adaptiveCoverCheck 8 CertificateCellsc156062d1b.phiAboveCell11100100 = true

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

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1110010_c1 : adaptiveCoverCheck 8 CertificateCellsdb4a23ce5a.phiAboveCell11100101 = true

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

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1110010_c2 : adaptiveCoverCheck 8 CertificateCells8ced9a3143.phiAboveCell11100102 = true

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

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1110010_c3 : adaptiveCoverCheck 8 CertificateCells1c46ec9a00.phiAboveCell11100103 = true

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

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1110011_c0 : adaptiveCoverCheck 8 CertificateCellsc9ea34c02b.phiAboveCell11100110 = true

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

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1110011_c1 : adaptiveCoverCheck 8 CertificateCells7575776df3.phiAboveCell11100111 = true

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

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1110011_c2 : adaptiveCoverCheck 8 CertificateCells8b638b7054.phiAboveCell11100112 = true

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

theorem GerverSofa.PartE.e24KC2PhiAboveLeaf1110011_c3 : adaptiveCoverCheck 8 CertificateCells3bd9cbb8df.phiAboveCell11100113 = true

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

theorem GerverSofa.PartE.e24KC2PhiBelowLeaf33203_c0 : adaptiveCoverCheck 8 (childLL (childHH CertificateCells41c704a1f1.phiBelowCell3320)) = true

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

theorem GerverSofa.PartE.e24KC2PhiBelowLeaf33203_c1 : adaptiveCoverCheck 8 (childLH (childHH CertificateCells67d940c92a.phiBelowCell3320)) = true

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

theorem GerverSofa.PartE.e24KC2PhiBelowLeaf33203_c2 : adaptiveCoverCheck 8 (childHL (childHH CertificateCells8d68909634.phiBelowCell3320)) = true

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

theorem GerverSofa.PartE.e24KC2PhiBelowLeaf33203_c3 : adaptiveCoverCheck 8 (childHH (childHH CertificateCellsc208943a95.phiBelowCell3320)) = true

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

theorem GerverSofa.PartE.e24KC2PhiBelowLeaf33221_c0 : adaptiveCoverCheck 8 (childLL (childLH CertificateCells42a66228ec.phiBelowCell3322)) = true

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

theorem GerverSofa.PartE.e24KC2PhiBelowLeaf33221_c1 : adaptiveCoverCheck 8 (childLH (childLH CertificateCells67af310b24.phiBelowCell3322)) = true

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

theorem GerverSofa.PartE.e24KC2PhiBelowLeaf33221_c2 : adaptiveCoverCheck 8 (childHL (childLH CertificateCells9b91503b21.phiBelowCell3322)) = true

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

theorem GerverSofa.PartE.e24KC2PhiBelowLeaf33221_c3 : adaptiveCoverCheck 8 (childHH (childLH CertificateCellsb36cfca8f0.phiBelowCell3322)) = true