Search for blocks/addresses/...
Proofgold Asset
asset id
bd510fda85f12f1b95f01abdeb8c4eae28a8e962522c1e5bc8b7107e928dff87
asset hash
dc341e37a04fb6845afac8d3f5be8109a5459481848ee65a45375a3b26450ac1
bday / block
16946
tx
e55e5..
preasset
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)