Search for blocks/addresses/...
Proofgold Signed Transaction
vin
PrS2B..
/
fa922..
PUe9x..
/
6faf6..
vout
PrS2B..
/
cfcab..
0.00 bars
TMc2Z..
/
cf432..
ownership of
5bea3..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMUcA..
/
7fff5..
ownership of
2a3ea..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMMyX..
/
3f450..
ownership of
ca554..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMHnw..
/
9569d..
ownership of
e2935..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMS8h..
/
3592f..
ownership of
3a34f..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMaeC..
/
39955..
ownership of
22158..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
PUbvB..
/
e769d..
doc published by
Pr4zB..
Definition
Church6_p
:=
λ x0 :
ι →
ι →
ι →
ι →
ι →
ι → ι
.
∀ x1 :
(
ι →
ι →
ι →
ι →
ι →
ι → ι
)
→ ο
.
x1
(
λ x2 x3 x4 x5 x6 x7 .
x2
)
⟶
x1
(
λ x2 x3 x4 x5 x6 x7 .
x3
)
⟶
x1
(
λ x2 x3 x4 x5 x6 x7 .
x4
)
⟶
x1
(
λ x2 x3 x4 x5 x6 x7 .
x5
)
⟶
x1
(
λ x2 x3 x4 x5 x6 x7 .
x6
)
⟶
x1
(
λ x2 x3 x4 x5 x6 x7 .
x7
)
⟶
x1
x0
Definition
Church6_lt4p
:=
λ x0 :
ι →
ι →
ι →
ι →
ι →
ι → ι
.
∀ x1 :
(
ι →
ι →
ι →
ι →
ι →
ι → ι
)
→ ο
.
x1
(
λ x2 x3 x4 x5 x6 x7 .
x2
)
⟶
x1
(
λ x2 x3 x4 x5 x6 x7 .
x3
)
⟶
x1
(
λ x2 x3 x4 x5 x6 x7 .
x4
)
⟶
x1
(
λ x2 x3 x4 x5 x6 x7 .
x5
)
⟶
x1
x0
Definition
permargs_i_1_0_3_2_4_5
:=
λ x0 :
ι →
ι →
ι →
ι →
ι →
ι → ι
.
λ x1 x2 x3 x4 .
x0
x2
x1
x4
x3
Definition
Church6_squared_permutation__1_0_3_2_4_5__1_0_3_2_4_5__1_0_3_2_4_5__1_0_3_2_4_5__1_0_3_2_4_5__1_0_3_2_4_5
:=
λ x0 x1 :
ι →
ι →
ι →
ι →
ι →
ι → ι
.
λ x2 x3 x4 x5 x6 x7 .
x0
(
permargs_i_1_0_3_2_4_5
x1
x2
x3
x4
x5
x7
x6
)
(
permargs_i_1_0_3_2_4_5
x1
x2
x3
x4
x5
x7
x6
)
(
permargs_i_1_0_3_2_4_5
x1
x2
x3
x4
x5
x7
x6
)
(
permargs_i_1_0_3_2_4_5
x1
x2
x3
x4
x5
x7
x6
)
(
permargs_i_1_0_3_2_4_5
x1
x2
x3
x4
x5
x7
x6
)
(
permargs_i_1_0_3_2_4_5
x1
x2
x3
x4
x5
x6
x7
)
Known
3f4a9..
:
∀ x0 :
ι →
ι →
ι →
ι →
ι →
ι → ι
.
Church6_lt4p
x0
⟶
Church6_lt4p
(
permargs_i_1_0_3_2_4_5
x0
)
Known
bc219..
:
Church6_lt4p
(
λ x0 x1 x2 x3 x4 x5 .
x1
)
Known
39a8c..
:
Church6_lt4p
(
λ x0 x1 x2 x3 x4 x5 .
x0
)
Known
22a13..
:
Church6_lt4p
(
λ x0 x1 x2 x3 x4 x5 .
x3
)
Known
a050d..
:
Church6_lt4p
(
λ x0 x1 x2 x3 x4 x5 .
x2
)
Theorem
3a34f..
:
∀ x0 :
ι →
ι →
ι →
ι →
ι →
ι → ι
.
Church6_p
x0
⟶
∀ x1 :
ι →
ι →
ι →
ι →
ι →
ι → ι
.
Church6_lt4p
x1
⟶
Church6_lt4p
(
Church6_squared_permutation__1_0_3_2_4_5__1_0_3_2_4_5__1_0_3_2_4_5__1_0_3_2_4_5__1_0_3_2_4_5__1_0_3_2_4_5
x0
x1
)
(proof)
Definition
permargs_i_2_3_0_1_4_5
:=
λ x0 :
ι →
ι →
ι →
ι →
ι →
ι → ι
.
λ x1 x2 x3 x4 .
x0
x3
x4
x1
x2
Definition
Church6_squared_permutation__2_3_0_1_4_5__2_3_0_1_4_5__2_3_0_1_4_5__2_3_0_1_4_5__2_3_0_1_4_5__2_3_0_1_4_5
:=
λ x0 x1 :
ι →
ι →
ι →
ι →
ι →
ι → ι
.
λ x2 x3 x4 x5 x6 x7 .
x0
(
permargs_i_2_3_0_1_4_5
x1
x2
x3
x4
x5
x7
x6
)
(
permargs_i_2_3_0_1_4_5
x1
x2
x3
x4
x5
x6
x7
)
(
permargs_i_2_3_0_1_4_5
x1
x2
x3
x4
x5
x6
x7
)
(
permargs_i_2_3_0_1_4_5
x1
x2
x3
x4
x5
x7
x6
)
(
permargs_i_2_3_0_1_4_5
x1
x2
x3
x4
x5
x6
x7
)
(
permargs_i_2_3_0_1_4_5
x1
x2
x3
x4
x5
x6
x7
)
Known
bc9c2..
:
∀ x0 :
ι →
ι →
ι →
ι →
ι →
ι → ι
.
Church6_lt4p
x0
⟶
Church6_lt4p
(
permargs_i_2_3_0_1_4_5
x0
)
Theorem
ca554..
:
∀ x0 :
ι →
ι →
ι →
ι →
ι →
ι → ι
.
Church6_p
x0
⟶
∀ x1 :
ι →
ι →
ι →
ι →
ι →
ι → ι
.
Church6_lt4p
x1
⟶
Church6_lt4p
(
Church6_squared_permutation__2_3_0_1_4_5__2_3_0_1_4_5__2_3_0_1_4_5__2_3_0_1_4_5__2_3_0_1_4_5__2_3_0_1_4_5
x0
x1
)
(proof)
Definition
permargs_i_3_2_1_0_4_5
:=
λ x0 :
ι →
ι →
ι →
ι →
ι →
ι → ι
.
λ x1 x2 x3 x4 .
x0
x4
x3
x2
x1
Definition
Church6_squared_permutation__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5
:=
λ x0 x1 :
ι →
ι →
ι →
ι →
ι →
ι → ι
.
λ x2 x3 x4 x5 x6 x7 .
x0
(
permargs_i_3_2_1_0_4_5
x1
x2
x3
x4
x5
x6
x7
)
(
permargs_i_3_2_1_0_4_5
x1
x2
x3
x4
x5
x7
x6
)
(
permargs_i_3_2_1_0_4_5
x1
x2
x3
x4
x5
x7
x6
)
(
permargs_i_3_2_1_0_4_5
x1
x2
x3
x4
x5
x6
x7
)
(
permargs_i_3_2_1_0_4_5
x1
x2
x3
x4
x5
x7
x6
)
(
permargs_i_3_2_1_0_4_5
x1
x2
x3
x4
x5
x6
x7
)
Known
bcfec..
:
∀ x0 :
ι →
ι →
ι →
ι →
ι →
ι → ι
.
Church6_lt4p
x0
⟶
Church6_lt4p
(
permargs_i_3_2_1_0_4_5
x0
)
Theorem
5bea3..
:
∀ x0 :
ι →
ι →
ι →
ι →
ι →
ι → ι
.
Church6_p
x0
⟶
∀ x1 :
ι →
ι →
ι →
ι →
ι →
ι → ι
.
Church6_lt4p
x1
⟶
Church6_lt4p
(
Church6_squared_permutation__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5
x0
x1
)
(proof)