Search for blocks/addresses/...
Proofgold Signed Transaction
vin
PrR6y..
/
cb8bb..
PUb3c..
/
30a9d..
vout
PrR6y..
/
da6e6..
1.00 bars
TMSMz..
/
cafed..
ownership of
6e151..
as prop with payaddr
PrJJf..
rights free controlledby
PrJJf..
upto 0
TMNbK..
/
5ef31..
ownership of
03ceb..
as prop with payaddr
PrJJf..
rights free controlledby
PrJJf..
upto 0
PUWvf..
/
9d156..
doc published by
PrJJf..
Known
eb789..
andER
:
∀ x0 x1 : ο .
and
x0
x1
⟶
x1
Known
False_def
False_def
:
False
=
∀ x1 : ο .
x1
Known
22d74..
atleast5_def
:
atleast5
=
λ x1 .
∀ x2 : ο .
(
∀ x3 .
and
(
Subq
x3
x1
)
(
and
(
not
(
Subq
x1
x3
)
)
(
atleast4
x3
)
)
⟶
x2
)
⟶
x2
Known
notE
notE
:
∀ x0 : ο .
not
x0
⟶
x0
⟶
False
Known
37124..
orE
:
∀ x0 x1 : ο .
or
x0
x1
⟶
∀ x2 : ο .
(
x0
⟶
x2
)
⟶
(
x1
⟶
x2
)
⟶
x2
Known
9ac15..
xm
:
∀ x0 : ο .
or
x0
(
not
x0
)
Theorem
6e151..
:
∀ x0 .
(
∀ x1 .
nat_p
x1
)
⟶
∀ x1 .
In
x1
x0
⟶
∀ x2 : ο .
(
∀ x3 .
(
(
∀ x4 : ο .
(
∀ x5 .
and
(
Subq
x5
x3
)
(
∃ x6 .
and
(
exactly2
(
binrep
(
Power
(
Power
(
Power
0
)
)
)
0
)
)
(
not
(
atleast4
(
Power
0
)
)
)
)
⟶
x4
)
⟶
x4
)
⟶
∀ x4 .
atleast5
(
Union
0
)
⟶
atleast4
x3
)
⟶
x2
)
⟶
x2
(proof)