Search for blocks/addresses/...
Proofgold Signed Transaction
vin
PrA6r..
/
8a532..
PUZfL..
/
d4c5e..
vout
PrA6r..
/
ca3d1..
47.47 bars
TMceY..
/
c2d93..
ownership of
40c10..
as prop with payaddr
PrHSW..
rightscost 0.00 controlledby
PrHSW..
upto 0
TMbo6..
/
9e271..
ownership of
57a2b..
as prop with payaddr
PrHSW..
rightscost 0.00 controlledby
PrHSW..
upto 0
TMR2f..
/
f66ea..
ownership of
027bb..
as prop with payaddr
PrHSW..
rightscost 0.00 controlledby
PrHSW..
upto 0
TMNQS..
/
63b4c..
ownership of
a6711..
as prop with payaddr
PrHSW..
rightscost 0.00 controlledby
PrHSW..
upto 0
TMSRn..
/
fcedb..
ownership of
ffcac..
as obj with payaddr
PrHSW..
rightscost 0.00 controlledby
PrHSW..
upto 0
TMdoZ..
/
e6c34..
ownership of
6b892..
as obj with payaddr
PrHSW..
rightscost 0.00 controlledby
PrHSW..
upto 0
TMH2P..
/
639f9..
ownership of
e8894..
as obj with payaddr
PrHSW..
rightscost 0.00 controlledby
PrHSW..
upto 0
TMGh6..
/
6b7e3..
ownership of
e641a..
as obj with payaddr
PrHSW..
rightscost 0.00 controlledby
PrHSW..
upto 0
TMWmE..
/
25808..
ownership of
60be4..
as obj with payaddr
PrHSW..
rightscost 0.00 controlledby
PrHSW..
upto 0
TMSsT..
/
f8c34..
ownership of
44508..
as obj with payaddr
PrHSW..
rightscost 0.00 controlledby
PrHSW..
upto 0
PUMJH..
/
036b0..
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)