Search for blocks/addresses/...
Proofgold Signed Transaction
vin
PrRV1..
/
1727a..
PUYKe..
/
a42f1..
vout
PrRV1..
/
baeed..
0.10 bars
TMP59..
/
fb8c9..
ownership of
8dc43..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMNhx..
/
fda75..
ownership of
64bb5..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMWtG..
/
15f02..
ownership of
feb67..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMWkF..
/
7629e..
ownership of
b706a..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMSQK..
/
5d59f..
ownership of
5d33b..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMV47..
/
f3eef..
ownership of
9e519..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMHLY..
/
d322c..
ownership of
6c8ea..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMSFc..
/
6acc2..
ownership of
0e273..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMN8E..
/
573bd..
ownership of
b59af..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMSER..
/
1c223..
ownership of
c987d..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMMGf..
/
f80b9..
ownership of
89802..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMaFh..
/
876a8..
ownership of
5f48f..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMYWQ..
/
dd196..
ownership of
cba4d..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMdYU..
/
48d33..
ownership of
351d6..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMFNK..
/
ffcbb..
ownership of
8a6af..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMN5d..
/
57f3e..
ownership of
b4223..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMMZ6..
/
f0a92..
ownership of
64656..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMJW8..
/
734cc..
ownership of
c88fd..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMWPT..
/
7e657..
ownership of
eb39a..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMVS7..
/
926d1..
ownership of
44918..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMFXd..
/
8297e..
ownership of
785b0..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMdBF..
/
0e190..
ownership of
375ba..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMKzt..
/
40031..
ownership of
84cc1..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMa2P..
/
7fccd..
ownership of
d56bb..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMEqb..
/
7367c..
ownership of
02e83..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMLd8..
/
d88e0..
ownership of
c7236..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMUoW..
/
a01c9..
ownership of
471ea..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMJYd..
/
bb993..
ownership of
027e4..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMcq7..
/
65401..
ownership of
093ad..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMN7A..
/
a8f1e..
ownership of
45d9d..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMLGa..
/
2b098..
ownership of
82c3c..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMVa9..
/
2a454..
ownership of
08840..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMZcK..
/
6dd7b..
ownership of
fcf17..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMYft..
/
0e76d..
ownership of
b63ec..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMaJT..
/
05617..
ownership of
e8788..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMQ5Y..
/
3806c..
ownership of
a7414..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
PUJyx..
/
369cb..
doc published by
PrCmT..
Known
df_rmo__df_rab__df_v__df_cdeq__df_sbc__df_csb__df_dif__df_un__df_in__df_ss__df_pss__df_symdif__df_nul__df_if__df_pw__df_sn__df_pr__df_tp
:
∀ x0 : ο .
(
(
∀ x1 :
ι → ο
.
∀ x2 :
ι →
ι → ο
.
wb
(
wrmo
x1
x2
)
(
wmo
(
λ x3 .
wa
(
wcel
(
cv
x3
)
(
x2
x3
)
)
(
x1
x3
)
)
)
)
⟶
(
∀ x1 :
ι → ο
.
∀ x2 :
ι →
ι → ο
.
wceq
(
crab
x1
x2
)
(
cab
(
λ x3 .
wa
(
wcel
(
cv
x3
)
(
x2
x3
)
)
(
x1
x3
)
)
)
)
⟶
wceq
cvv
(
cab
(
λ x1 .
wceq
(
cv
x1
)
(
cv
x1
)
)
)
⟶
(
∀ x1 : ο .
∀ x2 x3 .
wb
(
wcdeq
x1
x2
x3
)
(
wceq
(
cv
x2
)
(
cv
x3
)
⟶
x1
)
)
⟶
(
∀ x1 :
ι → ο
.
∀ x2 :
ι →
ι → ο
.
∀ x3 .
wb
(
wsbc
x1
(
x2
x3
)
)
(
wcel
(
x2
x3
)
(
cab
x1
)
)
)
⟶
(
∀ x1 x2 :
ι →
ι → ο
.
∀ x3 .
wceq
(
csb
(
x1
x3
)
x2
)
(
cab
(
λ x4 .
wsbc
(
λ x5 .
wcel
(
cv
x4
)
(
x2
x5
)
)
(
x1
x3
)
)
)
)
⟶
(
∀ x1 x2 :
ι → ο
.
wceq
(
cdif
x1
x2
)
(
cab
(
λ x3 .
wa
(
wcel
(
cv
x3
)
x1
)
(
wn
(
wcel
(
cv
x3
)
x2
)
)
)
)
)
⟶
(
∀ x1 x2 :
ι → ο
.
wceq
(
cun
x1
x2
)
(
cab
(
λ x3 .
wo
(
wcel
(
cv
x3
)
x1
)
(
wcel
(
cv
x3
)
x2
)
)
)
)
⟶
(
∀ x1 x2 :
ι → ο
.
wceq
(
cin
x1
x2
)
(
cab
(
λ x3 .
wa
(
wcel
(
cv
x3
)
x1
)
(
wcel
(
cv
x3
)
x2
)
)
)
)
⟶
(
∀ x1 x2 :
ι → ο
.
wb
(
wss
x1
x2
)
(
wceq
(
cin
x1
x2
)
x1
)
)
⟶
(
∀ x1 x2 :
ι → ο
.
wb
(
wpss
x1
x2
)
(
wa
(
wss
x1
x2
)
(
wne
x1
x2
)
)
)
⟶
(
∀ x1 x2 :
ι → ο
.
wceq
(
csymdif
x1
x2
)
(
cun
(
cdif
x1
x2
)
(
cdif
x2
x1
)
)
)
⟶
wceq
c0
(
cdif
cvv
cvv
)
⟶
(
∀ x1 : ο .
∀ x2 x3 :
ι → ο
.
wceq
(
cif
x1
x2
x3
)
(
cab
(
λ x4 .
wo
(
wa
(
wcel
(
cv
x4
)
x2
)
x1
)
(
wa
(
wcel
(
cv
x4
)
x3
)
(
wn
x1
)
)
)
)
)
⟶
(
∀ x1 :
ι → ο
.
wceq
(
cpw
x1
)
(
cab
(
λ x2 .
wss
(
cv
x2
)
x1
)
)
)
⟶
(
∀ x1 :
ι → ο
.
wceq
(
csn
x1
)
(
cab
(
λ x2 .
wceq
(
cv
x2
)
x1
)
)
)
⟶
(
∀ x1 x2 :
ι → ο
.
wceq
(
cpr
x1
x2
)
(
cun
(
csn
x1
)
(
csn
x2
)
)
)
⟶
(
∀ x1 x2 x3 :
ι → ο
.
wceq
(
ctp
x1
x2
x3
)
(
cun
(
cpr
x1
x2
)
(
csn
x3
)
)
)
⟶
x0
)
⟶
x0
Theorem
df_rmo
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ο
.
wb
(
wrmo
x0
x1
)
(
wmo
(
λ x2 .
wa
(
wcel
(
cv
x2
)
(
x1
x2
)
)
(
x0
x2
)
)
)
(proof)
Theorem
df_rab
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ο
.
wceq
(
crab
x0
x1
)
(
cab
(
λ x2 .
wa
(
wcel
(
cv
x2
)
(
x1
x2
)
)
(
x0
x2
)
)
)
(proof)
Theorem
df_v
:
wceq
cvv
(
cab
(
λ x0 .
wceq
(
cv
x0
)
(
cv
x0
)
)
)
(proof)
Theorem
df_cdeq
:
∀ x0 : ο .
∀ x1 x2 .
wb
(
wcdeq
x0
x1
x2
)
(
wceq
(
cv
x1
)
(
cv
x2
)
⟶
x0
)
(proof)
Theorem
df_sbc
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ο
.
∀ x2 .
wb
(
wsbc
x0
(
x1
x2
)
)
(
wcel
(
x1
x2
)
(
cab
x0
)
)
(proof)
Theorem
df_csb
:
∀ x0 x1 :
ι →
ι → ο
.
∀ x2 .
wceq
(
csb
(
x0
x2
)
x1
)
(
cab
(
λ x3 .
wsbc
(
λ x4 .
wcel
(
cv
x3
)
(
x1
x4
)
)
(
x0
x2
)
)
)
(proof)
Theorem
df_dif
:
∀ x0 x1 :
ι → ο
.
wceq
(
cdif
x0
x1
)
(
cab
(
λ x2 .
wa
(
wcel
(
cv
x2
)
x0
)
(
wn
(
wcel
(
cv
x2
)
x1
)
)
)
)
(proof)
Theorem
df_un
:
∀ x0 x1 :
ι → ο
.
wceq
(
cun
x0
x1
)
(
cab
(
λ x2 .
wo
(
wcel
(
cv
x2
)
x0
)
(
wcel
(
cv
x2
)
x1
)
)
)
(proof)
Theorem
df_in
:
∀ x0 x1 :
ι → ο
.
wceq
(
cin
x0
x1
)
(
cab
(
λ x2 .
wa
(
wcel
(
cv
x2
)
x0
)
(
wcel
(
cv
x2
)
x1
)
)
)
(proof)
Theorem
df_ss
:
∀ x0 x1 :
ι → ο
.
wb
(
wss
x0
x1
)
(
wceq
(
cin
x0
x1
)
x0
)
(proof)
Theorem
df_pss
:
∀ x0 x1 :
ι → ο
.
wb
(
wpss
x0
x1
)
(
wa
(
wss
x0
x1
)
(
wne
x0
x1
)
)
(proof)
Theorem
df_symdif
:
∀ x0 x1 :
ι → ο
.
wceq
(
csymdif
x0
x1
)
(
cun
(
cdif
x0
x1
)
(
cdif
x1
x0
)
)
(proof)
Theorem
df_nul
:
wceq
c0
(
cdif
cvv
cvv
)
(proof)
Theorem
df_if
:
∀ x0 : ο .
∀ x1 x2 :
ι → ο
.
wceq
(
cif
x0
x1
x2
)
(
cab
(
λ x3 .
wo
(
wa
(
wcel
(
cv
x3
)
x1
)
x0
)
(
wa
(
wcel
(
cv
x3
)
x2
)
(
wn
x0
)
)
)
)
(proof)
Theorem
df_pw
:
∀ x0 :
ι → ο
.
wceq
(
cpw
x0
)
(
cab
(
λ x1 .
wss
(
cv
x1
)
x0
)
)
(proof)
Theorem
df_sn
:
∀ x0 :
ι → ο
.
wceq
(
csn
x0
)
(
cab
(
λ x1 .
wceq
(
cv
x1
)
x0
)
)
(proof)
Theorem
df_pr
:
∀ x0 x1 :
ι → ο
.
wceq
(
cpr
x0
x1
)
(
cun
(
csn
x0
)
(
csn
x1
)
)
(proof)
Theorem
df_tp
:
∀ x0 x1 x2 :
ι → ο
.
wceq
(
ctp
x0
x1
x2
)
(
cun
(
cpr
x0
x1
)
(
csn
x2
)
)
(proof)