Search for blocks/addresses/...
Proofgold Asset
asset id
424760e9a2c7522ec4de8d4ce5d7e881ddf25c292083c4507e38c8bb212c3bba
asset hash
584b084424c0c9a5abce119d3e6450eed65c79c8748de5fdd380fa50f894af67
bday / block
4913
tx
15807..
preasset
doc published by
Pr6Pc..
Param
lam
Sigma
:
ι
→
(
ι
→
ι
) →
ι
Param
ordsucc
ordsucc
:
ι
→
ι
Param
If_i
If_i
:
ο
→
ι
→
ι
→
ι
Param
encode_r
encode_r
:
ι
→
(
ι
→
ι
→
ο
) →
ι
Param
Sep
Sep
:
ι
→
(
ι
→
ο
) →
ι
Definition
pack_u_r_p
:=
λ x0 .
λ x1 :
ι → ι
.
λ x2 :
ι →
ι → ο
.
λ x3 :
ι → ο
.
lam
4
(
λ x4 .
If_i
(
x4
=
0
)
x0
(
If_i
(
x4
=
1
)
(
lam
x0
x1
)
(
If_i
(
x4
=
2
)
(
encode_r
x0
x2
)
(
Sep
x0
x3
)
)
)
)
Param
ap
ap
:
ι
→
ι
→
ι
Known
tuple_4_0_eq
tuple_4_0_eq
:
∀ x0 x1 x2 x3 .
ap
(
lam
4
(
λ x5 .
If_i
(
x5
=
0
)
x0
(
If_i
(
x5
=
1
)
x1
(
If_i
(
x5
=
2
)
x2
x3
)
)
)
)
0
=
x0
Theorem
pack_u_r_p_0_eq
:
∀ x0 x1 .
∀ x2 :
ι → ι
.
∀ x3 :
ι →
ι → ο
.
∀ x4 :
ι → ο
.
x0
=
pack_u_r_p
x1
x2
x3
x4
⟶
x1
=
ap
x0
0
(proof)
Theorem
pack_u_r_p_0_eq2
:
∀ x0 .
∀ x1 :
ι → ι
.
∀ x2 :
ι →
ι → ο
.
∀ x3 :
ι → ο
.
x0
=
ap
(
pack_u_r_p
x0
x1
x2
x3
)
0
(proof)
Known
tuple_4_1_eq
tuple_4_1_eq
:
∀ x0 x1 x2 x3 .
ap
(
lam
4
(
λ x5 .
If_i
(
x5
=
0
)
x0
(
If_i
(
x5
=
1
)
x1
(
If_i
(
x5
=
2
)
x2
x3
)
)
)
)
1
=
x1
Known
beta
beta
:
∀ x0 .
∀ x1 :
ι → ι
.
∀ x2 .
x2
∈
x0
⟶
ap
(
lam
x0
x1
)
x2
=
x1
x2
Theorem
pack_u_r_p_1_eq
:
∀ x0 x1 .
∀ x2 :
ι → ι
.
∀ x3 :
ι →
ι → ο
.
∀ x4 :
ι → ο
.
x0
=
pack_u_r_p
x1
x2
x3
x4
⟶
∀ x5 .
x5
∈
x1
⟶
x2
x5
=
ap
(
ap
x0
1
)
x5
(proof)
Theorem
pack_u_r_p_1_eq2
:
∀ x0 .
∀ x1 :
ι → ι
.
∀ x2 :
ι →
ι → ο
.
∀ x3 :
ι → ο
.
∀ x4 .
x4
∈
x0
⟶
x1
x4
=
ap
(
ap
(
pack_u_r_p
x0
x1
x2
x3
)
1
)
x4
(proof)
Param
decode_r
decode_r
:
ι
→
ι
→
ι
→
ο
Known
tuple_4_2_eq
tuple_4_2_eq
:
∀ x0 x1 x2 x3 .
ap
(
lam
4
(
λ x5 .
If_i
(
x5
=
0
)
x0
(
If_i
(
x5
=
1
)
x1
(
If_i
(
x5
=
2
)
x2
x3
)
)
)
)
2
=
x2
Known
decode_encode_r
decode_encode_r
:
∀ x0 .
∀ x1 :
ι →
ι → ο
.
∀ x2 .
x2
∈
x0
⟶
∀ x3 .
x3
∈
x0
⟶
decode_r
(
encode_r
x0
x1
)
x2
x3
=
x1
x2
x3
Theorem
pack_u_r_p_2_eq
:
∀ x0 x1 .
∀ x2 :
ι → ι
.
∀ x3 :
ι →
ι → ο
.
∀ x4 :
ι → ο
.
x0
=
pack_u_r_p
x1
x2
x3
x4
⟶
∀ x5 .
x5
∈
x1
⟶
∀ x6 .
x6
∈
x1
⟶
x3
x5
x6
=
decode_r
(
ap
x0
2
)
x5
x6
(proof)
Theorem
pack_u_r_p_2_eq2
:
∀ x0 .
∀ x1 :
ι → ι
.
∀ x2 :
ι →
ι → ο
.
∀ x3 :
ι → ο
.
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
x2
x4
x5
=
decode_r
(
ap
(
pack_u_r_p
x0
x1
x2
x3
)
2
)
x4
x5
(proof)
Param
decode_p
decode_p
:
ι
→
ι
→
ο
Known
tuple_4_3_eq
tuple_4_3_eq
:
∀ x0 x1 x2 x3 .
ap
(
lam
4
(
λ x5 .
If_i
(
x5
=
0
)
x0
(
If_i
(
x5
=
1
)
x1
(
If_i
(
x5
=
2
)
x2
x3
)
)
)
)
3
=
x3
Known
decode_encode_p
decode_encode_p
:
∀ x0 .
∀ x1 :
ι → ο
.
∀ x2 .
x2
∈
x0
⟶
decode_p
(
Sep
x0
x1
)
x2
=
x1
x2
Theorem
pack_u_r_p_3_eq
:
∀ x0 x1 .
∀ x2 :
ι → ι
.
∀ x3 :
ι →
ι → ο
.
∀ x4 :
ι → ο
.
x0
=
pack_u_r_p
x1
x2
x3
x4
⟶
∀ x5 .
x5
∈
x1
⟶
x4
x5
=
decode_p
(
ap
x0
3
)
x5
(proof)
Theorem
pack_u_r_p_3_eq2
:
∀ x0 .
∀ x1 :
ι → ι
.
∀ x2 :
ι →
ι → ο
.
∀ x3 :
ι → ο
.
∀ x4 .
x4
∈
x0
⟶
x3
x4
=
decode_p
(
ap
(
pack_u_r_p
x0
x1
x2
x3
)
3
)
x4
(proof)
Definition
and
and
:=
λ x0 x1 : ο .
∀ x2 : ο .
(
x0
⟶
x1
⟶
x2
)
⟶
x2
Known
and4I
and4I
:
∀ x0 x1 x2 x3 : ο .
x0
⟶
x1
⟶
x2
⟶
x3
⟶
and
(
and
(
and
x0
x1
)
x2
)
x3
Theorem
pack_u_r_p_inj
:
∀ x0 x1 .
∀ x2 x3 :
ι → ι
.
∀ x4 x5 :
ι →
ι → ο
.
∀ x6 x7 :
ι → ο
.
pack_u_r_p
x0
x2
x4
x6
=
pack_u_r_p
x1
x3
x5
x7
⟶
and
(
and
(
and
(
x0
=
x1
)
(
∀ x8 .
x8
∈
x0
⟶
x2
x8
=
x3
x8
)
)
(
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
x4
x8
x9
=
x5
x8
x9
)
)
(
∀ x8 .
x8
∈
x0
⟶
x6
x8
=
x7
x8
)
(proof)
Param
iff
iff
:
ο
→
ο
→
ο
Known
encode_p_ext
encode_p_ext
:
∀ x0 .
∀ x1 x2 :
ι → ο
.
(
∀ x3 .
x3
∈
x0
⟶
iff
(
x1
x3
)
(
x2
x3
)
)
⟶
Sep
x0
x1
=
Sep
x0
x2
Known
encode_r_ext
encode_r_ext
:
∀ x0 .
∀ x1 x2 :
ι →
ι → ο
.
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
iff
(
x1
x3
x4
)
(
x2
x3
x4
)
)
⟶
encode_r
x0
x1
=
encode_r
x0
x2
Known
encode_u_ext
encode_u_ext
:
∀ x0 .
∀ x1 x2 :
ι → ι
.
(
∀ x3 .
x3
∈
x0
⟶
x1
x3
=
x2
x3
)
⟶
lam
x0
x1
=
lam
x0
x2
Theorem
pack_u_r_p_ext
:
∀ x0 .
∀ x1 x2 :
ι → ι
.
∀ x3 x4 :
ι →
ι → ο
.
∀ x5 x6 :
ι → ο
.
(
∀ x7 .
x7
∈
x0
⟶
x1
x7
=
x2
x7
)
⟶
(
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
iff
(
x3
x7
x8
)
(
x4
x7
x8
)
)
⟶
(
∀ x7 .
x7
∈
x0
⟶
iff
(
x5
x7
)
(
x6
x7
)
)
⟶
pack_u_r_p
x0
x1
x3
x5
=
pack_u_r_p
x0
x2
x4
x6
(proof)
Definition
struct_u_r_p
:=
λ x0 .
∀ x1 :
ι → ο
.
(
∀ x2 .
∀ x3 :
ι → ι
.
(
∀ x4 .
x4
∈
x2
⟶
x3
x4
∈
x2
)
⟶
∀ x4 :
ι →
ι → ο
.
∀ x5 :
ι → ο
.
x1
(
pack_u_r_p
x2
x3
x4
x5
)
)
⟶
x1
x0
Theorem
pack_struct_u_r_p_I
:
∀ x0 .
∀ x1 :
ι → ι
.
(
∀ x2 .
x2
∈
x0
⟶
x1
x2
∈
x0
)
⟶
∀ x2 :
ι →
ι → ο
.
∀ x3 :
ι → ο
.
struct_u_r_p
(
pack_u_r_p
x0
x1
x2
x3
)
(proof)
Theorem
pack_struct_u_r_p_E1
:
∀ x0 .
∀ x1 :
ι → ι
.
∀ x2 :
ι →
ι → ο
.
∀ x3 :
ι → ο
.
struct_u_r_p
(
pack_u_r_p
x0
x1
x2
x3
)
⟶
∀ x4 .
x4
∈
x0
⟶
x1
x4
∈
x0
(proof)
Known
iff_refl
iff_refl
:
∀ x0 : ο .
iff
x0
x0
Theorem
struct_u_r_p_eta
:
∀ x0 .
struct_u_r_p
x0
⟶
x0
=
pack_u_r_p
(
ap
x0
0
)
(
ap
(
ap
x0
1
)
)
(
decode_r
(
ap
x0
2
)
)
(
decode_p
(
ap
x0
3
)
)
(proof)
Definition
unpack_u_r_p_i
:=
λ x0 .
λ x1 :
ι →
(
ι → ι
)
→
(
ι →
ι → ο
)
→
(
ι → ο
)
→ ι
.
x1
(
ap
x0
0
)
(
ap
(
ap
x0
1
)
)
(
decode_r
(
ap
x0
2
)
)
(
decode_p
(
ap
x0
3
)
)
Theorem
unpack_u_r_p_i_eq
:
∀ x0 :
ι →
(
ι → ι
)
→
(
ι →
ι → ο
)
→
(
ι → ο
)
→ ι
.
∀ x1 .
∀ x2 :
ι → ι
.
∀ x3 :
ι →
ι → ο
.
∀ x4 :
ι → ο
.
(
∀ x5 :
ι → ι
.
(
∀ x6 .
x6
∈
x1
⟶
x2
x6
=
x5
x6
)
⟶
∀ x6 :
ι →
ι → ο
.
(
∀ x7 .
x7
∈
x1
⟶
∀ x8 .
x8
∈
x1
⟶
iff
(
x3
x7
x8
)
(
x6
x7
x8
)
)
⟶
∀ x7 :
ι → ο
.
(
∀ x8 .
x8
∈
x1
⟶
iff
(
x4
x8
)
(
x7
x8
)
)
⟶
x0
x1
x5
x6
x7
=
x0
x1
x2
x3
x4
)
⟶
unpack_u_r_p_i
(
pack_u_r_p
x1
x2
x3
x4
)
x0
=
x0
x1
x2
x3
x4
(proof)
Definition
unpack_u_r_p_o
:=
λ x0 .
λ x1 :
ι →
(
ι → ι
)
→
(
ι →
ι → ο
)
→
(
ι → ο
)
→ ο
.
x1
(
ap
x0
0
)
(
ap
(
ap
x0
1
)
)
(
decode_r
(
ap
x0
2
)
)
(
decode_p
(
ap
x0
3
)
)
Theorem
unpack_u_r_p_o_eq
:
∀ x0 :
ι →
(
ι → ι
)
→
(
ι →
ι → ο
)
→
(
ι → ο
)
→ ο
.
∀ x1 .
∀ x2 :
ι → ι
.
∀ x3 :
ι →
ι → ο
.
∀ x4 :
ι → ο
.
(
∀ x5 :
ι → ι
.
(
∀ x6 .
x6
∈
x1
⟶
x2
x6
=
x5
x6
)
⟶
∀ x6 :
ι →
ι → ο
.
(
∀ x7 .
x7
∈
x1
⟶
∀ x8 .
x8
∈
x1
⟶
iff
(
x3
x7
x8
)
(
x6
x7
x8
)
)
⟶
∀ x7 :
ι → ο
.
(
∀ x8 .
x8
∈
x1
⟶
iff
(
x4
x8
)
(
x7
x8
)
)
⟶
x0
x1
x5
x6
x7
=
x0
x1
x2
x3
x4
)
⟶
unpack_u_r_p_o
(
pack_u_r_p
x1
x2
x3
x4
)
x0
=
x0
x1
x2
x3
x4
(proof)
Definition
pack_u_r_e
:=
λ x0 .
λ x1 :
ι → ι
.
λ x2 :
ι →
ι → ο
.
λ x3 .
lam
4
(
λ x4 .
If_i
(
x4
=
0
)
x0
(
If_i
(
x4
=
1
)
(
lam
x0
x1
)
(
If_i
(
x4
=
2
)
(
encode_r
x0
x2
)
x3
)
)
)
Theorem
pack_u_r_e_0_eq
:
∀ x0 x1 .
∀ x2 :
ι → ι
.
∀ x3 :
ι →
ι → ο
.
∀ x4 .
x0
=
pack_u_r_e
x1
x2
x3
x4
⟶
x1
=
ap
x0
0
(proof)
Theorem
pack_u_r_e_0_eq2
:
∀ x0 .
∀ x1 :
ι → ι
.
∀ x2 :
ι →
ι → ο
.
∀ x3 .
x0
=
ap
(
pack_u_r_e
x0
x1
x2
x3
)
0
(proof)
Theorem
pack_u_r_e_1_eq
:
∀ x0 x1 .
∀ x2 :
ι → ι
.
∀ x3 :
ι →
ι → ο
.
∀ x4 .
x0
=
pack_u_r_e
x1
x2
x3
x4
⟶
∀ x5 .
x5
∈
x1
⟶
x2
x5
=
ap
(
ap
x0
1
)
x5
(proof)
Theorem
pack_u_r_e_1_eq2
:
∀ x0 .
∀ x1 :
ι → ι
.
∀ x2 :
ι →
ι → ο
.
∀ x3 x4 .
x4
∈
x0
⟶
x1
x4
=
ap
(
ap
(
pack_u_r_e
x0
x1
x2
x3
)
1
)
x4
(proof)
Theorem
pack_u_r_e_2_eq
:
∀ x0 x1 .
∀ x2 :
ι → ι
.
∀ x3 :
ι →
ι → ο
.
∀ x4 .
x0
=
pack_u_r_e
x1
x2
x3
x4
⟶
∀ x5 .
x5
∈
x1
⟶
∀ x6 .
x6
∈
x1
⟶
x3
x5
x6
=
decode_r
(
ap
x0
2
)
x5
x6
(proof)
Theorem
pack_u_r_e_2_eq2
:
∀ x0 .
∀ x1 :
ι → ι
.
∀ x2 :
ι →
ι → ο
.
∀ x3 x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
x2
x4
x5
=
decode_r
(
ap
(
pack_u_r_e
x0
x1
x2
x3
)
2
)
x4
x5
(proof)
Theorem
pack_u_r_e_3_eq
:
∀ x0 x1 .
∀ x2 :
ι → ι
.
∀ x3 :
ι →
ι → ο
.
∀ x4 .
x0
=
pack_u_r_e
x1
x2
x3
x4
⟶
x4
=
ap
x0
3
(proof)
Theorem
pack_u_r_e_3_eq2
:
∀ x0 .
∀ x1 :
ι → ι
.
∀ x2 :
ι →
ι → ο
.
∀ x3 .
x3
=
ap
(
pack_u_r_e
x0
x1
x2
x3
)
3
(proof)
Theorem
pack_u_r_e_inj
:
∀ x0 x1 .
∀ x2 x3 :
ι → ι
.
∀ x4 x5 :
ι →
ι → ο
.
∀ x6 x7 .
pack_u_r_e
x0
x2
x4
x6
=
pack_u_r_e
x1
x3
x5
x7
⟶
and
(
and
(
and
(
x0
=
x1
)
(
∀ x8 .
x8
∈
x0
⟶
x2
x8
=
x3
x8
)
)
(
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
x4
x8
x9
=
x5
x8
x9
)
)
(
x6
=
x7
)
(proof)
Theorem
pack_u_r_e_ext
:
∀ x0 .
∀ x1 x2 :
ι → ι
.
∀ x3 x4 :
ι →
ι → ο
.
∀ x5 .
(
∀ x6 .
x6
∈
x0
⟶
x1
x6
=
x2
x6
)
⟶
(
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
iff
(
x3
x6
x7
)
(
x4
x6
x7
)
)
⟶
pack_u_r_e
x0
x1
x3
x5
=
pack_u_r_e
x0
x2
x4
x5
(proof)
Definition
struct_u_r_e
:=
λ x0 .
∀ x1 :
ι → ο
.
(
∀ x2 .
∀ x3 :
ι → ι
.
(
∀ x4 .
x4
∈
x2
⟶
x3
x4
∈
x2
)
⟶
∀ x4 :
ι →
ι → ο
.
∀ x5 .
x5
∈
x2
⟶
x1
(
pack_u_r_e
x2
x3
x4
x5
)
)
⟶
x1
x0
Theorem
pack_struct_u_r_e_I
:
∀ x0 .
∀ x1 :
ι → ι
.
(
∀ x2 .
x2
∈
x0
⟶
x1
x2
∈
x0
)
⟶
∀ x2 :
ι →
ι → ο
.
∀ x3 .
x3
∈
x0
⟶
struct_u_r_e
(
pack_u_r_e
x0
x1
x2
x3
)
(proof)
Theorem
pack_struct_u_r_e_E1
:
∀ x0 .
∀ x1 :
ι → ι
.
∀ x2 :
ι →
ι → ο
.
∀ x3 .
struct_u_r_e
(
pack_u_r_e
x0
x1
x2
x3
)
⟶
∀ x4 .
x4
∈
x0
⟶
x1
x4
∈
x0
(proof)
Theorem
pack_struct_u_r_e_E3
:
∀ x0 .
∀ x1 :
ι → ι
.
∀ x2 :
ι →
ι → ο
.
∀ x3 .
struct_u_r_e
(
pack_u_r_e
x0
x1
x2
x3
)
⟶
x3
∈
x0
(proof)
Theorem
struct_u_r_e_eta
:
∀ x0 .
struct_u_r_e
x0
⟶
x0
=
pack_u_r_e
(
ap
x0
0
)
(
ap
(
ap
x0
1
)
)
(
decode_r
(
ap
x0
2
)
)
(
ap
x0
3
)
(proof)
Definition
unpack_u_r_e_i
:=
λ x0 .
λ x1 :
ι →
(
ι → ι
)
→
(
ι →
ι → ο
)
→
ι → ι
.
x1
(
ap
x0
0
)
(
ap
(
ap
x0
1
)
)
(
decode_r
(
ap
x0
2
)
)
(
ap
x0
3
)
Theorem
unpack_u_r_e_i_eq
:
∀ x0 :
ι →
(
ι → ι
)
→
(
ι →
ι → ο
)
→
ι → ι
.
∀ x1 .
∀ x2 :
ι → ι
.
∀ x3 :
ι →
ι → ο
.
∀ x4 .
(
∀ x5 :
ι → ι
.
(
∀ x6 .
x6
∈
x1
⟶
x2
x6
=
x5
x6
)
⟶
∀ x6 :
ι →
ι → ο
.
(
∀ x7 .
x7
∈
x1
⟶
∀ x8 .
x8
∈
x1
⟶
iff
(
x3
x7
x8
)
(
x6
x7
x8
)
)
⟶
x0
x1
x5
x6
x4
=
x0
x1
x2
x3
x4
)
⟶
unpack_u_r_e_i
(
pack_u_r_e
x1
x2
x3
x4
)
x0
=
x0
x1
x2
x3
x4
(proof)
Definition
unpack_u_r_e_o
:=
λ x0 .
λ x1 :
ι →
(
ι → ι
)
→
(
ι →
ι → ο
)
→
ι → ο
.
x1
(
ap
x0
0
)
(
ap
(
ap
x0
1
)
)
(
decode_r
(
ap
x0
2
)
)
(
ap
x0
3
)
Theorem
unpack_u_r_e_o_eq
:
∀ x0 :
ι →
(
ι → ι
)
→
(
ι →
ι → ο
)
→
ι → ο
.
∀ x1 .
∀ x2 :
ι → ι
.
∀ x3 :
ι →
ι → ο
.
∀ x4 .
(
∀ x5 :
ι → ι
.
(
∀ x6 .
x6
∈
x1
⟶
x2
x6
=
x5
x6
)
⟶
∀ x6 :
ι →
ι → ο
.
(
∀ x7 .
x7
∈
x1
⟶
∀ x8 .
x8
∈
x1
⟶
iff
(
x3
x7
x8
)
(
x6
x7
x8
)
)
⟶
x0
x1
x5
x6
x4
=
x0
x1
x2
x3
x4
)
⟶
unpack_u_r_e_o
(
pack_u_r_e
x1
x2
x3
x4
)
x0
=
x0
x1
x2
x3
x4
(proof)
Definition
pack_u_p_e
:=
λ x0 .
λ x1 :
ι → ι
.
λ x2 :
ι → ο
.
λ x3 .
lam
4
(
λ x4 .
If_i
(
x4
=
0
)
x0
(
If_i
(
x4
=
1
)
(
lam
x0
x1
)
(
If_i
(
x4
=
2
)
(
Sep
x0
x2
)
x3
)
)
)
Theorem
pack_u_p_e_0_eq
:
∀ x0 x1 .
∀ x2 :
ι → ι
.
∀ x3 :
ι → ο
.
∀ x4 .
x0
=
pack_u_p_e
x1
x2
x3
x4
⟶
x1
=
ap
x0
0
(proof)
Theorem
pack_u_p_e_0_eq2
:
∀ x0 .
∀ x1 :
ι → ι
.
∀ x2 :
ι → ο
.
∀ x3 .
x0
=
ap
(
pack_u_p_e
x0
x1
x2
x3
)
0
(proof)
Theorem
pack_u_p_e_1_eq
:
∀ x0 x1 .
∀ x2 :
ι → ι
.
∀ x3 :
ι → ο
.
∀ x4 .
x0
=
pack_u_p_e
x1
x2
x3
x4
⟶
∀ x5 .
x5
∈
x1
⟶
x2
x5
=
ap
(
ap
x0
1
)
x5
(proof)
Theorem
pack_u_p_e_1_eq2
:
∀ x0 .
∀ x1 :
ι → ι
.
∀ x2 :
ι → ο
.
∀ x3 x4 .
x4
∈
x0
⟶
x1
x4
=
ap
(
ap
(
pack_u_p_e
x0
x1
x2
x3
)
1
)
x4
(proof)
Theorem
pack_u_p_e_2_eq
:
∀ x0 x1 .
∀ x2 :
ι → ι
.
∀ x3 :
ι → ο
.
∀ x4 .
x0
=
pack_u_p_e
x1
x2
x3
x4
⟶
∀ x5 .
x5
∈
x1
⟶
x3
x5
=
decode_p
(
ap
x0
2
)
x5
(proof)
Theorem
pack_u_p_e_2_eq2
:
∀ x0 .
∀ x1 :
ι → ι
.
∀ x2 :
ι → ο
.
∀ x3 x4 .
x4
∈
x0
⟶
x2
x4
=
decode_p
(
ap
(
pack_u_p_e
x0
x1
x2
x3
)
2
)
x4
(proof)
Theorem
pack_u_p_e_3_eq
:
∀ x0 x1 .
∀ x2 :
ι → ι
.
∀ x3 :
ι → ο
.
∀ x4 .
x0
=
pack_u_p_e
x1
x2
x3
x4
⟶
x4
=
ap
x0
3
(proof)
Theorem
pack_u_p_e_3_eq2
:
∀ x0 .
∀ x1 :
ι → ι
.
∀ x2 :
ι → ο
.
∀ x3 .
x3
=
ap
(
pack_u_p_e
x0
x1
x2
x3
)
3
(proof)
Theorem
pack_u_p_e_inj
:
∀ x0 x1 .
∀ x2 x3 :
ι → ι
.
∀ x4 x5 :
ι → ο
.
∀ x6 x7 .
pack_u_p_e
x0
x2
x4
x6
=
pack_u_p_e
x1
x3
x5
x7
⟶
and
(
and
(
and
(
x0
=
x1
)
(
∀ x8 .
x8
∈
x0
⟶
x2
x8
=
x3
x8
)
)
(
∀ x8 .
x8
∈
x0
⟶
x4
x8
=
x5
x8
)
)
(
x6
=
x7
)
(proof)
Theorem
pack_u_p_e_ext
:
∀ x0 .
∀ x1 x2 :
ι → ι
.
∀ x3 x4 :
ι → ο
.
∀ x5 .
(
∀ x6 .
x6
∈
x0
⟶
x1
x6
=
x2
x6
)
⟶
(
∀ x6 .
x6
∈
x0
⟶
iff
(
x3
x6
)
(
x4
x6
)
)
⟶
pack_u_p_e
x0
x1
x3
x5
=
pack_u_p_e
x0
x2
x4
x5
(proof)
Definition
struct_u_p_e
:=
λ x0 .
∀ x1 :
ι → ο
.
(
∀ x2 .
∀ x3 :
ι → ι
.
(
∀ x4 .
x4
∈
x2
⟶
x3
x4
∈
x2
)
⟶
∀ x4 :
ι → ο
.
∀ x5 .
x5
∈
x2
⟶
x1
(
pack_u_p_e
x2
x3
x4
x5
)
)
⟶
x1
x0
Theorem
pack_struct_u_p_e_I
:
∀ x0 .
∀ x1 :
ι → ι
.
(
∀ x2 .
x2
∈
x0
⟶
x1
x2
∈
x0
)
⟶
∀ x2 :
ι → ο
.
∀ x3 .
x3
∈
x0
⟶
struct_u_p_e
(
pack_u_p_e
x0
x1
x2
x3
)
(proof)
Theorem
pack_struct_u_p_e_E1
:
∀ x0 .
∀ x1 :
ι → ι
.
∀ x2 :
ι → ο
.
∀ x3 .
struct_u_p_e
(
pack_u_p_e
x0
x1
x2
x3
)
⟶
∀ x4 .
x4
∈
x0
⟶
x1
x4
∈
x0
(proof)
Theorem
pack_struct_u_p_e_E3
:
∀ x0 .
∀ x1 :
ι → ι
.
∀ x2 :
ι → ο
.
∀ x3 .
struct_u_p_e
(
pack_u_p_e
x0
x1
x2
x3
)
⟶
x3
∈
x0
(proof)
Theorem
struct_u_p_e_eta
:
∀ x0 .
struct_u_p_e
x0
⟶
x0
=
pack_u_p_e
(
ap
x0
0
)
(
ap
(
ap
x0
1
)
)
(
decode_p
(
ap
x0
2
)
)
(
ap
x0
3
)
(proof)
Definition
unpack_u_p_e_i
:=
λ x0 .
λ x1 :
ι →
(
ι → ι
)
→
(
ι → ο
)
→
ι → ι
.
x1
(
ap
x0
0
)
(
ap
(
ap
x0
1
)
)
(
decode_p
(
ap
x0
2
)
)
(
ap
x0
3
)
Theorem
unpack_u_p_e_i_eq
:
∀ x0 :
ι →
(
ι → ι
)
→
(
ι → ο
)
→
ι → ι
.
∀ x1 .
∀ x2 :
ι → ι
.
∀ x3 :
ι → ο
.
∀ x4 .
(
∀ x5 :
ι → ι
.
(
∀ x6 .
x6
∈
x1
⟶
x2
x6
=
x5
x6
)
⟶
∀ x6 :
ι → ο
.
(
∀ x7 .
x7
∈
x1
⟶
iff
(
x3
x7
)
(
x6
x7
)
)
⟶
x0
x1
x5
x6
x4
=
x0
x1
x2
x3
x4
)
⟶
unpack_u_p_e_i
(
pack_u_p_e
x1
x2
x3
x4
)
x0
=
x0
x1
x2
x3
x4
(proof)
Definition
unpack_u_p_e_o
:=
λ x0 .
λ x1 :
ι →
(
ι → ι
)
→
(
ι → ο
)
→
ι → ο
.
x1
(
ap
x0
0
)
(
ap
(
ap
x0
1
)
)
(
decode_p
(
ap
x0
2
)
)
(
ap
x0
3
)
Theorem
unpack_u_p_e_o_eq
:
∀ x0 :
ι →
(
ι → ι
)
→
(
ι → ο
)
→
ι → ο
.
∀ x1 .
∀ x2 :
ι → ι
.
∀ x3 :
ι → ο
.
∀ x4 .
(
∀ x5 :
ι → ι
.
(
∀ x6 .
x6
∈
x1
⟶
x2
x6
=
x5
x6
)
⟶
∀ x6 :
ι → ο
.
(
∀ x7 .
x7
∈
x1
⟶
iff
(
x3
x7
)
(
x6
x7
)
)
⟶
x0
x1
x5
x6
x4
=
x0
x1
x2
x3
x4
)
⟶
unpack_u_p_e_o
(
pack_u_p_e
x1
x2
x3
x4
)
x0
=
x0
x1
x2
x3
x4
(proof)
Definition
pack_r_r_p
:=
λ x0 .
λ x1 x2 :
ι →
ι → ο
.
λ x3 :
ι → ο
.
lam
4
(
λ x4 .
If_i
(
x4
=
0
)
x0
(
If_i
(
x4
=
1
)
(
encode_r
x0
x1
)
(
If_i
(
x4
=
2
)
(
encode_r
x0
x2
)
(
Sep
x0
x3
)
)
)
)
Theorem
pack_r_r_p_0_eq
:
∀ x0 x1 .
∀ x2 x3 :
ι →
ι → ο
.
∀ x4 :
ι → ο
.
x0
=
pack_r_r_p
x1
x2
x3
x4
⟶
x1
=
ap
x0
0
(proof)
Theorem
pack_r_r_p_0_eq2
:
∀ x0 .
∀ x1 x2 :
ι →
ι → ο
.
∀ x3 :
ι → ο
.
x0
=
ap
(
pack_r_r_p
x0
x1
x2
x3
)
0
(proof)
Theorem
pack_r_r_p_1_eq
:
∀ x0 x1 .
∀ x2 x3 :
ι →
ι → ο
.
∀ x4 :
ι → ο
.
x0
=
pack_r_r_p
x1
x2
x3
x4
⟶
∀ x5 .
x5
∈
x1
⟶
∀ x6 .
x6
∈
x1
⟶
x2
x5
x6
=
decode_r
(
ap
x0
1
)
x5
x6
(proof)
Theorem
pack_r_r_p_1_eq2
:
∀ x0 .
∀ x1 x2 :
ι →
ι → ο
.
∀ x3 :
ι → ο
.
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
x1
x4
x5
=
decode_r
(
ap
(
pack_r_r_p
x0
x1
x2
x3
)
1
)
x4
x5
(proof)
Theorem
pack_r_r_p_2_eq
:
∀ x0 x1 .
∀ x2 x3 :
ι →
ι → ο
.
∀ x4 :
ι → ο
.
x0
=
pack_r_r_p
x1
x2
x3
x4
⟶
∀ x5 .
x5
∈
x1
⟶
∀ x6 .
x6
∈
x1
⟶
x3
x5
x6
=
decode_r
(
ap
x0
2
)
x5
x6
(proof)
Theorem
pack_r_r_p_2_eq2
:
∀ x0 .
∀ x1 x2 :
ι →
ι → ο
.
∀ x3 :
ι → ο
.
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
x2
x4
x5
=
decode_r
(
ap
(
pack_r_r_p
x0
x1
x2
x3
)
2
)
x4
x5
(proof)
Theorem
pack_r_r_p_3_eq
:
∀ x0 x1 .
∀ x2 x3 :
ι →
ι → ο
.
∀ x4 :
ι → ο
.
x0
=
pack_r_r_p
x1
x2
x3
x4
⟶
∀ x5 .
x5
∈
x1
⟶
x4
x5
=
decode_p
(
ap
x0
3
)
x5
(proof)
Theorem
pack_r_r_p_3_eq2
:
∀ x0 .
∀ x1 x2 :
ι →
ι → ο
.
∀ x3 :
ι → ο
.
∀ x4 .
x4
∈
x0
⟶
x3
x4
=
decode_p
(
ap
(
pack_r_r_p
x0
x1
x2
x3
)
3
)
x4
(proof)
Theorem
pack_r_r_p_inj
:
∀ x0 x1 .
∀ x2 x3 x4 x5 :
ι →
ι → ο
.
∀ x6 x7 :
ι → ο
.
pack_r_r_p
x0
x2
x4
x6
=
pack_r_r_p
x1
x3
x5
x7
⟶
and
(
and
(
and
(
x0
=
x1
)
(
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
x2
x8
x9
=
x3
x8
x9
)
)
(
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
x4
x8
x9
=
x5
x8
x9
)
)
(
∀ x8 .
x8
∈
x0
⟶
x6
x8
=
x7
x8
)
(proof)
Theorem
pack_r_r_p_ext
:
∀ x0 .
∀ x1 x2 x3 x4 :
ι →
ι → ο
.
∀ x5 x6 :
ι → ο
.
(
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
iff
(
x1
x7
x8
)
(
x2
x7
x8
)
)
⟶
(
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
iff
(
x3
x7
x8
)
(
x4
x7
x8
)
)
⟶
(
∀ x7 .
x7
∈
x0
⟶
iff
(
x5
x7
)
(
x6
x7
)
)
⟶
pack_r_r_p
x0
x1
x3
x5
=
pack_r_r_p
x0
x2
x4
x6
(proof)
Definition
struct_r_r_p
:=
λ x0 .
∀ x1 :
ι → ο
.
(
∀ x2 .
∀ x3 x4 :
ι →
ι → ο
.
∀ x5 :
ι → ο
.
x1
(
pack_r_r_p
x2
x3
x4
x5
)
)
⟶
x1
x0
Theorem
pack_struct_r_r_p_I
:
∀ x0 .
∀ x1 x2 :
ι →
ι → ο
.
∀ x3 :
ι → ο
.
struct_r_r_p
(
pack_r_r_p
x0
x1
x2
x3
)
(proof)
Theorem
struct_r_r_p_eta
:
∀ x0 .
struct_r_r_p
x0
⟶
x0
=
pack_r_r_p
(
ap
x0
0
)
(
decode_r
(
ap
x0
1
)
)
(
decode_r
(
ap
x0
2
)
)
(
decode_p
(
ap
x0
3
)
)
(proof)
Definition
unpack_r_r_p_i
:=
λ x0 .
λ x1 :
ι →
(
ι →
ι → ο
)
→
(
ι →
ι → ο
)
→
(
ι → ο
)
→ ι
.
x1
(
ap
x0
0
)
(
decode_r
(
ap
x0
1
)
)
(
decode_r
(
ap
x0
2
)
)
(
decode_p
(
ap
x0
3
)
)
Theorem
unpack_r_r_p_i_eq
:
∀ x0 :
ι →
(
ι →
ι → ο
)
→
(
ι →
ι → ο
)
→
(
ι → ο
)
→ ι
.
∀ x1 .
∀ x2 x3 :
ι →
ι → ο
.
∀ x4 :
ι → ο
.
(
∀ x5 :
ι →
ι → ο
.
(
∀ x6 .
x6
∈
x1
⟶
∀ x7 .
x7
∈
x1
⟶
iff
(
x2
x6
x7
)
(
x5
x6
x7
)
)
⟶
∀ x6 :
ι →
ι → ο
.
(
∀ x7 .
x7
∈
x1
⟶
∀ x8 .
x8
∈
x1
⟶
iff
(
x3
x7
x8
)
(
x6
x7
x8
)
)
⟶
∀ x7 :
ι → ο
.
(
∀ x8 .
x8
∈
x1
⟶
iff
(
x4
x8
)
(
x7
x8
)
)
⟶
x0
x1
x5
x6
x7
=
x0
x1
x2
x3
x4
)
⟶
unpack_r_r_p_i
(
pack_r_r_p
x1
x2
x3
x4
)
x0
=
x0
x1
x2
x3
x4
(proof)
Definition
unpack_r_r_p_o
:=
λ x0 .
λ x1 :
ι →
(
ι →
ι → ο
)
→
(
ι →
ι → ο
)
→
(
ι → ο
)
→ ο
.
x1
(
ap
x0
0
)
(
decode_r
(
ap
x0
1
)
)
(
decode_r
(
ap
x0
2
)
)
(
decode_p
(
ap
x0
3
)
)
Theorem
unpack_r_r_p_o_eq
:
∀ x0 :
ι →
(
ι →
ι → ο
)
→
(
ι →
ι → ο
)
→
(
ι → ο
)
→ ο
.
∀ x1 .
∀ x2 x3 :
ι →
ι → ο
.
∀ x4 :
ι → ο
.
(
∀ x5 :
ι →
ι → ο
.
(
∀ x6 .
x6
∈
x1
⟶
∀ x7 .
x7
∈
x1
⟶
iff
(
x2
x6
x7
)
(
x5
x6
x7
)
)
⟶
∀ x6 :
ι →
ι → ο
.
(
∀ x7 .
x7
∈
x1
⟶
∀ x8 .
x8
∈
x1
⟶
iff
(
x3
x7
x8
)
(
x6
x7
x8
)
)
⟶
∀ x7 :
ι → ο
.
(
∀ x8 .
x8
∈
x1
⟶
iff
(
x4
x8
)
(
x7
x8
)
)
⟶
x0
x1
x5
x6
x7
=
x0
x1
x2
x3
x4
)
⟶
unpack_r_r_p_o
(
pack_r_r_p
x1
x2
x3
x4
)
x0
=
x0
x1
x2
x3
x4
(proof)
Definition
pack_r_r_e
:=
λ x0 .
λ x1 x2 :
ι →
ι → ο
.
λ x3 .
lam
4
(
λ x4 .
If_i
(
x4
=
0
)
x0
(
If_i
(
x4
=
1
)
(
encode_r
x0
x1
)
(
If_i
(
x4
=
2
)
(
encode_r
x0
x2
)
x3
)
)
)
Theorem
pack_r_r_e_0_eq
:
∀ x0 x1 .
∀ x2 x3 :
ι →
ι → ο
.
∀ x4 .
x0
=
pack_r_r_e
x1
x2
x3
x4
⟶
x1
=
ap
x0
0
(proof)
Theorem
pack_r_r_e_0_eq2
:
∀ x0 .
∀ x1 x2 :
ι →
ι → ο
.
∀ x3 .
x0
=
ap
(
pack_r_r_e
x0
x1
x2
x3
)
0
(proof)
Theorem
pack_r_r_e_1_eq
:
∀ x0 x1 .
∀ x2 x3 :
ι →
ι → ο
.
∀ x4 .
x0
=
pack_r_r_e
x1
x2
x3
x4
⟶
∀ x5 .
x5
∈
x1
⟶
∀ x6 .
x6
∈
x1
⟶
x2
x5
x6
=
decode_r
(
ap
x0
1
)
x5
x6
(proof)
Theorem
pack_r_r_e_1_eq2
:
∀ x0 .
∀ x1 x2 :
ι →
ι → ο
.
∀ x3 x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
x1
x4
x5
=
decode_r
(
ap
(
pack_r_r_e
x0
x1
x2
x3
)
1
)
x4
x5
(proof)
Theorem
pack_r_r_e_2_eq
:
∀ x0 x1 .
∀ x2 x3 :
ι →
ι → ο
.
∀ x4 .
x0
=
pack_r_r_e
x1
x2
x3
x4
⟶
∀ x5 .
x5
∈
x1
⟶
∀ x6 .
x6
∈
x1
⟶
x3
x5
x6
=
decode_r
(
ap
x0
2
)
x5
x6
(proof)
Theorem
pack_r_r_e_2_eq2
:
∀ x0 .
∀ x1 x2 :
ι →
ι → ο
.
∀ x3 x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
x2
x4
x5
=
decode_r
(
ap
(
pack_r_r_e
x0
x1
x2
x3
)
2
)
x4
x5
(proof)
Theorem
pack_r_r_e_3_eq
:
∀ x0 x1 .
∀ x2 x3 :
ι →
ι → ο
.
∀ x4 .
x0
=
pack_r_r_e
x1
x2
x3
x4
⟶
x4
=
ap
x0
3
(proof)
Theorem
pack_r_r_e_3_eq2
:
∀ x0 .
∀ x1 x2 :
ι →
ι → ο
.
∀ x3 .
x3
=
ap
(
pack_r_r_e
x0
x1
x2
x3
)
3
(proof)
Theorem
pack_r_r_e_inj
:
∀ x0 x1 .
∀ x2 x3 x4 x5 :
ι →
ι → ο
.
∀ x6 x7 .
pack_r_r_e
x0
x2
x4
x6
=
pack_r_r_e
x1
x3
x5
x7
⟶
and
(
and
(
and
(
x0
=
x1
)
(
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
x2
x8
x9
=
x3
x8
x9
)
)
(
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
x4
x8
x9
=
x5
x8
x9
)
)
(
x6
=
x7
)
(proof)
Theorem
pack_r_r_e_ext
:
∀ x0 .
∀ x1 x2 x3 x4 :
ι →
ι → ο
.
∀ x5 .
(
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
iff
(
x1
x6
x7
)
(
x2
x6
x7
)
)
⟶
(
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
iff
(
x3
x6
x7
)
(
x4
x6
x7
)
)
⟶
pack_r_r_e
x0
x1
x3
x5
=
pack_r_r_e
x0
x2
x4
x5
(proof)
Definition
struct_r_r_e
:=
λ x0 .
∀ x1 :
ι → ο
.
(
∀ x2 .
∀ x3 x4 :
ι →
ι → ο
.
∀ x5 .
x5
∈
x2
⟶
x1
(
pack_r_r_e
x2
x3
x4
x5
)
)
⟶
x1
x0
Theorem
pack_struct_r_r_e_I
:
∀ x0 .
∀ x1 x2 :
ι →
ι → ο
.
∀ x3 .
x3
∈
x0
⟶
struct_r_r_e
(
pack_r_r_e
x0
x1
x2
x3
)
(proof)
Theorem
pack_struct_r_r_e_E3
:
∀ x0 .
∀ x1 x2 :
ι →
ι → ο
.
∀ x3 .
struct_r_r_e
(
pack_r_r_e
x0
x1
x2
x3
)
⟶
x3
∈
x0
(proof)
Theorem
struct_r_r_e_eta
:
∀ x0 .
struct_r_r_e
x0
⟶
x0
=
pack_r_r_e
(
ap
x0
0
)
(
decode_r
(
ap
x0
1
)
)
(
decode_r
(
ap
x0
2
)
)
(
ap
x0
3
)
(proof)
Definition
unpack_r_r_e_i
:=
λ x0 .
λ x1 :
ι →
(
ι →
ι → ο
)
→
(
ι →
ι → ο
)
→
ι → ι
.
x1
(
ap
x0
0
)
(
decode_r
(
ap
x0
1
)
)
(
decode_r
(
ap
x0
2
)
)
(
ap
x0
3
)
Theorem
unpack_r_r_e_i_eq
:
∀ x0 :
ι →
(
ι →
ι → ο
)
→
(
ι →
ι → ο
)
→
ι → ι
.
∀ x1 .
∀ x2 x3 :
ι →
ι → ο
.
∀ x4 .
(
∀ x5 :
ι →
ι → ο
.
(
∀ x6 .
x6
∈
x1
⟶
∀ x7 .
x7
∈
x1
⟶
iff
(
x2
x6
x7
)
(
x5
x6
x7
)
)
⟶
∀ x6 :
ι →
ι → ο
.
(
∀ x7 .
x7
∈
x1
⟶
∀ x8 .
x8
∈
x1
⟶
iff
(
x3
x7
x8
)
(
x6
x7
x8
)
)
⟶
x0
x1
x5
x6
x4
=
x0
x1
x2
x3
x4
)
⟶
unpack_r_r_e_i
(
pack_r_r_e
x1
x2
x3
x4
)
x0
=
x0
x1
x2
x3
x4
(proof)
Definition
unpack_r_r_e_o
:=
λ x0 .
λ x1 :
ι →
(
ι →
ι → ο
)
→
(
ι →
ι → ο
)
→
ι → ο
.
x1
(
ap
x0
0
)
(
decode_r
(
ap
x0
1
)
)
(
decode_r
(
ap
x0
2
)
)
(
ap
x0
3
)
Theorem
unpack_r_r_e_o_eq
:
∀ x0 :
ι →
(
ι →
ι → ο
)
→
(
ι →
ι → ο
)
→
ι → ο
.
∀ x1 .
∀ x2 x3 :
ι →
ι → ο
.
∀ x4 .
(
∀ x5 :
ι →
ι → ο
.
(
∀ x6 .
x6
∈
x1
⟶
∀ x7 .
x7
∈
x1
⟶
iff
(
x2
x6
x7
)
(
x5
x6
x7
)
)
⟶
∀ x6 :
ι →
ι → ο
.
(
∀ x7 .
x7
∈
x1
⟶
∀ x8 .
x8
∈
x1
⟶
iff
(
x3
x7
x8
)
(
x6
x7
x8
)
)
⟶
x0
x1
x5
x6
x4
=
x0
x1
x2
x3
x4
)
⟶
unpack_r_r_e_o
(
pack_r_r_e
x1
x2
x3
x4
)
x0
=
x0
x1
x2
x3
x4
(proof)