Search for blocks/addresses/...

Proofgold Proposition

∀ x0 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ∀ x1 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ChurchNum_3ary_proj_p x0ChurchNum_8ary_proj_p x1(TwoRamseyGraph_4_5_24_ChurchNums_3x8 (λ x3 x4 x5 : (ι → ι)ι → ι . x3) (λ x3 x4 x5 x6 x7 x8 x9 x10 : (ι → ι)ι → ι . x3) x0 x1 = λ x3 x4 . x4)∀ x2 : ο . ((x0 = λ x4 x5 x6 : (ι → ι)ι → ι . x4)(x1 = λ x4 x5 x6 x7 x8 x9 x10 x11 : (ι → ι)ι → ι . x7)x2)((x0 = λ x4 x5 x6 : (ι → ι)ι → ι . x4)(x1 = λ x4 x5 x6 x7 x8 x9 x10 x11 : (ι → ι)ι → ι . x9)x2)((x0 = λ x4 x5 x6 : (ι → ι)ι → ι . x4)(x1 = λ x4 x5 x6 x7 x8 x9 x10 x11 : (ι → ι)ι → ι . x10)x2)((x0 = λ x4 x5 x6 : (ι → ι)ι → ι . x4)(x1 = λ x4 x5 x6 x7 x8 x9 x10 x11 : (ι → ι)ι → ι . x11)x2)((x0 = λ x4 x5 x6 : (ι → ι)ι → ι . x5)(x1 = λ x4 x5 x6 x7 x8 x9 x10 x11 : (ι → ι)ι → ι . x6)x2)((x0 = λ x4 x5 x6 : (ι → ι)ι → ι . x5)(x1 = λ x4 x5 x6 x7 x8 x9 x10 x11 : (ι → ι)ι → ι . x7)x2)((x0 = λ x4 x5 x6 : (ι → ι)ι → ι . x5)(x1 = λ x4 x5 x6 x7 x8 x9 x10 x11 : (ι → ι)ι → ι . x8)x2)((x0 = λ x4 x5 x6 : (ι → ι)ι → ι . x5)(x1 = λ x4 x5 x6 x7 x8 x9 x10 x11 : (ι → ι)ι → ι . x9)x2)((x0 = λ x4 x5 x6 : (ι → ι)ι → ι . x5)(x1 = λ x4 x5 x6 x7 x8 x9 x10 x11 : (ι → ι)ι → ι . x10)x2)((x0 = λ x4 x5 x6 : (ι → ι)ι → ι . x6)(x1 = λ x4 x5 x6 x7 x8 x9 x10 x11 : (ι → ι)ι → ι . x5)x2)((x0 = λ x4 x5 x6 : (ι → ι)ι → ι . x6)(x1 = λ x4 x5 x6 x7 x8 x9 x10 x11 : (ι → ι)ι → ι . x6)x2)((x0 = λ x4 x5 x6 : (ι → ι)ι → ι . x6)(x1 = λ x4 x5 x6 x7 x8 x9 x10 x11 : (ι → ι)ι → ι . x7)x2)((x0 = λ x4 x5 x6 : (ι → ι)ι → ι . x6)(x1 = λ x4 x5 x6 x7 x8 x9 x10 x11 : (ι → ι)ι → ι . x9)x2)x2
type
prop
theory
HotG
name
-
proof
PUaJB..
Megalodon
-
proofgold address
TMLkC..
creator
18387 Pr4zB../501c3..
owner
18387 Pr4zB../501c3..
term root
d2bdc..