Documentation

LeanPool.ConwaySoifer.Simplified.Certificates.Steps.Aown2700002800002

Aown 270000 280000 2 #

Kernel-checked forced assignments and closed-interval exclusions.

source
def ConwaySoifer.Simplified.Certificates.Aown270000280000.fan16Owner0Part0 :
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.Aown270000280000.fan16Owner0Part1 :
    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.Aown270000280000.fan16Owner0Part2 :
      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.Aown270000280000.fan17Owner0Part0 :
        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.Aown270000280000.fan17Owner0Part1 :
          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.Aown270000280000.fan17Owner0Part2 :
            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.Aown270000280000.fan18Owner2Part0 :
              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.Aown270000280000.fan20Owner2Part0 :
                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.Aown270000280000.excluded16_0 :
                  Certificates.ExcludedOn (model16.B 0 ++ [step16.q]) 9000000000000 (model16.caps 0) (model16.ord 0) 0 1 100
                  source
                  theorem ConwaySoifer.Simplified.Certificates.Aown270000280000.excluded16_1 :
                  Certificates.ExcludedOn (model16.B 1 ++ [step16.q]) 9000000000000 (model16.caps 1) (model16.ord 1) 0 1 100
                  source
                  theorem ConwaySoifer.Simplified.Certificates.Aown270000280000.excluded16_3 :
                  Certificates.ExcludedOn (model16.B 3 ++ [step16.q]) 9000000000000 (model16.caps 3) (model16.ord 3) 0 1 100
                  source
                  theorem ConwaySoifer.Simplified.Certificates.Aown270000280000.excluded16_4 :
                  Certificates.ExcludedOn (model16.B 4 ++ [step16.q]) 9000000000000 (model16.caps 4) (model16.ord 4) 0 1 100
                  source
                  theorem ConwaySoifer.Simplified.Certificates.Aown270000280000.excluded16_5 :
                  Certificates.ExcludedOn (model16.B 5 ++ [step16.q]) 9000000000000 (model16.caps 5) (model16.ord 5) 0 1 100
                  source
                  theorem ConwaySoifer.Simplified.Certificates.Aown270000280000.excluded16_6 :
                  Certificates.ExcludedOn (model16.B 6 ++ [step16.q]) 9000000000000 (model16.caps 6) (model16.ord 6) 0 1 100
                  source
                  theorem ConwaySoifer.Simplified.Certificates.Aown270000280000.excluded16_7 :
                  Certificates.ExcludedOn (model16.B 7 ++ [step16.q]) 9000000000000 (model16.caps 7) (model16.ord 7) 0 1 100
                  source
                  theorem ConwaySoifer.Simplified.Certificates.Aown270000280000.excluded16_8 :
                  Certificates.ExcludedOn (model16.B 8 ++ [step16.q]) 9000000000000 (model16.caps 8) (model16.ord 8) 0 1 100
                  source
                  theorem ConwaySoifer.Simplified.Certificates.Aown270000280000.excluded16_9 :
                  Certificates.ExcludedOn (model16.B 9 ++ [step16.q]) 9000000000000 (model16.caps 9) (model16.ord 9) 0 1 100
                  source
                  theorem ConwaySoifer.Simplified.Certificates.Aown270000280000.checked16 :
                  Certificates.StepValid model16 9000000000000 step16 0 1 100
                  source
                  theorem ConwaySoifer.Simplified.Certificates.Aown270000280000.next16 :
                  model16.insert step16 = model17
                  source
                  theorem ConwaySoifer.Simplified.Certificates.Aown270000280000.excluded17_0 :
                  Certificates.ExcludedOn (model17.B 0 ++ [step17.q]) 9000000000000 (model17.caps 0) (model17.ord 0) 0 1 100
                  source
                  theorem ConwaySoifer.Simplified.Certificates.Aown270000280000.excluded17_1 :
                  Certificates.ExcludedOn (model17.B 1 ++ [step17.q]) 9000000000000 (model17.caps 1) (model17.ord 1) 0 1 100
                  source
                  theorem ConwaySoifer.Simplified.Certificates.Aown270000280000.excluded17_2 :
                  Certificates.ExcludedOn (model17.B 2 ++ [step17.q]) 9000000000000 (model17.caps 2) (model17.ord 2) 0 1 100
                  source
                  theorem ConwaySoifer.Simplified.Certificates.Aown270000280000.excluded17_3 :
                  Certificates.ExcludedOn (model17.B 3 ++ [step17.q]) 9000000000000 (model17.caps 3) (model17.ord 3) 0 1 100
                  source
                  theorem ConwaySoifer.Simplified.Certificates.Aown270000280000.excluded17_4 :
                  Certificates.ExcludedOn (model17.B 4 ++ [step17.q]) 9000000000000 (model17.caps 4) (model17.ord 4) 0 1 100
                  source
                  theorem ConwaySoifer.Simplified.Certificates.Aown270000280000.excluded17_5 :
                  Certificates.ExcludedOn (model17.B 5 ++ [step17.q]) 9000000000000 (model17.caps 5) (model17.ord 5) 0 1 100
                  source
                  theorem ConwaySoifer.Simplified.Certificates.Aown270000280000.excluded17_7 :
                  Certificates.ExcludedOn (model17.B 7 ++ [step17.q]) 9000000000000 (model17.caps 7) (model17.ord 7) 0 1 100
                  source
                  theorem ConwaySoifer.Simplified.Certificates.Aown270000280000.excluded17_8 :
                  Certificates.ExcludedOn (model17.B 8 ++ [step17.q]) 9000000000000 (model17.caps 8) (model17.ord 8) 0 1 100
                  source
                  theorem ConwaySoifer.Simplified.Certificates.Aown270000280000.excluded17_9 :
                  Certificates.ExcludedOn (model17.B 9 ++ [step17.q]) 9000000000000 (model17.caps 9) (model17.ord 9) 0 1 100
                  source
                  theorem ConwaySoifer.Simplified.Certificates.Aown270000280000.checked17 :
                  Certificates.StepValid model17 9000000000000 step17 0 1 100
                  source
                  theorem ConwaySoifer.Simplified.Certificates.Aown270000280000.next17 :
                  model17.insert step17 = model18
                  source
                  theorem ConwaySoifer.Simplified.Certificates.Aown270000280000.excluded18_1 :
                  Certificates.ExcludedOn (model18.B 1 ++ [step18.q]) 9000000000000 (model18.caps 1) (model18.ord 1) 0 1 100
                  source
                  theorem ConwaySoifer.Simplified.Certificates.Aown270000280000.excluded18_2 :
                  Certificates.ExcludedOn (model18.B 2 ++ [step18.q]) 9000000000000 (model18.caps 2) (model18.ord 2) 0 1 100
                  source
                  theorem ConwaySoifer.Simplified.Certificates.Aown270000280000.excluded18_3 :
                  Certificates.ExcludedOn (model18.B 3 ++ [step18.q]) 9000000000000 (model18.caps 3) (model18.ord 3) 0 1 100
                  source
                  theorem ConwaySoifer.Simplified.Certificates.Aown270000280000.excluded18_4 :
                  Certificates.ExcludedOn (model18.B 4 ++ [step18.q]) 9000000000000 (model18.caps 4) (model18.ord 4) 0 1 100
                  source
                  theorem ConwaySoifer.Simplified.Certificates.Aown270000280000.excluded18_5 :
                  Certificates.ExcludedOn (model18.B 5 ++ [step18.q]) 9000000000000 (model18.caps 5) (model18.ord 5) 0 1 100
                  source
                  theorem ConwaySoifer.Simplified.Certificates.Aown270000280000.excluded18_6 :
                  Certificates.ExcludedOn (model18.B 6 ++ [step18.q]) 9000000000000 (model18.caps 6) (model18.ord 6) 0 1 100
                  source
                  theorem ConwaySoifer.Simplified.Certificates.Aown270000280000.excluded18_7 :
                  Certificates.ExcludedOn (model18.B 7 ++ [step18.q]) 9000000000000 (model18.caps 7) (model18.ord 7) 0 1 100
                  source
                  theorem ConwaySoifer.Simplified.Certificates.Aown270000280000.excluded18_8 :
                  Certificates.ExcludedOn (model18.B 8 ++ [step18.q]) 9000000000000 (model18.caps 8) (model18.ord 8) 0 1 100
                  source
                  theorem ConwaySoifer.Simplified.Certificates.Aown270000280000.excluded18_9 :
                  Certificates.ExcludedOn (model18.B 9 ++ [step18.q]) 9000000000000 (model18.caps 9) (model18.ord 9) 0 1 100
                  source
                  theorem ConwaySoifer.Simplified.Certificates.Aown270000280000.checked18 :
                  Certificates.StepValid model18 9000000000000 step18 0 1 100
                  source
                  theorem ConwaySoifer.Simplified.Certificates.Aown270000280000.next18 :
                  model18.insert step18 = model19
                  source
                  theorem ConwaySoifer.Simplified.Certificates.Aown270000280000.excluded19_1 :
                  Certificates.ExcludedOn (model19.B 1 ++ [step19.q]) 9000000000000 (model19.caps 1) (model19.ord 1) 0 1 100
                  source
                  theorem ConwaySoifer.Simplified.Certificates.Aown270000280000.excluded19_2 :
                  Certificates.ExcludedOn (model19.B 2 ++ [step19.q]) 9000000000000 (model19.caps 2) (model19.ord 2) 0 1 100
                  source
                  theorem ConwaySoifer.Simplified.Certificates.Aown270000280000.excluded19_3 :
                  Certificates.ExcludedOn (model19.B 3 ++ [step19.q]) 9000000000000 (model19.caps 3) (model19.ord 3) 0 1 100
                  source
                  theorem ConwaySoifer.Simplified.Certificates.Aown270000280000.excluded19_4 :
                  Certificates.ExcludedOn (model19.B 4 ++ [step19.q]) 9000000000000 (model19.caps 4) (model19.ord 4) 0 1 100
                  source
                  theorem ConwaySoifer.Simplified.Certificates.Aown270000280000.excluded19_5 :
                  Certificates.ExcludedOn (model19.B 5 ++ [step19.q]) 9000000000000 (model19.caps 5) (model19.ord 5) 0 1 100
                  source
                  theorem ConwaySoifer.Simplified.Certificates.Aown270000280000.excluded19_6 :
                  Certificates.ExcludedOn (model19.B 6 ++ [step19.q]) 9000000000000 (model19.caps 6) (model19.ord 6) 0 1 100
                  source
                  theorem ConwaySoifer.Simplified.Certificates.Aown270000280000.excluded19_7 :
                  Certificates.ExcludedOn (model19.B 7 ++ [step19.q]) 9000000000000 (model19.caps 7) (model19.ord 7) 0 1 100
                  source
                  theorem ConwaySoifer.Simplified.Certificates.Aown270000280000.excluded19_8 :
                  Certificates.ExcludedOn (model19.B 8 ++ [step19.q]) 9000000000000 (model19.caps 8) (model19.ord 8) 0 1 100
                  source
                  theorem ConwaySoifer.Simplified.Certificates.Aown270000280000.excluded19_9 :
                  Certificates.ExcludedOn (model19.B 9 ++ [step19.q]) 9000000000000 (model19.caps 9) (model19.ord 9) 0 1 100
                  source
                  theorem ConwaySoifer.Simplified.Certificates.Aown270000280000.checked19 :
                  Certificates.StepValid model19 9000000000000 step19 0 1 100
                  source
                  theorem ConwaySoifer.Simplified.Certificates.Aown270000280000.next19 :
                  model19.insert step19 = model20
                  source
                  theorem ConwaySoifer.Simplified.Certificates.Aown270000280000.excluded20_1 :
                  Certificates.ExcludedOn (model20.B 1 ++ [step20.q]) 9000000000000 (model20.caps 1) (model20.ord 1) 0 1 100
                  source
                  theorem ConwaySoifer.Simplified.Certificates.Aown270000280000.excluded20_2 :
                  Certificates.ExcludedOn (model20.B 2 ++ [step20.q]) 9000000000000 (model20.caps 2) (model20.ord 2) 0 1 100
                  source
                  theorem ConwaySoifer.Simplified.Certificates.Aown270000280000.excluded20_3 :
                  Certificates.ExcludedOn (model20.B 3 ++ [step20.q]) 9000000000000 (model20.caps 3) (model20.ord 3) 0 1 100
                  source
                  theorem ConwaySoifer.Simplified.Certificates.Aown270000280000.excluded20_4 :
                  Certificates.ExcludedOn (model20.B 4 ++ [step20.q]) 9000000000000 (model20.caps 4) (model20.ord 4) 0 1 100
                  source
                  theorem ConwaySoifer.Simplified.Certificates.Aown270000280000.excluded20_5 :
                  Certificates.ExcludedOn (model20.B 5 ++ [step20.q]) 9000000000000 (model20.caps 5) (model20.ord 5) 0 1 100
                  source
                  theorem ConwaySoifer.Simplified.Certificates.Aown270000280000.excluded20_6 :
                  Certificates.ExcludedOn (model20.B 6 ++ [step20.q]) 9000000000000 (model20.caps 6) (model20.ord 6) 0 1 100
                  source
                  theorem ConwaySoifer.Simplified.Certificates.Aown270000280000.excluded20_7 :
                  Certificates.ExcludedOn (model20.B 7 ++ [step20.q]) 9000000000000 (model20.caps 7) (model20.ord 7) 0 1 100
                  source
                  theorem ConwaySoifer.Simplified.Certificates.Aown270000280000.excluded20_8 :
                  Certificates.ExcludedOn (model20.B 8 ++ [step20.q]) 9000000000000 (model20.caps 8) (model20.ord 8) 0 1 100
                  source
                  theorem ConwaySoifer.Simplified.Certificates.Aown270000280000.excluded20_9 :
                  Certificates.ExcludedOn (model20.B 9 ++ [step20.q]) 9000000000000 (model20.caps 9) (model20.ord 9) 0 1 100
                  source
                  theorem ConwaySoifer.Simplified.Certificates.Aown270000280000.checked20 :
                  Certificates.StepValid model20 9000000000000 step20 0 1 100
                  source
                  theorem ConwaySoifer.Simplified.Certificates.Aown270000280000.next20 :
                  model20.insert step20 = model21