Proofgold Proposition

∀ x0 x1 x2 x3 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ∀ x4 x5 x6 x7 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNum_3ary_proj_p x0 ⟶ ChurchNum_3ary_proj_p x1 ⟶ ChurchNum_3ary_proj_p x2 ⟶ ChurchNum_3ary_proj_p x3 ⟶ ChurchNum_8ary_proj_p x4 ⟶ ChurchNum_8ary_proj_p x5 ⟶ ChurchNum_8ary_proj_p x6 ⟶ ChurchNum_8ary_proj_p x7 ⟶ (TwoRamseyGraph_4_5_24_ChurchNums_3x8 x0 x4 x1 x5 = λ x9 x10 . x9) ⟶ (TwoRamseyGraph_4_5_24_ChurchNums_3x8 x0 x4 x2 x6 = λ x9 x10 . x9) ⟶ (TwoRamseyGraph_4_5_24_ChurchNums_3x8 x0 x4 x3 x7 = λ x9 x10 . x9) ⟶ (TwoRamseyGraph_4_5_24_ChurchNums_3x8 x1 x5 x2 x6 = λ x9 x10 . x9) ⟶ (TwoRamseyGraph_4_5_24_ChurchNums_3x8 x1 x5 x3 x7 = λ x9 x10 . x9) ⟶ (TwoRamseyGraph_4_5_24_ChurchNums_3x8 x2 x6 x3 x7 = λ x9 x10 . x9) ⟶ ChurchNums_3x8_neq x0 x4 x1 x5 ⟶ ChurchNums_3x8_neq x0 x4 x2 x6 ⟶ ChurchNums_3x8_neq x0 x4 x3 x7 ⟶ ChurchNums_3x8_neq x1 x5 x2 x6 ⟶ ChurchNums_3x8_neq x1 x5 x3 x7 ⟶ ChurchNums_3x8_neq x2 x6 x3 x7 ⟶ False

type
prop

theory
HotG

name
-

proof
PUKW4..

Megalodon
-

proofgold address
TML3k..

creator
18661 Pr4zB../361a3..

owner
18661 Pr4zB../361a3..

term root
fc1c5..