Documentation

LeanPool.MovingSofa.GerverSofa.KernelOnly.PartE.Certificates.Bundle025

Gerver sofa: related certificate and semantic modules #

source
@[reducible, inline]
abbrev GerverSofa.PartE.CertificateCells8d1955d9db.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.
Instances For
    source
    @[reducible, inline]
    abbrev GerverSofa.PartE.CertificateCells5a22a388aa.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.
    Instances For
      source
      @[reducible, inline]
      abbrev GerverSofa.PartE.CertificateCells24ba63b604.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.
      Instances For
        source
        @[reducible, inline]
        abbrev GerverSofa.PartE.CertificateCells78208ba1a7.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.
        Instances For
          source
          @[reducible, inline]
          abbrev GerverSofa.PartE.CertificateCellsc3455a44b7.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.
          Instances For
            source
            @[reducible, inline]
            abbrev GerverSofa.PartE.CertificateCells9c4f656d63.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.
            Instances For
              source
              @[reducible, inline]
              abbrev GerverSofa.PartE.CertificateCells37244c6e24.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.
              Instances For
                source
                @[reducible, inline]
                abbrev GerverSofa.PartE.CertificateCells3e4038f4ea.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.
                Instances For
                  source
                  @[reducible, inline]
                  abbrev GerverSofa.PartE.CertificateCells25be007753.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.
                  Instances For
                    source
                    @[reducible, inline]
                    abbrev GerverSofa.PartE.CertificateCells9371db9199.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.
                    Instances For
                      source
                      @[reducible, inline]
                      abbrev GerverSofa.PartE.CertificateCells2426e39946.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.
                      Instances For
                        source
                        @[reducible, inline]
                        abbrev GerverSofa.PartE.CertificateCellsa09b62ac68.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.
                        Instances For
                          source
                          @[reducible, inline]
                          abbrev GerverSofa.PartE.CertificateCells296b03de2f.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.
                          Instances For
                            source
                            @[reducible, inline]
                            abbrev GerverSofa.PartE.CertificateCells230653113b.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.
                            Instances For
                              source
                              @[reducible, inline]
                              abbrev GerverSofa.PartE.CertificateCells02421cb4a8.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.
                              Instances For
                                source
                                @[reducible, inline]
                                abbrev GerverSofa.PartE.CertificateCells8af559ef49.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.
                                Instances For
                                  source
                                  @[reducible, inline]
                                  abbrev GerverSofa.PartE.CertificateCells874482b603.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.
                                  Instances For
                                    source
                                    @[reducible, inline]
                                    abbrev GerverSofa.PartE.CertificateCellse5b788289b.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.
                                    Instances For
                                      source
                                      @[reducible, inline]
                                      abbrev GerverSofa.PartE.CertificateCellsc2714ba804.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.
                                      Instances For
                                        source
                                        @[reducible, inline]
                                        abbrev GerverSofa.PartE.CertificateCellsc2714ba804.phiBelowCell33232100 :
                                        AngleCell

                                        Subcell 33232100 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.
                                        Instances For
                                          source
                                          @[reducible, inline]
                                          abbrev GerverSofa.PartE.CertificateCellscab6c01cd3.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.
                                          Instances For
                                            source
                                            @[reducible, inline]
                                            abbrev GerverSofa.PartE.CertificateCellscab6c01cd3.phiBelowCell33232101 :
                                            AngleCell

                                            Subcell 33232101 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.
                                            Instances For
                                              source
                                              @[reducible, inline]
                                              abbrev GerverSofa.PartE.CertificateCells50cb464285.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.
                                              Instances For
                                                source
                                                @[reducible, inline]
                                                abbrev GerverSofa.PartE.CertificateCells50cb464285.phiBelowCell33232102 :
                                                AngleCell

                                                Subcell 33232102 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.
                                                Instances For
                                                  source
                                                  @[reducible, inline]
                                                  abbrev GerverSofa.PartE.CertificateCellsb0d9885c34.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.
                                                  Instances For
                                                    source
                                                    @[reducible, inline]
                                                    abbrev GerverSofa.PartE.CertificateCellsb0d9885c34.phiBelowCell33232103 :
                                                    AngleCell

                                                    Subcell 33232103 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.
                                                    Instances For
                                                      source
                                                      @[reducible, inline]
                                                      abbrev GerverSofa.PartE.CertificateCellsa6cd731e2a.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.
                                                      Instances For
                                                        source
                                                        @[reducible, inline]
                                                        abbrev GerverSofa.PartE.CertificateCells786c9d28c6.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.
                                                        Instances For
                                                          source
                                                          @[reducible, inline]
                                                          abbrev GerverSofa.PartE.CertificateCells786c9d28c6.phiBelowCell33232120 :
                                                          AngleCell

                                                          Subcell 33232120 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.
                                                          Instances For
                                                            source
                                                            @[reducible, inline]
                                                            abbrev GerverSofa.PartE.CertificateCellsf9e248a6ed.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.
                                                            Instances For
                                                              source
                                                              @[reducible, inline]
                                                              abbrev GerverSofa.PartE.CertificateCellsf9e248a6ed.phiBelowCell33232121 :
                                                              AngleCell

                                                              Subcell 33232121 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.
                                                              Instances For
                                                                source
                                                                @[reducible, inline]
                                                                abbrev GerverSofa.PartE.CertificateCells576f3a7876.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.
                                                                Instances For
                                                                  source
                                                                  @[reducible, inline]
                                                                  abbrev GerverSofa.PartE.CertificateCells576f3a7876.phiBelowCell33232122 :
                                                                  AngleCell

                                                                  Subcell 33232122 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.
                                                                  Instances For
                                                                    source
                                                                    @[reducible, inline]
                                                                    abbrev GerverSofa.PartE.CertificateCellsf783690d6f.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.
                                                                    Instances For
                                                                      source
                                                                      @[reducible, inline]
                                                                      abbrev GerverSofa.PartE.CertificateCellsf783690d6f.phiBelowCell33232123 :
                                                                      AngleCell

                                                                      Subcell 33232123 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.
                                                                      Instances For
                                                                        source
                                                                        @[reducible, inline]
                                                                        abbrev GerverSofa.PartE.CertificateCellsde47ee26bd.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.
                                                                        Instances For
                                                                          source
                                                                          @[reducible, inline]
                                                                          abbrev GerverSofa.PartE.CertificateCellsde47ee26bd.phiBelowCell33232130 :
                                                                          AngleCell

                                                                          Subcell 33232130 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.
                                                                          Instances For
                                                                            source
                                                                            @[reducible, inline]
                                                                            abbrev GerverSofa.PartE.CertificateCells05c25def9b.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.
                                                                            Instances For
                                                                              source
                                                                              @[reducible, inline]
                                                                              abbrev GerverSofa.PartE.CertificateCells05c25def9b.phiBelowCell33232131 :
                                                                              AngleCell

                                                                              Subcell 33232131 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.
                                                                              Instances For
                                                                                source
                                                                                @[reducible, inline]
                                                                                abbrev GerverSofa.PartE.CertificateCellsc4f0c2a140.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.
                                                                                Instances For
                                                                                  source
                                                                                  @[reducible, inline]
                                                                                  abbrev GerverSofa.PartE.CertificateCellsc4f0c2a140.phiBelowCell33232132 :
                                                                                  AngleCell

                                                                                  Subcell 33232132 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.
                                                                                  Instances For
                                                                                    source
                                                                                    @[reducible, inline]
                                                                                    abbrev GerverSofa.PartE.CertificateCellsc119914926.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.
                                                                                    Instances For
                                                                                      source
                                                                                      @[reducible, inline]
                                                                                      abbrev GerverSofa.PartE.CertificateCellsc119914926.phiBelowCell33232133 :
                                                                                      AngleCell

                                                                                      Subcell 33232133 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.
                                                                                      Instances For
                                                                                        source
                                                                                        @[reducible, inline]
                                                                                        abbrev GerverSofa.PartE.CertificateCells70881db6a6.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.
                                                                                        Instances For
                                                                                          source
                                                                                          @[reducible, inline]
                                                                                          abbrev GerverSofa.PartE.CertificateCellsfed0e78e01.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.
                                                                                          Instances For
                                                                                            source
                                                                                            @[reducible, inline]
                                                                                            abbrev GerverSofa.PartE.CertificateCells4781918595.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.
                                                                                            Instances For
                                                                                              source
                                                                                              @[reducible, inline]
                                                                                              abbrev GerverSofa.PartE.CertificateCells4781918595.phiBelowCell33232310 :
                                                                                              AngleCell

                                                                                              Subcell 33232310 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.
                                                                                              Instances For
                                                                                                source
                                                                                                @[reducible, inline]
                                                                                                abbrev GerverSofa.PartE.CertificateCellsa584418aa1.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.
                                                                                                Instances For
                                                                                                  source
                                                                                                  @[reducible, inline]
                                                                                                  abbrev GerverSofa.PartE.CertificateCellsa584418aa1.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.
                                                                                                  Instances For
                                                                                                    source
                                                                                                    @[reducible, inline]
                                                                                                    abbrev GerverSofa.PartE.CertificateCells09c85e6b71.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.
                                                                                                    Instances For
                                                                                                      source
                                                                                                      @[reducible, inline]
                                                                                                      abbrev GerverSofa.PartE.CertificateCells09c85e6b71.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.
                                                                                                      Instances For

                                                                                                        Gerver sofa dependency batch #

                                                                                                        Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Phi Below Leaf33223_c0_8_00265 #

                                                                                                        source
                                                                                                        theorem GerverSofa.PartE.e24KC2PhiBelowLeaf33223_c0 :
                                                                                                        adaptiveCoverCheck 8 (childLL (childHH CertificateCells8d1955d9db.phiBelowCell3322)) = true

                                                                                                        Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Phi Below Leaf33223_c1_8_00266 #

                                                                                                        source
                                                                                                        theorem GerverSofa.PartE.e24KC2PhiBelowLeaf33223_c1 :
                                                                                                        adaptiveCoverCheck 8 (childLH (childHH CertificateCells5a22a388aa.phiBelowCell3322)) = true

                                                                                                        Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Phi Below Leaf33223_c2_8_00267 #

                                                                                                        source
                                                                                                        theorem GerverSofa.PartE.e24KC2PhiBelowLeaf33223_c2 :
                                                                                                        adaptiveCoverCheck 8 (childHL (childHH CertificateCells24ba63b604.phiBelowCell3322)) = true

                                                                                                        Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Phi Below Leaf33223_c3_8_00268 #

                                                                                                        source
                                                                                                        theorem GerverSofa.PartE.e24KC2PhiBelowLeaf33223_c3 :
                                                                                                        adaptiveCoverCheck 8 (childHH (childHH CertificateCells78208ba1a7.phiBelowCell3322)) = true

                                                                                                        Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Phi Below Leaf33230_c0_8_00271 #

                                                                                                        source
                                                                                                        theorem GerverSofa.PartE.e24KC2PhiBelowLeaf33230_c0 :
                                                                                                        adaptiveCoverCheck 8 (childLL (childLL CertificateCellsc3455a44b7.phiBelowCell3323)) = true

                                                                                                        Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Phi Below Leaf33230_c1_8_00272 #

                                                                                                        source
                                                                                                        theorem GerverSofa.PartE.e24KC2PhiBelowLeaf33230_c1 :
                                                                                                        adaptiveCoverCheck 8 (childLH (childLL CertificateCells9c4f656d63.phiBelowCell3323)) = true

                                                                                                        Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Phi Below Leaf33230_c2_c0_7_00274 #

                                                                                                        source
                                                                                                        theorem GerverSofa.PartE.e24KC2PhiBelowLeaf33230_c2_c0 :
                                                                                                        adaptiveCoverCheck 7 (childLL (childHL (childLL CertificateCells37244c6e24.phiBelowCell3323))) = true

                                                                                                        Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Phi Below Leaf33230_c2_c1_7_00275 #

                                                                                                        source
                                                                                                        theorem GerverSofa.PartE.e24KC2PhiBelowLeaf33230_c2_c1 :
                                                                                                        adaptiveCoverCheck 7 (childLH (childHL (childLL CertificateCells3e4038f4ea.phiBelowCell3323))) = true

                                                                                                        Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Phi Below Leaf33230_c2_c2_7_00276 #

                                                                                                        source
                                                                                                        theorem GerverSofa.PartE.e24KC2PhiBelowLeaf33230_c2_c2 :
                                                                                                        adaptiveCoverCheck 7 (childHL (childHL (childLL CertificateCells25be007753.phiBelowCell3323))) = true

                                                                                                        Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Phi Below Leaf33230_c2_c3_7_00277 #

                                                                                                        source
                                                                                                        theorem GerverSofa.PartE.e24KC2PhiBelowLeaf33230_c2_c3 :
                                                                                                        adaptiveCoverCheck 7 (childHH (childHL (childLL CertificateCells9371db9199.phiBelowCell3323))) = true

                                                                                                        Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Phi Below Leaf33230_c3_c0_7_00280 #

                                                                                                        source
                                                                                                        theorem GerverSofa.PartE.e24KC2PhiBelowLeaf33230_c3_c0 :
                                                                                                        adaptiveCoverCheck 7 (childLL (childHH (childLL CertificateCells2426e39946.phiBelowCell3323))) = true

                                                                                                        Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Phi Below Leaf33230_c3_c1_7_00281 #

                                                                                                        source
                                                                                                        theorem GerverSofa.PartE.e24KC2PhiBelowLeaf33230_c3_c1 :
                                                                                                        adaptiveCoverCheck 7 (childLH (childHH (childLL CertificateCellsa09b62ac68.phiBelowCell3323))) = true

                                                                                                        Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Phi Below Leaf33230_c3_c2_7_00282 #

                                                                                                        source
                                                                                                        theorem GerverSofa.PartE.e24KC2PhiBelowLeaf33230_c3_c2 :
                                                                                                        adaptiveCoverCheck 7 (childHL (childHH (childLL CertificateCells296b03de2f.phiBelowCell3323))) = true

                                                                                                        Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Phi Below Leaf33230_c3_c3_7_00283 #

                                                                                                        source
                                                                                                        theorem GerverSofa.PartE.e24KC2PhiBelowLeaf33230_c3_c3 :
                                                                                                        adaptiveCoverCheck 7 (childHH (childHH (childLL CertificateCells230653113b.phiBelowCell3323))) = true

                                                                                                        Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Phi Below Leaf33232_c0_c0_7_00290 #

                                                                                                        source
                                                                                                        theorem GerverSofa.PartE.e24KC2PhiBelowLeaf33232_c0_c0 :
                                                                                                        adaptiveCoverCheck 7 (childLL (childLL (childHL CertificateCells02421cb4a8.phiBelowCell3323))) = true

                                                                                                        Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Phi Below Leaf33232_c0_c1_7_00291 #

                                                                                                        source
                                                                                                        theorem GerverSofa.PartE.e24KC2PhiBelowLeaf33232_c0_c1 :
                                                                                                        adaptiveCoverCheck 7 (childLH (childLL (childHL CertificateCells8af559ef49.phiBelowCell3323))) = true

                                                                                                        Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Phi Below Leaf33232_c0_c2_7_00292 #

                                                                                                        source
                                                                                                        theorem GerverSofa.PartE.e24KC2PhiBelowLeaf33232_c0_c2 :
                                                                                                        adaptiveCoverCheck 7 (childHL (childLL (childHL CertificateCells874482b603.phiBelowCell3323))) = true

                                                                                                        Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Phi Below Leaf33232_c0_c3_7_00293 #

                                                                                                        source
                                                                                                        theorem GerverSofa.PartE.e24KC2PhiBelowLeaf33232_c0_c3 :
                                                                                                        adaptiveCoverCheck 7 (childHH (childLL (childHL CertificateCellse5b788289b.phiBelowCell3323))) = true

                                                                                                        Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Phi Below Leaf33232_c1_c0_c0_6_00297 #

                                                                                                        source
                                                                                                        theorem GerverSofa.PartE.e24KC2PhiBelowLeaf33232_c1_c0_c0 :
                                                                                                        adaptiveCoverCheck 6 CertificateCellsc2714ba804.phiBelowCell33232100 = true

                                                                                                        Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Phi Below Leaf33232_c1_c0_c1_6_00298 #

                                                                                                        source
                                                                                                        theorem GerverSofa.PartE.e24KC2PhiBelowLeaf33232_c1_c0_c1 :
                                                                                                        adaptiveCoverCheck 6 CertificateCellscab6c01cd3.phiBelowCell33232101 = true

                                                                                                        Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Phi Below Leaf33232_c1_c0_c2_6_00299 #

                                                                                                        source
                                                                                                        theorem GerverSofa.PartE.e24KC2PhiBelowLeaf33232_c1_c0_c2 :
                                                                                                        adaptiveCoverCheck 6 CertificateCells50cb464285.phiBelowCell33232102 = true

                                                                                                        Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Phi Below Leaf33232_c1_c0_c3_6_00300 #

                                                                                                        source
                                                                                                        theorem GerverSofa.PartE.e24KC2PhiBelowLeaf33232_c1_c0_c3 :
                                                                                                        adaptiveCoverCheck 6 CertificateCellsb0d9885c34.phiBelowCell33232103 = true

                                                                                                        Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Phi Below Leaf33232_c1_c1_7_00302 #

                                                                                                        source
                                                                                                        theorem GerverSofa.PartE.e24KC2PhiBelowLeaf33232_c1_c1 :
                                                                                                        adaptiveCoverCheck 7 (childLH (childLH (childHL CertificateCellsa6cd731e2a.phiBelowCell3323))) = true

                                                                                                        Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Phi Below Leaf33232_c1_c2_c0_6_00304 #

                                                                                                        source
                                                                                                        theorem GerverSofa.PartE.e24KC2PhiBelowLeaf33232_c1_c2_c0 :
                                                                                                        adaptiveCoverCheck 6 CertificateCells786c9d28c6.phiBelowCell33232120 = true

                                                                                                        Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Phi Below Leaf33232_c1_c2_c1_6_00305 #

                                                                                                        source
                                                                                                        theorem GerverSofa.PartE.e24KC2PhiBelowLeaf33232_c1_c2_c1 :
                                                                                                        adaptiveCoverCheck 6 CertificateCellsf9e248a6ed.phiBelowCell33232121 = true

                                                                                                        Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Phi Below Leaf33232_c1_c2_c2_6_00306 #

                                                                                                        source
                                                                                                        theorem GerverSofa.PartE.e24KC2PhiBelowLeaf33232_c1_c2_c2 :
                                                                                                        adaptiveCoverCheck 6 CertificateCells576f3a7876.phiBelowCell33232122 = true

                                                                                                        Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Phi Below Leaf33232_c1_c2_c3_6_00307 #

                                                                                                        source
                                                                                                        theorem GerverSofa.PartE.e24KC2PhiBelowLeaf33232_c1_c2_c3 :
                                                                                                        adaptiveCoverCheck 6 CertificateCellsf783690d6f.phiBelowCell33232123 = true

                                                                                                        Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Phi Below Leaf33232_c1_c3_c0_6_00310 #

                                                                                                        source
                                                                                                        theorem GerverSofa.PartE.e24KC2PhiBelowLeaf33232_c1_c3_c0 :
                                                                                                        adaptiveCoverCheck 6 CertificateCellsde47ee26bd.phiBelowCell33232130 = true

                                                                                                        Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Phi Below Leaf33232_c1_c3_c1_6_00311 #

                                                                                                        source
                                                                                                        theorem GerverSofa.PartE.e24KC2PhiBelowLeaf33232_c1_c3_c1 :
                                                                                                        adaptiveCoverCheck 6 CertificateCells05c25def9b.phiBelowCell33232131 = true

                                                                                                        Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Phi Below Leaf33232_c1_c3_c2_6_00312 #

                                                                                                        source
                                                                                                        theorem GerverSofa.PartE.e24KC2PhiBelowLeaf33232_c1_c3_c2 :
                                                                                                        adaptiveCoverCheck 6 CertificateCellsc4f0c2a140.phiBelowCell33232132 = true

                                                                                                        Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Phi Below Leaf33232_c1_c3_c3_6_00313 #

                                                                                                        source
                                                                                                        theorem GerverSofa.PartE.e24KC2PhiBelowLeaf33232_c1_c3_c3 :
                                                                                                        adaptiveCoverCheck 6 CertificateCellsc119914926.phiBelowCell33232133 = true

                                                                                                        Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Phi Below Leaf33232_c2_8_00316 #

                                                                                                        source
                                                                                                        theorem GerverSofa.PartE.e24KC2PhiBelowLeaf33232_c2 :
                                                                                                        adaptiveCoverCheck 8 (childHL (childHL CertificateCells70881db6a6.phiBelowCell3323)) = true

                                                                                                        Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Phi Below Leaf33232_c3_c0_7_00318 #

                                                                                                        source
                                                                                                        theorem GerverSofa.PartE.e24KC2PhiBelowLeaf33232_c3_c0 :
                                                                                                        adaptiveCoverCheck 7 (childLL (childHH (childHL CertificateCellsfed0e78e01.phiBelowCell3323))) = true

                                                                                                        Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Phi Below Leaf33232_c3_c1_c0_6_00320 #

                                                                                                        source
                                                                                                        theorem GerverSofa.PartE.e24KC2PhiBelowLeaf33232_c3_c1_c0 :
                                                                                                        adaptiveCoverCheck 6 CertificateCells4781918595.phiBelowCell33232310 = true

                                                                                                        Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Phi Below Leaf33232_c3_c1_c1_c0_5_00322 #

                                                                                                        source
                                                                                                        theorem GerverSofa.PartE.e24KC2PhiBelowLeaf33232_c3_c1_c1_c0 :
                                                                                                        adaptiveCoverCheck 5 (childLL CertificateCellsa584418aa1.phiBelowCell33232311) = true

                                                                                                        Gerver Sofa / Kernel Only / Part E / E24KC5Direct_e24KC2Phi Below Leaf33232_c3_c1_c1_c1_5_00323 #

                                                                                                        source
                                                                                                        theorem GerverSofa.PartE.e24KC2PhiBelowLeaf33232_c3_c1_c1_c1 :
                                                                                                        adaptiveCoverCheck 5 (childLH CertificateCells09c85e6b71.phiBelowCell33232311) = true