Search for blocks/addresses/...
Proofgold Proposition
∀ x0 :
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
ι → ι
)
→
ι → ι
.
∀ x1 :
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
ι → ι
)
→
ι → ι
.
ChurchNum_8ary_proj_p
x1
⟶
ChurchNums_3x8_3_lt1_swap_1_2_ge1_rot2
(
ChurchNums_3x8_3_lt1_swap_1_2_ge1_rot2
x0
x1
)
(
ChurchNums_8_perm_0_7_6_5_4_3_2_1
x1
)
=
x0
type
prop
theory
HotG
name
-
proof
PUYUy..
Megalodon
-
proofgold address
TMQxJ..
creator
18523
Pr4zB..
/
d7189..
owner
18523
Pr4zB..
/
d7189..
term root
3a03f..