Search for blocks/addresses/...
Proofgold Signed Transaction
vin
PrJGW..
/
c89ec..
PUSBB..
/
b9278..
vout
PrJGW..
/
06ef8..
2.00 bars
TMVxE..
/
1a0f9..
BOUNTY
1.00 bars
TMFJm..
/
e070b..
ownership of
1b30d..
as obj with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMQ7e..
/
8f1bd..
ownership of
5b814..
as obj with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMS2v..
/
c11c7..
ownership of
79006..
as obj with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMTJg..
/
13df6..
ownership of
39a81..
as obj with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMRFf..
/
99a33..
ownership of
5ad3b..
as obj with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMK1L..
/
dafd0..
ownership of
11baf..
as obj with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMagQ..
/
f678e..
ownership of
70c47..
as obj with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMcSs..
/
d4afd..
ownership of
7dadd..
as obj with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
PURiK..
/
f3334..
doc published by
PrGxv..
Definition
70c47..
:=
λ x0 .
and
(
nat_p
x0
)
(
∀ x1 : ο .
(
∀ x2 .
and
(
nat_p
x2
)
(
x0
=
mul_nat
2
x2
)
⟶
x1
)
⟶
x1
)
Definition
5ad3b..
:=
nat_primrec
0
(
λ x0 x1 .
If_i
(
70c47..
x0
)
x1
(
ordsucc
x1
)
)
Definition
79006..
:=
λ x0 .
If_i
(
70c47..
x0
)
(
5ad3b..
x0
)
(
ordsucc
(
mul_nat
3
x0
)
)
Definition
1b30d..
:=
λ x0 .
λ x1 :
ι → ι
.
λ x2 .
nat_primrec
x2
(
λ x3 .
x1
)
x0
Conjecture
aa000..
:
∀ x0 .
nat_p
x0
⟶
not
(
x0
=
0
)
⟶
∀ x1 : ο .
(
∀ x2 .
and
(
nat_p
x2
)
(
1b30d..
x2
79006..
x0
=
1
)
⟶
x1
)
⟶
x1