Search for blocks/addresses/...
Proofgold Signed Transaction
vin
PrNeb..
/
7f334..
PUYBZ..
/
15bb2..
vout
PrNeb..
/
e3716..
0.00 bars
TMMS2..
/
fd80d..
ownership of
442b3..
as prop with payaddr
PrGxv..
rightscost 0.00 controlledby
PrGxv..
upto 0
TMNrb..
/
1d2da..
ownership of
0ea3a..
as prop with payaddr
PrGxv..
rightscost 0.00 controlledby
PrGxv..
upto 0
TMQRA..
/
70179..
ownership of
f9e57..
as prop with payaddr
PrGxv..
rightscost 0.00 controlledby
PrGxv..
upto 0
TMLdE..
/
10e5e..
ownership of
e7a58..
as prop with payaddr
PrGxv..
rightscost 0.00 controlledby
PrGxv..
upto 0
TMNex..
/
7cd91..
ownership of
2c199..
as prop with payaddr
PrGxv..
rightscost 0.00 controlledby
PrGxv..
upto 0
TMNSy..
/
fbf96..
ownership of
b9b99..
as prop with payaddr
PrGxv..
rightscost 0.00 controlledby
PrGxv..
upto 0
PUhu1..
/
bd510..
doc published by
PrGxv..
Param
lam
Sigma
:
ι
→
(
ι
→
ι
) →
ι
Definition
setprod
setprod
:=
λ x0 x1 .
lam
x0
(
λ x2 .
x1
)
Param
ap
ap
:
ι
→
ι
→
ι
Known
ap0_Sigma
ap0_Sigma
:
∀ x0 .
∀ x1 :
ι → ι
.
∀ x2 .
x2
∈
lam
x0
x1
⟶
ap
x2
0
∈
x0
Theorem
2c199..
:
∀ x0 x1 x2 .
x2
∈
setprod
x0
x1
⟶
ap
x2
0
∈
x0
(proof)
Param
ordsucc
ordsucc
:
ι
→
ι
Known
ap1_Sigma
ap1_Sigma
:
∀ x0 .
∀ x1 :
ι → ι
.
∀ x2 .
x2
∈
lam
x0
x1
⟶
ap
x2
1
∈
x1
(
ap
x2
0
)
Theorem
f9e57..
:
∀ x0 x1 x2 .
x2
∈
setprod
x0
x1
⟶
ap
x2
1
∈
x1
(proof)
Param
If_i
If_i
:
ο
→
ι
→
ι
→
ι
Known
tuple_Sigma_eta
tuple_Sigma_eta
:
∀ x0 .
∀ x1 :
ι → ι
.
∀ x2 .
x2
∈
lam
x0
x1
⟶
lam
2
(
λ x4 .
If_i
(
x4
=
0
)
(
ap
x2
0
)
(
ap
x2
1
)
)
=
x2
Theorem
442b3..
:
∀ x0 x1 x2 .
x2
∈
setprod
x0
x1
⟶
lam
2
(
λ x4 .
If_i
(
x4
=
0
)
(
ap
x2
0
)
(
ap
x2
1
)
)
=
x2
(proof)