Proofgold Asset

Param u17 : ι
Param Church17_p : (ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι) → ο
Param TwoRamseyGraph_3_6_Church17 : (ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι) → ι → ι → ι
Definition Subq^Subq := λ x0 x1 . ∀ x2 . x2 ∈ x0 ⟶ x2 ∈ x1
Param atleastp^atleastp : ι → ι → ο
Param ordsucc^ordsucc : ι → ι
Definition u1 := 1
Definition u2 := ordsucc u1
Definition u3 := ordsucc u2
Definition False^False := ∀ x0 : ο . x0
Definition not^not := λ x0 : ο . x0 ⟶ False
Known f03aa.. : ∀ x0 . atleastp 3 x0 ⟶ ∀ x1 : ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ (x2 = x3 ⟶ ∀ x5 : ο . x5) ⟶ (x2 = x4 ⟶ ∀ x5 : ο . x5) ⟶ (x3 = x4 ⟶ ∀ x5 : ο . x5) ⟶ x1) ⟶ x1
Known 90040.. : ∀ x0 x1 x2 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_p x0 ⟶ Church17_p x1 ⟶ Church17_p x2 ⟶ (x0 = x1 ⟶ ∀ x3 : ο . x3) ⟶ (x0 = x2 ⟶ ∀ x3 : ο . x3) ⟶ (x1 = x2 ⟶ ∀ x3 : ο . x3) ⟶ (TwoRamseyGraph_3_6_Church17 x0 x1 = λ x4 x5 . x4) ⟶ (TwoRamseyGraph_3_6_Church17 x0 x2 = λ x4 x5 . x4) ⟶ (TwoRamseyGraph_3_6_Church17 x1 x2 = λ x4 x5 . x4) ⟶ False
Theorem 12554.. : ∀ x0 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . (∀ x1 . x1 ∈ u17 ⟶ Church17_p (x0 x1)) ⟶ (∀ x1 . x1 ∈ u17 ⟶ ∀ x2 . x2 ∈ u17 ⟶ x0 x1 = x0 x2 ⟶ x1 = x2) ⟶ ∀ x1 : ι → ι → ο . (∀ x2 x3 . x1 x2 x3 ⟶ x2 ∈ u17 ⟶ x3 ∈ u17 ⟶ TwoRamseyGraph_3_6_Church17 (x0 x2) (x0 x3) = λ x5 x6 . x5) ⟶ ∀ x2 . x2 ⊆ u17 ⟶ atleastp u3 x2 ⟶ not (∀ x3 . x3 ∈ x2 ⟶ ∀ x4 . x4 ∈ x2 ⟶ (x3 = x4 ⟶ ∀ x5 : ο . x5) ⟶ x1 x3 x4) (proof)