Search for blocks/addresses/...
Proofgold Signed Transaction
vin
PrJGW..
/
6ae7b..
PUKJY..
/
067d7..
vout
PrJGW..
/
7aad8..
3.00 bars
TMHKv..
/
d77da..
negprop ownership controlledby
PrGxv..
upto 0
TMRTU..
/
9bcfd..
ownership of
732ef..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMKsy..
/
22adf..
ownership of
8353f..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMGeP..
/
d827d..
ownership of
48046..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMFka..
/
1f3bb..
ownership of
aef7b..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TML6U..
/
9db16..
ownership of
2042d..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMXmB..
/
24138..
ownership of
b0c33..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMHxx..
/
d4d50..
ownership of
0286c..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMZWV..
/
01252..
ownership of
ffff6..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMMd5..
/
8baa4..
ownership of
db6fe..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMGL8..
/
856b0..
ownership of
ede72..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMZWY..
/
e2210..
ownership of
92e6a..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMRq8..
/
87691..
ownership of
9a58e..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMTVi..
/
98b0b..
ownership of
93754..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMPzp..
/
28b4b..
ownership of
3b556..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMYHp..
/
a994e..
ownership of
50787..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMZpS..
/
8e739..
ownership of
d0954..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
PUaq1..
/
227b1..
doc published by
PrGxv..
Known
128d8..
:
∀ x0 x1 x2 x3 .
prim0
x0
x1
=
prim0
x2
x3
⟶
∀ x4 : ο .
(
x0
=
x2
⟶
x1
=
x3
⟶
x4
)
⟶
x4
Theorem
50787..
:
∀ x0 x1 x2 x3 .
prim0
x0
x1
=
prim0
x2
x3
⟶
x0
=
x2
(proof)
Theorem
93754..
:
∀ x0 x1 x2 x3 .
prim0
x0
x1
=
prim0
x2
x3
⟶
x1
=
x3
(proof)
Definition
False
:=
∀ x0 : ο .
x0
Known
9aea6..
:
∀ x0 x1 .
∀ x2 :
ι → ι
.
prim0
x0
x1
=
prim1
x2
⟶
∀ x3 : ο .
x3
Theorem
92e6a..
:
∀ x0 :
ι → ι
.
∀ x1 x2 .
prim1
x0
=
prim0
x1
x2
⟶
False
(proof)
Known
b4755..
:
∀ x0 x1 :
ι → ι
.
prim1
x0
=
prim1
x1
⟶
x0
=
x1
Theorem
db6fe..
:
∀ x0 x1 :
ι → ι
.
∀ x2 .
prim1
x0
=
prim1
x1
⟶
x0
x2
=
x1
x2
(proof)
Definition
236c6..
:=
prim1
(
λ x0 .
x0
)
Known
f558c..
:
∀ x0 x1 .
236c6..
=
prim0
x0
x1
⟶
∀ x2 : ο .
x2
Theorem
0286c..
:
∀ x0 x1 .
prim0
x0
x1
=
236c6..
⟶
False
(proof)
Known
148f8..
:
∀ x0 :
ι →
ι → ι
.
236c6..
=
prim1
(
λ x2 .
prim1
(
x0
x2
)
)
⟶
∀ x1 : ο .
x1
Theorem
2042d..
:
∀ x0 :
ι →
ι → ι
.
prim1
(
λ x2 .
prim1
(
x0
x2
)
)
=
236c6..
⟶
False
(proof)
Known
f2c23..
:
∀ x0 x1 :
ι → ι
.
236c6..
=
prim1
(
λ x3 .
prim0
(
x0
x3
)
(
x1
x3
)
)
⟶
∀ x2 : ο .
x2
Theorem
48046..
:
∀ x0 x1 :
ι → ι
.
prim1
(
λ x3 .
prim0
(
x0
x3
)
(
x1
x3
)
)
=
236c6..
⟶
False
(proof)
Known
61590..
:
236c6..
=
prim1
(
λ x1 .
236c6..
)
⟶
False
Theorem
732ef..
:
prim1
(
λ x1 .
236c6..
)
=
236c6..
⟶
False
(proof)