Search for blocks/addresses/...
Proofgold Address
address
PUeLQfL2tiWRZ44GpDHJ2HyjUcFETS7nJ9r
total
0
mg
-
conjpub
-
current assets
65681..
/
d3ce9..
bday:
19014
doc published by
Pr4zB..
Param
u17
:
ι
Param
Church17_p
:
(
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
) →
ο
Param
TwoRamseyGraph_3_6_Church17
:
(
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
) →
(
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
) →
ι
→
ι
→
ι
Definition
Subq
Subq
:=
λ x0 x1 .
∀ x2 .
x2
∈
x0
⟶
x2
∈
x1
Param
atleastp
atleastp
:
ι
→
ι
→
ο
Param
ordsucc
ordsucc
:
ι
→
ι
Definition
u1
:=
1
Definition
u2
:=
ordsucc
u1
Definition
u3
:=
ordsucc
u2
Definition
False
False
:=
∀ x0 : ο .
x0
Definition
not
not
:=
λ x0 : ο .
x0
⟶
False
Known
f03aa..
:
∀ x0 .
atleastp
3
x0
⟶
∀ x1 : ο .
(
∀ x2 .
x2
∈
x0
⟶
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
(
x2
=
x3
⟶
∀ x5 : ο .
x5
)
⟶
(
x2
=
x4
⟶
∀ x5 : ο .
x5
)
⟶
(
x3
=
x4
⟶
∀ x5 : ο .
x5
)
⟶
x1
)
⟶
x1
Known
90040..
:
∀ x0 x1 x2 :
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι → ι
.
Church17_p
x0
⟶
Church17_p
x1
⟶
Church17_p
x2
⟶
(
x0
=
x1
⟶
∀ x3 : ο .
x3
)
⟶
(
x0
=
x2
⟶
∀ x3 : ο .
x3
)
⟶
(
x1
=
x2
⟶
∀ x3 : ο .
x3
)
⟶
(
TwoRamseyGraph_3_6_Church17
x0
x1
=
λ x4 x5 .
x4
)
⟶
(
TwoRamseyGraph_3_6_Church17
x0
x2
=
λ x4 x5 .
x4
)
⟶
(
TwoRamseyGraph_3_6_Church17
x1
x2
=
λ x4 x5 .
x4
)
⟶
False
Theorem
12554..
:
∀ x0 :
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι → ι
.
(
∀ x1 .
x1
∈
u17
⟶
Church17_p
(
x0
x1
)
)
⟶
(
∀ x1 .
x1
∈
u17
⟶
∀ x2 .
x2
∈
u17
⟶
x0
x1
=
x0
x2
⟶
x1
=
x2
)
⟶
∀ x1 :
ι →
ι → ο
.
(
∀ x2 x3 .
x1
x2
x3
⟶
x2
∈
u17
⟶
x3
∈
u17
⟶
TwoRamseyGraph_3_6_Church17
(
x0
x2
)
(
x0
x3
)
=
λ x5 x6 .
x5
)
⟶
∀ x2 .
x2
⊆
u17
⟶
atleastp
u3
x2
⟶
not
(
∀ x3 .
x3
∈
x2
⟶
∀ x4 .
x4
∈
x2
⟶
(
x3
=
x4
⟶
∀ x5 : ο .
x5
)
⟶
x1
x3
x4
)
...
previous assets