Proofgold Address

Definition Church6_p := λ x0 : ι → ι → ι → ι → ι → ι → ι . ∀ x1 : (ι → ι → ι → ι → ι → ι → ι) → ο . x1 (λ x2 x3 x4 x5 x6 x7 . x2) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 . x3) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 . x4) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 . x5) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 . x6) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 . x7) ⟶ x1 x0
Definition False^False := ∀ x0 : ο . x0
Param TwoRamseyGraph_4_6_Church6_squared_b : (ι → ι → ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι → ι → ι) → ι → ι → ι
Param TwoRamseyGraph_4_6_Church6_squared_a : (ι → ι → ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι → ι → ι) → ι → ι → ι
Param a4ee9.. : (ι → ι → ι → ι → ι → ι → ι) → ο
Known 2e0bc.. : ∀ x0 x1 x2 x3 : ι → ι → ι → ι → ι → ι → ι . a4ee9.. x0 ⟶ Church6_p x1 ⟶ Church6_p x2 ⟶ Church6_p x3 ⟶ ((x2 = λ x5 x6 x7 x8 x9 x10 . x10) ⟶ (x3 = λ x5 x6 x7 x8 x9 x10 . x10) ⟶ False) ⟶ (TwoRamseyGraph_4_6_Church6_squared_b x0 x1 x2 x3 = λ x5 x6 . x5) ⟶ TwoRamseyGraph_4_6_Church6_squared_a x0 x1 x2 x3 = λ x5 x6 . x5
Known 9367f.. : a4ee9.. (λ x0 x1 x2 x3 x4 x5 . x0)
Known 6b245.. : a4ee9.. (λ x0 x1 x2 x3 x4 x5 . x1)
Known 32eba.. : a4ee9.. (λ x0 x1 x2 x3 x4 x5 . x2)
Known 77b75.. : a4ee9.. (λ x0 x1 x2 x3 x4 x5 . x3)
Known eca3f.. : a4ee9.. (λ x0 x1 x2 x3 x4 x5 . x4)
Known d20f9.. : ∀ x0 x1 x2 : ι → ι → ι → ι → ι → ι → ι . a4ee9.. x0 ⟶ Church6_p x1 ⟶ Church6_p x2 ⟶ ((x1 = λ x4 x5 x6 x7 x8 x9 . x9) ⟶ (x2 = λ x4 x5 x6 x7 x8 x9 . x9) ⟶ False) ⟶ (TwoRamseyGraph_4_6_Church6_squared_b (λ x4 x5 x6 x7 x8 x9 . x9) x0 x1 x2 = λ x4 x5 . x4) ⟶ TwoRamseyGraph_4_6_Church6_squared_a (λ x4 x5 x6 x7 x8 x9 . x9) x0 x1 x2 = λ x4 x5 . x4
Known FalseE^FalseE : False ⟶ ∀ x0 : ο . x0
Known 768c1.. : ((λ x1 x2 . x2) = λ x1 x2 . x1) ⟶ ∀ x0 : ο . x0
Theorem f59e9.. : ∀ x0 x1 x2 x3 : ι → ι → ι → ι → ι → ι → ι . Church6_p x0 ⟶ Church6_p x1 ⟶ Church6_p x2 ⟶ Church6_p x3 ⟶ ((x0 = λ x5 x6 x7 x8 x9 x10 . x10) ⟶ (x1 = λ x5 x6 x7 x8 x9 x10 . x10) ⟶ False) ⟶ ((x2 = λ x5 x6 x7 x8 x9 x10 . x10) ⟶ (x3 = λ x5 x6 x7 x8 x9 x10 . x10) ⟶ False) ⟶ (TwoRamseyGraph_4_6_Church6_squared_b x0 x1 x2 x3 = λ x5 x6 . x5) ⟶ TwoRamseyGraph_4_6_Church6_squared_a x0 x1 x2 x3 = λ x5 x6 . x5 (proof)
Param u6 : ι
Param u5 : ι
Param nth_6_tuple : ι → ι → ι → ι → ι → ι → ι → ι
Definition TwoRamseyGraph_4_6_35_b := λ x0 x1 x2 x3 . x0 ∈ u6 ⟶ x1 ∈ u6 ⟶ x2 ∈ u6 ⟶ x3 ∈ u6 ⟶ TwoRamseyGraph_4_6_Church6_squared_b (nth_6_tuple x0) (nth_6_tuple x1) (nth_6_tuple x2) (nth_6_tuple x3) = λ x5 x6 . x5
Definition TwoRamseyGraph_4_6_35_a := λ x0 x1 x2 x3 . TwoRamseyGraph_4_6_Church6_squared_a (nth_6_tuple x0) (nth_6_tuple x1) (nth_6_tuple x2) (nth_6_tuple x3) = λ x5 x6 . x5
Known 3b8c0.. : ∀ x0 . x0 ∈ u6 ⟶ Church6_p (nth_6_tuple x0)
Known fed6d.. : nth_6_tuple u5 = λ x1 x2 x3 x4 x5 x6 . x6
Known 60d0e.. : ∀ x0 . x0 ∈ u6 ⟶ ∀ x1 . x1 ∈ u6 ⟶ nth_6_tuple x0 = nth_6_tuple x1 ⟶ x0 = x1
Known In_5_6^In_5_6 : u5 ∈ u6
Theorem 76062.. : ∀ x0 . x0 ∈ u6 ⟶ ∀ x1 . x1 ∈ u6 ⟶ ∀ x2 . x2 ∈ u6 ⟶ ∀ x3 . x3 ∈ u6 ⟶ (x0 = u5 ⟶ x1 = u5 ⟶ False) ⟶ (x2 = u5 ⟶ x3 = u5 ⟶ False) ⟶ TwoRamseyGraph_4_6_35_b x0 x1 x2 x3 ⟶ TwoRamseyGraph_4_6_35_a x0 x1 x2 x3 (proof)