Documentation

LeanPool.ConwaySoifer.Simplified.Certificates.Steps.Sext1500001600007

Sext 150000 160000 7 #

Kernel-checked forced assignments and closed-interval exclusions.

source
def ConwaySoifer.Simplified.Certificates.Sext150000160000.fan56Owner3Part0 :
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.Sext150000160000.fan56Owner3Part1 :
    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.Sext150000160000.fan57Owner3Part0 :
      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.Sext150000160000.excluded56_0 :
        Certificates.ExcludedOn (model56.B 0 ++ [step56.q]) 9000000000000 (model56.caps 0) (model56.ord 0) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sext150000160000.excluded56_1 :
        Certificates.ExcludedOn (model56.B 1 ++ [step56.q]) 9000000000000 (model56.caps 1) (model56.ord 1) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sext150000160000.excluded56_2 :
        Certificates.ExcludedOn (model56.B 2 ++ [step56.q]) 9000000000000 (model56.caps 2) (model56.ord 2) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sext150000160000.excluded56_3 :
        Certificates.ExcludedOn (model56.B 3 ++ [step56.q]) 9000000000000 (model56.caps 3) (model56.ord 3) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sext150000160000.excluded56_4 :
        Certificates.ExcludedOn (model56.B 4 ++ [step56.q]) 9000000000000 (model56.caps 4) (model56.ord 4) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sext150000160000.excluded56_5 :
        Certificates.ExcludedOn (model56.B 5 ++ [step56.q]) 9000000000000 (model56.caps 5) (model56.ord 5) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sext150000160000.excluded56_6 :
        Certificates.ExcludedOn (model56.B 6 ++ [step56.q]) 9000000000000 (model56.caps 6) (model56.ord 6) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sext150000160000.excluded56_7 :
        Certificates.ExcludedOn (model56.B 7 ++ [step56.q]) 9000000000000 (model56.caps 7) (model56.ord 7) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sext150000160000.excluded56_9 :
        Certificates.ExcludedOn (model56.B 9 ++ [step56.q]) 9000000000000 (model56.caps 9) (model56.ord 9) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sext150000160000.checked56 :
        Certificates.StepValid model56 9000000000000 step56 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sext150000160000.next56 :
        model56.insert step56 = model57
        source
        theorem ConwaySoifer.Simplified.Certificates.Sext150000160000.excluded57_0 :
        Certificates.ExcludedOn (model57.B 0 ++ [step57.q]) 9000000000000 (model57.caps 0) (model57.ord 0) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sext150000160000.excluded57_1 :
        Certificates.ExcludedOn (model57.B 1 ++ [step57.q]) 9000000000000 (model57.caps 1) (model57.ord 1) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sext150000160000.excluded57_2 :
        Certificates.ExcludedOn (model57.B 2 ++ [step57.q]) 9000000000000 (model57.caps 2) (model57.ord 2) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sext150000160000.excluded57_3 :
        Certificates.ExcludedOn (model57.B 3 ++ [step57.q]) 9000000000000 (model57.caps 3) (model57.ord 3) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sext150000160000.excluded57_4 :
        Certificates.ExcludedOn (model57.B 4 ++ [step57.q]) 9000000000000 (model57.caps 4) (model57.ord 4) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sext150000160000.excluded57_5 :
        Certificates.ExcludedOn (model57.B 5 ++ [step57.q]) 9000000000000 (model57.caps 5) (model57.ord 5) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sext150000160000.excluded57_6 :
        Certificates.ExcludedOn (model57.B 6 ++ [step57.q]) 9000000000000 (model57.caps 6) (model57.ord 6) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sext150000160000.excluded57_7 :
        Certificates.ExcludedOn (model57.B 7 ++ [step57.q]) 9000000000000 (model57.caps 7) (model57.ord 7) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sext150000160000.excluded57_9 :
        Certificates.ExcludedOn (model57.B 9 ++ [step57.q]) 9000000000000 (model57.caps 9) (model57.ord 9) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sext150000160000.checked57 :
        Certificates.StepValid model57 9000000000000 step57 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sext150000160000.next57 :
        model57.insert step57 = model58
        source
        theorem ConwaySoifer.Simplified.Certificates.Sext150000160000.excluded58_0 :
        Certificates.ExcludedOn (model58.B 0 ++ [step58.q]) 9000000000000 (model58.caps 0) (model58.ord 0) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sext150000160000.excluded58_1 :
        Certificates.ExcludedOn (model58.B 1 ++ [step58.q]) 9000000000000 (model58.caps 1) (model58.ord 1) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sext150000160000.excluded58_2 :
        Certificates.ExcludedOn (model58.B 2 ++ [step58.q]) 9000000000000 (model58.caps 2) (model58.ord 2) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sext150000160000.excluded58_4 :
        Certificates.ExcludedOn (model58.B 4 ++ [step58.q]) 9000000000000 (model58.caps 4) (model58.ord 4) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sext150000160000.excluded58_5 :
        Certificates.ExcludedOn (model58.B 5 ++ [step58.q]) 9000000000000 (model58.caps 5) (model58.ord 5) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sext150000160000.excluded58_6 :
        Certificates.ExcludedOn (model58.B 6 ++ [step58.q]) 9000000000000 (model58.caps 6) (model58.ord 6) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sext150000160000.excluded58_7 :
        Certificates.ExcludedOn (model58.B 7 ++ [step58.q]) 9000000000000 (model58.caps 7) (model58.ord 7) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sext150000160000.excluded58_8 :
        Certificates.ExcludedOn (model58.B 8 ++ [step58.q]) 9000000000000 (model58.caps 8) (model58.ord 8) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sext150000160000.excluded58_9 :
        Certificates.ExcludedOn (model58.B 9 ++ [step58.q]) 9000000000000 (model58.caps 9) (model58.ord 9) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sext150000160000.checked58 :
        Certificates.StepValid model58 9000000000000 step58 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sext150000160000.next58 :
        model58.insert step58 = model59
        source
        theorem ConwaySoifer.Simplified.Certificates.Sext150000160000.excluded59_0 :
        Certificates.ExcludedOn (model59.B 0 ++ [step59.q]) 9000000000000 (model59.caps 0) (model59.ord 0) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sext150000160000.excluded59_1 :
        Certificates.ExcludedOn (model59.B 1 ++ [step59.q]) 9000000000000 (model59.caps 1) (model59.ord 1) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sext150000160000.excluded59_2 :
        Certificates.ExcludedOn (model59.B 2 ++ [step59.q]) 9000000000000 (model59.caps 2) (model59.ord 2) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sext150000160000.excluded59_4 :
        Certificates.ExcludedOn (model59.B 4 ++ [step59.q]) 9000000000000 (model59.caps 4) (model59.ord 4) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sext150000160000.excluded59_5 :
        Certificates.ExcludedOn (model59.B 5 ++ [step59.q]) 9000000000000 (model59.caps 5) (model59.ord 5) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sext150000160000.excluded59_6 :
        Certificates.ExcludedOn (model59.B 6 ++ [step59.q]) 9000000000000 (model59.caps 6) (model59.ord 6) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sext150000160000.excluded59_7 :
        Certificates.ExcludedOn (model59.B 7 ++ [step59.q]) 9000000000000 (model59.caps 7) (model59.ord 7) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sext150000160000.excluded59_8 :
        Certificates.ExcludedOn (model59.B 8 ++ [step59.q]) 9000000000000 (model59.caps 8) (model59.ord 8) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sext150000160000.excluded59_9 :
        Certificates.ExcludedOn (model59.B 9 ++ [step59.q]) 9000000000000 (model59.caps 9) (model59.ord 9) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sext150000160000.checked59 :
        Certificates.StepValid model59 9000000000000 step59 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sext150000160000.next59 :
        model59.insert step59 = model60
        source
        theorem ConwaySoifer.Simplified.Certificates.Sext150000160000.excluded60_0 :
        Certificates.ExcludedOn (model60.B 0 ++ [step60.q]) 9000000000000 (model60.caps 0) (model60.ord 0) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sext150000160000.excluded60_1 :
        Certificates.ExcludedOn (model60.B 1 ++ [step60.q]) 9000000000000 (model60.caps 1) (model60.ord 1) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sext150000160000.excluded60_3 :
        Certificates.ExcludedOn (model60.B 3 ++ [step60.q]) 9000000000000 (model60.caps 3) (model60.ord 3) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sext150000160000.excluded60_4 :
        Certificates.ExcludedOn (model60.B 4 ++ [step60.q]) 9000000000000 (model60.caps 4) (model60.ord 4) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sext150000160000.excluded60_5 :
        Certificates.ExcludedOn (model60.B 5 ++ [step60.q]) 9000000000000 (model60.caps 5) (model60.ord 5) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sext150000160000.excluded60_6 :
        Certificates.ExcludedOn (model60.B 6 ++ [step60.q]) 9000000000000 (model60.caps 6) (model60.ord 6) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sext150000160000.excluded60_7 :
        Certificates.ExcludedOn (model60.B 7 ++ [step60.q]) 9000000000000 (model60.caps 7) (model60.ord 7) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sext150000160000.excluded60_8 :
        Certificates.ExcludedOn (model60.B 8 ++ [step60.q]) 9000000000000 (model60.caps 8) (model60.ord 8) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sext150000160000.excluded60_9 :
        Certificates.ExcludedOn (model60.B 9 ++ [step60.q]) 9000000000000 (model60.caps 9) (model60.ord 9) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sext150000160000.checked60 :
        Certificates.StepValid model60 9000000000000 step60 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sext150000160000.next60 :
        model60.insert step60 = model61
        source
        theorem ConwaySoifer.Simplified.Certificates.Sext150000160000.excluded61_0 :
        Certificates.ExcludedOn (model61.B 0 ++ [step61.q]) 9000000000000 (model61.caps 0) (model61.ord 0) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sext150000160000.excluded61_1 :
        Certificates.ExcludedOn (model61.B 1 ++ [step61.q]) 9000000000000 (model61.caps 1) (model61.ord 1) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sext150000160000.excluded61_2 :
        Certificates.ExcludedOn (model61.B 2 ++ [step61.q]) 9000000000000 (model61.caps 2) (model61.ord 2) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sext150000160000.excluded61_4 :
        Certificates.ExcludedOn (model61.B 4 ++ [step61.q]) 9000000000000 (model61.caps 4) (model61.ord 4) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sext150000160000.excluded61_5 :
        Certificates.ExcludedOn (model61.B 5 ++ [step61.q]) 9000000000000 (model61.caps 5) (model61.ord 5) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sext150000160000.excluded61_6 :
        Certificates.ExcludedOn (model61.B 6 ++ [step61.q]) 9000000000000 (model61.caps 6) (model61.ord 6) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sext150000160000.excluded61_7 :
        Certificates.ExcludedOn (model61.B 7 ++ [step61.q]) 9000000000000 (model61.caps 7) (model61.ord 7) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sext150000160000.excluded61_8 :
        Certificates.ExcludedOn (model61.B 8 ++ [step61.q]) 9000000000000 (model61.caps 8) (model61.ord 8) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sext150000160000.excluded61_9 :
        Certificates.ExcludedOn (model61.B 9 ++ [step61.q]) 9000000000000 (model61.caps 9) (model61.ord 9) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sext150000160000.checked61 :
        Certificates.StepValid model61 9000000000000 step61 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sext150000160000.next61 :
        model61.insert step61 = model62
        source
        theorem ConwaySoifer.Simplified.Certificates.Sext150000160000.excluded62_0 :
        Certificates.ExcludedOn (model62.B 0 ++ [step62.q]) 9000000000000 (model62.caps 0) (model62.ord 0) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sext150000160000.excluded62_1 :
        Certificates.ExcludedOn (model62.B 1 ++ [step62.q]) 9000000000000 (model62.caps 1) (model62.ord 1) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sext150000160000.excluded62_3 :
        Certificates.ExcludedOn (model62.B 3 ++ [step62.q]) 9000000000000 (model62.caps 3) (model62.ord 3) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sext150000160000.excluded62_4 :
        Certificates.ExcludedOn (model62.B 4 ++ [step62.q]) 9000000000000 (model62.caps 4) (model62.ord 4) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sext150000160000.excluded62_5 :
        Certificates.ExcludedOn (model62.B 5 ++ [step62.q]) 9000000000000 (model62.caps 5) (model62.ord 5) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sext150000160000.excluded62_6 :
        Certificates.ExcludedOn (model62.B 6 ++ [step62.q]) 9000000000000 (model62.caps 6) (model62.ord 6) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sext150000160000.excluded62_7 :
        Certificates.ExcludedOn (model62.B 7 ++ [step62.q]) 9000000000000 (model62.caps 7) (model62.ord 7) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sext150000160000.excluded62_8 :
        Certificates.ExcludedOn (model62.B 8 ++ [step62.q]) 9000000000000 (model62.caps 8) (model62.ord 8) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sext150000160000.excluded62_9 :
        Certificates.ExcludedOn (model62.B 9 ++ [step62.q]) 9000000000000 (model62.caps 9) (model62.ord 9) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sext150000160000.checked62 :
        Certificates.StepValid model62 9000000000000 step62 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sext150000160000.next62 :
        model62.insert step62 = model63
        source
        theorem ConwaySoifer.Simplified.Certificates.Sext150000160000.excluded63_0 :
        Certificates.ExcludedOn (model63.B 0 ++ [step63.q]) 9000000000000 (model63.caps 0) (model63.ord 0) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sext150000160000.excluded63_1 :
        Certificates.ExcludedOn (model63.B 1 ++ [step63.q]) 9000000000000 (model63.caps 1) (model63.ord 1) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sext150000160000.excluded63_3 :
        Certificates.ExcludedOn (model63.B 3 ++ [step63.q]) 9000000000000 (model63.caps 3) (model63.ord 3) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sext150000160000.excluded63_4 :
        Certificates.ExcludedOn (model63.B 4 ++ [step63.q]) 9000000000000 (model63.caps 4) (model63.ord 4) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sext150000160000.excluded63_5 :
        Certificates.ExcludedOn (model63.B 5 ++ [step63.q]) 9000000000000 (model63.caps 5) (model63.ord 5) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sext150000160000.excluded63_6 :
        Certificates.ExcludedOn (model63.B 6 ++ [step63.q]) 9000000000000 (model63.caps 6) (model63.ord 6) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sext150000160000.excluded63_7 :
        Certificates.ExcludedOn (model63.B 7 ++ [step63.q]) 9000000000000 (model63.caps 7) (model63.ord 7) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sext150000160000.excluded63_8 :
        Certificates.ExcludedOn (model63.B 8 ++ [step63.q]) 9000000000000 (model63.caps 8) (model63.ord 8) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sext150000160000.excluded63_9 :
        Certificates.ExcludedOn (model63.B 9 ++ [step63.q]) 9000000000000 (model63.caps 9) (model63.ord 9) 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sext150000160000.checked63 :
        Certificates.StepValid model63 9000000000000 step63 0 1 100
        source
        theorem ConwaySoifer.Simplified.Certificates.Sext150000160000.next63 :
        model63.insert step63 = model64