Search for blocks/addresses/...
Proofgold Signed Transaction
vin
PrJQW..
/
20ca4..
PUTnU..
/
d4d8b..
vout
PrJQW..
/
58def..
0.08 bars
TMWPC..
/
db0b0..
ownership of
b11d9..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMZ8s..
/
5469f..
ownership of
613fb..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMZUY..
/
94c4b..
ownership of
89450..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMJHg..
/
2d4f4..
ownership of
7e878..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMJkd..
/
c33a4..
ownership of
8f994..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMK9t..
/
92e92..
ownership of
76855..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMXqo..
/
e2af4..
ownership of
7aed6..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMcfp..
/
6d4b6..
ownership of
bb461..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMEuY..
/
9cf03..
ownership of
faa73..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMbNS..
/
0ab72..
ownership of
2ae65..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMX8h..
/
c30d6..
ownership of
84c13..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMT34..
/
d5051..
ownership of
4735f..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMLdR..
/
69df1..
ownership of
51c1a..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMXHG..
/
47bbe..
ownership of
8fb34..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMS6T..
/
16056..
ownership of
0aec3..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMSY5..
/
afc30..
ownership of
e8f3c..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMH4k..
/
6dad0..
ownership of
6b99c..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMPrh..
/
1cb0c..
ownership of
fe2ed..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMdEL..
/
a0a52..
ownership of
6d751..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMQpm..
/
745e8..
ownership of
3c75e..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMcVa..
/
6b4f2..
ownership of
3ea33..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMMj8..
/
7b080..
ownership of
a51fb..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMPy9..
/
b90bb..
ownership of
7941d..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMSae..
/
9b1a4..
ownership of
979d3..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMaGz..
/
f21ab..
ownership of
26e91..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMQ1E..
/
41e48..
ownership of
d1070..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMF7C..
/
35f55..
ownership of
3e8d2..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMX13..
/
766e1..
ownership of
d5682..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMPwJ..
/
0ade5..
ownership of
b4eef..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMcMa..
/
e6133..
ownership of
1a51c..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMGdM..
/
ab81b..
ownership of
c5c2a..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMZYh..
/
a484f..
ownership of
c586e..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMQQ6..
/
10a2d..
ownership of
64d80..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMHZd..
/
cfc3a..
ownership of
58345..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMPSB..
/
73282..
ownership of
c8b0c..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMYw5..
/
74645..
ownership of
2c712..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
PUM7X..
/
57f7e..
doc published by
PrCmT..
Known
df_q__df_rp__df_xneg__df_xadd__df_xmul__df_ioo__df_ioc__df_ico__df_icc__df_fz__df_fzo__df_fl__df_ceil__df_mod__df_seq__df_exp__df_fac__df_bc
:
∀ x0 : ο .
(
wceq
cq
(
cima
cdiv
(
cxp
cz
cn
)
)
⟶
wceq
crp
(
crab
(
λ x1 .
wbr
cc0
(
cv
x1
)
clt
)
(
λ x1 .
cr
)
)
⟶
(
∀ x1 :
ι → ο
.
wceq
(
cxne
x1
)
(
cif
(
wceq
x1
cpnf
)
cmnf
(
cif
(
wceq
x1
cmnf
)
cpnf
(
cneg
x1
)
)
)
)
⟶
wceq
cxad
(
cmpt2
(
λ x1 x2 .
cxr
)
(
λ x1 x2 .
cxr
)
(
λ x1 x2 .
cif
(
wceq
(
cv
x1
)
cpnf
)
(
cif
(
wceq
(
cv
x2
)
cmnf
)
cc0
cpnf
)
(
cif
(
wceq
(
cv
x1
)
cmnf
)
(
cif
(
wceq
(
cv
x2
)
cpnf
)
cc0
cmnf
)
(
cif
(
wceq
(
cv
x2
)
cpnf
)
cpnf
(
cif
(
wceq
(
cv
x2
)
cmnf
)
cmnf
(
co
(
cv
x1
)
(
cv
x2
)
caddc
)
)
)
)
)
)
⟶
wceq
cxmu
(
cmpt2
(
λ x1 x2 .
cxr
)
(
λ x1 x2 .
cxr
)
(
λ x1 x2 .
cif
(
wo
(
wceq
(
cv
x1
)
cc0
)
(
wceq
(
cv
x2
)
cc0
)
)
cc0
(
cif
(
wo
(
wo
(
wa
(
wbr
cc0
(
cv
x2
)
clt
)
(
wceq
(
cv
x1
)
cpnf
)
)
(
wa
(
wbr
(
cv
x2
)
cc0
clt
)
(
wceq
(
cv
x1
)
cmnf
)
)
)
(
wo
(
wa
(
wbr
cc0
(
cv
x1
)
clt
)
(
wceq
(
cv
x2
)
cpnf
)
)
(
wa
(
wbr
(
cv
x1
)
cc0
clt
)
(
wceq
(
cv
x2
)
cmnf
)
)
)
)
cpnf
(
cif
(
wo
(
wo
(
wa
(
wbr
cc0
(
cv
x2
)
clt
)
(
wceq
(
cv
x1
)
cmnf
)
)
(
wa
(
wbr
(
cv
x2
)
cc0
clt
)
(
wceq
(
cv
x1
)
cpnf
)
)
)
(
wo
(
wa
(
wbr
cc0
(
cv
x1
)
clt
)
(
wceq
(
cv
x2
)
cmnf
)
)
(
wa
(
wbr
(
cv
x1
)
cc0
clt
)
(
wceq
(
cv
x2
)
cpnf
)
)
)
)
cmnf
(
co
(
cv
x1
)
(
cv
x2
)
cmul
)
)
)
)
)
⟶
wceq
cioo
(
cmpt2
(
λ x1 x2 .
cxr
)
(
λ x1 x2 .
cxr
)
(
λ x1 x2 .
crab
(
λ x3 .
wa
(
wbr
(
cv
x1
)
(
cv
x3
)
clt
)
(
wbr
(
cv
x3
)
(
cv
x2
)
clt
)
)
(
λ x3 .
cxr
)
)
)
⟶
wceq
cioc
(
cmpt2
(
λ x1 x2 .
cxr
)
(
λ x1 x2 .
cxr
)
(
λ x1 x2 .
crab
(
λ x3 .
wa
(
wbr
(
cv
x1
)
(
cv
x3
)
clt
)
(
wbr
(
cv
x3
)
(
cv
x2
)
cle
)
)
(
λ x3 .
cxr
)
)
)
⟶
wceq
cico
(
cmpt2
(
λ x1 x2 .
cxr
)
(
λ x1 x2 .
cxr
)
(
λ x1 x2 .
crab
(
λ x3 .
wa
(
wbr
(
cv
x1
)
(
cv
x3
)
cle
)
(
wbr
(
cv
x3
)
(
cv
x2
)
clt
)
)
(
λ x3 .
cxr
)
)
)
⟶
wceq
cicc
(
cmpt2
(
λ x1 x2 .
cxr
)
(
λ x1 x2 .
cxr
)
(
λ x1 x2 .
crab
(
λ x3 .
wa
(
wbr
(
cv
x1
)
(
cv
x3
)
cle
)
(
wbr
(
cv
x3
)
(
cv
x2
)
cle
)
)
(
λ x3 .
cxr
)
)
)
⟶
wceq
cfz
(
cmpt2
(
λ x1 x2 .
cz
)
(
λ x1 x2 .
cz
)
(
λ x1 x2 .
crab
(
λ x3 .
wa
(
wbr
(
cv
x1
)
(
cv
x3
)
cle
)
(
wbr
(
cv
x3
)
(
cv
x2
)
cle
)
)
(
λ x3 .
cz
)
)
)
⟶
wceq
cfzo
(
cmpt2
(
λ x1 x2 .
cz
)
(
λ x1 x2 .
cz
)
(
λ x1 x2 .
co
(
cv
x1
)
(
co
(
cv
x2
)
c1
cmin
)
cfz
)
)
⟶
wceq
cfl
(
cmpt
(
λ x1 .
cr
)
(
λ x1 .
crio
(
λ x2 .
wa
(
wbr
(
cv
x2
)
(
cv
x1
)
cle
)
(
wbr
(
cv
x1
)
(
co
(
cv
x2
)
c1
caddc
)
clt
)
)
(
λ x2 .
cz
)
)
)
⟶
wceq
cceil
(
cmpt
(
λ x1 .
cr
)
(
λ x1 .
cneg
(
cfv
(
cneg
(
cv
x1
)
)
cfl
)
)
)
⟶
wceq
cmo
(
cmpt2
(
λ x1 x2 .
cr
)
(
λ x1 x2 .
crp
)
(
λ x1 x2 .
co
(
cv
x1
)
(
co
(
cv
x2
)
(
cfv
(
co
(
cv
x1
)
(
cv
x2
)
cdiv
)
cfl
)
cmul
)
cmin
)
)
⟶
(
∀ x1 x2 x3 :
ι → ο
.
wceq
(
cseq
x1
x2
x3
)
(
cima
(
crdg
(
cmpt2
(
λ x4 x5 .
cvv
)
(
λ x4 x5 .
cvv
)
(
λ x4 x5 .
cop
(
co
(
cv
x4
)
c1
caddc
)
(
co
(
cv
x5
)
(
cfv
(
co
(
cv
x4
)
c1
caddc
)
x2
)
x1
)
)
)
(
cop
x3
(
cfv
x3
x2
)
)
)
com
)
)
⟶
wceq
cexp
(
cmpt2
(
λ x1 x2 .
cc
)
(
λ x1 x2 .
cz
)
(
λ x1 x2 .
cif
(
wceq
(
cv
x2
)
cc0
)
c1
(
cif
(
wbr
cc0
(
cv
x2
)
clt
)
(
cfv
(
cv
x2
)
(
cseq
cmul
(
cxp
cn
(
csn
(
cv
x1
)
)
)
c1
)
)
(
co
c1
(
cfv
(
cneg
(
cv
x2
)
)
(
cseq
cmul
(
cxp
cn
(
csn
(
cv
x1
)
)
)
c1
)
)
cdiv
)
)
)
)
⟶
wceq
cfa
(
cun
(
csn
(
cop
cc0
c1
)
)
(
cseq
cmul
cid
c1
)
)
⟶
wceq
cbc
(
cmpt2
(
λ x1 x2 .
cn0
)
(
λ x1 x2 .
cz
)
(
λ x1 x2 .
cif
(
wcel
(
cv
x2
)
(
co
cc0
(
cv
x1
)
cfz
)
)
(
co
(
cfv
(
cv
x1
)
cfa
)
(
co
(
cfv
(
co
(
cv
x1
)
(
cv
x2
)
cmin
)
cfa
)
(
cfv
(
cv
x2
)
cfa
)
cmul
)
cdiv
)
cc0
)
)
⟶
x0
)
⟶
x0
Theorem
df_q
:
wceq
cq
(
cima
cdiv
(
cxp
cz
cn
)
)
...
Theorem
df_rp
:
wceq
crp
(
crab
(
λ x0 .
wbr
cc0
(
cv
x0
)
clt
)
(
λ x0 .
cr
)
)
...
Theorem
df_xneg
:
∀ x0 :
ι → ο
.
wceq
(
cxne
x0
)
(
cif
(
wceq
x0
cpnf
)
cmnf
(
cif
(
wceq
x0
cmnf
)
cpnf
(
cneg
x0
)
)
)
...
Theorem
df_xadd
:
wceq
cxad
(
cmpt2
(
λ x0 x1 .
cxr
)
(
λ x0 x1 .
cxr
)
(
λ x0 x1 .
cif
(
wceq
(
cv
x0
)
cpnf
)
(
cif
(
wceq
(
cv
x1
)
cmnf
)
cc0
cpnf
)
(
cif
(
wceq
(
cv
x0
)
cmnf
)
(
cif
(
wceq
(
cv
x1
)
cpnf
)
cc0
cmnf
)
(
cif
(
wceq
(
cv
x1
)
cpnf
)
cpnf
(
cif
(
wceq
(
cv
x1
)
cmnf
)
cmnf
(
co
(
cv
x0
)
(
cv
x1
)
caddc
)
)
)
)
)
)
...
Theorem
df_xmul
:
wceq
cxmu
(
cmpt2
(
λ x0 x1 .
cxr
)
(
λ x0 x1 .
cxr
)
(
λ x0 x1 .
cif
(
wo
(
wceq
(
cv
x0
)
cc0
)
(
wceq
(
cv
x1
)
cc0
)
)
cc0
(
cif
(
wo
(
wo
(
wa
(
wbr
cc0
(
cv
x1
)
clt
)
(
wceq
(
cv
x0
)
cpnf
)
)
(
wa
(
wbr
(
cv
x1
)
cc0
clt
)
(
wceq
(
cv
x0
)
cmnf
)
)
)
(
wo
(
wa
(
wbr
cc0
(
cv
x0
)
clt
)
(
wceq
(
cv
x1
)
cpnf
)
)
(
wa
(
wbr
(
cv
x0
)
cc0
clt
)
(
wceq
(
cv
x1
)
cmnf
)
)
)
)
cpnf
(
cif
(
wo
(
wo
(
wa
(
wbr
cc0
(
cv
x1
)
clt
)
(
wceq
(
cv
x0
)
cmnf
)
)
(
wa
(
wbr
(
cv
x1
)
cc0
clt
)
(
wceq
(
cv
x0
)
cpnf
)
)
)
(
wo
(
wa
(
wbr
cc0
(
cv
x0
)
clt
)
(
wceq
(
cv
x1
)
cmnf
)
)
(
wa
(
wbr
(
cv
x0
)
cc0
clt
)
(
wceq
(
cv
x1
)
cpnf
)
)
)
)
cmnf
(
co
(
cv
x0
)
(
cv
x1
)
cmul
)
)
)
)
)
...
Theorem
df_ioo
:
wceq
cioo
(
cmpt2
(
λ x0 x1 .
cxr
)
(
λ x0 x1 .
cxr
)
(
λ x0 x1 .
crab
(
λ x2 .
wa
(
wbr
(
cv
x0
)
(
cv
x2
)
clt
)
(
wbr
(
cv
x2
)
(
cv
x1
)
clt
)
)
(
λ x2 .
cxr
)
)
)
...
Theorem
df_ioc
:
wceq
cioc
(
cmpt2
(
λ x0 x1 .
cxr
)
(
λ x0 x1 .
cxr
)
(
λ x0 x1 .
crab
(
λ x2 .
wa
(
wbr
(
cv
x0
)
(
cv
x2
)
clt
)
(
wbr
(
cv
x2
)
(
cv
x1
)
cle
)
)
(
λ x2 .
cxr
)
)
)
...
Theorem
df_ico
:
wceq
cico
(
cmpt2
(
λ x0 x1 .
cxr
)
(
λ x0 x1 .
cxr
)
(
λ x0 x1 .
crab
(
λ x2 .
wa
(
wbr
(
cv
x0
)
(
cv
x2
)
cle
)
(
wbr
(
cv
x2
)
(
cv
x1
)
clt
)
)
(
λ x2 .
cxr
)
)
)
...
Theorem
df_icc
:
wceq
cicc
(
cmpt2
(
λ x0 x1 .
cxr
)
(
λ x0 x1 .
cxr
)
(
λ x0 x1 .
crab
(
λ x2 .
wa
(
wbr
(
cv
x0
)
(
cv
x2
)
cle
)
(
wbr
(
cv
x2
)
(
cv
x1
)
cle
)
)
(
λ x2 .
cxr
)
)
)
...
Theorem
df_fz
:
wceq
cfz
(
cmpt2
(
λ x0 x1 .
cz
)
(
λ x0 x1 .
cz
)
(
λ x0 x1 .
crab
(
λ x2 .
wa
(
wbr
(
cv
x0
)
(
cv
x2
)
cle
)
(
wbr
(
cv
x2
)
(
cv
x1
)
cle
)
)
(
λ x2 .
cz
)
)
)
...
Theorem
df_fzo
:
wceq
cfzo
(
cmpt2
(
λ x0 x1 .
cz
)
(
λ x0 x1 .
cz
)
(
λ x0 x1 .
co
(
cv
x0
)
(
co
(
cv
x1
)
c1
cmin
)
cfz
)
)
...
Theorem
df_fl
:
wceq
cfl
(
cmpt
(
λ x0 .
cr
)
(
λ x0 .
crio
(
λ x1 .
wa
(
wbr
(
cv
x1
)
(
cv
x0
)
cle
)
(
wbr
(
cv
x0
)
(
co
(
cv
x1
)
c1
caddc
)
clt
)
)
(
λ x1 .
cz
)
)
)
...
Theorem
df_ceil
:
wceq
cceil
(
cmpt
(
λ x0 .
cr
)
(
λ x0 .
cneg
(
cfv
(
cneg
(
cv
x0
)
)
cfl
)
)
)
...
Theorem
df_mod
:
wceq
cmo
(
cmpt2
(
λ x0 x1 .
cr
)
(
λ x0 x1 .
crp
)
(
λ x0 x1 .
co
(
cv
x0
)
(
co
(
cv
x1
)
(
cfv
(
co
(
cv
x0
)
(
cv
x1
)
cdiv
)
cfl
)
cmul
)
cmin
)
)
...
Theorem
df_seq
:
∀ x0 x1 x2 :
ι → ο
.
wceq
(
cseq
x0
x1
x2
)
(
cima
(
crdg
(
cmpt2
(
λ x3 x4 .
cvv
)
(
λ x3 x4 .
cvv
)
(
λ x3 x4 .
cop
(
co
(
cv
x3
)
c1
caddc
)
(
co
(
cv
x4
)
(
cfv
(
co
(
cv
x3
)
c1
caddc
)
x1
)
x0
)
)
)
(
cop
x2
(
cfv
x2
x1
)
)
)
com
)
...
Theorem
df_exp
:
wceq
cexp
(
cmpt2
(
λ x0 x1 .
cc
)
(
λ x0 x1 .
cz
)
(
λ x0 x1 .
cif
(
wceq
(
cv
x1
)
cc0
)
c1
(
cif
(
wbr
cc0
(
cv
x1
)
clt
)
(
cfv
(
cv
x1
)
(
cseq
cmul
(
cxp
cn
(
csn
(
cv
x0
)
)
)
c1
)
)
(
co
c1
(
cfv
(
cneg
(
cv
x1
)
)
(
cseq
cmul
(
cxp
cn
(
csn
(
cv
x0
)
)
)
c1
)
)
cdiv
)
)
)
)
...
Theorem
df_fac
:
wceq
cfa
(
cun
(
csn
(
cop
cc0
c1
)
)
(
cseq
cmul
cid
c1
)
)
...
Theorem
df_bc
:
wceq
cbc
(
cmpt2
(
λ x0 x1 .
cn0
)
(
λ x0 x1 .
cz
)
(
λ x0 x1 .
cif
(
wcel
(
cv
x1
)
(
co
cc0
(
cv
x0
)
cfz
)
)
(
co
(
cfv
(
cv
x0
)
cfa
)
(
co
(
cfv
(
co
(
cv
x0
)
(
cv
x1
)
cmin
)
cfa
)
(
cfv
(
cv
x1
)
cfa
)
cmul
)
cdiv
)
cc0
)
)
...