Documentation

LeanPool.ConwaySoifer.Simplified.Certificates.Steps.Sint2000002100005

Sint 200000 210000 5 #

Kernel-checked forced assignments and closed-interval exclusions.

source
def ConwaySoifer.Simplified.Certificates.Sint200000210000.fan41Owner5Part0 :
Certificates.FanWitness

Shared exact orientation-fan tail for this local exclusion.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def ConwaySoifer.Simplified.Certificates.Sint200000210000.fan42Owner0Part0 :
    Certificates.FanWitness

    Shared exact orientation-fan tail for this local exclusion.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def ConwaySoifer.Simplified.Certificates.Sint200000210000.fan42Owner0Part1 :
      Certificates.FanWitness

      Shared exact orientation-fan tail for this local exclusion.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def ConwaySoifer.Simplified.Certificates.Sint200000210000.fan42Owner0Part2 :
        Certificates.FanWitness

        Shared exact orientation-fan tail for this local exclusion.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def ConwaySoifer.Simplified.Certificates.Sint200000210000.fan42Owner5Part0 :
          Certificates.FanWitness

          Shared exact orientation-fan tail for this local exclusion.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            def ConwaySoifer.Simplified.Certificates.Sint200000210000.fan43Owner0Part0 :
            Certificates.FanWitness

            Shared exact orientation-fan tail for this local exclusion.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              def ConwaySoifer.Simplified.Certificates.Sint200000210000.fan43Owner0Part1 :
              Certificates.FanWitness

              Shared exact orientation-fan tail for this local exclusion.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                def ConwaySoifer.Simplified.Certificates.Sint200000210000.fan43Owner0Part2 :
                Certificates.FanWitness

                Shared exact orientation-fan tail for this local exclusion.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  def ConwaySoifer.Simplified.Certificates.Sint200000210000.fan46Owner0Part0 :
                  Certificates.FanWitness

                  Shared exact orientation-fan tail for this local exclusion.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    source
                    def ConwaySoifer.Simplified.Certificates.Sint200000210000.fan46Owner0Part1 :
                    Certificates.FanWitness

                    Shared exact orientation-fan tail for this local exclusion.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      source
                      def ConwaySoifer.Simplified.Certificates.Sint200000210000.fan46Owner0Part2 :
                      Certificates.FanWitness

                      Shared exact orientation-fan tail for this local exclusion.

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        source
                        theorem ConwaySoifer.Simplified.Certificates.Sint200000210000.excluded40_0 :
                        Certificates.ExcludedOn (model40.B 0 ++ [step40.q]) 9000000000000 (model40.caps 0) (model40.ord 0) 0 1 100
                        source
                        theorem ConwaySoifer.Simplified.Certificates.Sint200000210000.excluded40_1 :
                        Certificates.ExcludedOn (model40.B 1 ++ [step40.q]) 9000000000000 (model40.caps 1) (model40.ord 1) 0 1 100
                        source
                        theorem ConwaySoifer.Simplified.Certificates.Sint200000210000.excluded40_2 :
                        Certificates.ExcludedOn (model40.B 2 ++ [step40.q]) 9000000000000 (model40.caps 2) (model40.ord 2) 0 1 100
                        source
                        theorem ConwaySoifer.Simplified.Certificates.Sint200000210000.excluded40_3 :
                        Certificates.ExcludedOn (model40.B 3 ++ [step40.q]) 9000000000000 (model40.caps 3) (model40.ord 3) 0 1 100
                        source
                        theorem ConwaySoifer.Simplified.Certificates.Sint200000210000.excluded40_4 :
                        Certificates.ExcludedOn (model40.B 4 ++ [step40.q]) 9000000000000 (model40.caps 4) (model40.ord 4) 0 1 100
                        source
                        theorem ConwaySoifer.Simplified.Certificates.Sint200000210000.excluded40_6 :
                        Certificates.ExcludedOn (model40.B 6 ++ [step40.q]) 9000000000000 (model40.caps 6) (model40.ord 6) 0 1 100
                        source
                        theorem ConwaySoifer.Simplified.Certificates.Sint200000210000.excluded40_7 :
                        Certificates.ExcludedOn (model40.B 7 ++ [step40.q]) 9000000000000 (model40.caps 7) (model40.ord 7) 0 1 100
                        source
                        theorem ConwaySoifer.Simplified.Certificates.Sint200000210000.excluded40_8 :
                        Certificates.ExcludedOn (model40.B 8 ++ [step40.q]) 9000000000000 (model40.caps 8) (model40.ord 8) 0 1 100
                        source
                        theorem ConwaySoifer.Simplified.Certificates.Sint200000210000.excluded40_9 :
                        Certificates.ExcludedOn (model40.B 9 ++ [step40.q]) 9000000000000 (model40.caps 9) (model40.ord 9) 0 1 100
                        source
                        theorem ConwaySoifer.Simplified.Certificates.Sint200000210000.checked40 :
                        Certificates.StepValid model40 9000000000000 step40 0 1 100
                        source
                        theorem ConwaySoifer.Simplified.Certificates.Sint200000210000.next40 :
                        model40.insert step40 = model41
                        source
                        theorem ConwaySoifer.Simplified.Certificates.Sint200000210000.excluded41_0 :
                        Certificates.ExcludedOn (model41.B 0 ++ [step41.q]) 9000000000000 (model41.caps 0) (model41.ord 0) 0 1 100
                        source
                        theorem ConwaySoifer.Simplified.Certificates.Sint200000210000.excluded41_1 :
                        Certificates.ExcludedOn (model41.B 1 ++ [step41.q]) 9000000000000 (model41.caps 1) (model41.ord 1) 0 1 100
                        source
                        theorem ConwaySoifer.Simplified.Certificates.Sint200000210000.excluded41_2 :
                        Certificates.ExcludedOn (model41.B 2 ++ [step41.q]) 9000000000000 (model41.caps 2) (model41.ord 2) 0 1 100
                        source
                        theorem ConwaySoifer.Simplified.Certificates.Sint200000210000.excluded41_3 :
                        Certificates.ExcludedOn (model41.B 3 ++ [step41.q]) 9000000000000 (model41.caps 3) (model41.ord 3) 0 1 100
                        source
                        theorem ConwaySoifer.Simplified.Certificates.Sint200000210000.excluded41_5 :
                        Certificates.ExcludedOn (model41.B 5 ++ [step41.q]) 9000000000000 (model41.caps 5) (model41.ord 5) 0 1 100
                        source
                        theorem ConwaySoifer.Simplified.Certificates.Sint200000210000.excluded41_6 :
                        Certificates.ExcludedOn (model41.B 6 ++ [step41.q]) 9000000000000 (model41.caps 6) (model41.ord 6) 0 1 100
                        source
                        theorem ConwaySoifer.Simplified.Certificates.Sint200000210000.excluded41_7 :
                        Certificates.ExcludedOn (model41.B 7 ++ [step41.q]) 9000000000000 (model41.caps 7) (model41.ord 7) 0 1 100
                        source
                        theorem ConwaySoifer.Simplified.Certificates.Sint200000210000.excluded41_8 :
                        Certificates.ExcludedOn (model41.B 8 ++ [step41.q]) 9000000000000 (model41.caps 8) (model41.ord 8) 0 1 100
                        source
                        theorem ConwaySoifer.Simplified.Certificates.Sint200000210000.excluded41_9 :
                        Certificates.ExcludedOn (model41.B 9 ++ [step41.q]) 9000000000000 (model41.caps 9) (model41.ord 9) 0 1 100
                        source
                        theorem ConwaySoifer.Simplified.Certificates.Sint200000210000.checked41 :
                        Certificates.StepValid model41 9000000000000 step41 0 1 100
                        source
                        theorem ConwaySoifer.Simplified.Certificates.Sint200000210000.next41 :
                        model41.insert step41 = model42
                        source
                        theorem ConwaySoifer.Simplified.Certificates.Sint200000210000.excluded42_0 :
                        Certificates.ExcludedOn (model42.B 0 ++ [step42.q]) 9000000000000 (model42.caps 0) (model42.ord 0) 0 1 100
                        source
                        theorem ConwaySoifer.Simplified.Certificates.Sint200000210000.excluded42_1 :
                        Certificates.ExcludedOn (model42.B 1 ++ [step42.q]) 9000000000000 (model42.caps 1) (model42.ord 1) 0 1 100
                        source
                        theorem ConwaySoifer.Simplified.Certificates.Sint200000210000.excluded42_2 :
                        Certificates.ExcludedOn (model42.B 2 ++ [step42.q]) 9000000000000 (model42.caps 2) (model42.ord 2) 0 1 100
                        source
                        theorem ConwaySoifer.Simplified.Certificates.Sint200000210000.excluded42_3 :
                        Certificates.ExcludedOn (model42.B 3 ++ [step42.q]) 9000000000000 (model42.caps 3) (model42.ord 3) 0 1 100
                        source
                        theorem ConwaySoifer.Simplified.Certificates.Sint200000210000.excluded42_5 :
                        Certificates.ExcludedOn (model42.B 5 ++ [step42.q]) 9000000000000 (model42.caps 5) (model42.ord 5) 0 1 100
                        source
                        theorem ConwaySoifer.Simplified.Certificates.Sint200000210000.excluded42_6 :
                        Certificates.ExcludedOn (model42.B 6 ++ [step42.q]) 9000000000000 (model42.caps 6) (model42.ord 6) 0 1 100
                        source
                        theorem ConwaySoifer.Simplified.Certificates.Sint200000210000.excluded42_7 :
                        Certificates.ExcludedOn (model42.B 7 ++ [step42.q]) 9000000000000 (model42.caps 7) (model42.ord 7) 0 1 100
                        source
                        theorem ConwaySoifer.Simplified.Certificates.Sint200000210000.excluded42_8 :
                        Certificates.ExcludedOn (model42.B 8 ++ [step42.q]) 9000000000000 (model42.caps 8) (model42.ord 8) 0 1 100
                        source
                        theorem ConwaySoifer.Simplified.Certificates.Sint200000210000.excluded42_9 :
                        Certificates.ExcludedOn (model42.B 9 ++ [step42.q]) 9000000000000 (model42.caps 9) (model42.ord 9) 0 1 100
                        source
                        theorem ConwaySoifer.Simplified.Certificates.Sint200000210000.checked42 :
                        Certificates.StepValid model42 9000000000000 step42 0 1 100
                        source
                        theorem ConwaySoifer.Simplified.Certificates.Sint200000210000.next42 :
                        model42.insert step42 = model43
                        source
                        theorem ConwaySoifer.Simplified.Certificates.Sint200000210000.excluded43_0 :
                        Certificates.ExcludedOn (model43.B 0 ++ [step43.q]) 9000000000000 (model43.caps 0) (model43.ord 0) 0 1 100
                        source
                        theorem ConwaySoifer.Simplified.Certificates.Sint200000210000.excluded43_1 :
                        Certificates.ExcludedOn (model43.B 1 ++ [step43.q]) 9000000000000 (model43.caps 1) (model43.ord 1) 0 1 100
                        source
                        theorem ConwaySoifer.Simplified.Certificates.Sint200000210000.excluded43_2 :
                        Certificates.ExcludedOn (model43.B 2 ++ [step43.q]) 9000000000000 (model43.caps 2) (model43.ord 2) 0 1 100
                        source
                        theorem ConwaySoifer.Simplified.Certificates.Sint200000210000.excluded43_4 :
                        Certificates.ExcludedOn (model43.B 4 ++ [step43.q]) 9000000000000 (model43.caps 4) (model43.ord 4) 0 1 100
                        source
                        theorem ConwaySoifer.Simplified.Certificates.Sint200000210000.excluded43_5 :
                        Certificates.ExcludedOn (model43.B 5 ++ [step43.q]) 9000000000000 (model43.caps 5) (model43.ord 5) 0 1 100
                        source
                        theorem ConwaySoifer.Simplified.Certificates.Sint200000210000.excluded43_6 :
                        Certificates.ExcludedOn (model43.B 6 ++ [step43.q]) 9000000000000 (model43.caps 6) (model43.ord 6) 0 1 100
                        source
                        theorem ConwaySoifer.Simplified.Certificates.Sint200000210000.excluded43_7 :
                        Certificates.ExcludedOn (model43.B 7 ++ [step43.q]) 9000000000000 (model43.caps 7) (model43.ord 7) 0 1 100
                        source
                        theorem ConwaySoifer.Simplified.Certificates.Sint200000210000.excluded43_8 :
                        Certificates.ExcludedOn (model43.B 8 ++ [step43.q]) 9000000000000 (model43.caps 8) (model43.ord 8) 0 1 100
                        source
                        theorem ConwaySoifer.Simplified.Certificates.Sint200000210000.excluded43_9 :
                        Certificates.ExcludedOn (model43.B 9 ++ [step43.q]) 9000000000000 (model43.caps 9) (model43.ord 9) 0 1 100
                        source
                        theorem ConwaySoifer.Simplified.Certificates.Sint200000210000.checked43 :
                        Certificates.StepValid model43 9000000000000 step43 0 1 100
                        source
                        theorem ConwaySoifer.Simplified.Certificates.Sint200000210000.next43 :
                        model43.insert step43 = model44
                        source
                        theorem ConwaySoifer.Simplified.Certificates.Sint200000210000.excluded44_1 :
                        Certificates.ExcludedOn (model44.B 1 ++ [step44.q]) 9000000000000 (model44.caps 1) (model44.ord 1) 0 1 100
                        source
                        theorem ConwaySoifer.Simplified.Certificates.Sint200000210000.excluded44_2 :
                        Certificates.ExcludedOn (model44.B 2 ++ [step44.q]) 9000000000000 (model44.caps 2) (model44.ord 2) 0 1 100
                        source
                        theorem ConwaySoifer.Simplified.Certificates.Sint200000210000.excluded44_3 :
                        Certificates.ExcludedOn (model44.B 3 ++ [step44.q]) 9000000000000 (model44.caps 3) (model44.ord 3) 0 1 100
                        source
                        theorem ConwaySoifer.Simplified.Certificates.Sint200000210000.excluded44_4 :
                        Certificates.ExcludedOn (model44.B 4 ++ [step44.q]) 9000000000000 (model44.caps 4) (model44.ord 4) 0 1 100
                        source
                        theorem ConwaySoifer.Simplified.Certificates.Sint200000210000.excluded44_5 :
                        Certificates.ExcludedOn (model44.B 5 ++ [step44.q]) 9000000000000 (model44.caps 5) (model44.ord 5) 0 1 100
                        source
                        theorem ConwaySoifer.Simplified.Certificates.Sint200000210000.excluded44_6 :
                        Certificates.ExcludedOn (model44.B 6 ++ [step44.q]) 9000000000000 (model44.caps 6) (model44.ord 6) 0 1 100
                        source
                        theorem ConwaySoifer.Simplified.Certificates.Sint200000210000.excluded44_7 :
                        Certificates.ExcludedOn (model44.B 7 ++ [step44.q]) 9000000000000 (model44.caps 7) (model44.ord 7) 0 1 100
                        source
                        theorem ConwaySoifer.Simplified.Certificates.Sint200000210000.excluded44_8 :
                        Certificates.ExcludedOn (model44.B 8 ++ [step44.q]) 9000000000000 (model44.caps 8) (model44.ord 8) 0 1 100
                        source
                        theorem ConwaySoifer.Simplified.Certificates.Sint200000210000.excluded44_9 :
                        Certificates.ExcludedOn (model44.B 9 ++ [step44.q]) 9000000000000 (model44.caps 9) (model44.ord 9) 0 1 100
                        source
                        theorem ConwaySoifer.Simplified.Certificates.Sint200000210000.checked44 :
                        Certificates.StepValid model44 9000000000000 step44 0 1 100
                        source
                        theorem ConwaySoifer.Simplified.Certificates.Sint200000210000.next44 :
                        model44.insert step44 = model45
                        source
                        theorem ConwaySoifer.Simplified.Certificates.Sint200000210000.excluded45_1 :
                        Certificates.ExcludedOn (model45.B 1 ++ [step45.q]) 9000000000000 (model45.caps 1) (model45.ord 1) 0 1 100
                        source
                        theorem ConwaySoifer.Simplified.Certificates.Sint200000210000.excluded45_2 :
                        Certificates.ExcludedOn (model45.B 2 ++ [step45.q]) 9000000000000 (model45.caps 2) (model45.ord 2) 0 1 100
                        source
                        theorem ConwaySoifer.Simplified.Certificates.Sint200000210000.excluded45_3 :
                        Certificates.ExcludedOn (model45.B 3 ++ [step45.q]) 9000000000000 (model45.caps 3) (model45.ord 3) 0 1 100
                        source
                        theorem ConwaySoifer.Simplified.Certificates.Sint200000210000.excluded45_4 :
                        Certificates.ExcludedOn (model45.B 4 ++ [step45.q]) 9000000000000 (model45.caps 4) (model45.ord 4) 0 1 100
                        source
                        theorem ConwaySoifer.Simplified.Certificates.Sint200000210000.excluded45_5 :
                        Certificates.ExcludedOn (model45.B 5 ++ [step45.q]) 9000000000000 (model45.caps 5) (model45.ord 5) 0 1 100
                        source
                        theorem ConwaySoifer.Simplified.Certificates.Sint200000210000.excluded45_6 :
                        Certificates.ExcludedOn (model45.B 6 ++ [step45.q]) 9000000000000 (model45.caps 6) (model45.ord 6) 0 1 100
                        source
                        theorem ConwaySoifer.Simplified.Certificates.Sint200000210000.excluded45_7 :
                        Certificates.ExcludedOn (model45.B 7 ++ [step45.q]) 9000000000000 (model45.caps 7) (model45.ord 7) 0 1 100
                        source
                        theorem ConwaySoifer.Simplified.Certificates.Sint200000210000.excluded45_8 :
                        Certificates.ExcludedOn (model45.B 8 ++ [step45.q]) 9000000000000 (model45.caps 8) (model45.ord 8) 0 1 100
                        source
                        theorem ConwaySoifer.Simplified.Certificates.Sint200000210000.excluded45_9 :
                        Certificates.ExcludedOn (model45.B 9 ++ [step45.q]) 9000000000000 (model45.caps 9) (model45.ord 9) 0 1 100
                        source
                        theorem ConwaySoifer.Simplified.Certificates.Sint200000210000.checked45 :
                        Certificates.StepValid model45 9000000000000 step45 0 1 100
                        source
                        theorem ConwaySoifer.Simplified.Certificates.Sint200000210000.next45 :
                        model45.insert step45 = model46
                        source
                        theorem ConwaySoifer.Simplified.Certificates.Sint200000210000.excluded46_0 :
                        Certificates.ExcludedOn (model46.B 0 ++ [step46.q]) 9000000000000 (model46.caps 0) (model46.ord 0) 0 1 100
                        source
                        theorem ConwaySoifer.Simplified.Certificates.Sint200000210000.excluded46_2 :
                        Certificates.ExcludedOn (model46.B 2 ++ [step46.q]) 9000000000000 (model46.caps 2) (model46.ord 2) 0 1 100
                        source
                        theorem ConwaySoifer.Simplified.Certificates.Sint200000210000.excluded46_3 :
                        Certificates.ExcludedOn (model46.B 3 ++ [step46.q]) 9000000000000 (model46.caps 3) (model46.ord 3) 0 1 100
                        source
                        theorem ConwaySoifer.Simplified.Certificates.Sint200000210000.excluded46_4 :
                        Certificates.ExcludedOn (model46.B 4 ++ [step46.q]) 9000000000000 (model46.caps 4) (model46.ord 4) 0 1 100
                        source
                        theorem ConwaySoifer.Simplified.Certificates.Sint200000210000.excluded46_5 :
                        Certificates.ExcludedOn (model46.B 5 ++ [step46.q]) 9000000000000 (model46.caps 5) (model46.ord 5) 0 1 100
                        source
                        theorem ConwaySoifer.Simplified.Certificates.Sint200000210000.excluded46_6 :
                        Certificates.ExcludedOn (model46.B 6 ++ [step46.q]) 9000000000000 (model46.caps 6) (model46.ord 6) 0 1 100
                        source
                        theorem ConwaySoifer.Simplified.Certificates.Sint200000210000.excluded46_7 :
                        Certificates.ExcludedOn (model46.B 7 ++ [step46.q]) 9000000000000 (model46.caps 7) (model46.ord 7) 0 1 100
                        source
                        theorem ConwaySoifer.Simplified.Certificates.Sint200000210000.excluded46_8 :
                        Certificates.ExcludedOn (model46.B 8 ++ [step46.q]) 9000000000000 (model46.caps 8) (model46.ord 8) 0 1 100
                        source
                        theorem ConwaySoifer.Simplified.Certificates.Sint200000210000.excluded46_9 :
                        Certificates.ExcludedOn (model46.B 9 ++ [step46.q]) 9000000000000 (model46.caps 9) (model46.ord 9) 0 1 100
                        source
                        theorem ConwaySoifer.Simplified.Certificates.Sint200000210000.checked46 :
                        Certificates.StepValid model46 9000000000000 step46 0 1 100
                        source
                        theorem ConwaySoifer.Simplified.Certificates.Sint200000210000.next46 :
                        model46.insert step46 = model47
                        source
                        theorem ConwaySoifer.Simplified.Certificates.Sint200000210000.excluded47_0 :
                        Certificates.ExcludedOn (model47.B 0 ++ [step47.q]) 9000000000000 (model47.caps 0) (model47.ord 0) 0 1 100
                        source
                        theorem ConwaySoifer.Simplified.Certificates.Sint200000210000.excluded47_1 :
                        Certificates.ExcludedOn (model47.B 1 ++ [step47.q]) 9000000000000 (model47.caps 1) (model47.ord 1) 0 1 100
                        source
                        theorem ConwaySoifer.Simplified.Certificates.Sint200000210000.excluded47_2 :
                        Certificates.ExcludedOn (model47.B 2 ++ [step47.q]) 9000000000000 (model47.caps 2) (model47.ord 2) 0 1 100
                        source
                        theorem ConwaySoifer.Simplified.Certificates.Sint200000210000.excluded47_3 :
                        Certificates.ExcludedOn (model47.B 3 ++ [step47.q]) 9000000000000 (model47.caps 3) (model47.ord 3) 0 1 100
                        source
                        theorem ConwaySoifer.Simplified.Certificates.Sint200000210000.excluded47_4 :
                        Certificates.ExcludedOn (model47.B 4 ++ [step47.q]) 9000000000000 (model47.caps 4) (model47.ord 4) 0 1 100
                        source
                        theorem ConwaySoifer.Simplified.Certificates.Sint200000210000.excluded47_5 :
                        Certificates.ExcludedOn (model47.B 5 ++ [step47.q]) 9000000000000 (model47.caps 5) (model47.ord 5) 0 1 100
                        source
                        theorem ConwaySoifer.Simplified.Certificates.Sint200000210000.excluded47_6 :
                        Certificates.ExcludedOn (model47.B 6 ++ [step47.q]) 9000000000000 (model47.caps 6) (model47.ord 6) 0 1 100
                        source
                        theorem ConwaySoifer.Simplified.Certificates.Sint200000210000.excluded47_7 :
                        Certificates.ExcludedOn (model47.B 7 ++ [step47.q]) 9000000000000 (model47.caps 7) (model47.ord 7) 0 1 100
                        source
                        theorem ConwaySoifer.Simplified.Certificates.Sint200000210000.excluded47_9 :
                        Certificates.ExcludedOn (model47.B 9 ++ [step47.q]) 9000000000000 (model47.caps 9) (model47.ord 9) 0 1 100
                        source
                        theorem ConwaySoifer.Simplified.Certificates.Sint200000210000.checked47 :
                        Certificates.StepValid model47 9000000000000 step47 0 1 100
                        source
                        theorem ConwaySoifer.Simplified.Certificates.Sint200000210000.next47 :
                        model47.insert step47 = model48