Search for blocks/addresses/...

Proofgold Proposition

∀ x0 x1 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ∀ x2 x3 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ChurchNum_3ary_proj_p x0ChurchNum_8ary_proj_p x2ChurchNum_3ary_proj_p x1ChurchNum_8ary_proj_p x3(x0 = λ x5 x6 x7 : (ι → ι)ι → ι . x1 x6 x7 x5)ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt5_id_ge5_rot2 x2 x0) (ChurchNums_8_perm_3_4_5_6_7_0_1_2 x2) = ChurchNums_3x8_to_u24 x1 x3∀ x4 : ο . x4
type
prop
theory
HotG
name
-
proof
PUX3W..
Megalodon
-
proofgold address
TMZk9..
creator
18840 Pr4zB../0e2cf..
owner
18840 Pr4zB../0e2cf..
term root
9d122..