Search for blocks/addresses/...
Proofgold Proposition
∀ x0 x1 x2 x3 x4 :
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
ι → ι
)
→
ι → ι
.
∀ x5 x6 x7 x8 x9 :
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
ι → ι
)
→
ι → ι
.
ChurchNum_3ary_proj_p
x0
⟶
ChurchNum_3ary_proj_p
x1
⟶
ChurchNum_3ary_proj_p
x2
⟶
ChurchNum_3ary_proj_p
x3
⟶
ChurchNum_3ary_proj_p
x4
⟶
ChurchNum_8ary_proj_p
x5
⟶
ChurchNum_8ary_proj_p
x6
⟶
ChurchNum_8ary_proj_p
x7
⟶
ChurchNum_8ary_proj_p
x8
⟶
ChurchNum_8ary_proj_p
x9
⟶
(
TwoRamseyGraph_4_5_24_ChurchNums_3x8
x0
x5
x1
x6
=
λ x11 x12 .
x12
)
⟶
(
TwoRamseyGraph_4_5_24_ChurchNums_3x8
x0
x5
x2
x7
=
λ x11 x12 .
x12
)
⟶
(
TwoRamseyGraph_4_5_24_ChurchNums_3x8
x0
x5
x3
x8
=
λ x11 x12 .
x12
)
⟶
(
TwoRamseyGraph_4_5_24_ChurchNums_3x8
x0
x5
x4
x9
=
λ x11 x12 .
x12
)
⟶
(
TwoRamseyGraph_4_5_24_ChurchNums_3x8
x1
x6
x2
x7
=
λ x11 x12 .
x12
)
⟶
(
TwoRamseyGraph_4_5_24_ChurchNums_3x8
x1
x6
x3
x8
=
λ x11 x12 .
x12
)
⟶
(
TwoRamseyGraph_4_5_24_ChurchNums_3x8
x1
x6
x4
x9
=
λ x11 x12 .
x12
)
⟶
(
TwoRamseyGraph_4_5_24_ChurchNums_3x8
x2
x7
x3
x8
=
λ x11 x12 .
x12
)
⟶
(
TwoRamseyGraph_4_5_24_ChurchNums_3x8
x2
x7
x4
x9
=
λ x11 x12 .
x12
)
⟶
(
TwoRamseyGraph_4_5_24_ChurchNums_3x8
x3
x8
x4
x9
=
λ x11 x12 .
x12
)
⟶
∀ x10 :
(
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
ι → ι
)
→
ι → ι
)
→
(
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
ι → ι
)
→
ι → ι
)
→ ι
.
(
∀ x11 :
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
ι → ι
)
→
ι → ι
.
∀ x12 :
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
ι → ι
)
→
ι → ι
.
ap
(
x10
x11
x12
)
0
=
ChurchNums_3x8_to_u24
x11
x12
)
⟶
(
∀ x11 :
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
ι → ι
)
→
ι → ι
.
∀ x12 :
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
ι → ι
)
→
ι → ι
.
ap
(
x10
x11
x12
)
u1
=
ChurchNums_3x8_to_u24
(
ChurchNums_8x3_to_3_lt7_id_ge7_rot2
x12
x11
)
(
ChurchNums_8_perm_1_2_3_4_5_6_7_0
x12
)
)
⟶
(
∀ x11 :
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
ι → ι
)
→
ι → ι
.
∀ x12 :
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
ι → ι
)
→
ι → ι
.
ap
(
x10
x11
x12
)
u2
=
ChurchNums_3x8_to_u24
(
ChurchNums_8x3_to_3_lt6_id_ge6_rot2
x12
x11
)
(
ChurchNums_8_perm_2_3_4_5_6_7_0_1
x12
)
)
⟶
(
∀ x11 :
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
ι → ι
)
→
ι → ι
.
∀ x12 :
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
ι → ι
)
→
ι → ι
.
ap
(
x10
x11
x12
)
u3
=
ChurchNums_3x8_to_u24
(
ChurchNums_8x3_to_3_lt5_id_ge5_rot2
x12
x11
)
(
ChurchNums_8_perm_3_4_5_6_7_0_1_2
x12
)
)
⟶
(
∀ x11 :
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
ι → ι
)
→
ι → ι
.
∀ x12 :
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
ι → ι
)
→
ι → ι
.
ap
(
x10
x11
x12
)
u4
=
ChurchNums_3x8_to_u24
(
ChurchNums_8x3_to_3_lt4_id_ge4_rot2
x12
x11
)
(
ChurchNums_8_perm_4_5_6_7_0_1_2_3
x12
)
)
⟶
(
∀ x11 :
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
ι → ι
)
→
ι → ι
.
∀ x12 :
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
ι → ι
)
→
ι → ι
.
ChurchNum_3ary_proj_p
x11
⟶
ChurchNum_8ary_proj_p
x12
⟶
∀ x13 .
x13
∈
u5
⟶
∀ x14 .
x14
∈
u5
⟶
ap
(
x10
x11
x12
)
x13
=
ap
(
x10
x11
x12
)
x14
⟶
x13
=
x14
)
⟶
(
∀ x11 x12 :
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
ι → ι
)
→
ι → ι
.
∀ x13 x14 :
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
ι → ι
)
→
ι → ι
.
ChurchNum_3ary_proj_p
x11
⟶
ChurchNum_8ary_proj_p
x13
⟶
ChurchNum_3ary_proj_p
x12
⟶
ChurchNum_8ary_proj_p
x14
⟶
(
TwoRamseyGraph_4_5_24_ChurchNums_3x8
x11
x13
x12
x14
=
λ x16 x17 .
x17
)
⟶
∀ x15 .
x15
∈
u5
⟶
∀ x16 .
x16
∈
u5
⟶
ap
(
x10
x11
x13
)
x15
=
ap
(
x10
x12
x14
)
x16
⟶
∀ x17 : ο .
(
x12
=
ChurchNums_8x3_to_3_lt5_id_ge5_rot2
x13
x11
⟶
x14
=
ChurchNums_8_perm_3_4_5_6_7_0_1_2
x13
⟶
x17
)
⟶
(
x11
=
ChurchNums_8x3_to_3_lt5_id_ge5_rot2
x14
x12
⟶
x13
=
ChurchNums_8_perm_3_4_5_6_7_0_1_2
x14
⟶
x17
)
⟶
x17
)
⟶
False
type
prop
theory
HotG
name
-
proof
PUUX7..
Megalodon
-
proofgold address
TMaV1..
creator
18893
Pr4zB..
/
6cf8a..
owner
18893
Pr4zB..
/
6cf8a..
term root
39301..