Search for blocks/addresses/...
Proofgold Signed Transaction
vin
PrCit..
/
808dc..
PUe2T..
/
e3f71..
vout
PrCit..
/
06368..
4.91 bars
TMaug..
/
423a4..
ownership of
7a51b..
as prop with payaddr
Pr4zB..
rightscost 0.00 controlledby
Pr4zB..
upto 0
TMWi6..
/
eff8a..
ownership of
1f833..
as prop with payaddr
Pr4zB..
rightscost 0.00 controlledby
Pr4zB..
upto 0
TMScZ..
/
21c4b..
ownership of
0b928..
as prop with payaddr
Pr4zB..
rightscost 0.00 controlledby
Pr4zB..
upto 0
TMFXM..
/
0b9e4..
ownership of
88072..
as prop with payaddr
Pr4zB..
rightscost 0.00 controlledby
Pr4zB..
upto 0
TMW4r..
/
027f2..
ownership of
b98f5..
as prop with payaddr
Pr4zB..
rightscost 0.00 controlledby
Pr4zB..
upto 0
TMGGa..
/
f8758..
ownership of
4f5b2..
as prop with payaddr
Pr4zB..
rightscost 0.00 controlledby
Pr4zB..
upto 0
TMdvV..
/
74708..
ownership of
f4bbb..
as prop with payaddr
Pr4zB..
rightscost 0.00 controlledby
Pr4zB..
upto 0
TMM1F..
/
4b7d0..
ownership of
aa5dc..
as prop with payaddr
Pr4zB..
rightscost 0.00 controlledby
Pr4zB..
upto 0
TMJaM..
/
7879b..
ownership of
b410a..
as prop with payaddr
Pr4zB..
rightscost 0.00 controlledby
Pr4zB..
upto 0
TMUAK..
/
c98d4..
ownership of
4872c..
as prop with payaddr
Pr4zB..
rightscost 0.00 controlledby
Pr4zB..
upto 0
TMQwS..
/
859a8..
ownership of
b4e0c..
as prop with payaddr
Pr4zB..
rightscost 0.00 controlledby
Pr4zB..
upto 0
TMUbV..
/
8565d..
ownership of
c63c0..
as prop with payaddr
Pr4zB..
rightscost 0.00 controlledby
Pr4zB..
upto 0
TMceD..
/
5a522..
ownership of
b4e23..
as prop with payaddr
Pr4zB..
rightscost 0.00 controlledby
Pr4zB..
upto 0
TMGBd..
/
a07ae..
ownership of
9a709..
as prop with payaddr
Pr4zB..
rightscost 0.00 controlledby
Pr4zB..
upto 0
TMMua..
/
b74e4..
ownership of
3ac64..
as prop with payaddr
Pr4zB..
rightscost 0.00 controlledby
Pr4zB..
upto 0
TMMHP..
/
34e1d..
ownership of
1df6c..
as prop with payaddr
Pr4zB..
rightscost 0.00 controlledby
Pr4zB..
upto 0
TMK9C..
/
c762d..
ownership of
60d0e..
as prop with payaddr
Pr4zB..
rightscost 0.00 controlledby
Pr4zB..
upto 0
TMR6P..
/
50d94..
ownership of
c75cf..
as prop with payaddr
Pr4zB..
rightscost 0.00 controlledby
Pr4zB..
upto 0
TMVxz..
/
f4077..
ownership of
985a3..
as prop with payaddr
Pr4zB..
rightscost 0.00 controlledby
Pr4zB..
upto 0
TMTQf..
/
2e876..
ownership of
72649..
as prop with payaddr
Pr4zB..
rightscost 0.00 controlledby
Pr4zB..
upto 0
TMJc5..
/
a3f47..
ownership of
3b8c0..
as prop with payaddr
Pr4zB..
rightscost 0.00 controlledby
Pr4zB..
upto 0
TMJDo..
/
38253..
ownership of
90460..
as prop with payaddr
Pr4zB..
rightscost 0.00 controlledby
Pr4zB..
upto 0
TMG6S..
/
8b624..
ownership of
38ba0..
as prop with payaddr
Pr4zB..
rightscost 0.00 controlledby
Pr4zB..
upto 0
TMZrk..
/
f30d5..
ownership of
1b4f2..
as prop with payaddr
Pr4zB..
rightscost 0.00 controlledby
Pr4zB..
upto 0
TMdfF..
/
17adb..
ownership of
fed6d..
as prop with payaddr
Pr4zB..
rightscost 0.00 controlledby
Pr4zB..
upto 0
TMLRR..
/
dca42..
ownership of
d1ab6..
as prop with payaddr
Pr4zB..
rightscost 0.00 controlledby
Pr4zB..
upto 0
TMPS9..
/
f35eb..
ownership of
33924..
as prop with payaddr
Pr4zB..
rightscost 0.00 controlledby
Pr4zB..
upto 0
TMRTT..
/
e84e6..
ownership of
d3b79..
as prop with payaddr
Pr4zB..
rightscost 0.00 controlledby
Pr4zB..
upto 0
TMcLd..
/
8dfb3..
ownership of
89684..
as prop with payaddr
Pr4zB..
rightscost 0.00 controlledby
Pr4zB..
upto 0
TMa36..
/
2357e..
ownership of
d77ac..
as prop with payaddr
Pr4zB..
rightscost 0.00 controlledby
Pr4zB..
upto 0
TMPa7..
/
29414..
ownership of
a0d60..
as prop with payaddr
Pr4zB..
rightscost 0.00 controlledby
Pr4zB..
upto 0
TMFhL..
/
e7fc6..
ownership of
92052..
as prop with payaddr
Pr4zB..
rightscost 0.00 controlledby
Pr4zB..
upto 0
TMR8M..
/
ce5b1..
ownership of
a7cad..
as prop with payaddr
Pr4zB..
rightscost 0.00 controlledby
Pr4zB..
upto 0
TMXBT..
/
b52c6..
ownership of
487e0..
as prop with payaddr
Pr4zB..
rightscost 0.00 controlledby
Pr4zB..
upto 0
TMNDQ..
/
683a2..
ownership of
a1243..
as prop with payaddr
Pr4zB..
rightscost 0.00 controlledby
Pr4zB..
upto 0
TMQUB..
/
ba2cb..
ownership of
5e063..
as prop with payaddr
Pr4zB..
rightscost 0.00 controlledby
Pr4zB..
upto 0
TMb6f..
/
07de6..
ownership of
f957d..
as prop with payaddr
Pr4zB..
rightscost 0.00 controlledby
Pr4zB..
upto 0
TMbTE..
/
d809a..
ownership of
9b7e0..
as prop with payaddr
Pr4zB..
rightscost 0.00 controlledby
Pr4zB..
upto 0
TMJx9..
/
7bff0..
ownership of
17ae2..
as prop with payaddr
Pr4zB..
rightscost 0.00 controlledby
Pr4zB..
upto 0
TMKNZ..
/
031c4..
ownership of
4c4a3..
as prop with payaddr
Pr4zB..
rightscost 0.00 controlledby
Pr4zB..
upto 0
TMUyh..
/
abf77..
ownership of
28e18..
as prop with payaddr
Pr4zB..
rightscost 0.00 controlledby
Pr4zB..
upto 0
TMaq1..
/
99366..
ownership of
4d859..
as prop with payaddr
Pr4zB..
rightscost 0.00 controlledby
Pr4zB..
upto 0
TMVCT..
/
b2dc6..
ownership of
41e6a..
as prop with payaddr
Pr4zB..
rightscost 0.00 controlledby
Pr4zB..
upto 0
TMZpf..
/
ac687..
ownership of
c2058..
as prop with payaddr
Pr4zB..
rightscost 0.00 controlledby
Pr4zB..
upto 0
TMNC3..
/
c21a7..
ownership of
3b22d..
as prop with payaddr
Pr4zB..
rightscost 0.00 controlledby
Pr4zB..
upto 0
TMWJt..
/
4b508..
ownership of
829cc..
as prop with payaddr
Pr4zB..
rightscost 0.00 controlledby
Pr4zB..
upto 0
TMZFo..
/
70cad..
ownership of
8c295..
as prop with payaddr
Pr4zB..
rightscost 0.00 controlledby
Pr4zB..
upto 0
TMEgb..
/
ab315..
ownership of
616c9..
as prop with payaddr
Pr4zB..
rightscost 0.00 controlledby
Pr4zB..
upto 0
TMEsd..
/
28742..
ownership of
bebec..
as prop with payaddr
Pr4zB..
rightscost 0.00 controlledby
Pr4zB..
upto 0
TMbeo..
/
784a7..
ownership of
043e4..
as prop with payaddr
Pr4zB..
rightscost 0.00 controlledby
Pr4zB..
upto 0
TMZs3..
/
8d198..
ownership of
2d0c6..
as prop with payaddr
Pr4zB..
rightscost 0.00 controlledby
Pr4zB..
upto 0
TMWPK..
/
84094..
ownership of
331ad..
as prop with payaddr
Pr4zB..
rightscost 0.00 controlledby
Pr4zB..
upto 0
TMVkX..
/
fbfa1..
ownership of
884c6..
as obj with payaddr
Pr4zB..
rightscost 0.00 controlledby
Pr4zB..
upto 0
TMPPg..
/
20957..
ownership of
89013..
as obj with payaddr
Pr4zB..
rightscost 0.00 controlledby
Pr4zB..
upto 0
TMTsk..
/
03b8b..
ownership of
4aafd..
as obj with payaddr
Pr4zB..
rightscost 0.00 controlledby
Pr4zB..
upto 0
TMLuC..
/
0e9a4..
ownership of
673af..
as obj with payaddr
Pr4zB..
rightscost 0.00 controlledby
Pr4zB..
upto 0
TMLNF..
/
78db3..
ownership of
8915b..
as obj with payaddr
Pr4zB..
rightscost 0.00 controlledby
Pr4zB..
upto 0
TMdQF..
/
0e210..
ownership of
a73ce..
as obj with payaddr
Pr4zB..
rightscost 0.00 controlledby
Pr4zB..
upto 0
TMGkd..
/
0b2ce..
ownership of
d82dc..
as obj with payaddr
Pr4zB..
rightscost 0.00 controlledby
Pr4zB..
upto 0
TMP3S..
/
86544..
ownership of
d45c1..
as obj with payaddr
Pr4zB..
rightscost 0.00 controlledby
Pr4zB..
upto 0
TMMHi..
/
65f3a..
ownership of
8b66f..
as obj with payaddr
Pr4zB..
rightscost 0.00 controlledby
Pr4zB..
upto 0
TMExm..
/
34290..
ownership of
eb5db..
as obj with payaddr
Pr4zB..
rightscost 0.00 controlledby
Pr4zB..
upto 0
TMaN2..
/
e364c..
ownership of
68312..
as obj with payaddr
Pr4zB..
rightscost 0.00 controlledby
Pr4zB..
upto 0
TMWEQ..
/
c4ecd..
ownership of
d09d2..
as obj with payaddr
Pr4zB..
rightscost 0.00 controlledby
Pr4zB..
upto 0
PULrD..
/
4b476..
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
Theorem
2d0c6..
:
Church6_p
(
λ x0 x1 x2 x3 x4 x5 .
x0
)
(proof)
Theorem
bebec..
:
Church6_p
(
λ x0 x1 x2 x3 x4 x5 .
x1
)
(proof)
Theorem
8c295..
:
Church6_p
(
λ x0 x1 x2 x3 x4 x5 .
x2
)
(proof)
Theorem
3b22d..
:
Church6_p
(
λ x0 x1 x2 x3 x4 x5 .
x3
)
(proof)
Theorem
41e6a..
:
Church6_p
(
λ x0 x1 x2 x3 x4 x5 .
x4
)
(proof)
Theorem
28e18..
:
Church6_p
(
λ x0 x1 x2 x3 x4 x5 .
x5
)
(proof)
Param
ordsucc
ordsucc
:
ι
→
ι
Definition
u1
:=
1
Param
u2
:
ι
Param
u3
:
ι
Param
u4
:
ι
Param
u5
:
ι
Definition
Church6_to_u6
:=
λ x0 :
ι →
ι →
ι →
ι →
ι →
ι → ι
.
x0
0
u1
u2
u3
u4
u5
Param
u6
:
ι
Known
cases_6
cases_6
:
∀ x0 .
x0
∈
u6
⟶
∀ x1 :
ι → ο
.
x1
0
⟶
x1
u1
⟶
x1
u2
⟶
x1
u3
⟶
x1
u4
⟶
x1
u5
⟶
x1
x0
Theorem
cases_6
cases_6
:
∀ x0 .
x0
∈
u6
⟶
∀ x1 :
ι → ο
.
x1
0
⟶
x1
u1
⟶
x1
u2
⟶
x1
u3
⟶
x1
u4
⟶
x1
u5
⟶
x1
x0
(proof)
Known
In_0_6
In_0_6
:
0
∈
u6
Theorem
In_0_6
In_0_6
:
0
∈
u6
(proof)
Known
In_1_6
In_1_6
:
u1
∈
u6
Theorem
In_1_6
In_1_6
:
u1
∈
u6
(proof)
Known
In_2_6
In_2_6
:
u2
∈
u6
Theorem
In_2_6
In_2_6
:
u2
∈
u6
(proof)
Known
In_3_6
In_3_6
:
u3
∈
u6
Theorem
In_3_6
In_3_6
:
u3
∈
u6
(proof)
Known
In_4_6
In_4_6
:
u4
∈
u6
Theorem
In_4_6
In_4_6
:
u4
∈
u6
(proof)
Known
In_5_6
In_5_6
:
u5
∈
u6
Theorem
In_5_6
In_5_6
:
u5
∈
u6
(proof)
Theorem
17ae2..
:
∀ x0 .
x0
∈
u6
⟶
∀ x1 : ο .
(
∀ x2 :
ι →
ι →
ι →
ι →
ι →
ι → ι
.
Church6_p
x2
⟶
x0
=
Church6_to_u6
x2
⟶
x1
)
⟶
x1
(proof)
Param
ap
ap
:
ι
→
ι
→
ι
Param
lam
Sigma
:
ι
→
(
ι
→
ι
) →
ι
Param
If_i
If_i
:
ο
→
ι
→
ι
→
ι
Definition
nth_6_tuple
:=
λ x0 x1 x2 x3 x4 x5 x6 .
ap
(
lam
6
(
λ x7 .
If_i
(
x7
=
0
)
x1
(
If_i
(
x7
=
1
)
x2
(
If_i
(
x7
=
2
)
x3
(
If_i
(
x7
=
3
)
x4
(
If_i
(
x7
=
4
)
x5
x6
)
)
)
)
)
)
x0
Theorem
f957d..
:
∀ x0 .
∀ x1 :
ι →
ι →
ι →
ι →
ι →
ι → ι
.
(
∀ x2 x3 x4 x5 x6 x7 .
nth_6_tuple
x0
x2
x3
x4
x5
x6
x7
=
x1
x2
x3
x4
x5
x6
x7
)
⟶
nth_6_tuple
x0
=
x1
(proof)
Known
tuple_6_1_eq
tuple_6_1_eq
:
∀ x0 x1 x2 x3 x4 x5 .
ap
(
lam
6
(
λ x7 .
If_i
(
x7
=
0
)
x0
(
If_i
(
x7
=
1
)
x1
(
If_i
(
x7
=
2
)
x2
(
If_i
(
x7
=
3
)
x3
(
If_i
(
x7
=
4
)
x4
x5
)
)
)
)
)
)
u1
=
x1
Theorem
tuple_6_1_eq
tuple_6_1_eq
:
∀ x0 x1 x2 x3 x4 x5 .
ap
(
lam
6
(
λ x7 .
If_i
(
x7
=
0
)
x0
(
If_i
(
x7
=
1
)
x1
(
If_i
(
x7
=
2
)
x2
(
If_i
(
x7
=
3
)
x3
(
If_i
(
x7
=
4
)
x4
x5
)
)
)
)
)
)
u1
=
x1
(proof)
Known
tuple_6_2_eq
tuple_6_2_eq
:
∀ x0 x1 x2 x3 x4 x5 .
ap
(
lam
6
(
λ x7 .
If_i
(
x7
=
0
)
x0
(
If_i
(
x7
=
1
)
x1
(
If_i
(
x7
=
2
)
x2
(
If_i
(
x7
=
3
)
x3
(
If_i
(
x7
=
4
)
x4
x5
)
)
)
)
)
)
u2
=
x2
Theorem
tuple_6_2_eq
tuple_6_2_eq
:
∀ x0 x1 x2 x3 x4 x5 .
ap
(
lam
6
(
λ x7 .
If_i
(
x7
=
0
)
x0
(
If_i
(
x7
=
1
)
x1
(
If_i
(
x7
=
2
)
x2
(
If_i
(
x7
=
3
)
x3
(
If_i
(
x7
=
4
)
x4
x5
)
)
)
)
)
)
u2
=
x2
(proof)
Known
tuple_6_3_eq
tuple_6_3_eq
:
∀ x0 x1 x2 x3 x4 x5 .
ap
(
lam
6
(
λ x7 .
If_i
(
x7
=
0
)
x0
(
If_i
(
x7
=
1
)
x1
(
If_i
(
x7
=
2
)
x2
(
If_i
(
x7
=
3
)
x3
(
If_i
(
x7
=
4
)
x4
x5
)
)
)
)
)
)
u3
=
x3
Theorem
tuple_6_3_eq
tuple_6_3_eq
:
∀ x0 x1 x2 x3 x4 x5 .
ap
(
lam
6
(
λ x7 .
If_i
(
x7
=
0
)
x0
(
If_i
(
x7
=
1
)
x1
(
If_i
(
x7
=
2
)
x2
(
If_i
(
x7
=
3
)
x3
(
If_i
(
x7
=
4
)
x4
x5
)
)
)
)
)
)
u3
=
x3
(proof)
Known
tuple_6_4_eq
tuple_6_4_eq
:
∀ x0 x1 x2 x3 x4 x5 .
ap
(
lam
6
(
λ x7 .
If_i
(
x7
=
0
)
x0
(
If_i
(
x7
=
1
)
x1
(
If_i
(
x7
=
2
)
x2
(
If_i
(
x7
=
3
)
x3
(
If_i
(
x7
=
4
)
x4
x5
)
)
)
)
)
)
u4
=
x4
Theorem
tuple_6_4_eq
tuple_6_4_eq
:
∀ x0 x1 x2 x3 x4 x5 .
ap
(
lam
6
(
λ x7 .
If_i
(
x7
=
0
)
x0
(
If_i
(
x7
=
1
)
x1
(
If_i
(
x7
=
2
)
x2
(
If_i
(
x7
=
3
)
x3
(
If_i
(
x7
=
4
)
x4
x5
)
)
)
)
)
)
u4
=
x4
(proof)
Known
tuple_6_5_eq
tuple_6_5_eq
:
∀ x0 x1 x2 x3 x4 x5 .
ap
(
lam
6
(
λ x7 .
If_i
(
x7
=
0
)
x0
(
If_i
(
x7
=
1
)
x1
(
If_i
(
x7
=
2
)
x2
(
If_i
(
x7
=
3
)
x3
(
If_i
(
x7
=
4
)
x4
x5
)
)
)
)
)
)
u5
=
x5
Theorem
tuple_6_5_eq
tuple_6_5_eq
:
∀ x0 x1 x2 x3 x4 x5 .
ap
(
lam
6
(
λ x7 .
If_i
(
x7
=
0
)
x0
(
If_i
(
x7
=
1
)
x1
(
If_i
(
x7
=
2
)
x2
(
If_i
(
x7
=
3
)
x3
(
If_i
(
x7
=
4
)
x4
x5
)
)
)
)
)
)
u5
=
x5
(proof)
Known
tuple_6_0_eq
tuple_6_0_eq
:
∀ x0 x1 x2 x3 x4 x5 .
ap
(
lam
6
(
λ x7 .
If_i
(
x7
=
0
)
x0
(
If_i
(
x7
=
1
)
x1
(
If_i
(
x7
=
2
)
x2
(
If_i
(
x7
=
3
)
x3
(
If_i
(
x7
=
4
)
x4
x5
)
)
)
)
)
)
0
=
x0
Theorem
a1243..
:
nth_6_tuple
0
=
λ x1 x2 x3 x4 x5 x6 .
x1
(proof)
Theorem
a7cad..
:
nth_6_tuple
u1
=
λ x1 x2 x3 x4 x5 x6 .
x2
(proof)
Theorem
a0d60..
:
nth_6_tuple
u2
=
λ x1 x2 x3 x4 x5 x6 .
x3
(proof)
Theorem
89684..
:
nth_6_tuple
u3
=
λ x1 x2 x3 x4 x5 x6 .
x4
(proof)
Theorem
33924..
:
nth_6_tuple
u4
=
λ x1 x2 x3 x4 x5 x6 .
x5
(proof)
Theorem
fed6d..
:
nth_6_tuple
u5
=
λ x1 x2 x3 x4 x5 x6 .
x6
(proof)
Theorem
38ba0..
:
∀ x0 :
ι →
ι →
ι →
ι →
ι →
ι → ι
.
Church6_p
x0
⟶
Church6_to_u6
x0
∈
u6
(proof)
Theorem
3b8c0..
:
∀ x0 .
x0
∈
u6
⟶
Church6_p
(
nth_6_tuple
x0
)
(proof)
Theorem
985a3..
:
∀ x0 .
x0
∈
u6
⟶
Church6_to_u6
(
nth_6_tuple
x0
)
=
x0
(proof)
Theorem
60d0e..
:
∀ x0 .
x0
∈
u6
⟶
∀ x1 .
x1
∈
u6
⟶
nth_6_tuple
x0
=
nth_6_tuple
x1
⟶
x0
=
x1
(proof)
Theorem
3ac64..
:
∀ x0 :
ι →
ι →
ι →
ι →
ι →
ι → ι
.
Church6_p
x0
⟶
nth_6_tuple
(
Church6_to_u6
x0
)
=
x0
(proof)
Theorem
b4e23..
:
∀ x0 x1 :
ι →
ι →
ι →
ι →
ι →
ι → ι
.
Church6_p
x0
⟶
Church6_p
x1
⟶
Church6_to_u6
x0
=
Church6_to_u6
x1
⟶
x0
=
x1
(proof)
Definition
8915b..
:=
λ x0 :
(
(
ι →
ι →
ι →
ι →
ι →
ι → ι
)
→
(
ι →
ι →
ι →
ι →
ι →
ι → ι
)
→
ι →
ι →
ι →
ι →
ι →
ι → ι
)
→
ι →
ι →
ι →
ι →
ι →
ι → ι
.
lam
2
(
λ x1 .
If_i
(
x1
=
0
)
(
Church6_to_u6
(
x0
(
λ x2 x3 :
ι →
ι →
ι →
ι →
ι →
ι → ι
.
x2
)
)
)
(
Church6_to_u6
(
x0
(
λ x2 x3 :
ι →
ι →
ι →
ι →
ι →
ι → ι
.
x3
)
)
)
)
Definition
4aafd..
:=
λ x0 .
λ x1 :
(
ι →
ι →
ι →
ι →
ι →
ι → ι
)
→
(
ι →
ι →
ι →
ι →
ι →
ι → ι
)
→
ι →
ι →
ι →
ι →
ι →
ι → ι
.
x1
(
nth_6_tuple
(
ap
x0
0
)
)
(
nth_6_tuple
(
ap
x0
u1
)
)
Definition
884c6..
:=
λ x0 :
(
(
ι →
ι →
ι →
ι →
ι →
ι → ι
)
→
(
ι →
ι →
ι →
ι →
ι →
ι → ι
)
→
ι →
ι →
ι →
ι →
ι →
ι → ι
)
→
ι →
ι →
ι →
ι →
ι →
ι → ι
.
∀ x1 :
(
(
(
ι →
ι →
ι →
ι →
ι →
ι → ι
)
→
(
ι →
ι →
ι →
ι →
ι →
ι → ι
)
→
ι →
ι →
ι →
ι →
ι →
ι → ι
)
→
ι →
ι →
ι →
ι →
ι →
ι → ι
)
→ ο
.
(
∀ x2 x3 :
ι →
ι →
ι →
ι →
ι →
ι → ι
.
Church6_p
x2
⟶
Church6_p
x3
⟶
x1
(
λ x4 :
(
ι →
ι →
ι →
ι →
ι →
ι → ι
)
→
(
ι →
ι →
ι →
ι →
ι →
ι → ι
)
→
ι →
ι →
ι →
ι →
ι →
ι → ι
.
x4
x2
x3
)
)
⟶
x1
x0
Definition
setprod
setprod
:=
λ x0 x1 .
lam
x0
(
λ x2 .
x1
)
Known
tuple_2_setprod
tuple_2_setprod
:
∀ x0 x1 x2 .
x2
∈
x0
⟶
∀ x3 .
x3
∈
x1
⟶
lam
2
(
λ x4 .
If_i
(
x4
=
0
)
x2
x3
)
∈
setprod
x0
x1
Theorem
b4e0c..
:
∀ x0 :
(
(
ι →
ι →
ι →
ι →
ι →
ι → ι
)
→
(
ι →
ι →
ι →
ι →
ι →
ι → ι
)
→
ι →
ι →
ι →
ι →
ι →
ι → ι
)
→
ι →
ι →
ι →
ι →
ι →
ι → ι
.
884c6..
x0
⟶
8915b..
x0
∈
setprod
u6
u6
(proof)
Known
ap0_Sigma
ap0_Sigma
:
∀ x0 .
∀ x1 :
ι → ι
.
∀ x2 .
x2
∈
lam
x0
x1
⟶
ap
x2
0
∈
x0
Known
ap1_Sigma
ap1_Sigma
:
∀ x0 .
∀ x1 :
ι → ι
.
∀ x2 .
x2
∈
lam
x0
x1
⟶
ap
x2
1
∈
x1
(
ap
x2
0
)
Theorem
b410a..
:
∀ x0 .
x0
∈
setprod
u6
u6
⟶
884c6..
(
4aafd..
x0
)
(proof)
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
f4bbb..
:
∀ x0 .
x0
∈
setprod
u6
u6
⟶
8915b..
(
4aafd..
x0
)
=
x0
(proof)
Known
tuple_2_0_eq
tuple_2_0_eq
:
∀ x0 x1 .
ap
(
lam
2
(
λ x3 .
If_i
(
x3
=
0
)
x0
x1
)
)
0
=
x0
Known
tuple_2_1_eq
tuple_2_1_eq
:
∀ x0 x1 .
ap
(
lam
2
(
λ x3 .
If_i
(
x3
=
0
)
x0
x1
)
)
1
=
x1
Theorem
b98f5..
:
∀ x0 :
(
(
ι →
ι →
ι →
ι →
ι →
ι → ι
)
→
(
ι →
ι →
ι →
ι →
ι →
ι → ι
)
→
ι →
ι →
ι →
ι →
ι →
ι → ι
)
→
ι →
ι →
ι →
ι →
ι →
ι → ι
.
884c6..
x0
⟶
4aafd..
(
8915b..
x0
)
=
x0
(proof)
Theorem
0b928..
:
∀ x0 .
x0
∈
setprod
u6
u6
⟶
∀ x1 .
x1
∈
setprod
u6
u6
⟶
4aafd..
x0
=
4aafd..
x1
⟶
x0
=
x1
(proof)
Theorem
7a51b..
:
∀ x0 x1 :
(
(
ι →
ι →
ι →
ι →
ι →
ι → ι
)
→
(
ι →
ι →
ι →
ι →
ι →
ι → ι
)
→
ι →
ι →
ι →
ι →
ι →
ι → ι
)
→
ι →
ι →
ι →
ι →
ι →
ι → ι
.
884c6..
x0
⟶
884c6..
x1
⟶
8915b..
x0
=
8915b..
x1
⟶
x0
=
x1
(proof)