Search for blocks/addresses/...
Proofgold Proposition
∀ x0 x1 :
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
ι → ι
)
→
ι → ι
.
∀ x2 x3 :
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
ι → ι
)
→
ι → ι
.
ChurchNums_3x8_eq
x0
x2
x1
x3
⟶
ChurchNums_3x8_eq
(
ChurchNums_3x8_3_lt1_swap_1_2_ge1_rot2
x0
x2
)
(
ChurchNums_8_perm_0_7_6_5_4_3_2_1
x2
)
(
ChurchNums_3x8_3_lt1_swap_1_2_ge1_rot2
x1
x3
)
(
ChurchNums_8_perm_0_7_6_5_4_3_2_1
x3
)
type
prop
theory
HotG
name
-
proof
PUYUy..
Megalodon
-
proofgold address
TMa3R..
creator
18523
Pr4zB..
/
993f8..
owner
18523
Pr4zB..
/
993f8..
term root
1250d..