Search for blocks/addresses/...
Proofgold Signed Transaction
vin
PrP4d..
/
894c8..
PUKrs..
/
acfab..
vout
PrP4d..
/
59a8b..
0.08 bars
TMTJy..
/
086d0..
ownership of
24ac9..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMFeJ..
/
b8814..
ownership of
89e42..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
PUNVa..
/
d4e8d..
doc published by
PrCmT..
Known
ax_mp
ax_mp
:
∀ x0 x1 : ο .
x0
⟶
(
x0
⟶
x1
)
⟶
x1
Known
ax_frege52c
ax_frege52c
:
∀ x0 :
ι → ο
.
∀ x1 x2 :
ι →
ι → ο
.
∀ x3 .
wceq
(
x1
x3
)
(
x2
x3
)
⟶
wsbc
x0
(
x1
x3
)
⟶
wsbc
x0
(
x2
x3
)
Known
ax_frege8
ax_frege8
:
∀ x0 x1 x2 : ο .
(
x0
⟶
x1
⟶
x2
)
⟶
x1
⟶
x0
⟶
x2
Theorem
24ac9..
frege53c
:
∀ x0 :
ι → ο
.
∀ x1 x2 :
ι →
ι → ο
.
∀ x3 .
wsbc
x0
(
x1
x3
)
⟶
wceq
(
x1
x3
)
(
x2
x3
)
⟶
wsbc
x0
(
x2
x3
)
(proof)