Documentation

LeanPool.ConwaySoifer.Simplified.Certificates.Steps.Aown1900002000003

Aown 190000 200000 3 #

Kernel-checked forced assignments and closed-interval exclusions.

source
def ConwaySoifer.Simplified.Certificates.Aown190000200000.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.Aown190000200000.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.Aown190000200000.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.Aown190000200000.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.Aown190000200000.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
            theorem ConwaySoifer.Simplified.Certificates.Aown190000200000.excluded24_0 :
            Certificates.ExcludedOn (model24.B 0 ++ [step24.q]) 9000000000000 (model24.caps 0) (model24.ord 0) 0 1 100
            source
            theorem ConwaySoifer.Simplified.Certificates.Aown190000200000.excluded24_1 :
            Certificates.ExcludedOn (model24.B 1 ++ [step24.q]) 9000000000000 (model24.caps 1) (model24.ord 1) 0 1 100
            source
            theorem ConwaySoifer.Simplified.Certificates.Aown190000200000.excluded24_2 :
            Certificates.ExcludedOn (model24.B 2 ++ [step24.q]) 9000000000000 (model24.caps 2) (model24.ord 2) 0 1 100
            source
            theorem ConwaySoifer.Simplified.Certificates.Aown190000200000.excluded24_3 :
            Certificates.ExcludedOn (model24.B 3 ++ [step24.q]) 9000000000000 (model24.caps 3) (model24.ord 3) 0 1 100
            source
            theorem ConwaySoifer.Simplified.Certificates.Aown190000200000.excluded24_5 :
            Certificates.ExcludedOn (model24.B 5 ++ [step24.q]) 9000000000000 (model24.caps 5) (model24.ord 5) 0 1 100
            source
            theorem ConwaySoifer.Simplified.Certificates.Aown190000200000.excluded24_6 :
            Certificates.ExcludedOn (model24.B 6 ++ [step24.q]) 9000000000000 (model24.caps 6) (model24.ord 6) 0 1 100
            source
            theorem ConwaySoifer.Simplified.Certificates.Aown190000200000.excluded24_7 :
            Certificates.ExcludedOn (model24.B 7 ++ [step24.q]) 9000000000000 (model24.caps 7) (model24.ord 7) 0 1 100
            source
            theorem ConwaySoifer.Simplified.Certificates.Aown190000200000.excluded24_8 :
            Certificates.ExcludedOn (model24.B 8 ++ [step24.q]) 9000000000000 (model24.caps 8) (model24.ord 8) 0 1 100
            source
            theorem ConwaySoifer.Simplified.Certificates.Aown190000200000.excluded24_9 :
            Certificates.ExcludedOn (model24.B 9 ++ [step24.q]) 9000000000000 (model24.caps 9) (model24.ord 9) 0 1 100
            source
            theorem ConwaySoifer.Simplified.Certificates.Aown190000200000.checked24 :
            Certificates.StepValid model24 9000000000000 step24 0 1 100
            source
            theorem ConwaySoifer.Simplified.Certificates.Aown190000200000.next24 :
            model24.insert step24 = model25
            source
            theorem ConwaySoifer.Simplified.Certificates.Aown190000200000.excluded25_1 :
            Certificates.ExcludedOn (model25.B 1 ++ [step25.q]) 9000000000000 (model25.caps 1) (model25.ord 1) 0 1 100
            source
            theorem ConwaySoifer.Simplified.Certificates.Aown190000200000.excluded25_2 :
            Certificates.ExcludedOn (model25.B 2 ++ [step25.q]) 9000000000000 (model25.caps 2) (model25.ord 2) 0 1 100
            source
            theorem ConwaySoifer.Simplified.Certificates.Aown190000200000.excluded25_3 :
            Certificates.ExcludedOn (model25.B 3 ++ [step25.q]) 9000000000000 (model25.caps 3) (model25.ord 3) 0 1 100
            source
            theorem ConwaySoifer.Simplified.Certificates.Aown190000200000.excluded25_4 :
            Certificates.ExcludedOn (model25.B 4 ++ [step25.q]) 9000000000000 (model25.caps 4) (model25.ord 4) 0 1 100
            source
            theorem ConwaySoifer.Simplified.Certificates.Aown190000200000.excluded25_5 :
            Certificates.ExcludedOn (model25.B 5 ++ [step25.q]) 9000000000000 (model25.caps 5) (model25.ord 5) 0 1 100
            source
            theorem ConwaySoifer.Simplified.Certificates.Aown190000200000.excluded25_6 :
            Certificates.ExcludedOn (model25.B 6 ++ [step25.q]) 9000000000000 (model25.caps 6) (model25.ord 6) 0 1 100
            source
            theorem ConwaySoifer.Simplified.Certificates.Aown190000200000.excluded25_7 :
            Certificates.ExcludedOn (model25.B 7 ++ [step25.q]) 9000000000000 (model25.caps 7) (model25.ord 7) 0 1 100
            source
            theorem ConwaySoifer.Simplified.Certificates.Aown190000200000.excluded25_8 :
            Certificates.ExcludedOn (model25.B 8 ++ [step25.q]) 9000000000000 (model25.caps 8) (model25.ord 8) 0 1 100
            source
            theorem ConwaySoifer.Simplified.Certificates.Aown190000200000.excluded25_9 :
            Certificates.ExcludedOn (model25.B 9 ++ [step25.q]) 9000000000000 (model25.caps 9) (model25.ord 9) 0 1 100
            source
            theorem ConwaySoifer.Simplified.Certificates.Aown190000200000.checked25 :
            Certificates.StepValid model25 9000000000000 step25 0 1 100
            source
            theorem ConwaySoifer.Simplified.Certificates.Aown190000200000.next25 :
            model25.insert step25 = model26