Search for blocks/addresses/...
Proofgold Signed Transaction
vin
Pr5Hs..
/
19542..
PUMFt..
/
35d47..
vout
Pr5Hs..
/
989e7..
6,170.70 bars
TMS38..
/
5adcb..
negprop ownership controlledby
Pr4zB..
upto 0
TMbvP..
/
322e6..
negprop ownership controlledby
Pr4zB..
upto 0
TMXaE..
/
70cf6..
ownership of
51503..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMHPK..
/
584d8..
ownership of
9ca42..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMJuq..
/
0933f..
ownership of
13908..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMYy9..
/
2b9f0..
ownership of
0d78a..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMSwp..
/
60631..
ownership of
6af4c..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMJ2y..
/
96d33..
ownership of
c75ca..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMQ1t..
/
42660..
ownership of
165ef..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMa6w..
/
a0136..
ownership of
b89cf..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
Pr4zB..
/
44d89..
800.00 bars
PUVnt..
/
a9708..
doc published by
Pr4zB..
Param
ChurchNum_3ary_proj_p
:
(
(
(
ι
→
ι
) →
ι
→
ι
) →
(
(
ι
→
ι
) →
ι
→
ι
) →
CN (
ι
→
ι
)
) →
ο
Param
ChurchNum_8ary_proj_p
:
(
(
(
ι
→
ι
) →
ι
→
ι
) →
(
(
ι
→
ι
) →
ι
→
ι
) →
(
(
ι
→
ι
) →
ι
→
ι
) →
(
(
ι
→
ι
) →
ι
→
ι
) →
(
(
ι
→
ι
) →
ι
→
ι
) →
(
(
ι
→
ι
) →
ι
→
ι
) →
(
(
ι
→
ι
) →
ι
→
ι
) →
CN (
ι
→
ι
)
) →
ο
Param
TwoRamseyGraph_4_5_24_ChurchNums_3x8
:
(
(
(
ι
→
ι
) →
ι
→
ι
) →
(
(
ι
→
ι
) →
ι
→
ι
) →
CN (
ι
→
ι
)
) →
(
(
(
ι
→
ι
) →
ι
→
ι
) →
(
(
ι
→
ι
) →
ι
→
ι
) →
(
(
ι
→
ι
) →
ι
→
ι
) →
(
(
ι
→
ι
) →
ι
→
ι
) →
(
(
ι
→
ι
) →
ι
→
ι
) →
(
(
ι
→
ι
) →
ι
→
ι
) →
(
(
ι
→
ι
) →
ι
→
ι
) →
CN (
ι
→
ι
)
) →
(
(
(
ι
→
ι
) →
ι
→
ι
) →
(
(
ι
→
ι
) →
ι
→
ι
) →
CN (
ι
→
ι
)
) →
(
(
(
ι
→
ι
) →
ι
→
ι
) →
(
(
ι
→
ι
) →
ι
→
ι
) →
(
(
ι
→
ι
) →
ι
→
ι
) →
(
(
ι
→
ι
) →
ι
→
ι
) →
(
(
ι
→
ι
) →
ι
→
ι
) →
(
(
ι
→
ι
) →
ι
→
ι
) →
(
(
ι
→
ι
) →
ι
→
ι
) →
CN (
ι
→
ι
)
) →
ι
→
ι
→
ι
Param
ChurchNums_3x8_to_u24
:
(
(
(
ι
→
ι
) →
ι
→
ι
) →
(
(
ι
→
ι
) →
ι
→
ι
) →
CN (
ι
→
ι
)
) →
(
(
(
ι
→
ι
) →
ι
→
ι
) →
(
(
ι
→
ι
) →
ι
→
ι
) →
(
(
ι
→
ι
) →
ι
→
ι
) →
(
(
ι
→
ι
) →
ι
→
ι
) →
(
(
ι
→
ι
) →
ι
→
ι
) →
(
(
ι
→
ι
) →
ι
→
ι
) →
(
(
ι
→
ι
) →
ι
→
ι
) →
CN (
ι
→
ι
)
) →
ι
Definition
False
False
:=
∀ x0 : ο .
x0
Known
01925..
:
∀ x0 x1 :
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
ι → ι
)
→
ι → ι
.
∀ x2 x3 :
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
ι → ι
)
→
ι → ι
.
ChurchNum_3ary_proj_p
x0
⟶
ChurchNum_8ary_proj_p
x2
⟶
ChurchNum_3ary_proj_p
x1
⟶
ChurchNum_8ary_proj_p
x3
⟶
(
TwoRamseyGraph_4_5_24_ChurchNums_3x8
x0
x2
x1
x3
=
λ x5 x6 .
x6
)
⟶
ChurchNums_3x8_to_u24
x0
x2
=
ChurchNums_3x8_to_u24
x1
x3
⟶
False
Param
ChurchNums_8x3_to_3_lt7_id_ge7_rot2
:
(
(
(
ι
→
ι
) →
ι
→
ι
) →
(
(
ι
→
ι
) →
ι
→
ι
) →
(
(
ι
→
ι
) →
ι
→
ι
) →
(
(
ι
→
ι
) →
ι
→
ι
) →
(
(
ι
→
ι
) →
ι
→
ι
) →
(
(
ι
→
ι
) →
ι
→
ι
) →
(
(
ι
→
ι
) →
ι
→
ι
) →
CN (
ι
→
ι
)
) →
(
(
(
ι
→
ι
) →
ι
→
ι
) →
(
(
ι
→
ι
) →
ι
→
ι
) →
CN (
ι
→
ι
)
) →
(
(
ι
→
ι
) →
ι
→
ι
) →
(
(
ι
→
ι
) →
ι
→
ι
) →
CN (
ι
→
ι
)
Param
ChurchNums_8_perm_1_2_3_4_5_6_7_0
:
(
(
(
ι
→
ι
) →
ι
→
ι
) →
(
(
ι
→
ι
) →
ι
→
ι
) →
(
(
ι
→
ι
) →
ι
→
ι
) →
(
(
ι
→
ι
) →
ι
→
ι
) →
(
(
ι
→
ι
) →
ι
→
ι
) →
(
(
ι
→
ι
) →
ι
→
ι
) →
(
(
ι
→
ι
) →
ι
→
ι
) →
CN (
ι
→
ι
)
) →
(
(
ι
→
ι
) →
ι
→
ι
) →
(
(
ι
→
ι
) →
ι
→
ι
) →
(
(
ι
→
ι
) →
ι
→
ι
) →
(
(
ι
→
ι
) →
ι
→
ι
) →
(
(
ι
→
ι
) →
ι
→
ι
) →
(
(
ι
→
ι
) →
ι
→
ι
) →
(
(
ι
→
ι
) →
ι
→
ι
) →
CN (
ι
→
ι
)
Known
d7bcc..
:
∀ x0 x1 :
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
ι → ι
)
→
ι → ι
.
∀ x2 x3 :
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
ι → ι
)
→
ι → ι
.
ChurchNum_3ary_proj_p
x0
⟶
ChurchNum_8ary_proj_p
x2
⟶
ChurchNum_3ary_proj_p
x1
⟶
ChurchNum_8ary_proj_p
x3
⟶
(
TwoRamseyGraph_4_5_24_ChurchNums_3x8
x0
x2
x1
x3
=
λ x5 x6 .
x6
)
⟶
ChurchNums_3x8_to_u24
(
ChurchNums_8x3_to_3_lt7_id_ge7_rot2
x2
x0
)
(
ChurchNums_8_perm_1_2_3_4_5_6_7_0
x2
)
=
ChurchNums_3x8_to_u24
x1
x3
⟶
False
Known
b428c..
:
∀ x0 x1 :
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
ι → ι
)
→
ι → ι
.
∀ x2 x3 :
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
ι → ι
)
→
ι → ι
.
ChurchNum_3ary_proj_p
x0
⟶
ChurchNum_8ary_proj_p
x2
⟶
ChurchNum_3ary_proj_p
x1
⟶
ChurchNum_8ary_proj_p
x3
⟶
(
TwoRamseyGraph_4_5_24_ChurchNums_3x8
x0
x2
x1
x3
=
λ x5 x6 .
x6
)
⟶
ChurchNums_3x8_to_u24
(
ChurchNums_8x3_to_3_lt7_id_ge7_rot2
x2
x0
)
(
ChurchNums_8_perm_1_2_3_4_5_6_7_0
x2
)
=
ChurchNums_3x8_to_u24
(
ChurchNums_8x3_to_3_lt7_id_ge7_rot2
x3
x1
)
(
ChurchNums_8_perm_1_2_3_4_5_6_7_0
x3
)
⟶
False
Param
ChurchNums_8x3_to_3_lt6_id_ge6_rot2
:
(
(
(
ι
→
ι
) →
ι
→
ι
) →
(
(
ι
→
ι
) →
ι
→
ι
) →
(
(
ι
→
ι
) →
ι
→
ι
) →
(
(
ι
→
ι
) →
ι
→
ι
) →
(
(
ι
→
ι
) →
ι
→
ι
) →
(
(
ι
→
ι
) →
ι
→
ι
) →
(
(
ι
→
ι
) →
ι
→
ι
) →
CN (
ι
→
ι
)
) →
(
(
(
ι
→
ι
) →
ι
→
ι
) →
(
(
ι
→
ι
) →
ι
→
ι
) →
CN (
ι
→
ι
)
) →
(
(
ι
→
ι
) →
ι
→
ι
) →
(
(
ι
→
ι
) →
ι
→
ι
) →
CN (
ι
→
ι
)
Param
ChurchNums_8_perm_2_3_4_5_6_7_0_1
:
(
(
(
ι
→
ι
) →
ι
→
ι
) →
(
(
ι
→
ι
) →
ι
→
ι
) →
(
(
ι
→
ι
) →
ι
→
ι
) →
(
(
ι
→
ι
) →
ι
→
ι
) →
(
(
ι
→
ι
) →
ι
→
ι
) →
(
(
ι
→
ι
) →
ι
→
ι
) →
(
(
ι
→
ι
) →
ι
→
ι
) →
CN (
ι
→
ι
)
) →
(
(
ι
→
ι
) →
ι
→
ι
) →
(
(
ι
→
ι
) →
ι
→
ι
) →
(
(
ι
→
ι
) →
ι
→
ι
) →
(
(
ι
→
ι
) →
ι
→
ι
) →
(
(
ι
→
ι
) →
ι
→
ι
) →
(
(
ι
→
ι
) →
ι
→
ι
) →
(
(
ι
→
ι
) →
ι
→
ι
) →
CN (
ι
→
ι
)
Known
7787a..
:
∀ x0 x1 :
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
ι → ι
)
→
ι → ι
.
∀ x2 x3 :
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
ι → ι
)
→
ι → ι
.
ChurchNum_3ary_proj_p
x0
⟶
ChurchNum_8ary_proj_p
x2
⟶
ChurchNum_3ary_proj_p
x1
⟶
ChurchNum_8ary_proj_p
x3
⟶
(
TwoRamseyGraph_4_5_24_ChurchNums_3x8
x0
x2
x1
x3
=
λ x5 x6 .
x6
)
⟶
ChurchNums_3x8_to_u24
(
ChurchNums_8x3_to_3_lt6_id_ge6_rot2
x2
x0
)
(
ChurchNums_8_perm_2_3_4_5_6_7_0_1
x2
)
=
ChurchNums_3x8_to_u24
x1
x3
⟶
False
Known
f0975..
:
∀ x0 x1 :
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
ι → ι
)
→
ι → ι
.
∀ x2 x3 :
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
ι → ι
)
→
ι → ι
.
ChurchNum_3ary_proj_p
x0
⟶
ChurchNum_8ary_proj_p
x2
⟶
ChurchNum_3ary_proj_p
x1
⟶
ChurchNum_8ary_proj_p
x3
⟶
(
TwoRamseyGraph_4_5_24_ChurchNums_3x8
x0
x2
x1
x3
=
λ x5 x6 .
x6
)
⟶
ChurchNums_3x8_to_u24
(
ChurchNums_8x3_to_3_lt6_id_ge6_rot2
x2
x0
)
(
ChurchNums_8_perm_2_3_4_5_6_7_0_1
x2
)
=
ChurchNums_3x8_to_u24
(
ChurchNums_8x3_to_3_lt7_id_ge7_rot2
x3
x1
)
(
ChurchNums_8_perm_1_2_3_4_5_6_7_0
x3
)
⟶
False
Known
28750..
:
∀ x0 x1 :
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
ι → ι
)
→
ι → ι
.
∀ x2 x3 :
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
ι → ι
)
→
ι → ι
.
ChurchNum_3ary_proj_p
x0
⟶
ChurchNum_8ary_proj_p
x2
⟶
ChurchNum_3ary_proj_p
x1
⟶
ChurchNum_8ary_proj_p
x3
⟶
(
TwoRamseyGraph_4_5_24_ChurchNums_3x8
x0
x2
x1
x3
=
λ x5 x6 .
x6
)
⟶
ChurchNums_3x8_to_u24
(
ChurchNums_8x3_to_3_lt6_id_ge6_rot2
x2
x0
)
(
ChurchNums_8_perm_2_3_4_5_6_7_0_1
x2
)
=
ChurchNums_3x8_to_u24
(
ChurchNums_8x3_to_3_lt6_id_ge6_rot2
x3
x1
)
(
ChurchNums_8_perm_2_3_4_5_6_7_0_1
x3
)
⟶
False
Param
ChurchNums_8x3_to_3_lt5_id_ge5_rot2
:
(
(
(
ι
→
ι
) →
ι
→
ι
) →
(
(
ι
→
ι
) →
ι
→
ι
) →
(
(
ι
→
ι
) →
ι
→
ι
) →
(
(
ι
→
ι
) →
ι
→
ι
) →
(
(
ι
→
ι
) →
ι
→
ι
) →
(
(
ι
→
ι
) →
ι
→
ι
) →
(
(
ι
→
ι
) →
ι
→
ι
) →
CN (
ι
→
ι
)
) →
(
(
(
ι
→
ι
) →
ι
→
ι
) →
(
(
ι
→
ι
) →
ι
→
ι
) →
CN (
ι
→
ι
)
) →
(
(
ι
→
ι
) →
ι
→
ι
) →
(
(
ι
→
ι
) →
ι
→
ι
) →
CN (
ι
→
ι
)
Param
ChurchNums_8_perm_3_4_5_6_7_0_1_2
:
(
(
(
ι
→
ι
) →
ι
→
ι
) →
(
(
ι
→
ι
) →
ι
→
ι
) →
(
(
ι
→
ι
) →
ι
→
ι
) →
(
(
ι
→
ι
) →
ι
→
ι
) →
(
(
ι
→
ι
) →
ι
→
ι
) →
(
(
ι
→
ι
) →
ι
→
ι
) →
(
(
ι
→
ι
) →
ι
→
ι
) →
CN (
ι
→
ι
)
) →
(
(
ι
→
ι
) →
ι
→
ι
) →
(
(
ι
→
ι
) →
ι
→
ι
) →
(
(
ι
→
ι
) →
ι
→
ι
) →
(
(
ι
→
ι
) →
ι
→
ι
) →
(
(
ι
→
ι
) →
ι
→
ι
) →
(
(
ι
→
ι
) →
ι
→
ι
) →
(
(
ι
→
ι
) →
ι
→
ι
) →
CN (
ι
→
ι
)
Known
b9a6b..
:
∀ x0 x1 :
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
ι → ι
)
→
ι → ι
.
∀ x2 x3 :
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
ι → ι
)
→
ι → ι
.
ChurchNum_3ary_proj_p
x0
⟶
ChurchNum_8ary_proj_p
x2
⟶
ChurchNum_3ary_proj_p
x1
⟶
ChurchNum_8ary_proj_p
x3
⟶
(
TwoRamseyGraph_4_5_24_ChurchNums_3x8
x0
x2
x1
x3
=
λ x5 x6 .
x6
)
⟶
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
(
ChurchNums_8x3_to_3_lt7_id_ge7_rot2
x3
x1
)
(
ChurchNums_8_perm_1_2_3_4_5_6_7_0
x3
)
⟶
False
Known
e5001..
:
∀ x0 x1 :
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
ι → ι
)
→
ι → ι
.
∀ x2 x3 :
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
ι → ι
)
→
ι → ι
.
ChurchNum_3ary_proj_p
x0
⟶
ChurchNum_8ary_proj_p
x2
⟶
ChurchNum_3ary_proj_p
x1
⟶
ChurchNum_8ary_proj_p
x3
⟶
(
TwoRamseyGraph_4_5_24_ChurchNums_3x8
x0
x2
x1
x3
=
λ x5 x6 .
x6
)
⟶
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
(
ChurchNums_8x3_to_3_lt6_id_ge6_rot2
x3
x1
)
(
ChurchNums_8_perm_2_3_4_5_6_7_0_1
x3
)
⟶
False
Known
09666..
:
∀ x0 x1 :
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
ι → ι
)
→
ι → ι
.
∀ x2 x3 :
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
ι → ι
)
→
ι → ι
.
ChurchNum_3ary_proj_p
x0
⟶
ChurchNum_8ary_proj_p
x2
⟶
ChurchNum_3ary_proj_p
x1
⟶
ChurchNum_8ary_proj_p
x3
⟶
(
TwoRamseyGraph_4_5_24_ChurchNums_3x8
x0
x2
x1
x3
=
λ x5 x6 .
x6
)
⟶
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
(
ChurchNums_8x3_to_3_lt5_id_ge5_rot2
x3
x1
)
(
ChurchNums_8_perm_3_4_5_6_7_0_1_2
x3
)
⟶
False
Param
ChurchNums_8x3_to_3_lt4_id_ge4_rot2
:
(
(
(
ι
→
ι
) →
ι
→
ι
) →
(
(
ι
→
ι
) →
ι
→
ι
) →
(
(
ι
→
ι
) →
ι
→
ι
) →
(
(
ι
→
ι
) →
ι
→
ι
) →
(
(
ι
→
ι
) →
ι
→
ι
) →
(
(
ι
→
ι
) →
ι
→
ι
) →
(
(
ι
→
ι
) →
ι
→
ι
) →
CN (
ι
→
ι
)
) →
(
(
(
ι
→
ι
) →
ι
→
ι
) →
(
(
ι
→
ι
) →
ι
→
ι
) →
CN (
ι
→
ι
)
) →
(
(
ι
→
ι
) →
ι
→
ι
) →
(
(
ι
→
ι
) →
ι
→
ι
) →
CN (
ι
→
ι
)
Param
ChurchNums_8_perm_4_5_6_7_0_1_2_3
:
(
(
(
ι
→
ι
) →
ι
→
ι
) →
(
(
ι
→
ι
) →
ι
→
ι
) →
(
(
ι
→
ι
) →
ι
→
ι
) →
(
(
ι
→
ι
) →
ι
→
ι
) →
(
(
ι
→
ι
) →
ι
→
ι
) →
(
(
ι
→
ι
) →
ι
→
ι
) →
(
(
ι
→
ι
) →
ι
→
ι
) →
CN (
ι
→
ι
)
) →
(
(
ι
→
ι
) →
ι
→
ι
) →
(
(
ι
→
ι
) →
ι
→
ι
) →
(
(
ι
→
ι
) →
ι
→
ι
) →
(
(
ι
→
ι
) →
ι
→
ι
) →
(
(
ι
→
ι
) →
ι
→
ι
) →
(
(
ι
→
ι
) →
ι
→
ι
) →
(
(
ι
→
ι
) →
ι
→
ι
) →
CN (
ι
→
ι
)
Known
74048..
:
∀ x0 x1 :
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
ι → ι
)
→
ι → ι
.
∀ x2 x3 :
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
ι → ι
)
→
ι → ι
.
ChurchNum_3ary_proj_p
x0
⟶
ChurchNum_8ary_proj_p
x2
⟶
ChurchNum_3ary_proj_p
x1
⟶
ChurchNum_8ary_proj_p
x3
⟶
(
TwoRamseyGraph_4_5_24_ChurchNums_3x8
x0
x2
x1
x3
=
λ x5 x6 .
x6
)
⟶
ChurchNums_3x8_to_u24
(
ChurchNums_8x3_to_3_lt4_id_ge4_rot2
x2
x0
)
(
ChurchNums_8_perm_4_5_6_7_0_1_2_3
x2
)
=
ChurchNums_3x8_to_u24
x1
x3
⟶
False
Known
f9a56..
:
∀ x0 x1 :
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
ι → ι
)
→
ι → ι
.
∀ x2 x3 :
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
ι → ι
)
→
ι → ι
.
ChurchNum_3ary_proj_p
x0
⟶
ChurchNum_8ary_proj_p
x2
⟶
ChurchNum_3ary_proj_p
x1
⟶
ChurchNum_8ary_proj_p
x3
⟶
(
TwoRamseyGraph_4_5_24_ChurchNums_3x8
x0
x2
x1
x3
=
λ x5 x6 .
x6
)
⟶
ChurchNums_3x8_to_u24
(
ChurchNums_8x3_to_3_lt4_id_ge4_rot2
x2
x0
)
(
ChurchNums_8_perm_4_5_6_7_0_1_2_3
x2
)
=
ChurchNums_3x8_to_u24
(
ChurchNums_8x3_to_3_lt6_id_ge6_rot2
x3
x1
)
(
ChurchNums_8_perm_2_3_4_5_6_7_0_1
x3
)
⟶
False
Known
9b117..
:
∀ x0 x1 :
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
ι → ι
)
→
ι → ι
.
∀ x2 x3 :
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
ι → ι
)
→
ι → ι
.
ChurchNum_3ary_proj_p
x0
⟶
ChurchNum_8ary_proj_p
x2
⟶
ChurchNum_3ary_proj_p
x1
⟶
ChurchNum_8ary_proj_p
x3
⟶
(
TwoRamseyGraph_4_5_24_ChurchNums_3x8
x0
x2
x1
x3
=
λ x5 x6 .
x6
)
⟶
ChurchNums_3x8_to_u24
(
ChurchNums_8x3_to_3_lt4_id_ge4_rot2
x2
x0
)
(
ChurchNums_8_perm_4_5_6_7_0_1_2_3
x2
)
=
ChurchNums_3x8_to_u24
(
ChurchNums_8x3_to_3_lt5_id_ge5_rot2
x3
x1
)
(
ChurchNums_8_perm_3_4_5_6_7_0_1_2
x3
)
⟶
False
Known
9fd37..
:
∀ x0 x1 :
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
ι → ι
)
→
ι → ι
.
∀ x2 x3 :
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
ι → ι
)
→
ι → ι
.
ChurchNum_3ary_proj_p
x0
⟶
ChurchNum_8ary_proj_p
x2
⟶
ChurchNum_3ary_proj_p
x1
⟶
ChurchNum_8ary_proj_p
x3
⟶
(
TwoRamseyGraph_4_5_24_ChurchNums_3x8
x0
x2
x1
x3
=
λ x5 x6 .
x6
)
⟶
ChurchNums_3x8_to_u24
(
ChurchNums_8x3_to_3_lt4_id_ge4_rot2
x2
x0
)
(
ChurchNums_8_perm_4_5_6_7_0_1_2_3
x2
)
=
ChurchNums_3x8_to_u24
(
ChurchNums_8x3_to_3_lt4_id_ge4_rot2
x3
x1
)
(
ChurchNums_8_perm_4_5_6_7_0_1_2_3
x3
)
⟶
False
Definition
and
and
:=
λ x0 x1 : ο .
∀ x2 : ο .
(
x0
⟶
x1
⟶
x2
)
⟶
x2
Known
85ac5..
:
∀ x0 x1 :
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
ι → ι
)
→
ι → ι
.
∀ x2 x3 :
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
ι → ι
)
→
ι → ι
.
ChurchNum_3ary_proj_p
x0
⟶
ChurchNum_8ary_proj_p
x2
⟶
ChurchNum_3ary_proj_p
x1
⟶
ChurchNum_8ary_proj_p
x3
⟶
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
⟶
and
(
x1
=
ChurchNums_8x3_to_3_lt5_id_ge5_rot2
x2
x0
)
(
x3
=
ChurchNums_8_perm_3_4_5_6_7_0_1_2
x2
)
Known
bae77..
:
∀ x0 x1 :
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
ι → ι
)
→
ι → ι
.
∀ x2 x3 :
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
ι → ι
)
→
ι → ι
.
ChurchNum_3ary_proj_p
x0
⟶
ChurchNum_8ary_proj_p
x2
⟶
ChurchNum_3ary_proj_p
x1
⟶
ChurchNum_8ary_proj_p
x3
⟶
ChurchNums_3x8_to_u24
(
ChurchNums_8x3_to_3_lt4_id_ge4_rot2
x2
x0
)
(
ChurchNums_8_perm_4_5_6_7_0_1_2_3
x2
)
=
ChurchNums_3x8_to_u24
(
ChurchNums_8x3_to_3_lt7_id_ge7_rot2
x3
x1
)
(
ChurchNums_8_perm_1_2_3_4_5_6_7_0
x3
)
⟶
and
(
x1
=
ChurchNums_8x3_to_3_lt5_id_ge5_rot2
x2
x0
)
(
x3
=
ChurchNums_8_perm_3_4_5_6_7_0_1_2
x2
)
Param
ap
ap
:
ι
→
ι
→
ι
Param
ordsucc
ordsucc
:
ι
→
ι
Definition
u1
:=
1
Definition
u2
:=
ordsucc
u1
Definition
u3
:=
ordsucc
u2
Definition
u4
:=
ordsucc
u3
Definition
u5
:=
ordsucc
u4
Known
99cbf..
:
∀ 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
Param
lam
Sigma
:
ι
→
(
ι
→
ι
) →
ι
Param
If_i
If_i
:
ο
→
ι
→
ι
→
ι
Param
ordinal
ordinal
:
ι
→
ο
Known
ordinal_trichotomy_or_impred
ordinal_trichotomy_or_impred
:
∀ x0 x1 .
ordinal
x0
⟶
ordinal
x1
⟶
∀ x2 : ο .
(
x0
∈
x1
⟶
x2
)
⟶
(
x0
=
x1
⟶
x2
)
⟶
(
x1
∈
x0
⟶
x2
)
⟶
x2
Param
nat_p
nat_p
:
ι
→
ο
Known
nat_p_ordinal
nat_p_ordinal
:
∀ x0 .
nat_p
x0
⟶
ordinal
x0
Known
nat_p_trans
nat_p_trans
:
∀ x0 .
nat_p
x0
⟶
∀ x1 .
x1
∈
x0
⟶
nat_p
x1
Known
nat_5
nat_5
:
nat_p
5
Known
f60cd..
:
∀ x0 x1 :
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
ι → ι
)
→
ι → ι
.
∀ x2 x3 :
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
ι → ι
)
→
ι → ι
.
ChurchNum_3ary_proj_p
x0
⟶
ChurchNum_3ary_proj_p
x1
⟶
ChurchNum_8ary_proj_p
x2
⟶
ChurchNum_8ary_proj_p
x3
⟶
TwoRamseyGraph_4_5_24_ChurchNums_3x8
x0
x2
x1
x3
=
TwoRamseyGraph_4_5_24_ChurchNums_3x8
x1
x3
x0
x2
Known
cases_5
cases_5
:
∀ x0 .
x0
∈
5
⟶
∀ x1 :
ι → ο
.
x1
0
⟶
x1
1
⟶
x1
2
⟶
x1
3
⟶
x1
4
⟶
x1
x0
Known
tuple_5_0_eq
tuple_5_0_eq
:
∀ x0 x1 x2 x3 x4 .
ap
(
lam
5
(
λ x6 .
If_i
(
x6
=
0
)
x0
(
If_i
(
x6
=
1
)
x1
(
If_i
(
x6
=
2
)
x2
(
If_i
(
x6
=
3
)
x3
x4
)
)
)
)
)
0
=
x0
Known
FalseE
FalseE
:
False
⟶
∀ x0 : ο .
x0
Known
tuple_5_1_eq
tuple_5_1_eq
:
∀ x0 x1 x2 x3 x4 .
ap
(
lam
5
(
λ x6 .
If_i
(
x6
=
0
)
x0
(
If_i
(
x6
=
1
)
x1
(
If_i
(
x6
=
2
)
x2
(
If_i
(
x6
=
3
)
x3
x4
)
)
)
)
)
1
=
x1
Known
tuple_5_2_eq
tuple_5_2_eq
:
∀ x0 x1 x2 x3 x4 .
ap
(
lam
5
(
λ x6 .
If_i
(
x6
=
0
)
x0
(
If_i
(
x6
=
1
)
x1
(
If_i
(
x6
=
2
)
x2
(
If_i
(
x6
=
3
)
x3
x4
)
)
)
)
)
2
=
x2
Known
tuple_5_3_eq
tuple_5_3_eq
:
∀ x0 x1 x2 x3 x4 .
ap
(
lam
5
(
λ x6 .
If_i
(
x6
=
0
)
x0
(
If_i
(
x6
=
1
)
x1
(
If_i
(
x6
=
2
)
x2
(
If_i
(
x6
=
3
)
x3
x4
)
)
)
)
)
3
=
x3
Known
tuple_5_4_eq
tuple_5_4_eq
:
∀ x0 x1 x2 x3 x4 .
ap
(
lam
5
(
λ x6 .
If_i
(
x6
=
0
)
x0
(
If_i
(
x6
=
1
)
x1
(
If_i
(
x6
=
2
)
x2
(
If_i
(
x6
=
3
)
x3
x4
)
)
)
)
)
4
=
x4
Definition
not
not
:=
λ x0 : ο .
x0
⟶
False
Definition
nIn
nIn
:=
λ x0 x1 .
not
(
x0
∈
x1
)
Known
EmptyE
EmptyE
:
∀ x0 .
nIn
x0
0
Known
cases_1
cases_1
:
∀ x0 .
x0
∈
1
⟶
∀ x1 :
ι → ο
.
x1
0
⟶
x1
x0
Known
cases_2
cases_2
:
∀ x0 .
x0
∈
2
⟶
∀ x1 :
ι → ο
.
x1
0
⟶
x1
1
⟶
x1
x0
Known
cases_3
cases_3
:
∀ x0 .
x0
∈
3
⟶
∀ x1 :
ι → ο
.
x1
0
⟶
x1
1
⟶
x1
2
⟶
x1
x0
Known
cases_4
cases_4
:
∀ x0 .
x0
∈
4
⟶
∀ x1 :
ι → ο
.
x1
0
⟶
x1
1
⟶
x1
2
⟶
x1
3
⟶
x1
x0
Known
8f0b2..
:
∀ x0 :
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
ι → ι
)
→
ι → ι
.
∀ x1 :
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
ι → ι
)
→
ι → ι
.
ChurchNum_3ary_proj_p
x0
⟶
ChurchNum_8ary_proj_p
x1
⟶
ChurchNums_3x8_to_u24
(
ChurchNums_8x3_to_3_lt7_id_ge7_rot2
x1
x0
)
(
ChurchNums_8_perm_1_2_3_4_5_6_7_0
x1
)
=
ChurchNums_3x8_to_u24
x0
x1
⟶
∀ x2 : ο .
x2
Known
7bf94..
:
∀ x0 :
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
ι → ι
)
→
ι → ι
.
∀ x1 :
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
ι → ι
)
→
ι → ι
.
ChurchNum_3ary_proj_p
x0
⟶
ChurchNum_8ary_proj_p
x1
⟶
ChurchNums_3x8_to_u24
(
ChurchNums_8x3_to_3_lt6_id_ge6_rot2
x1
x0
)
(
ChurchNums_8_perm_2_3_4_5_6_7_0_1
x1
)
=
ChurchNums_3x8_to_u24
x0
x1
⟶
∀ x2 : ο .
x2
Known
471b2..
:
∀ x0 :
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
ι → ι
)
→
ι → ι
.
∀ x1 :
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
ι → ι
)
→
ι → ι
.
ChurchNum_3ary_proj_p
x0
⟶
ChurchNum_8ary_proj_p
x1
⟶
ChurchNums_3x8_to_u24
(
ChurchNums_8x3_to_3_lt6_id_ge6_rot2
x1
x0
)
(
ChurchNums_8_perm_2_3_4_5_6_7_0_1
x1
)
=
ChurchNums_3x8_to_u24
(
ChurchNums_8x3_to_3_lt7_id_ge7_rot2
x1
x0
)
(
ChurchNums_8_perm_1_2_3_4_5_6_7_0
x1
)
⟶
∀ x2 : ο .
x2
Known
a9b55..
:
∀ x0 :
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
ι → ι
)
→
ι → ι
.
∀ x1 :
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
ι → ι
)
→
ι → ι
.
ChurchNum_3ary_proj_p
x0
⟶
ChurchNum_8ary_proj_p
x1
⟶
ChurchNums_3x8_to_u24
(
ChurchNums_8x3_to_3_lt5_id_ge5_rot2
x1
x0
)
(
ChurchNums_8_perm_3_4_5_6_7_0_1_2
x1
)
=
ChurchNums_3x8_to_u24
x0
x1
⟶
∀ x2 : ο .
x2
Known
08b75..
:
∀ x0 :
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
ι → ι
)
→
ι → ι
.
∀ x1 :
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
ι → ι
)
→
ι → ι
.
ChurchNum_3ary_proj_p
x0
⟶
ChurchNum_8ary_proj_p
x1
⟶
ChurchNums_3x8_to_u24
(
ChurchNums_8x3_to_3_lt5_id_ge5_rot2
x1
x0
)
(
ChurchNums_8_perm_3_4_5_6_7_0_1_2
x1
)
=
ChurchNums_3x8_to_u24
(
ChurchNums_8x3_to_3_lt7_id_ge7_rot2
x1
x0
)
(
ChurchNums_8_perm_1_2_3_4_5_6_7_0
x1
)
⟶
∀ x2 : ο .
x2
Known
373fc..
:
∀ x0 :
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
ι → ι
)
→
ι → ι
.
∀ x1 :
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
ι → ι
)
→
ι → ι
.
ChurchNum_3ary_proj_p
x0
⟶
ChurchNum_8ary_proj_p
x1
⟶
ChurchNums_3x8_to_u24
(
ChurchNums_8x3_to_3_lt5_id_ge5_rot2
x1
x0
)
(
ChurchNums_8_perm_3_4_5_6_7_0_1_2
x1
)
=
ChurchNums_3x8_to_u24
(
ChurchNums_8x3_to_3_lt6_id_ge6_rot2
x1
x0
)
(
ChurchNums_8_perm_2_3_4_5_6_7_0_1
x1
)
⟶
∀ x2 : ο .
x2
Known
d6534..
:
∀ x0 :
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
ι → ι
)
→
ι → ι
.
∀ x1 :
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
ι → ι
)
→
ι → ι
.
ChurchNum_3ary_proj_p
x0
⟶
ChurchNum_8ary_proj_p
x1
⟶
ChurchNums_3x8_to_u24
(
ChurchNums_8x3_to_3_lt4_id_ge4_rot2
x1
x0
)
(
ChurchNums_8_perm_4_5_6_7_0_1_2_3
x1
)
=
ChurchNums_3x8_to_u24
x0
x1
⟶
∀ x2 : ο .
x2
Known
83ebc..
:
∀ x0 :
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
ι → ι
)
→
ι → ι
.
∀ x1 :
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
ι → ι
)
→
ι → ι
.
ChurchNum_3ary_proj_p
x0
⟶
ChurchNum_8ary_proj_p
x1
⟶
ChurchNums_3x8_to_u24
(
ChurchNums_8x3_to_3_lt4_id_ge4_rot2
x1
x0
)
(
ChurchNums_8_perm_4_5_6_7_0_1_2_3
x1
)
=
ChurchNums_3x8_to_u24
(
ChurchNums_8x3_to_3_lt7_id_ge7_rot2
x1
x0
)
(
ChurchNums_8_perm_1_2_3_4_5_6_7_0
x1
)
⟶
∀ x2 : ο .
x2
Known
290ad..
:
∀ x0 :
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
ι → ι
)
→
ι → ι
.
∀ x1 :
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
ι → ι
)
→
ι → ι
.
ChurchNum_3ary_proj_p
x0
⟶
ChurchNum_8ary_proj_p
x1
⟶
ChurchNums_3x8_to_u24
(
ChurchNums_8x3_to_3_lt4_id_ge4_rot2
x1
x0
)
(
ChurchNums_8_perm_4_5_6_7_0_1_2_3
x1
)
=
ChurchNums_3x8_to_u24
(
ChurchNums_8x3_to_3_lt6_id_ge6_rot2
x1
x0
)
(
ChurchNums_8_perm_2_3_4_5_6_7_0_1
x1
)
⟶
∀ x2 : ο .
x2
Known
987aa..
:
∀ x0 :
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
ι → ι
)
→
ι → ι
.
∀ x1 :
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
ι → ι
)
→
ι → ι
.
ChurchNum_3ary_proj_p
x0
⟶
ChurchNum_8ary_proj_p
x1
⟶
ChurchNums_3x8_to_u24
(
ChurchNums_8x3_to_3_lt4_id_ge4_rot2
x1
x0
)
(
ChurchNums_8_perm_4_5_6_7_0_1_2_3
x1
)
=
ChurchNums_3x8_to_u24
(
ChurchNums_8x3_to_3_lt5_id_ge5_rot2
x1
x0
)
(
ChurchNums_8_perm_3_4_5_6_7_0_1_2
x1
)
⟶
∀ x2 : ο .
x2
Theorem
165ef..
:
∀ 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
)
⟶
False
(proof)
Definition
Subq
Subq
:=
λ x0 x1 .
∀ x2 .
x2
∈
x0
⟶
x2
∈
x1
Definition
u6
:=
ordsucc
u5
Definition
u7
:=
ordsucc
u6
Definition
u8
:=
ordsucc
u7
Definition
u9
:=
ordsucc
u8
Definition
u10
:=
ordsucc
u9
Definition
u11
:=
ordsucc
u10
Definition
u12
:=
ordsucc
u11
Definition
u13
:=
ordsucc
u12
Definition
u14
:=
ordsucc
u13
Definition
u15
:=
ordsucc
u14
Definition
u16
:=
ordsucc
u15
Definition
u17
:=
ordsucc
u16
Definition
u18
:=
ordsucc
u17
Definition
u19
:=
ordsucc
u18
Definition
u20
:=
ordsucc
u19
Definition
u21
:=
ordsucc
u20
Definition
u22
:=
ordsucc
u21
Definition
u23
:=
ordsucc
u22
Definition
u24
:=
ordsucc
u23
Param
atleastp
atleastp
:
ι
→
ι
→
ο
Definition
TwoRamseyGraph_4_5_24
:=
λ x0 x1 .
∀ x2 x3 :
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
ι → ι
)
→
ι → ι
.
∀ x4 x5 :
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
ι → ι
)
→
ι → ι
.
ChurchNum_3ary_proj_p
x2
⟶
ChurchNum_3ary_proj_p
x3
⟶
ChurchNum_8ary_proj_p
x4
⟶
ChurchNum_8ary_proj_p
x5
⟶
x0
=
x2
(
λ x7 :
ι → ι
.
λ x8 .
x8
)
(
λ x7 :
ι → ι
.
λ x8 .
x7
(
x7
(
x7
(
x7
(
x7
(
x7
(
x7
(
x7
x8
)
)
)
)
)
)
)
)
(
λ x7 :
ι → ι
.
λ x8 .
x7
(
x7
(
x7
(
x7
(
x7
(
x7
(
x7
(
x7
(
x7
(
x7
(
x7
(
x7
(
x7
(
x7
(
x7
(
x7
x8
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
ordsucc
(
x4
(
λ x7 :
ι → ι
.
λ x8 .
x8
)
(
λ x7 :
ι → ι
.
x7
)
(
λ x7 :
ι → ι
.
λ x8 .
x7
(
x7
x8
)
)
(
λ x7 :
ι → ι
.
λ x8 .
x7
(
x7
(
x7
x8
)
)
)
(
λ x7 :
ι → ι
.
λ x8 .
x7
(
x7
(
x7
(
x7
x8
)
)
)
)
(
λ x7 :
ι → ι
.
λ x8 .
x7
(
x7
(
x7
(
x7
(
x7
x8
)
)
)
)
)
(
λ x7 :
ι → ι
.
λ x8 .
x7
(
x7
(
x7
(
x7
(
x7
(
x7
x8
)
)
)
)
)
)
(
λ x7 :
ι → ι
.
λ x8 .
x7
(
x7
(
x7
(
x7
(
x7
(
x7
(
x7
x8
)
)
)
)
)
)
)
ordsucc
0
)
⟶
x1
=
x3
(
λ x7 :
ι → ι
.
λ x8 .
x8
)
(
λ x7 :
ι → ι
.
λ x8 .
x7
(
x7
(
x7
(
x7
(
x7
(
x7
(
x7
(
x7
x8
)
)
)
)
)
)
)
)
(
λ x7 :
ι → ι
.
λ x8 .
x7
(
x7
(
x7
(
x7
(
x7
(
x7
(
x7
(
x7
(
x7
(
x7
(
x7
(
x7
(
x7
(
x7
(
x7
(
x7
x8
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
ordsucc
(
x5
(
λ x7 :
ι → ι
.
λ x8 .
x8
)
(
λ x7 :
ι → ι
.
x7
)
(
λ x7 :
ι → ι
.
λ x8 .
x7
(
x7
x8
)
)
(
λ x7 :
ι → ι
.
λ x8 .
x7
(
x7
(
x7
x8
)
)
)
(
λ x7 :
ι → ι
.
λ x8 .
x7
(
x7
(
x7
(
x7
x8
)
)
)
)
(
λ x7 :
ι → ι
.
λ x8 .
x7
(
x7
(
x7
(
x7
(
x7
x8
)
)
)
)
)
(
λ x7 :
ι → ι
.
λ x8 .
x7
(
x7
(
x7
(
x7
(
x7
(
x7
x8
)
)
)
)
)
)
(
λ x7 :
ι → ι
.
λ x8 .
x7
(
x7
(
x7
(
x7
(
x7
(
x7
(
x7
x8
)
)
)
)
)
)
)
ordsucc
0
)
⟶
TwoRamseyGraph_4_5_24_ChurchNums_3x8
x2
x4
x3
x5
=
λ x7 x8 .
x7
Known
3ed86..
:
∀ x0 .
atleastp
u5
x0
⟶
∀ x1 : ο .
(
∀ x2 .
x2
∈
x0
⟶
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
(
x2
=
x3
⟶
∀ x7 : ο .
x7
)
⟶
(
x2
=
x4
⟶
∀ x7 : ο .
x7
)
⟶
(
x2
=
x5
⟶
∀ x7 : ο .
x7
)
⟶
(
x2
=
x6
⟶
∀ x7 : ο .
x7
)
⟶
(
x3
=
x4
⟶
∀ x7 : ο .
x7
)
⟶
(
x3
=
x5
⟶
∀ x7 : ο .
x7
)
⟶
(
x3
=
x6
⟶
∀ x7 : ο .
x7
)
⟶
(
x4
=
x5
⟶
∀ x7 : ο .
x7
)
⟶
(
x4
=
x6
⟶
∀ x7 : ο .
x7
)
⟶
(
x5
=
x6
⟶
∀ x7 : ο .
x7
)
⟶
x1
)
⟶
x1
Known
4f390..
:
∀ x0 .
x0
∈
u24
⟶
∀ x1 : ο .
(
∀ x2 :
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
ι → ι
)
→
ι → ι
.
∀ x3 :
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
ι → ι
)
→
ι → ι
.
ChurchNum_3ary_proj_p
x2
⟶
ChurchNum_8ary_proj_p
x3
⟶
x0
=
x2
(
λ x5 :
ι → ι
.
λ x6 .
x6
)
(
λ x5 :
ι → ι
.
λ x6 .
x5
(
x5
(
x5
(
x5
(
x5
(
x5
(
x5
(
x5
x6
)
)
)
)
)
)
)
)
(
λ x5 :
ι → ι
.
λ x6 .
x5
(
x5
(
x5
(
x5
(
x5
(
x5
(
x5
(
x5
(
x5
(
x5
(
x5
(
x5
(
x5
(
x5
(
x5
(
x5
x6
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
ordsucc
(
x3
(
λ x5 :
ι → ι
.
λ x6 .
x6
)
(
λ x5 :
ι → ι
.
x5
)
(
λ x5 :
ι → ι
.
λ x6 .
x5
(
x5
x6
)
)
(
λ x5 :
ι → ι
.
λ x6 .
x5
(
x5
(
x5
x6
)
)
)
(
λ x5 :
ι → ι
.
λ x6 .
x5
(
x5
(
x5
(
x5
x6
)
)
)
)
(
λ x5 :
ι → ι
.
λ x6 .
x5
(
x5
(
x5
(
x5
(
x5
x6
)
)
)
)
)
(
λ x5 :
ι → ι
.
λ x6 .
x5
(
x5
(
x5
(
x5
(
x5
(
x5
x6
)
)
)
)
)
)
(
λ x5 :
ι → ι
.
λ x6 .
x5
(
x5
(
x5
(
x5
(
x5
(
x5
(
x5
x6
)
)
)
)
)
)
)
ordsucc
0
)
⟶
x1
)
⟶
x1
Definition
or
or
:=
λ x0 x1 : ο .
∀ x2 : ο .
(
x0
⟶
x2
)
⟶
(
x1
⟶
x2
)
⟶
x2
Known
7f11d..
:
∀ x0 x1 :
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
ι → ι
)
→
ι → ι
.
∀ x2 x3 :
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
ι → ι
)
→
ι → ι
.
ChurchNum_3ary_proj_p
x0
⟶
ChurchNum_3ary_proj_p
x1
⟶
ChurchNum_8ary_proj_p
x2
⟶
ChurchNum_8ary_proj_p
x3
⟶
or
(
TwoRamseyGraph_4_5_24_ChurchNums_3x8
x0
x2
x1
x3
=
λ x5 x6 .
x5
)
(
TwoRamseyGraph_4_5_24_ChurchNums_3x8
x0
x2
x1
x3
=
λ x5 x6 .
x6
)
Known
bebde..
:
∀ x0 x1 :
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
ι → ι
)
→
ι → ι
.
∀ x2 x3 :
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
ι → ι
)
→
ι → ι
.
ChurchNum_3ary_proj_p
x0
⟶
ChurchNum_3ary_proj_p
x1
⟶
ChurchNum_8ary_proj_p
x2
⟶
ChurchNum_8ary_proj_p
x3
⟶
x0
(
λ x5 :
ι → ι
.
λ x6 .
x6
)
(
λ x5 :
ι → ι
.
λ x6 .
x5
(
x5
(
x5
(
x5
(
x5
(
x5
(
x5
(
x5
x6
)
)
)
)
)
)
)
)
(
λ x5 :
ι → ι
.
λ x6 .
x5
(
x5
(
x5
(
x5
(
x5
(
x5
(
x5
(
x5
(
x5
(
x5
(
x5
(
x5
(
x5
(
x5
(
x5
(
x5
x6
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
ordsucc
(
x2
(
λ x5 :
ι → ι
.
λ x6 .
x6
)
(
λ x5 :
ι → ι
.
x5
)
(
λ x5 :
ι → ι
.
λ x6 .
x5
(
x5
x6
)
)
(
λ x5 :
ι → ι
.
λ x6 .
x5
(
x5
(
x5
x6
)
)
)
(
λ x5 :
ι → ι
.
λ x6 .
x5
(
x5
(
x5
(
x5
x6
)
)
)
)
(
λ x5 :
ι → ι
.
λ x6 .
x5
(
x5
(
x5
(
x5
(
x5
x6
)
)
)
)
)
(
λ x5 :
ι → ι
.
λ x6 .
x5
(
x5
(
x5
(
x5
(
x5
(
x5
x6
)
)
)
)
)
)
(
λ x5 :
ι → ι
.
λ x6 .
x5
(
x5
(
x5
(
x5
(
x5
(
x5
(
x5
x6
)
)
)
)
)
)
)
ordsucc
0
)
=
x1
(
λ x5 :
ι → ι
.
λ x6 .
x6
)
(
λ x5 :
ι → ι
.
λ x6 .
x5
(
x5
(
x5
(
x5
(
x5
(
x5
(
x5
(
x5
x6
)
)
)
)
)
)
)
)
(
λ x5 :
ι → ι
.
λ x6 .
x5
(
x5
(
x5
(
x5
(
x5
(
x5
(
x5
(
x5
(
x5
(
x5
(
x5
(
x5
(
x5
(
x5
(
x5
(
x5
x6
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
ordsucc
(
x3
(
λ x5 :
ι → ι
.
λ x6 .
x6
)
(
λ x5 :
ι → ι
.
x5
)
(
λ x5 :
ι → ι
.
λ x6 .
x5
(
x5
x6
)
)
(
λ x5 :
ι → ι
.
λ x6 .
x5
(
x5
(
x5
x6
)
)
)
(
λ x5 :
ι → ι
.
λ x6 .
x5
(
x5
(
x5
(
x5
x6
)
)
)
)
(
λ x5 :
ι → ι
.
λ x6 .
x5
(
x5
(
x5
(
x5
(
x5
x6
)
)
)
)
)
(
λ x5 :
ι → ι
.
λ x6 .
x5
(
x5
(
x5
(
x5
(
x5
(
x5
x6
)
)
)
)
)
)
(
λ x5 :
ι → ι
.
λ x6 .
x5
(
x5
(
x5
(
x5
(
x5
(
x5
(
x5
x6
)
)
)
)
)
)
)
ordsucc
0
)
⟶
and
(
x0
=
x1
)
(
x2
=
x3
)
Theorem
6af4c..
:
∀ x0 .
x0
⊆
u24
⟶
atleastp
u5
x0
⟶
not
(
∀ x1 .
x1
∈
x0
⟶
∀ x2 .
x2
∈
x0
⟶
(
x1
=
x2
⟶
∀ x3 : ο .
x3
)
⟶
not
(
TwoRamseyGraph_4_5_24
x1
x2
)
)
(proof)
Definition
TwoRamseyProp_atleastp
:=
λ x0 x1 x2 .
∀ x3 :
ι →
ι → ο
.
(
∀ x4 x5 .
x3
x4
x5
⟶
x3
x5
x4
)
⟶
or
(
∀ x4 : ο .
(
∀ x5 .
and
(
x5
⊆
x2
)
(
and
(
atleastp
x0
x5
)
(
∀ x6 .
x6
∈
x5
⟶
∀ x7 .
x7
∈
x5
⟶
(
x6
=
x7
⟶
∀ x8 : ο .
x8
)
⟶
x3
x6
x7
)
)
⟶
x4
)
⟶
x4
)
(
∀ x4 : ο .
(
∀ x5 .
and
(
x5
⊆
x2
)
(
and
(
atleastp
x1
x5
)
(
∀ x6 .
x6
∈
x5
⟶
∀ x7 .
x7
∈
x5
⟶
(
x6
=
x7
⟶
∀ x8 : ο .
x8
)
⟶
not
(
x3
x6
x7
)
)
)
⟶
x4
)
⟶
x4
)
Known
9303b..
:
∀ x0 x1 .
TwoRamseyGraph_4_5_24
x0
x1
⟶
TwoRamseyGraph_4_5_24
x1
x0
Known
51a60..
:
∀ x0 .
x0
⊆
u24
⟶
atleastp
u4
x0
⟶
not
(
∀ x1 .
x1
∈
x0
⟶
∀ x2 .
x2
∈
x0
⟶
(
x1
=
x2
⟶
∀ x3 : ο .
x3
)
⟶
TwoRamseyGraph_4_5_24
x1
x2
)
Theorem
not_TwoRamseyProp_atleast_4_5_24
:
not
(
TwoRamseyProp_atleastp
4
5
24
)
(proof)
Param
TwoRamseyProp
TwoRamseyProp
:
ι
→
ι
→
ι
→
ο
Known
TwoRamseyProp_atleastp_atleastp
:
∀ x0 x1 x2 x3 x4 .
TwoRamseyProp
x0
x2
x4
⟶
atleastp
x1
x0
⟶
atleastp
x3
x2
⟶
TwoRamseyProp_atleastp
x1
x3
x4
Known
atleastp_ref
:
∀ x0 .
atleastp
x0
x0
Theorem
not_TwoRamseyProp_4_5_24
not_TwoRamseyProp_4_5_24
:
not
(
TwoRamseyProp
4
5
24
)
(proof)