Search for blocks/addresses/...

Proofgold Proposition

∀ x0 x1 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ∀ x2 x3 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ChurchNum_3ary_proj_p x0ChurchNum_3ary_proj_p x1ChurchNum_8ary_proj_p x2ChurchNum_8ary_proj_p x3(TwoRamseyGraph_4_5_24_ChurchNums_3x8 (λ x5 x6 x7 : (ι → ι)ι → ι . x5) (λ x5 x6 x7 x8 x9 x10 x11 x12 : (ι → ι)ι → ι . x5) x0 x2 = λ x5 x6 . x5)(TwoRamseyGraph_4_5_24_ChurchNums_3x8 (λ x5 x6 x7 : (ι → ι)ι → ι . x5) (λ x5 x6 x7 x8 x9 x10 x11 x12 : (ι → ι)ι → ι . x5) x1 x3 = λ x5 x6 . x5)(TwoRamseyGraph_4_5_24_ChurchNums_3x8 (λ x5 x6 x7 : (ι → ι)ι → ι . x5) (λ x5 x6 x7 x8 x9 x10 x11 x12 : (ι → ι)ι → ι . x6) x0 x2 = λ x5 x6 . x5)(TwoRamseyGraph_4_5_24_ChurchNums_3x8 (λ x5 x6 x7 : (ι → ι)ι → ι . x5) (λ x5 x6 x7 x8 x9 x10 x11 x12 : (ι → ι)ι → ι . x6) x1 x3 = λ x5 x6 . x5)(TwoRamseyGraph_4_5_24_ChurchNums_3x8 x0 x2 x1 x3 = λ x5 x6 . x5)ChurchNums_3x8_neq (λ x4 x5 x6 : (ι → ι)ι → ι . x4) (λ x4 x5 x6 x7 x8 x9 x10 x11 : (ι → ι)ι → ι . x4) x0 x2ChurchNums_3x8_neq (λ x4 x5 x6 : (ι → ι)ι → ι . x4) (λ x4 x5 x6 x7 x8 x9 x10 x11 : (ι → ι)ι → ι . x5) x0 x2ChurchNums_3x8_neq (λ x4 x5 x6 : (ι → ι)ι → ι . x4) (λ x4 x5 x6 x7 x8 x9 x10 x11 : (ι → ι)ι → ι . x4) x1 x3ChurchNums_3x8_neq (λ x4 x5 x6 : (ι → ι)ι → ι . x4) (λ x4 x5 x6 x7 x8 x9 x10 x11 : (ι → ι)ι → ι . x5) x1 x3ChurchNums_3x8_neq x0 x2 x1 x3False
type
prop
theory
HotG
name
-
proof
PUR79..
Megalodon
-
proofgold address
TMaf7..
creator
18506 Pr4zB../7d833..
owner
18506 Pr4zB../7d833..
term root
83e89..