Search for blocks/addresses/...

Proofgold Asset

asset id
424760e9a2c7522ec4de8d4ce5d7e881ddf25c292083c4507e38c8bb212c3bba
asset hash
584b084424c0c9a5abce119d3e6450eed65c79c8748de5fdd380fa50f894af67
bday / block
4913
tx
15807..
preasset
doc published by Pr6Pc..
Param lamSigma : ι(ιι) → ι
Param ordsuccordsucc : ιι
Param If_iIf_i : οιιι
Param encode_rencode_r : ι(ιιο) → ι
Param SepSep : ι(ιο) → ι
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 apap : ιιι
Known tuple_4_0_eqtuple_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 x4x1 = 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_eqtuple_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 betabeta : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2x0ap (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 . x5x1x2 x5 = ap (ap x0 1) x5 (proof)
Theorem pack_u_r_p_1_eq2 : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ο . ∀ x3 : ι → ο . ∀ x4 . x4x0x1 x4 = ap (ap (pack_u_r_p x0 x1 x2 x3) 1) x4 (proof)
Param decode_rdecode_r : ιιιο
Known tuple_4_2_eqtuple_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_rdecode_encode_r : ∀ x0 . ∀ x1 : ι → ι → ο . ∀ x2 . x2x0∀ x3 . x3x0decode_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 . x5x1∀ x6 . x6x1x3 x5 x6 = decode_r (ap x0 2) x5 x6 (proof)
Theorem pack_u_r_p_2_eq2 : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ο . ∀ x3 : ι → ο . ∀ x4 . x4x0∀ x5 . x5x0x2 x4 x5 = decode_r (ap (pack_u_r_p x0 x1 x2 x3) 2) x4 x5 (proof)
Param decode_pdecode_p : ιιο
Known tuple_4_3_eqtuple_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_pdecode_encode_p : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . x2x0decode_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 . x5x1x4 x5 = decode_p (ap x0 3) x5 (proof)
Theorem pack_u_r_p_3_eq2 : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ο . ∀ x3 : ι → ο . ∀ x4 . x4x0x3 x4 = decode_p (ap (pack_u_r_p x0 x1 x2 x3) 3) x4 (proof)
Definition andand := λ x0 x1 : ο . ∀ x2 : ο . (x0x1x2)x2
Known and4Iand4I : ∀ x0 x1 x2 x3 : ο . x0x1x2x3and (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 x7and (and (and (x0 = x1) (∀ x8 . x8x0x2 x8 = x3 x8)) (∀ x8 . x8x0∀ x9 . x9x0x4 x8 x9 = x5 x8 x9)) (∀ x8 . x8x0x6 x8 = x7 x8) (proof)
Param iffiff : οοο
Known encode_p_extencode_p_ext : ∀ x0 . ∀ x1 x2 : ι → ο . (∀ x3 . x3x0iff (x1 x3) (x2 x3))Sep x0 x1 = Sep x0 x2
Known encode_r_extencode_r_ext : ∀ x0 . ∀ x1 x2 : ι → ι → ο . (∀ x3 . x3x0∀ x4 . x4x0iff (x1 x3 x4) (x2 x3 x4))encode_r x0 x1 = encode_r x0 x2
Known encode_u_extencode_u_ext : ∀ x0 . ∀ x1 x2 : ι → ι . (∀ x3 . x3x0x1 x3 = x2 x3)lam x0 x1 = lam x0 x2
Theorem pack_u_r_p_ext : ∀ x0 . ∀ x1 x2 : ι → ι . ∀ x3 x4 : ι → ι → ο . ∀ x5 x6 : ι → ο . (∀ x7 . x7x0x1 x7 = x2 x7)(∀ x7 . x7x0∀ x8 . x8x0iff (x3 x7 x8) (x4 x7 x8))(∀ x7 . x7x0iff (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 . x4x2x3 x4x2)∀ x4 : ι → ι → ο . ∀ x5 : ι → ο . x1 (pack_u_r_p x2 x3 x4 x5))x1 x0
Theorem pack_struct_u_r_p_I : ∀ x0 . ∀ x1 : ι → ι . (∀ x2 . x2x0x1 x2x0)∀ 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 . x4x0x1 x4x0 (proof)
Known iff_refliff_refl : ∀ x0 : ο . iff x0 x0
Theorem struct_u_r_p_eta : ∀ x0 . struct_u_r_p x0x0 = 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 . x6x1x2 x6 = x5 x6)∀ x6 : ι → ι → ο . (∀ x7 . x7x1∀ x8 . x8x1iff (x3 x7 x8) (x6 x7 x8))∀ x7 : ι → ο . (∀ x8 . x8x1iff (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 . x6x1x2 x6 = x5 x6)∀ x6 : ι → ι → ο . (∀ x7 . x7x1∀ x8 . x8x1iff (x3 x7 x8) (x6 x7 x8))∀ x7 : ι → ο . (∀ x8 . x8x1iff (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 x4x1 = 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 . x5x1x2 x5 = ap (ap x0 1) x5 (proof)
Theorem pack_u_r_e_1_eq2 : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ο . ∀ x3 x4 . x4x0x1 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 . x5x1∀ x6 . x6x1x3 x5 x6 = decode_r (ap x0 2) x5 x6 (proof)
Theorem pack_u_r_e_2_eq2 : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ο . ∀ x3 x4 . x4x0∀ x5 . x5x0x2 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 x4x4 = 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 x7and (and (and (x0 = x1) (∀ x8 . x8x0x2 x8 = x3 x8)) (∀ x8 . x8x0∀ x9 . x9x0x4 x8 x9 = x5 x8 x9)) (x6 = x7) (proof)
Theorem pack_u_r_e_ext : ∀ x0 . ∀ x1 x2 : ι → ι . ∀ x3 x4 : ι → ι → ο . ∀ x5 . (∀ x6 . x6x0x1 x6 = x2 x6)(∀ x6 . x6x0∀ x7 . x7x0iff (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 . x4x2x3 x4x2)∀ x4 : ι → ι → ο . ∀ x5 . x5x2x1 (pack_u_r_e x2 x3 x4 x5))x1 x0
Theorem pack_struct_u_r_e_I : ∀ x0 . ∀ x1 : ι → ι . (∀ x2 . x2x0x1 x2x0)∀ x2 : ι → ι → ο . ∀ x3 . x3x0struct_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 . x4x0x1 x4x0 (proof)
Theorem pack_struct_u_r_e_E3 : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ο . ∀ x3 . struct_u_r_e (pack_u_r_e x0 x1 x2 x3)x3x0 (proof)
Theorem struct_u_r_e_eta : ∀ x0 . struct_u_r_e x0x0 = 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 . x6x1x2 x6 = x5 x6)∀ x6 : ι → ι → ο . (∀ x7 . x7x1∀ x8 . x8x1iff (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 . x6x1x2 x6 = x5 x6)∀ x6 : ι → ι → ο . (∀ x7 . x7x1∀ x8 . x8x1iff (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 x4x1 = 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 . x5x1x2 x5 = ap (ap x0 1) x5 (proof)
Theorem pack_u_p_e_1_eq2 : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ο . ∀ x3 x4 . x4x0x1 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 . x5x1x3 x5 = decode_p (ap x0 2) x5 (proof)
Theorem pack_u_p_e_2_eq2 : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ο . ∀ x3 x4 . x4x0x2 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 x4x4 = 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 x7and (and (and (x0 = x1) (∀ x8 . x8x0x2 x8 = x3 x8)) (∀ x8 . x8x0x4 x8 = x5 x8)) (x6 = x7) (proof)
Theorem pack_u_p_e_ext : ∀ x0 . ∀ x1 x2 : ι → ι . ∀ x3 x4 : ι → ο . ∀ x5 . (∀ x6 . x6x0x1 x6 = x2 x6)(∀ x6 . x6x0iff (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 . x4x2x3 x4x2)∀ x4 : ι → ο . ∀ x5 . x5x2x1 (pack_u_p_e x2 x3 x4 x5))x1 x0
Theorem pack_struct_u_p_e_I : ∀ x0 . ∀ x1 : ι → ι . (∀ x2 . x2x0x1 x2x0)∀ x2 : ι → ο . ∀ x3 . x3x0struct_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 . x4x0x1 x4x0 (proof)
Theorem pack_struct_u_p_e_E3 : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ο . ∀ x3 . struct_u_p_e (pack_u_p_e x0 x1 x2 x3)x3x0 (proof)
Theorem struct_u_p_e_eta : ∀ x0 . struct_u_p_e x0x0 = 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 . x6x1x2 x6 = x5 x6)∀ x6 : ι → ο . (∀ x7 . x7x1iff (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 . x6x1x2 x6 = x5 x6)∀ x6 : ι → ο . (∀ x7 . x7x1iff (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 x4x1 = 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 . x5x1∀ x6 . x6x1x2 x5 x6 = decode_r (ap x0 1) x5 x6 (proof)
Theorem pack_r_r_p_1_eq2 : ∀ x0 . ∀ x1 x2 : ι → ι → ο . ∀ x3 : ι → ο . ∀ x4 . x4x0∀ x5 . x5x0x1 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 . x5x1∀ x6 . x6x1x3 x5 x6 = decode_r (ap x0 2) x5 x6 (proof)
Theorem pack_r_r_p_2_eq2 : ∀ x0 . ∀ x1 x2 : ι → ι → ο . ∀ x3 : ι → ο . ∀ x4 . x4x0∀ x5 . x5x0x2 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 . x5x1x4 x5 = decode_p (ap x0 3) x5 (proof)
Theorem pack_r_r_p_3_eq2 : ∀ x0 . ∀ x1 x2 : ι → ι → ο . ∀ x3 : ι → ο . ∀ x4 . x4x0x3 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 x7and (and (and (x0 = x1) (∀ x8 . x8x0∀ x9 . x9x0x2 x8 x9 = x3 x8 x9)) (∀ x8 . x8x0∀ x9 . x9x0x4 x8 x9 = x5 x8 x9)) (∀ x8 . x8x0x6 x8 = x7 x8) (proof)
Theorem pack_r_r_p_ext : ∀ x0 . ∀ x1 x2 x3 x4 : ι → ι → ο . ∀ x5 x6 : ι → ο . (∀ x7 . x7x0∀ x8 . x8x0iff (x1 x7 x8) (x2 x7 x8))(∀ x7 . x7x0∀ x8 . x8x0iff (x3 x7 x8) (x4 x7 x8))(∀ x7 . x7x0iff (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 x0x0 = 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 . x6x1∀ x7 . x7x1iff (x2 x6 x7) (x5 x6 x7))∀ x6 : ι → ι → ο . (∀ x7 . x7x1∀ x8 . x8x1iff (x3 x7 x8) (x6 x7 x8))∀ x7 : ι → ο . (∀ x8 . x8x1iff (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 . x6x1∀ x7 . x7x1iff (x2 x6 x7) (x5 x6 x7))∀ x6 : ι → ι → ο . (∀ x7 . x7x1∀ x8 . x8x1iff (x3 x7 x8) (x6 x7 x8))∀ x7 : ι → ο . (∀ x8 . x8x1iff (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 x4x1 = 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 . x5x1∀ x6 . x6x1x2 x5 x6 = decode_r (ap x0 1) x5 x6 (proof)
Theorem pack_r_r_e_1_eq2 : ∀ x0 . ∀ x1 x2 : ι → ι → ο . ∀ x3 x4 . x4x0∀ x5 . x5x0x1 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 . x5x1∀ x6 . x6x1x3 x5 x6 = decode_r (ap x0 2) x5 x6 (proof)
Theorem pack_r_r_e_2_eq2 : ∀ x0 . ∀ x1 x2 : ι → ι → ο . ∀ x3 x4 . x4x0∀ x5 . x5x0x2 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 x4x4 = 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 x7and (and (and (x0 = x1) (∀ x8 . x8x0∀ x9 . x9x0x2 x8 x9 = x3 x8 x9)) (∀ x8 . x8x0∀ x9 . x9x0x4 x8 x9 = x5 x8 x9)) (x6 = x7) (proof)
Theorem pack_r_r_e_ext : ∀ x0 . ∀ x1 x2 x3 x4 : ι → ι → ο . ∀ x5 . (∀ x6 . x6x0∀ x7 . x7x0iff (x1 x6 x7) (x2 x6 x7))(∀ x6 . x6x0∀ x7 . x7x0iff (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 . x5x2x1 (pack_r_r_e x2 x3 x4 x5))x1 x0
Theorem pack_struct_r_r_e_I : ∀ x0 . ∀ x1 x2 : ι → ι → ο . ∀ x3 . x3x0struct_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)x3x0 (proof)
Theorem struct_r_r_e_eta : ∀ x0 . struct_r_r_e x0x0 = 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 . x6x1∀ x7 . x7x1iff (x2 x6 x7) (x5 x6 x7))∀ x6 : ι → ι → ο . (∀ x7 . x7x1∀ x8 . x8x1iff (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 . x6x1∀ x7 . x7x1iff (x2 x6 x7) (x5 x6 x7))∀ x6 : ι → ι → ο . (∀ x7 . x7x1∀ x8 . x8x1iff (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)