Search for blocks/addresses/...
Proofgold Address
address
PUPVJnzmcVeRzW3gFyPpru7Uymr8ZEkrHWi
total
0
mg
-
conjpub
-
current assets
473ea..
/
d625e..
bday:
18387
doc published by
Pr4zB..
Param
u24
:
ι
Param
ChurchNum_3ary_proj_p
:
(
(
(
ι
→
ι
) →
ι
→
ι
) →
(
(
ι
→
ι
) →
ι
→
ι
) →
CN (
ι
→
ι
)
) →
ο
Param
ChurchNum_8ary_proj_p
:
(
(
(
ι
→
ι
) →
ι
→
ι
) →
(
(
ι
→
ι
) →
ι
→
ι
) →
(
(
ι
→
ι
) →
ι
→
ι
) →
(
(
ι
→
ι
) →
ι
→
ι
) →
(
(
ι
→
ι
) →
ι
→
ι
) →
(
(
ι
→
ι
) →
ι
→
ι
) →
(
(
ι
→
ι
) →
ι
→
ι
) →
CN (
ι
→
ι
)
) →
ο
Param
ordsucc
ordsucc
:
ι
→
ι
Definition
u1
:=
1
Definition
u2
:=
ordsucc
u1
Definition
u3
:=
ordsucc
u2
Definition
u4
:=
ordsucc
u3
Definition
u5
:=
ordsucc
u4
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
Known
adedd..
:
∀ x0 .
x0
∈
u24
⟶
∀ x1 :
ι → ο
.
x1
0
⟶
x1
u1
⟶
x1
u2
⟶
x1
u3
⟶
x1
u4
⟶
x1
u5
⟶
x1
u6
⟶
x1
u7
⟶
x1
u8
⟶
x1
u9
⟶
x1
u10
⟶
x1
u11
⟶
x1
u12
⟶
x1
u13
⟶
x1
u14
⟶
x1
u15
⟶
x1
u16
⟶
x1
u17
⟶
x1
u18
⟶
x1
u19
⟶
x1
u20
⟶
x1
u21
⟶
x1
u22
⟶
x1
u23
⟶
x1
x0
Known
cef55..
:
ChurchNum_3ary_proj_p
(
λ x0 x1 x2 :
(
ι → ι
)
→
ι → ι
.
x0
)
Known
208f3..
:
ChurchNum_8ary_proj_p
(
λ x0 x1 x2 x3 x4 x5 x6 x7 :
(
ι → ι
)
→
ι → ι
.
x0
)
Known
ef1ab..
:
ChurchNum_8ary_proj_p
(
λ x0 x1 x2 x3 x4 x5 x6 x7 :
(
ι → ι
)
→
ι → ι
.
x1
)
Known
e5caa..
:
ChurchNum_8ary_proj_p
(
λ x0 x1 x2 x3 x4 x5 x6 x7 :
(
ι → ι
)
→
ι → ι
.
x2
)
Known
446d8..
:
ChurchNum_8ary_proj_p
(
λ x0 x1 x2 x3 x4 x5 x6 x7 :
(
ι → ι
)
→
ι → ι
.
x3
)
Known
3a83b..
:
ChurchNum_8ary_proj_p
(
λ x0 x1 x2 x3 x4 x5 x6 x7 :
(
ι → ι
)
→
ι → ι
.
x4
)
Known
0ab9f..
:
ChurchNum_8ary_proj_p
(
λ x0 x1 x2 x3 x4 x5 x6 x7 :
(
ι → ι
)
→
ι → ι
.
x5
)
Known
94187..
:
ChurchNum_8ary_proj_p
(
λ x0 x1 x2 x3 x4 x5 x6 x7 :
(
ι → ι
)
→
ι → ι
.
x6
)
Known
7734d..
:
ChurchNum_8ary_proj_p
(
λ x0 x1 x2 x3 x4 x5 x6 x7 :
(
ι → ι
)
→
ι → ι
.
x7
)
Known
18961..
:
ChurchNum_3ary_proj_p
(
λ x0 x1 x2 :
(
ι → ι
)
→
ι → ι
.
x1
)
Known
a5963..
:
ChurchNum_3ary_proj_p
(
λ x0 x1 x2 :
(
ι → ι
)
→
ι → ι
.
x2
)
Theorem
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
(proof)
previous assets