Search for blocks/addresses/...
Proofgold Asset
asset id
44d01545fa5f3e4d1cdaeb4ec9c89434e47ad9aa8c6e045bcd5e0d0c6ff85834
asset hash
7ed21ef7ef4fb3ac71a0071a4e0e8c523b878e3f4ac7dea4f720192e9d414d18
bday / block
18726
tx
ddad9..
preasset
doc published by
Pr4zB..
Definition
ChurchNum_p
:=
λ x0 :
(
ι → ι
)
→
ι → ι
.
∀ x1 :
(
(
ι → ι
)
→
ι → ι
)
→ ο
.
x1
(
λ x2 :
ι → ι
.
λ x3 .
x3
)
⟶
(
∀ x2 :
(
ι → ι
)
→
ι → ι
.
x1
x2
⟶
x1
(
λ x3 :
ι → ι
.
λ x4 .
x3
(
x2
x3
x4
)
)
)
⟶
x1
x0
Theorem
5252e..
:
ChurchNum_p
(
λ x0 :
ι → ι
.
λ x1 .
x1
)
...
Theorem
335fd..
:
∀ x0 :
(
ι → ι
)
→
ι → ι
.
ChurchNum_p
x0
⟶
ChurchNum_p
(
λ x1 :
ι → ι
.
λ x2 .
x1
(
x0
x1
x2
)
)
...
Theorem
83d4c..
:
ChurchNum_p
(
λ x0 :
ι → ι
.
x0
)
...
Theorem
4613e..
:
ChurchNum_p
(
λ x0 :
ι → ι
.
λ x1 .
x0
(
x0
x1
)
)
...
Theorem
9d632..
:
ChurchNum_p
(
λ x0 :
ι → ι
.
λ x1 .
x0
(
x0
(
x0
x1
)
)
)
...
Theorem
a1f0d..
:
ChurchNum_p
(
λ x0 :
ι → ι
.
λ x1 .
x0
(
x0
(
x0
(
x0
x1
)
)
)
)
...
Theorem
c9952..
:
ChurchNum_p
(
λ x0 :
ι → ι
.
λ x1 .
x0
(
x0
(
x0
(
x0
(
x0
x1
)
)
)
)
)
...
Theorem
5d5e3..
:
ChurchNum_p
(
λ x0 :
ι → ι
.
λ x1 .
x0
(
x0
(
x0
(
x0
(
x0
(
x0
x1
)
)
)
)
)
)
...
Theorem
68754..
:
ChurchNum_p
(
λ x0 :
ι → ι
.
λ x1 .
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
x1
)
)
)
)
)
)
)
...
Theorem
66cf5..
:
ChurchNum_p
(
λ x0 :
ι → ι
.
λ x1 .
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
x1
)
)
)
)
)
)
)
)
...
Theorem
66b3d..
:
ChurchNum_p
(
λ x0 :
ι → ι
.
λ x1 .
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
x1
)
)
)
)
)
)
)
)
)
...
Theorem
0a45b..
:
ChurchNum_p
(
λ x0 :
ι → ι
.
λ x1 .
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
x1
)
)
)
)
)
)
)
)
)
)
...
Theorem
1bf92..
:
ChurchNum_p
(
λ x0 :
ι → ι
.
λ x1 .
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
x1
)
)
)
)
)
)
)
)
)
)
)
...
Theorem
b848e..
:
ChurchNum_p
(
λ x0 :
ι → ι
.
λ x1 .
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
x1
)
)
)
)
)
)
)
)
)
)
)
)
...
Theorem
f6fb6..
:
ChurchNum_p
(
λ x0 :
ι → ι
.
λ x1 .
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
x1
)
)
)
)
)
)
)
)
)
)
)
)
)
...
Theorem
7c98b..
:
ChurchNum_p
(
λ x0 :
ι → ι
.
λ x1 .
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
x1
)
)
)
)
)
)
)
)
)
)
)
)
)
)
...
Theorem
466b2..
:
ChurchNum_p
(
λ x0 :
ι → ι
.
λ x1 .
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
x1
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
...
Theorem
d9243..
:
ChurchNum_p
(
λ x0 :
ι → ι
.
λ x1 .
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
x1
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
...
Theorem
43d3d..
:
ChurchNum_p
(
λ x0 :
ι → ι
.
λ x1 .
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
x1
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
...
Theorem
4b7da..
:
ChurchNum_p
(
λ x0 :
ι → ι
.
λ x1 .
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
x1
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
...
Theorem
bb726..
:
ChurchNum_p
(
λ x0 :
ι → ι
.
λ x1 .
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
x1
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
...
Theorem
4e557..
:
ChurchNum_p
(
λ x0 :
ι → ι
.
λ x1 .
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
x1
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
...
Theorem
b017b..
:
ChurchNum_p
(
λ x0 :
ι → ι
.
λ x1 .
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
x1
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
...
Theorem
f647d..
:
ChurchNum_p
(
λ x0 :
ι → ι
.
λ x1 .
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
x1
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
...
Theorem
43047..
:
ChurchNum_p
(
λ x0 :
ι → ι
.
λ x1 .
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
x1
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
...
Theorem
3f720..
:
ChurchNum_p
(
λ x0 :
ι → ι
.
λ x1 .
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
x1
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
...
Param
nat_p
nat_p
:
ι
→
ο
Param
ordsucc
ordsucc
:
ι
→
ι
Known
nat_0
nat_0
:
nat_p
0
Known
nat_ordsucc
nat_ordsucc
:
∀ x0 .
nat_p
x0
⟶
nat_p
(
ordsucc
x0
)
Theorem
b26f0..
:
∀ x0 :
(
ι → ι
)
→
ι → ι
.
ChurchNum_p
x0
⟶
nat_p
(
x0
ordsucc
0
)
...
Definition
and
and
:=
λ x0 x1 : ο .
∀ x2 : ο .
(
x0
⟶
x1
⟶
x2
)
⟶
x2
Known
andI
andI
:
∀ x0 x1 : ο .
x0
⟶
x1
⟶
and
x0
x1
Theorem
c0023..
:
∀ x0 :
(
(
ι → ι
)
→
ι → ι
)
→ ο
.
x0
(
λ x1 :
ι → ι
.
λ x2 .
x2
)
⟶
(
∀ x1 :
(
ι → ι
)
→
ι → ι
.
ChurchNum_p
x1
⟶
x0
x1
⟶
x0
(
λ x2 :
ι → ι
.
λ x3 .
x2
(
x1
x2
x3
)
)
)
⟶
∀ x1 :
(
ι → ι
)
→
ι → ι
.
ChurchNum_p
x1
⟶
x0
x1
...
Param
add_nat
add_nat
:
ι
→
ι
→
ι
Known
add_nat_0L
add_nat_0L
:
∀ x0 .
nat_p
x0
⟶
add_nat
0
x0
=
x0
Known
add_nat_SL
add_nat_SL
:
∀ x0 .
nat_p
x0
⟶
∀ x1 .
nat_p
x1
⟶
add_nat
(
ordsucc
x0
)
x1
=
ordsucc
(
add_nat
x0
x1
)
Theorem
39d66..
:
∀ x0 :
(
ι → ι
)
→
ι → ι
.
ChurchNum_p
x0
⟶
∀ x1 :
(
ι → ι
)
→
ι → ι
.
ChurchNum_p
x1
⟶
x0
ordsucc
(
x1
ordsucc
0
)
=
add_nat
(
x0
ordsucc
0
)
(
x1
ordsucc
0
)
...
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
Theorem
86c65..
:
nat_p
u18
...
Definition
u19
:=
ordsucc
u18
Theorem
d9e2e..
:
nat_p
u19
...
Definition
u20
:=
ordsucc
u19
Theorem
2669c..
:
nat_p
u20
...
Definition
u21
:=
ordsucc
u20
Theorem
e8a0a..
:
nat_p
u21
...
Definition
u22
:=
ordsucc
u21
Theorem
daa33..
:
nat_p
u22
...
Definition
u23
:=
ordsucc
u22
Theorem
b73b8..
:
nat_p
u23
...
Definition
u24
:=
ordsucc
u23
Theorem
73189..
:
nat_p
u24
...
Known
nat_0_in_ordsucc
nat_0_in_ordsucc
:
∀ x0 .
nat_p
x0
⟶
0
∈
ordsucc
x0
Theorem
4c607..
:
0
∈
u24
...
Known
d8085..
:
∀ x0 x1 .
nat_p
x1
⟶
x0
∈
ordsucc
(
add_nat
x0
x1
)
Theorem
610bf..
:
u1
∈
u24
...
Theorem
30da6..
:
u2
∈
u24
...
Theorem
3cb84..
:
u3
∈
u24
...
Theorem
43f74..
:
u4
∈
u24
...
Theorem
8f227..
:
u5
∈
u24
...
Known
nat_17
nat_17
:
nat_p
17
Theorem
469db..
:
u6
∈
u24
...
Known
nat_16
nat_16
:
nat_p
16
Theorem
bb94c..
:
u7
∈
u24
...
Known
nat_15
nat_15
:
nat_p
15
Theorem
d2f24..
:
u8
∈
u24
...
Known
nat_14
nat_14
:
nat_p
14
Theorem
fd0d9..
:
u9
∈
u24
...
Known
nat_13
nat_13
:
nat_p
13
Theorem
df5ed..
:
u10
∈
u24
...
Known
nat_12
nat_12
:
nat_p
12
Theorem
05672..
:
u11
∈
u24
...
Known
nat_11
nat_11
:
nat_p
11
Theorem
15af9..
:
u12
∈
u24
...
Known
nat_10
nat_10
:
nat_p
10
Theorem
e6799..
:
u13
∈
u24
...
Known
nat_9
nat_9
:
nat_p
9
Theorem
9522d..
:
u14
∈
u24
...
Known
nat_8
nat_8
:
nat_p
8
Theorem
fc764..
:
u15
∈
u24
...
Known
nat_7
nat_7
:
nat_p
7
Theorem
2d7ca..
:
u16
∈
u24
...
Known
nat_6
nat_6
:
nat_p
6
Theorem
e4fb5..
:
u17
∈
u24
...
Known
nat_5
nat_5
:
nat_p
5
Theorem
f0252..
:
u18
∈
u24
...
Known
nat_4
nat_4
:
nat_p
4
Theorem
a4364..
:
u19
∈
u24
...
Known
nat_3
nat_3
:
nat_p
3
Theorem
9da85..
:
u20
∈
u24
...
Known
nat_2
nat_2
:
nat_p
2
Theorem
3ee80..
:
u21
∈
u24
...
Definition
Subq
Subq
:=
λ x0 x1 .
∀ x2 .
x2
∈
x0
⟶
x2
∈
x1
Known
ordsuccI1
ordsuccI1
:
∀ x0 .
x0
⊆
ordsucc
x0
Known
ordsuccI2
ordsuccI2
:
∀ x0 .
x0
∈
ordsucc
x0
Theorem
9ec16..
:
u22
∈
u24
...
Theorem
d7b2c..
:
u23
∈
u24
...