Proofgold Asset

Definition Subq^Subq := λ x0 x1 . ∀ x2 . x2 ∈ x0 ⟶ x2 ∈ x1
Param ordsucc^ordsucc : ι → ι
Definition u1 := 1
Definition u2 := ordsucc u1
Definition u3 := ordsucc u2
Definition u4 := ordsucc u3
Definition u5 := ordsucc u4
Definition u6 := ordsucc u5
Definition u7 := ordsucc u6
Definition u8 := ordsucc u7
Definition u9 := ordsucc u8
Definition u10 := ordsucc u9
Definition u11 := ordsucc u10
Definition u12 := ordsucc u11
Definition u13 := ordsucc u12
Param atleastp^atleastp : ι → ι → ο
Definition False^False := ∀ x0 : ο . x0
Definition not^not := λ x0 : ο . x0 ⟶ False
Param Church13_p : (ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι) → ο
Param TwoRamseyGraph_3_5_Church13 : (ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι) → ι → ι → ι
Definition TwoRamseyGraph_3_5_13 := λ x0 x1 . ∀ x2 x3 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church13_p x2 ⟶ Church13_p x3 ⟶ x0 = x2 0 u1 u2 u3 u4 u5 u6 u7 u8 u9 u10 u11 u12 ⟶ x1 = x3 0 u1 u2 u3 u4 u5 u6 u7 u8 u9 u10 u11 u12 ⟶ TwoRamseyGraph_3_5_Church13 x2 x3 = λ x5 x6 . x5
Known 3ed86.. : ∀ x0 . atleastp u5 x0 ⟶ ∀ x1 : ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ (x2 = x3 ⟶ ∀ x7 : ο . x7) ⟶ (x2 = x4 ⟶ ∀ x7 : ο . x7) ⟶ (x2 = x5 ⟶ ∀ x7 : ο . x7) ⟶ (x2 = x6 ⟶ ∀ x7 : ο . x7) ⟶ (x3 = x4 ⟶ ∀ x7 : ο . x7) ⟶ (x3 = x5 ⟶ ∀ x7 : ο . x7) ⟶ (x3 = x6 ⟶ ∀ x7 : ο . x7) ⟶ (x4 = x5 ⟶ ∀ x7 : ο . x7) ⟶ (x4 = x6 ⟶ ∀ x7 : ο . x7) ⟶ (x5 = x6 ⟶ ∀ x7 : ο . x7) ⟶ x1) ⟶ x1
Known 783ed.. : ∀ x0 . x0 ∈ u13 ⟶ ∀ x1 : ο . (∀ x2 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church13_p x2 ⟶ x0 = x2 0 u1 u2 u3 u4 u5 u6 u7 u8 u9 u10 u11 u12 ⟶ x1) ⟶ x1
Known 4a8a6.. : ∀ x0 x1 x2 x3 x4 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church13_p x0 ⟶ Church13_p x1 ⟶ Church13_p x2 ⟶ Church13_p x3 ⟶ Church13_p x4 ⟶ (x0 = x1 ⟶ ∀ x5 : ο . x5) ⟶ (x0 = x2 ⟶ ∀ x5 : ο . x5) ⟶ (x0 = x3 ⟶ ∀ x5 : ο . x5) ⟶ (x0 = x4 ⟶ ∀ x5 : ο . x5) ⟶ (x1 = x2 ⟶ ∀ x5 : ο . x5) ⟶ (x1 = x3 ⟶ ∀ x5 : ο . x5) ⟶ (x1 = x4 ⟶ ∀ x5 : ο . x5) ⟶ (x2 = x3 ⟶ ∀ x5 : ο . x5) ⟶ (x2 = x4 ⟶ ∀ x5 : ο . x5) ⟶ (x3 = x4 ⟶ ∀ x5 : ο . x5) ⟶ (TwoRamseyGraph_3_5_Church13 x0 x1 = λ x6 x7 . x7) ⟶ (TwoRamseyGraph_3_5_Church13 x0 x2 = λ x6 x7 . x7) ⟶ (TwoRamseyGraph_3_5_Church13 x0 x3 = λ x6 x7 . x7) ⟶ (TwoRamseyGraph_3_5_Church13 x0 x4 = λ x6 x7 . x7) ⟶ (TwoRamseyGraph_3_5_Church13 x1 x2 = λ x6 x7 . x7) ⟶ (TwoRamseyGraph_3_5_Church13 x1 x3 = λ x6 x7 . x7) ⟶ (TwoRamseyGraph_3_5_Church13 x1 x4 = λ x6 x7 . x7) ⟶ (TwoRamseyGraph_3_5_Church13 x2 x3 = λ x6 x7 . x7) ⟶ (TwoRamseyGraph_3_5_Church13 x2 x4 = λ x6 x7 . x7) ⟶ (TwoRamseyGraph_3_5_Church13 x3 x4 = λ x6 x7 . x7) ⟶ False
Definition or^or := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x2) ⟶ (x1 ⟶ x2) ⟶ x2
Known cd49f.. : ∀ x0 x1 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church13_p x0 ⟶ Church13_p x1 ⟶ or (TwoRamseyGraph_3_5_Church13 x0 x1 = λ x3 x4 . x3) (TwoRamseyGraph_3_5_Church13 x0 x1 = λ x3 x4 . x4)
Known FalseE^FalseE : False ⟶ ∀ x0 : ο . x0
Known d7c49.. : ∀ x0 x1 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church13_p x0 ⟶ Church13_p x1 ⟶ x0 0 u1 u2 u3 u4 u5 u6 u7 u8 u9 u10 u11 u12 = x1 0 u1 u2 u3 u4 u5 u6 u7 u8 u9 u10 u11 u12 ⟶ x0 = x1
Theorem cedc9.. : ∀ x0 . x0 ⊆ u13 ⟶ atleastp u5 x0 ⟶ not (∀ x1 . x1 ∈ x0 ⟶ ∀ x2 . x2 ∈ x0 ⟶ (x1 = x2 ⟶ ∀ x3 : ο . x3) ⟶ not (TwoRamseyGraph_3_5_13 x1 x2)) (proof)
Definition and^and := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Definition TwoRamseyProp_atleastp := λ x0 x1 x2 . ∀ x3 : ι → ι → ο . (∀ x4 x5 . x3 x4 x5 ⟶ x3 x5 x4) ⟶ or (∀ x4 : ο . (∀ x5 . and (x5 ⊆ x2) (and (atleastp x0 x5) (∀ x6 . x6 ∈ x5 ⟶ ∀ x7 . x7 ∈ x5 ⟶ (x6 = x7 ⟶ ∀ x8 : ο . x8) ⟶ x3 x6 x7)) ⟶ x4) ⟶ x4) (∀ x4 : ο . (∀ x5 . and (x5 ⊆ x2) (and (atleastp x1 x5) (∀ x6 . x6 ∈ x5 ⟶ ∀ x7 . x7 ∈ x5 ⟶ (x6 = x7 ⟶ ∀ x8 : ο . x8) ⟶ not (x3 x6 x7))) ⟶ x4) ⟶ x4)
Known 09b0c.. : ∀ x0 x1 . TwoRamseyGraph_3_5_13 x0 x1 ⟶ TwoRamseyGraph_3_5_13 x1 x0
Known 0ff84.. : ∀ x0 . x0 ⊆ u13 ⟶ atleastp u3 x0 ⟶ not (∀ x1 . x1 ∈ x0 ⟶ ∀ x2 . x2 ∈ x0 ⟶ (x1 = x2 ⟶ ∀ x3 : ο . x3) ⟶ TwoRamseyGraph_3_5_13 x1 x2)
Theorem not_TwoRamseyProp_atleast_3_5_13 : not (TwoRamseyProp_atleastp 3 5 13) (proof)
Param TwoRamseyProp^{TwoRamseyProp} : ι → ι → ι → ο
Known TwoRamseyProp_atleastp_atleastp : ∀ x0 x1 x2 x3 x4 . TwoRamseyProp x0 x2 x4 ⟶ atleastp x1 x0 ⟶ atleastp x3 x2 ⟶ TwoRamseyProp_atleastp x1 x3 x4
Known atleastp_ref : ∀ x0 . atleastp x0 x0
Theorem not_TwoRamseyProp_3_5_13^{not_TwoRamseyProp_3_5_13} : not (TwoRamseyProp 3 5 13) (proof)