Documentation

LeanPool.ConwaySoifer.Simplified.Certificates.Steps.Sint1400001500006

Sint 140000 150000 6 #

Kernel-checked forced assignments and closed-interval exclusions.

source
def ConwaySoifer.Simplified.Certificates.Sint140000150000.fan50Owner6Part0 :
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.Sint140000150000.fan51Owner6Part0 :
    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.Sint140000150000.fan55Owner4Part0 :
      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.Sint140000150000.excluded48_0 :
        Certificates.ExcludedOn (model48.B 0 ++ [step48.q]) 9000000000000 (model48.caps 0) (model48.ord 0) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sint140000150000.excluded48_1 :
        Certificates.ExcludedOn (model48.B 1 ++ [step48.q]) 9000000000000 (model48.caps 1) (model48.ord 1) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sint140000150000.excluded48_2 :
        Certificates.ExcludedOn (model48.B 2 ++ [step48.q]) 9000000000000 (model48.caps 2) (model48.ord 2) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sint140000150000.excluded48_3 :
        Certificates.ExcludedOn (model48.B 3 ++ [step48.q]) 9000000000000 (model48.caps 3) (model48.ord 3) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sint140000150000.excluded48_4 :
        Certificates.ExcludedOn (model48.B 4 ++ [step48.q]) 9000000000000 (model48.caps 4) (model48.ord 4) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sint140000150000.excluded48_6 :
        Certificates.ExcludedOn (model48.B 6 ++ [step48.q]) 9000000000000 (model48.caps 6) (model48.ord 6) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sint140000150000.excluded48_7 :
        Certificates.ExcludedOn (model48.B 7 ++ [step48.q]) 9000000000000 (model48.caps 7) (model48.ord 7) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sint140000150000.excluded48_8 :
        Certificates.ExcludedOn (model48.B 8 ++ [step48.q]) 9000000000000 (model48.caps 8) (model48.ord 8) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sint140000150000.excluded48_9 :
        Certificates.ExcludedOn (model48.B 9 ++ [step48.q]) 9000000000000 (model48.caps 9) (model48.ord 9) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sint140000150000.checked48 :
        Certificates.StepValid model48 9000000000000 step48 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sint140000150000.next48 :
        model48.insert step48 = model49
        source
        theorem ConwaySoifer.Simplified.Certificates.Sint140000150000.excluded49_0 :
        Certificates.ExcludedOn (model49.B 0 ++ [step49.q]) 9000000000000 (model49.caps 0) (model49.ord 0) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sint140000150000.excluded49_1 :
        Certificates.ExcludedOn (model49.B 1 ++ [step49.q]) 9000000000000 (model49.caps 1) (model49.ord 1) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sint140000150000.excluded49_2 :
        Certificates.ExcludedOn (model49.B 2 ++ [step49.q]) 9000000000000 (model49.caps 2) (model49.ord 2) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sint140000150000.excluded49_3 :
        Certificates.ExcludedOn (model49.B 3 ++ [step49.q]) 9000000000000 (model49.caps 3) (model49.ord 3) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sint140000150000.excluded49_4 :
        Certificates.ExcludedOn (model49.B 4 ++ [step49.q]) 9000000000000 (model49.caps 4) (model49.ord 4) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sint140000150000.excluded49_5 :
        Certificates.ExcludedOn (model49.B 5 ++ [step49.q]) 9000000000000 (model49.caps 5) (model49.ord 5) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sint140000150000.excluded49_7 :
        Certificates.ExcludedOn (model49.B 7 ++ [step49.q]) 9000000000000 (model49.caps 7) (model49.ord 7) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sint140000150000.excluded49_8 :
        Certificates.ExcludedOn (model49.B 8 ++ [step49.q]) 9000000000000 (model49.caps 8) (model49.ord 8) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sint140000150000.excluded49_9 :
        Certificates.ExcludedOn (model49.B 9 ++ [step49.q]) 9000000000000 (model49.caps 9) (model49.ord 9) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sint140000150000.checked49 :
        Certificates.StepValid model49 9000000000000 step49 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sint140000150000.next49 :
        model49.insert step49 = model50
        source
        theorem ConwaySoifer.Simplified.Certificates.Sint140000150000.excluded50_0 :
        Certificates.ExcludedOn (model50.B 0 ++ [step50.q]) 9000000000000 (model50.caps 0) (model50.ord 0) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sint140000150000.excluded50_1 :
        Certificates.ExcludedOn (model50.B 1 ++ [step50.q]) 9000000000000 (model50.caps 1) (model50.ord 1) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sint140000150000.excluded50_2 :
        Certificates.ExcludedOn (model50.B 2 ++ [step50.q]) 9000000000000 (model50.caps 2) (model50.ord 2) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sint140000150000.excluded50_3 :
        Certificates.ExcludedOn (model50.B 3 ++ [step50.q]) 9000000000000 (model50.caps 3) (model50.ord 3) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sint140000150000.excluded50_4 :
        Certificates.ExcludedOn (model50.B 4 ++ [step50.q]) 9000000000000 (model50.caps 4) (model50.ord 4) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sint140000150000.excluded50_5 :
        Certificates.ExcludedOn (model50.B 5 ++ [step50.q]) 9000000000000 (model50.caps 5) (model50.ord 5) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sint140000150000.excluded50_6 :
        Certificates.ExcludedOn (model50.B 6 ++ [step50.q]) 9000000000000 (model50.caps 6) (model50.ord 6) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sint140000150000.excluded50_7 :
        Certificates.ExcludedOn (model50.B 7 ++ [step50.q]) 9000000000000 (model50.caps 7) (model50.ord 7) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sint140000150000.excluded50_8 :
        Certificates.ExcludedOn (model50.B 8 ++ [step50.q]) 9000000000000 (model50.caps 8) (model50.ord 8) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sint140000150000.checked50 :
        Certificates.StepValid model50 9000000000000 step50 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sint140000150000.next50 :
        model50.insert step50 = model51
        source
        theorem ConwaySoifer.Simplified.Certificates.Sint140000150000.excluded51_0 :
        Certificates.ExcludedOn (model51.B 0 ++ [step51.q]) 9000000000000 (model51.caps 0) (model51.ord 0) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sint140000150000.excluded51_1 :
        Certificates.ExcludedOn (model51.B 1 ++ [step51.q]) 9000000000000 (model51.caps 1) (model51.ord 1) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sint140000150000.excluded51_2 :
        Certificates.ExcludedOn (model51.B 2 ++ [step51.q]) 9000000000000 (model51.caps 2) (model51.ord 2) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sint140000150000.excluded51_3 :
        Certificates.ExcludedOn (model51.B 3 ++ [step51.q]) 9000000000000 (model51.caps 3) (model51.ord 3) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sint140000150000.excluded51_4 :
        Certificates.ExcludedOn (model51.B 4 ++ [step51.q]) 9000000000000 (model51.caps 4) (model51.ord 4) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sint140000150000.excluded51_5 :
        Certificates.ExcludedOn (model51.B 5 ++ [step51.q]) 9000000000000 (model51.caps 5) (model51.ord 5) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sint140000150000.excluded51_6 :
        Certificates.ExcludedOn (model51.B 6 ++ [step51.q]) 9000000000000 (model51.caps 6) (model51.ord 6) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sint140000150000.excluded51_7 :
        Certificates.ExcludedOn (model51.B 7 ++ [step51.q]) 9000000000000 (model51.caps 7) (model51.ord 7) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sint140000150000.excluded51_8 :
        Certificates.ExcludedOn (model51.B 8 ++ [step51.q]) 9000000000000 (model51.caps 8) (model51.ord 8) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sint140000150000.checked51 :
        Certificates.StepValid model51 9000000000000 step51 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sint140000150000.next51 :
        model51.insert step51 = model52
        source
        theorem ConwaySoifer.Simplified.Certificates.Sint140000150000.excluded52_0 :
        Certificates.ExcludedOn (model52.B 0 ++ [step52.q]) 9000000000000 (model52.caps 0) (model52.ord 0) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sint140000150000.excluded52_1 :
        Certificates.ExcludedOn (model52.B 1 ++ [step52.q]) 9000000000000 (model52.caps 1) (model52.ord 1) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sint140000150000.excluded52_2 :
        Certificates.ExcludedOn (model52.B 2 ++ [step52.q]) 9000000000000 (model52.caps 2) (model52.ord 2) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sint140000150000.excluded52_3 :
        Certificates.ExcludedOn (model52.B 3 ++ [step52.q]) 9000000000000 (model52.caps 3) (model52.ord 3) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sint140000150000.excluded52_4 :
        Certificates.ExcludedOn (model52.B 4 ++ [step52.q]) 9000000000000 (model52.caps 4) (model52.ord 4) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sint140000150000.excluded52_5 :
        Certificates.ExcludedOn (model52.B 5 ++ [step52.q]) 9000000000000 (model52.caps 5) (model52.ord 5) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sint140000150000.excluded52_6 :
        Certificates.ExcludedOn (model52.B 6 ++ [step52.q]) 9000000000000 (model52.caps 6) (model52.ord 6) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sint140000150000.excluded52_7 :
        Certificates.ExcludedOn (model52.B 7 ++ [step52.q]) 9000000000000 (model52.caps 7) (model52.ord 7) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sint140000150000.excluded52_9 :
        Certificates.ExcludedOn (model52.B 9 ++ [step52.q]) 9000000000000 (model52.caps 9) (model52.ord 9) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sint140000150000.checked52 :
        Certificates.StepValid model52 9000000000000 step52 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sint140000150000.next52 :
        model52.insert step52 = model53
        source
        theorem ConwaySoifer.Simplified.Certificates.Sint140000150000.excluded53_0 :
        Certificates.ExcludedOn (model53.B 0 ++ [step53.q]) 9000000000000 (model53.caps 0) (model53.ord 0) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sint140000150000.excluded53_1 :
        Certificates.ExcludedOn (model53.B 1 ++ [step53.q]) 9000000000000 (model53.caps 1) (model53.ord 1) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sint140000150000.excluded53_2 :
        Certificates.ExcludedOn (model53.B 2 ++ [step53.q]) 9000000000000 (model53.caps 2) (model53.ord 2) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sint140000150000.excluded53_3 :
        Certificates.ExcludedOn (model53.B 3 ++ [step53.q]) 9000000000000 (model53.caps 3) (model53.ord 3) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sint140000150000.excluded53_5 :
        Certificates.ExcludedOn (model53.B 5 ++ [step53.q]) 9000000000000 (model53.caps 5) (model53.ord 5) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sint140000150000.excluded53_6 :
        Certificates.ExcludedOn (model53.B 6 ++ [step53.q]) 9000000000000 (model53.caps 6) (model53.ord 6) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sint140000150000.excluded53_7 :
        Certificates.ExcludedOn (model53.B 7 ++ [step53.q]) 9000000000000 (model53.caps 7) (model53.ord 7) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sint140000150000.excluded53_8 :
        Certificates.ExcludedOn (model53.B 8 ++ [step53.q]) 9000000000000 (model53.caps 8) (model53.ord 8) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sint140000150000.excluded53_9 :
        Certificates.ExcludedOn (model53.B 9 ++ [step53.q]) 9000000000000 (model53.caps 9) (model53.ord 9) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sint140000150000.checked53 :
        Certificates.StepValid model53 9000000000000 step53 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sint140000150000.next53 :
        model53.insert step53 = model54
        source
        theorem ConwaySoifer.Simplified.Certificates.Sint140000150000.excluded54_0 :
        Certificates.ExcludedOn (model54.B 0 ++ [step54.q]) 9000000000000 (model54.caps 0) (model54.ord 0) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sint140000150000.excluded54_1 :
        Certificates.ExcludedOn (model54.B 1 ++ [step54.q]) 9000000000000 (model54.caps 1) (model54.ord 1) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sint140000150000.excluded54_2 :
        Certificates.ExcludedOn (model54.B 2 ++ [step54.q]) 9000000000000 (model54.caps 2) (model54.ord 2) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sint140000150000.excluded54_3 :
        Certificates.ExcludedOn (model54.B 3 ++ [step54.q]) 9000000000000 (model54.caps 3) (model54.ord 3) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sint140000150000.excluded54_4 :
        Certificates.ExcludedOn (model54.B 4 ++ [step54.q]) 9000000000000 (model54.caps 4) (model54.ord 4) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sint140000150000.excluded54_6 :
        Certificates.ExcludedOn (model54.B 6 ++ [step54.q]) 9000000000000 (model54.caps 6) (model54.ord 6) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sint140000150000.excluded54_7 :
        Certificates.ExcludedOn (model54.B 7 ++ [step54.q]) 9000000000000 (model54.caps 7) (model54.ord 7) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sint140000150000.excluded54_8 :
        Certificates.ExcludedOn (model54.B 8 ++ [step54.q]) 9000000000000 (model54.caps 8) (model54.ord 8) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sint140000150000.excluded54_9 :
        Certificates.ExcludedOn (model54.B 9 ++ [step54.q]) 9000000000000 (model54.caps 9) (model54.ord 9) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sint140000150000.checked54 :
        Certificates.StepValid model54 9000000000000 step54 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sint140000150000.next54 :
        model54.insert step54 = model55
        source
        theorem ConwaySoifer.Simplified.Certificates.Sint140000150000.excluded55_0 :
        Certificates.ExcludedOn (model55.B 0 ++ [step55.q]) 9000000000000 (model55.caps 0) (model55.ord 0) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sint140000150000.excluded55_1 :
        Certificates.ExcludedOn (model55.B 1 ++ [step55.q]) 9000000000000 (model55.caps 1) (model55.ord 1) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sint140000150000.excluded55_2 :
        Certificates.ExcludedOn (model55.B 2 ++ [step55.q]) 9000000000000 (model55.caps 2) (model55.ord 2) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sint140000150000.excluded55_3 :
        Certificates.ExcludedOn (model55.B 3 ++ [step55.q]) 9000000000000 (model55.caps 3) (model55.ord 3) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sint140000150000.excluded55_4 :
        Certificates.ExcludedOn (model55.B 4 ++ [step55.q]) 9000000000000 (model55.caps 4) (model55.ord 4) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sint140000150000.excluded55_6 :
        Certificates.ExcludedOn (model55.B 6 ++ [step55.q]) 9000000000000 (model55.caps 6) (model55.ord 6) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sint140000150000.excluded55_7 :
        Certificates.ExcludedOn (model55.B 7 ++ [step55.q]) 9000000000000 (model55.caps 7) (model55.ord 7) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sint140000150000.excluded55_8 :
        Certificates.ExcludedOn (model55.B 8 ++ [step55.q]) 9000000000000 (model55.caps 8) (model55.ord 8) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sint140000150000.excluded55_9 :
        Certificates.ExcludedOn (model55.B 9 ++ [step55.q]) 9000000000000 (model55.caps 9) (model55.ord 9) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sint140000150000.checked55 :
        Certificates.StepValid model55 9000000000000 step55 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sint140000150000.next55 :
        model55.insert step55 = model56