Search for blocks/addresses/...
Proofgold Signed Transaction
vin
PrEvg..
/
25d3c..
PUXLv..
/
6e838..
vout
PrEvg..
/
57819..
0.32 bars
TMUHH..
/
918f4..
ownership of
e9a29..
as prop with payaddr
PrQe3..
rights free controlledby
PrQe3..
upto 0
TMNa8..
/
ba6e1..
ownership of
7c8ab..
as prop with payaddr
PrQe3..
rights free controlledby
PrQe3..
upto 0
PUbuy..
/
98d20..
doc published by
PrQe3..
Known
FalseE
FalseE
:
False
⟶
∀ x0 : ο .
x0
Known
2901c..
EmptyE
:
∀ x0 .
In
x0
0
⟶
False
Theorem
e9a29..
:
∀ x0 .
In
x0
0
⟶
∀ x1 .
In
x1
x0
⟶
∀ x2 .
In
x2
x1
⟶
∀ x3 : ο .
(
∀ x4 .
(
∀ x5 .
(
ordinal
x4
⟶
and
(
exactly2
x4
)
(
not
(
exactly5
x5
)
)
)
⟶
(
(
ordinal
x4
⟶
exactly2
x4
)
⟶
atleast2
x4
⟶
(
(
not
(
atleast2
(
Power
(
binrep
(
Power
(
Power
0
)
)
0
)
)
)
⟶
x4
=
x5
)
⟶
atleast3
x4
)
⟶
and
(
atleast5
x2
)
(
not
(
exactly1of2
(
SNoLt
x2
(
binrep
(
Power
(
Power
(
Power
(
Power
0
)
)
)
)
0
)
)
(
TransSet
x5
)
)
)
)
⟶
nat_p
x4
)
⟶
x3
)
⟶
x3
(proof)