Search for blocks/addresses/...
Proofgold Signed Transaction
vin
PrQPb..
/
a3fa5..
PUM3M..
/
787f1..
vout
PrQPb..
/
93f69..
19.99 bars
TMV9d..
/
6e154..
negprop ownership controlledby
Pr6Pc..
upto 0
TMaPH..
/
f100b..
ownership of
5eb9b..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMYmp..
/
5a832..
ownership of
eabc1..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMSKJ..
/
8ab8f..
ownership of
651e5..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMZZC..
/
d87aa..
ownership of
36457..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMNky..
/
19d24..
ownership of
b20e6..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMFuo..
/
391a1..
ownership of
4de6f..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
PUbuz..
/
035a5..
doc published by
Pr6Pc..
Definition
and
and
:=
λ x0 x1 : ο .
∀ x2 : ο .
(
x0
⟶
x1
⟶
x2
)
⟶
x2
Definition
bij
bij
:=
λ x0 x1 .
λ x2 :
ι → ι
.
and
(
and
(
∀ x3 .
x3
∈
x0
⟶
x2
x3
∈
x1
)
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
x2
x3
=
x2
x4
⟶
x3
=
x4
)
)
(
∀ x3 .
x3
∈
x1
⟶
∀ x4 : ο .
(
∀ x5 .
and
(
x5
∈
x0
)
(
x2
x5
=
x3
)
⟶
x4
)
⟶
x4
)
Definition
surj
surj
:=
λ x0 x1 .
λ x2 :
ι → ι
.
and
(
∀ x3 .
x3
∈
x0
⟶
x2
x3
∈
x1
)
(
∀ x3 .
x3
∈
x1
⟶
∀ x4 : ο .
(
∀ x5 .
and
(
x5
∈
x0
)
(
x2
x5
=
x3
)
⟶
x4
)
⟶
x4
)
Known
andI
andI
:
∀ x0 x1 : ο .
x0
⟶
x1
⟶
and
x0
x1
Known
bij_surj
bij_surj
:
∀ x0 x1 .
∀ x2 :
ι → ι
.
bij
x0
x1
x2
⟶
surj
x0
x1
x2
Definition
False
False
:=
∀ x0 : ο .
x0
Definition
not
not
:=
λ x0 : ο .
x0
⟶
False
Param
omega
omega
:
ι
Param
Sep
Sep
:
ι
→
(
ι
→
ο
) →
ι
Definition
nIn
nIn
:=
λ x0 x1 .
not
(
x0
∈
x1
)
Known
SepI
SepI
:
∀ x0 .
∀ x1 :
ι → ο
.
∀ x2 .
x2
∈
x0
⟶
x1
x2
⟶
x2
∈
Sep
x0
x1
Known
SepE2
SepE2
:
∀ x0 .
∀ x1 :
ι → ο
.
∀ x2 .
x2
∈
Sep
x0
x1
⟶
x1
x2
Definition
Subq
Subq
:=
λ x0 x1 .
∀ x2 .
x2
∈
x0
⟶
x2
∈
x1
Known
PowerI
PowerI
:
∀ x0 x1 .
x1
⊆
x0
⟶
x1
∈
prim4
x0
Known
SepE1
SepE1
:
∀ x0 .
∀ x1 :
ι → ο
.
∀ x2 .
x2
∈
Sep
x0
x1
⟶
x2
∈
x0
Theorem
form100_22_v3
form100_22_v3
:
∀ x0 :
ι → ι
.
not
(
surj
omega
(
prim4
omega
)
x0
)
(proof)
Param
ccad8..
:
ι
→
ι
→
ο
Known
536c8..
:
∀ x0 x1 .
ccad8..
x0
x1
⟶
∀ x2 : ο .
(
∀ x3 :
ι → ι
.
bij
x0
x1
x3
⟶
x2
)
⟶
x2
Theorem
651e5..
:
not
(
ccad8..
omega
(
prim4
omega
)
)
(proof)
Definition
inj
inj
:=
λ x0 x1 .
λ x2 :
ι → ι
.
and
(
∀ x3 .
x3
∈
x0
⟶
x2
x3
∈
x1
)
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
x2
x3
=
x2
x4
⟶
x3
=
x4
)
Param
ReplSep
ReplSep
:
ι
→
(
ι
→
ο
) →
(
ι
→
ι
) →
ι
Known
ReplSepI
ReplSepI
:
∀ x0 .
∀ x1 :
ι → ο
.
∀ x2 :
ι → ι
.
∀ x3 .
x3
∈
x0
⟶
x1
x3
⟶
x2
x3
∈
ReplSep
x0
x1
x2
Known
ReplSepE_impred
ReplSepE_impred
:
∀ x0 .
∀ x1 :
ι → ο
.
∀ x2 :
ι → ι
.
∀ x3 .
x3
∈
ReplSep
x0
x1
x2
⟶
∀ x4 : ο .
(
∀ x5 .
x5
∈
x0
⟶
x1
x5
⟶
x3
=
x2
x5
⟶
x4
)
⟶
x4
Theorem
form100_22_v2
form100_22_v2
:
∀ x0 :
ι → ι
.
not
(
inj
(
prim4
omega
)
omega
x0
)
(proof)