Search for blocks/addresses/...
Proofgold Address
address
PUMJH3qQLpuW9J8v9kk3QTAzkdRoCVRf4Un
total
0
mg
-
conjpub
-
current assets
54a6c..
/
036b0..
bday:
17169
doc published by
PrHSW..
Definition
ChurchNum2
:=
λ x0 :
ι → ι
.
λ x1 .
x0
(
x0
x1
)
Definition
ChurchNum4
:=
λ x0 :
ι → ι
.
λ x1 .
x0
(
x0
(
x0
(
x0
x1
)
)
)
Definition
ChurchNum_plus
:=
λ x0 x1 :
(
ι → ι
)
→
ι → ι
.
λ x2 :
ι → ι
.
λ x3 .
x0
x2
(
x1
x2
x3
)
Definition
ChurchNum_mult
:=
λ x0 x1 :
(
ι → ι
)
→
ι → ι
.
λ x2 :
ι → ι
.
x0
(
x1
x2
)
Theorem
ChurchNum_plus_2_2
:
ChurchNum_plus
ChurchNum2
ChurchNum2
=
ChurchNum4
(proof)
Theorem
ChurchNum_mult_2_2
:
ChurchNum_mult
ChurchNum2
ChurchNum2
=
ChurchNum4
(proof)
previous assets