Documentation

LeanPool.ConwaySoifer.Simplified.Certificates.Steps.Aown2300002400003

Aown 230000 240000 3 #

Kernel-checked forced assignments and closed-interval exclusions.

source
def ConwaySoifer.Simplified.Certificates.Aown230000240000.fan24Owner0Part0 :
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.Aown230000240000.fan24Owner0Part1 :
    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.Aown230000240000.fan24Owner0Part2 :
      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.Aown230000240000.fan24Owner0Part3 :
        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.Aown230000240000.fan24Owner0Part4 :
          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.Aown230000240000.fan25Owner2Part0 :
            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.Aown230000240000.fan25Owner2Part1 :
              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.Aown230000240000.fan25Owner2Part2 :
                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.Aown230000240000.excluded24_0 :
                  Certificates.ExcludedOn (model24.B 0 ++ [step24.q]) 9000000000000 (model24.caps 0) (model24.ord 0) 0 1 100
                  source
                  theorem ConwaySoifer.Simplified.Certificates.Aown230000240000.excluded24_1 :
                  Certificates.ExcludedOn (model24.B 1 ++ [step24.q]) 9000000000000 (model24.caps 1) (model24.ord 1) 0 1 100
                  source
                  theorem ConwaySoifer.Simplified.Certificates.Aown230000240000.excluded24_2 :
                  Certificates.ExcludedOn (model24.B 2 ++ [step24.q]) 9000000000000 (model24.caps 2) (model24.ord 2) 0 1 100
                  source
                  theorem ConwaySoifer.Simplified.Certificates.Aown230000240000.excluded24_4 :
                  Certificates.ExcludedOn (model24.B 4 ++ [step24.q]) 9000000000000 (model24.caps 4) (model24.ord 4) 0 1 100
                  source
                  theorem ConwaySoifer.Simplified.Certificates.Aown230000240000.excluded24_5 :
                  Certificates.ExcludedOn (model24.B 5 ++ [step24.q]) 9000000000000 (model24.caps 5) (model24.ord 5) 0 1 100
                  source
                  theorem ConwaySoifer.Simplified.Certificates.Aown230000240000.excluded24_6 :
                  Certificates.ExcludedOn (model24.B 6 ++ [step24.q]) 9000000000000 (model24.caps 6) (model24.ord 6) 0 1 100
                  source
                  theorem ConwaySoifer.Simplified.Certificates.Aown230000240000.excluded24_7 :
                  Certificates.ExcludedOn (model24.B 7 ++ [step24.q]) 9000000000000 (model24.caps 7) (model24.ord 7) 0 1 100
                  source
                  theorem ConwaySoifer.Simplified.Certificates.Aown230000240000.excluded24_8 :
                  Certificates.ExcludedOn (model24.B 8 ++ [step24.q]) 9000000000000 (model24.caps 8) (model24.ord 8) 0 1 100
                  source
                  theorem ConwaySoifer.Simplified.Certificates.Aown230000240000.excluded24_9 :
                  Certificates.ExcludedOn (model24.B 9 ++ [step24.q]) 9000000000000 (model24.caps 9) (model24.ord 9) 0 1 100
                  source
                  theorem ConwaySoifer.Simplified.Certificates.Aown230000240000.checked24 :
                  Certificates.StepValid model24 9000000000000 step24 0 1 100
                  source
                  theorem ConwaySoifer.Simplified.Certificates.Aown230000240000.next24 :
                  model24.insert step24 = model25
                  source
                  theorem ConwaySoifer.Simplified.Certificates.Aown230000240000.excluded25_1 :
                  Certificates.ExcludedOn (model25.B 1 ++ [step25.q]) 9000000000000 (model25.caps 1) (model25.ord 1) 0 1 100
                  source
                  theorem ConwaySoifer.Simplified.Certificates.Aown230000240000.excluded25_2 :
                  Certificates.ExcludedOn (model25.B 2 ++ [step25.q]) 9000000000000 (model25.caps 2) (model25.ord 2) 0 1 100
                  source
                  theorem ConwaySoifer.Simplified.Certificates.Aown230000240000.excluded25_3 :
                  Certificates.ExcludedOn (model25.B 3 ++ [step25.q]) 9000000000000 (model25.caps 3) (model25.ord 3) 0 1 100
                  source
                  theorem ConwaySoifer.Simplified.Certificates.Aown230000240000.excluded25_4 :
                  Certificates.ExcludedOn (model25.B 4 ++ [step25.q]) 9000000000000 (model25.caps 4) (model25.ord 4) 0 1 100
                  source
                  theorem ConwaySoifer.Simplified.Certificates.Aown230000240000.excluded25_5 :
                  Certificates.ExcludedOn (model25.B 5 ++ [step25.q]) 9000000000000 (model25.caps 5) (model25.ord 5) 0 1 100
                  source
                  theorem ConwaySoifer.Simplified.Certificates.Aown230000240000.excluded25_6 :
                  Certificates.ExcludedOn (model25.B 6 ++ [step25.q]) 9000000000000 (model25.caps 6) (model25.ord 6) 0 1 100
                  source
                  theorem ConwaySoifer.Simplified.Certificates.Aown230000240000.excluded25_7 :
                  Certificates.ExcludedOn (model25.B 7 ++ [step25.q]) 9000000000000 (model25.caps 7) (model25.ord 7) 0 1 100
                  source
                  theorem ConwaySoifer.Simplified.Certificates.Aown230000240000.excluded25_8 :
                  Certificates.ExcludedOn (model25.B 8 ++ [step25.q]) 9000000000000 (model25.caps 8) (model25.ord 8) 0 1 100
                  source
                  theorem ConwaySoifer.Simplified.Certificates.Aown230000240000.excluded25_9 :
                  Certificates.ExcludedOn (model25.B 9 ++ [step25.q]) 9000000000000 (model25.caps 9) (model25.ord 9) 0 1 100
                  source
                  theorem ConwaySoifer.Simplified.Certificates.Aown230000240000.checked25 :
                  Certificates.StepValid model25 9000000000000 step25 0 1 100
                  source
                  theorem ConwaySoifer.Simplified.Certificates.Aown230000240000.next25 :
                  model25.insert step25 = model26
                  source
                  theorem ConwaySoifer.Simplified.Certificates.Aown230000240000.excluded26_1 :
                  Certificates.ExcludedOn (model26.B 1 ++ [step26.q]) 9000000000000 (model26.caps 1) (model26.ord 1) 0 1 100
                  source
                  theorem ConwaySoifer.Simplified.Certificates.Aown230000240000.excluded26_2 :
                  Certificates.ExcludedOn (model26.B 2 ++ [step26.q]) 9000000000000 (model26.caps 2) (model26.ord 2) 0 1 100
                  source
                  theorem ConwaySoifer.Simplified.Certificates.Aown230000240000.excluded26_3 :
                  Certificates.ExcludedOn (model26.B 3 ++ [step26.q]) 9000000000000 (model26.caps 3) (model26.ord 3) 0 1 100
                  source
                  theorem ConwaySoifer.Simplified.Certificates.Aown230000240000.excluded26_4 :
                  Certificates.ExcludedOn (model26.B 4 ++ [step26.q]) 9000000000000 (model26.caps 4) (model26.ord 4) 0 1 100
                  source
                  theorem ConwaySoifer.Simplified.Certificates.Aown230000240000.excluded26_5 :
                  Certificates.ExcludedOn (model26.B 5 ++ [step26.q]) 9000000000000 (model26.caps 5) (model26.ord 5) 0 1 100
                  source
                  theorem ConwaySoifer.Simplified.Certificates.Aown230000240000.excluded26_6 :
                  Certificates.ExcludedOn (model26.B 6 ++ [step26.q]) 9000000000000 (model26.caps 6) (model26.ord 6) 0 1 100
                  source
                  theorem ConwaySoifer.Simplified.Certificates.Aown230000240000.excluded26_7 :
                  Certificates.ExcludedOn (model26.B 7 ++ [step26.q]) 9000000000000 (model26.caps 7) (model26.ord 7) 0 1 100
                  source
                  theorem ConwaySoifer.Simplified.Certificates.Aown230000240000.excluded26_8 :
                  Certificates.ExcludedOn (model26.B 8 ++ [step26.q]) 9000000000000 (model26.caps 8) (model26.ord 8) 0 1 100
                  source
                  theorem ConwaySoifer.Simplified.Certificates.Aown230000240000.excluded26_9 :
                  Certificates.ExcludedOn (model26.B 9 ++ [step26.q]) 9000000000000 (model26.caps 9) (model26.ord 9) 0 1 100
                  source
                  theorem ConwaySoifer.Simplified.Certificates.Aown230000240000.checked26 :
                  Certificates.StepValid model26 9000000000000 step26 0 1 100
                  source
                  theorem ConwaySoifer.Simplified.Certificates.Aown230000240000.next26 :
                  model26.insert step26 = model27
                  source
                  theorem ConwaySoifer.Simplified.Certificates.Aown230000240000.excluded27_1 :
                  Certificates.ExcludedOn (model27.B 1 ++ [step27.q]) 9000000000000 (model27.caps 1) (model27.ord 1) 0 1 100
                  source
                  theorem ConwaySoifer.Simplified.Certificates.Aown230000240000.excluded27_2 :
                  Certificates.ExcludedOn (model27.B 2 ++ [step27.q]) 9000000000000 (model27.caps 2) (model27.ord 2) 0 1 100
                  source
                  theorem ConwaySoifer.Simplified.Certificates.Aown230000240000.excluded27_3 :
                  Certificates.ExcludedOn (model27.B 3 ++ [step27.q]) 9000000000000 (model27.caps 3) (model27.ord 3) 0 1 100
                  source
                  theorem ConwaySoifer.Simplified.Certificates.Aown230000240000.excluded27_4 :
                  Certificates.ExcludedOn (model27.B 4 ++ [step27.q]) 9000000000000 (model27.caps 4) (model27.ord 4) 0 1 100
                  source
                  theorem ConwaySoifer.Simplified.Certificates.Aown230000240000.excluded27_5 :
                  Certificates.ExcludedOn (model27.B 5 ++ [step27.q]) 9000000000000 (model27.caps 5) (model27.ord 5) 0 1 100
                  source
                  theorem ConwaySoifer.Simplified.Certificates.Aown230000240000.excluded27_6 :
                  Certificates.ExcludedOn (model27.B 6 ++ [step27.q]) 9000000000000 (model27.caps 6) (model27.ord 6) 0 1 100
                  source
                  theorem ConwaySoifer.Simplified.Certificates.Aown230000240000.excluded27_7 :
                  Certificates.ExcludedOn (model27.B 7 ++ [step27.q]) 9000000000000 (model27.caps 7) (model27.ord 7) 0 1 100
                  source
                  theorem ConwaySoifer.Simplified.Certificates.Aown230000240000.excluded27_8 :
                  Certificates.ExcludedOn (model27.B 8 ++ [step27.q]) 9000000000000 (model27.caps 8) (model27.ord 8) 0 1 100
                  source
                  theorem ConwaySoifer.Simplified.Certificates.Aown230000240000.excluded27_9 :
                  Certificates.ExcludedOn (model27.B 9 ++ [step27.q]) 9000000000000 (model27.caps 9) (model27.ord 9) 0 1 100
                  source
                  theorem ConwaySoifer.Simplified.Certificates.Aown230000240000.checked27 :
                  Certificates.StepValid model27 9000000000000 step27 0 1 100
                  source
                  theorem ConwaySoifer.Simplified.Certificates.Aown230000240000.next27 :
                  model27.insert step27 = model28