Search for blocks/addresses/...

Proofgold Asset

asset id
467b3356e5581cf9f89fca759c6e655a373282ef7cdad8d260bee6e024773a0e
asset hash
c465f3cbd5c38e9a8d86e2037df4dc238e8f14f571c5ba70940055e9a4050d49
bday / block
4915
tx
2a3aa..
preasset
doc published by Pr6Pc..
Param lamSigma : ι(ιι) → ι
Param ordsuccordsucc : ιι
Param If_iIf_i : οιιι
Param encode_bencode_b : ιCT2 ι
Param encode_rencode_r : ι(ιιο) → ι
Param SepSep : ι(ιο) → ι
Definition pack_b_u_r_p := λ x0 . λ x1 : ι → ι → ι . λ x2 : ι → ι . λ x3 : ι → ι → ο . λ x4 : ι → ο . lam 5 (λ x5 . If_i (x5 = 0) x0 (If_i (x5 = 1) (encode_b x0 x1) (If_i (x5 = 2) (lam x0 x2) (If_i (x5 = 3) (encode_r x0 x3) (Sep x0 x4)))))
Param apap : ιιι
Known tuple_5_0_eqtuple_5_0_eq : ∀ x0 x1 x2 x3 x4 . ap (lam 5 (λ x6 . If_i (x6 = 0) x0 (If_i (x6 = 1) x1 (If_i (x6 = 2) x2 (If_i (x6 = 3) x3 x4))))) 0 = x0
Theorem pack_b_u_r_p_0_eq : ∀ x0 x1 . ∀ x2 : ι → ι → ι . ∀ x3 : ι → ι . ∀ x4 : ι → ι → ο . ∀ x5 : ι → ο . x0 = pack_b_u_r_p x1 x2 x3 x4 x5x1 = ap x0 0 (proof)
Theorem pack_b_u_r_p_0_eq2 : ∀ x0 . ∀ x1 : ι → ι → ι . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ο . ∀ x4 : ι → ο . x0 = ap (pack_b_u_r_p x0 x1 x2 x3 x4) 0 (proof)
Param decode_bdecode_b : ιιιι
Known tuple_5_1_eqtuple_5_1_eq : ∀ x0 x1 x2 x3 x4 . ap (lam 5 (λ x6 . If_i (x6 = 0) x0 (If_i (x6 = 1) x1 (If_i (x6 = 2) x2 (If_i (x6 = 3) x3 x4))))) 1 = x1
Known decode_encode_bdecode_encode_b : ∀ x0 . ∀ x1 : ι → ι → ι . ∀ x2 . x2x0∀ x3 . x3x0decode_b (encode_b x0 x1) x2 x3 = x1 x2 x3
Theorem pack_b_u_r_p_1_eq : ∀ x0 x1 . ∀ x2 : ι → ι → ι . ∀ x3 : ι → ι . ∀ x4 : ι → ι → ο . ∀ x5 : ι → ο . x0 = pack_b_u_r_p x1 x2 x3 x4 x5∀ x6 . x6x1∀ x7 . x7x1x2 x6 x7 = decode_b (ap x0 1) x6 x7 (proof)
Theorem pack_b_u_r_p_1_eq2 : ∀ x0 . ∀ x1 : ι → ι → ι . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ο . ∀ x4 : ι → ο . ∀ x5 . x5x0∀ x6 . x6x0x1 x5 x6 = decode_b (ap (pack_b_u_r_p x0 x1 x2 x3 x4) 1) x5 x6 (proof)
Known tuple_5_2_eqtuple_5_2_eq : ∀ x0 x1 x2 x3 x4 . ap (lam 5 (λ x6 . If_i (x6 = 0) x0 (If_i (x6 = 1) x1 (If_i (x6 = 2) x2 (If_i (x6 = 3) x3 x4))))) 2 = x2
Known betabeta : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2x0ap (lam x0 x1) x2 = x1 x2
Theorem pack_b_u_r_p_2_eq : ∀ x0 x1 . ∀ x2 : ι → ι → ι . ∀ x3 : ι → ι . ∀ x4 : ι → ι → ο . ∀ x5 : ι → ο . x0 = pack_b_u_r_p x1 x2 x3 x4 x5∀ x6 . x6x1x3 x6 = ap (ap x0 2) x6 (proof)
Theorem pack_b_u_r_p_2_eq2 : ∀ x0 . ∀ x1 : ι → ι → ι . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ο . ∀ x4 : ι → ο . ∀ x5 . x5x0x2 x5 = ap (ap (pack_b_u_r_p x0 x1 x2 x3 x4) 2) x5 (proof)
Param decode_rdecode_r : ιιιο
Known tuple_5_3_eqtuple_5_3_eq : ∀ x0 x1 x2 x3 x4 . ap (lam 5 (λ x6 . If_i (x6 = 0) x0 (If_i (x6 = 1) x1 (If_i (x6 = 2) x2 (If_i (x6 = 3) x3 x4))))) 3 = x3
Known decode_encode_rdecode_encode_r : ∀ x0 . ∀ x1 : ι → ι → ο . ∀ x2 . x2x0∀ x3 . x3x0decode_r (encode_r x0 x1) x2 x3 = x1 x2 x3
Theorem pack_b_u_r_p_3_eq : ∀ x0 x1 . ∀ x2 : ι → ι → ι . ∀ x3 : ι → ι . ∀ x4 : ι → ι → ο . ∀ x5 : ι → ο . x0 = pack_b_u_r_p x1 x2 x3 x4 x5∀ x6 . x6x1∀ x7 . x7x1x4 x6 x7 = decode_r (ap x0 3) x6 x7 (proof)
Theorem pack_b_u_r_p_3_eq2 : ∀ x0 . ∀ x1 : ι → ι → ι . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ο . ∀ x4 : ι → ο . ∀ x5 . x5x0∀ x6 . x6x0x3 x5 x6 = decode_r (ap (pack_b_u_r_p x0 x1 x2 x3 x4) 3) x5 x6 (proof)
Param decode_pdecode_p : ιιο
Known tuple_5_4_eqtuple_5_4_eq : ∀ x0 x1 x2 x3 x4 . ap (lam 5 (λ x6 . If_i (x6 = 0) x0 (If_i (x6 = 1) x1 (If_i (x6 = 2) x2 (If_i (x6 = 3) x3 x4))))) 4 = x4
Known decode_encode_pdecode_encode_p : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . x2x0decode_p (Sep x0 x1) x2 = x1 x2
Theorem pack_b_u_r_p_4_eq : ∀ x0 x1 . ∀ x2 : ι → ι → ι . ∀ x3 : ι → ι . ∀ x4 : ι → ι → ο . ∀ x5 : ι → ο . x0 = pack_b_u_r_p x1 x2 x3 x4 x5∀ x6 . x6x1x5 x6 = decode_p (ap x0 4) x6 (proof)
Theorem pack_b_u_r_p_4_eq2 : ∀ x0 . ∀ x1 : ι → ι → ι . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ο . ∀ x4 : ι → ο . ∀ x5 . x5x0x4 x5 = decode_p (ap (pack_b_u_r_p x0 x1 x2 x3 x4) 4) x5 (proof)
Definition andand := λ x0 x1 : ο . ∀ x2 : ο . (x0x1x2)x2
Known and5Iand5I : ∀ x0 x1 x2 x3 x4 : ο . x0x1x2x3x4and (and (and (and x0 x1) x2) x3) x4
Theorem pack_b_u_r_p_inj : ∀ x0 x1 . ∀ x2 x3 : ι → ι → ι . ∀ x4 x5 : ι → ι . ∀ x6 x7 : ι → ι → ο . ∀ x8 x9 : ι → ο . pack_b_u_r_p x0 x2 x4 x6 x8 = pack_b_u_r_p x1 x3 x5 x7 x9and (and (and (and (x0 = x1) (∀ x10 . x10x0∀ x11 . x11x0x2 x10 x11 = x3 x10 x11)) (∀ x10 . x10x0x4 x10 = x5 x10)) (∀ x10 . x10x0∀ x11 . x11x0x6 x10 x11 = x7 x10 x11)) (∀ x10 . x10x0x8 x10 = x9 x10) (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
Known encode_b_extencode_b_ext : ∀ x0 . ∀ x1 x2 : ι → ι → ι . (∀ x3 . x3x0∀ x4 . x4x0x1 x3 x4 = x2 x3 x4)encode_b x0 x1 = encode_b x0 x2
Theorem pack_b_u_r_p_ext : ∀ x0 . ∀ x1 x2 : ι → ι → ι . ∀ x3 x4 : ι → ι . ∀ x5 x6 : ι → ι → ο . ∀ x7 x8 : ι → ο . (∀ x9 . x9x0∀ x10 . x10x0x1 x9 x10 = x2 x9 x10)(∀ x9 . x9x0x3 x9 = x4 x9)(∀ x9 . x9x0∀ x10 . x10x0iff (x5 x9 x10) (x6 x9 x10))(∀ x9 . x9x0iff (x7 x9) (x8 x9))pack_b_u_r_p x0 x1 x3 x5 x7 = pack_b_u_r_p x0 x2 x4 x6 x8 (proof)
Definition struct_b_u_r_p := λ x0 . ∀ x1 : ι → ο . (∀ x2 . ∀ x3 : ι → ι → ι . (∀ x4 . x4x2∀ x5 . x5x2x3 x4 x5x2)∀ x4 : ι → ι . (∀ x5 . x5x2x4 x5x2)∀ x5 : ι → ι → ο . ∀ x6 : ι → ο . x1 (pack_b_u_r_p x2 x3 x4 x5 x6))x1 x0
Theorem pack_struct_b_u_r_p_I : ∀ x0 . ∀ x1 : ι → ι → ι . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x0)∀ x2 : ι → ι . (∀ x3 . x3x0x2 x3x0)∀ x3 : ι → ι → ο . ∀ x4 : ι → ο . struct_b_u_r_p (pack_b_u_r_p x0 x1 x2 x3 x4) (proof)
Theorem pack_struct_b_u_r_p_E1 : ∀ x0 . ∀ x1 : ι → ι → ι . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ο . ∀ x4 : ι → ο . struct_b_u_r_p (pack_b_u_r_p x0 x1 x2 x3 x4)∀ x5 . x5x0∀ x6 . x6x0x1 x5 x6x0 (proof)
Theorem pack_struct_b_u_r_p_E2 : ∀ x0 . ∀ x1 : ι → ι → ι . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ο . ∀ x4 : ι → ο . struct_b_u_r_p (pack_b_u_r_p x0 x1 x2 x3 x4)∀ x5 . x5x0x2 x5x0 (proof)
Known iff_refliff_refl : ∀ x0 : ο . iff x0 x0
Theorem struct_b_u_r_p_eta : ∀ x0 . struct_b_u_r_p x0x0 = pack_b_u_r_p (ap x0 0) (decode_b (ap x0 1)) (ap (ap x0 2)) (decode_r (ap x0 3)) (decode_p (ap x0 4)) (proof)
Definition unpack_b_u_r_p_i := λ x0 . λ x1 : ι → (ι → ι → ι)(ι → ι)(ι → ι → ο)(ι → ο) → ι . x1 (ap x0 0) (decode_b (ap x0 1)) (ap (ap x0 2)) (decode_r (ap x0 3)) (decode_p (ap x0 4))
Theorem unpack_b_u_r_p_i_eq : ∀ x0 : ι → (ι → ι → ι)(ι → ι)(ι → ι → ο)(ι → ο) → ι . ∀ x1 . ∀ x2 : ι → ι → ι . ∀ x3 : ι → ι . ∀ x4 : ι → ι → ο . ∀ x5 : ι → ο . (∀ x6 : ι → ι → ι . (∀ x7 . x7x1∀ x8 . x8x1x2 x7 x8 = x6 x7 x8)∀ x7 : ι → ι . (∀ x8 . x8x1x3 x8 = x7 x8)∀ x8 : ι → ι → ο . (∀ x9 . x9x1∀ x10 . x10x1iff (x4 x9 x10) (x8 x9 x10))∀ x9 : ι → ο . (∀ x10 . x10x1iff (x5 x10) (x9 x10))x0 x1 x6 x7 x8 x9 = x0 x1 x2 x3 x4 x5)unpack_b_u_r_p_i (pack_b_u_r_p x1 x2 x3 x4 x5) x0 = x0 x1 x2 x3 x4 x5 (proof)
Definition unpack_b_u_r_p_o := λ x0 . λ x1 : ι → (ι → ι → ι)(ι → ι)(ι → ι → ο)(ι → ο) → ο . x1 (ap x0 0) (decode_b (ap x0 1)) (ap (ap x0 2)) (decode_r (ap x0 3)) (decode_p (ap x0 4))
Theorem unpack_b_u_r_p_o_eq : ∀ x0 : ι → (ι → ι → ι)(ι → ι)(ι → ι → ο)(ι → ο) → ο . ∀ x1 . ∀ x2 : ι → ι → ι . ∀ x3 : ι → ι . ∀ x4 : ι → ι → ο . ∀ x5 : ι → ο . (∀ x6 : ι → ι → ι . (∀ x7 . x7x1∀ x8 . x8x1x2 x7 x8 = x6 x7 x8)∀ x7 : ι → ι . (∀ x8 . x8x1x3 x8 = x7 x8)∀ x8 : ι → ι → ο . (∀ x9 . x9x1∀ x10 . x10x1iff (x4 x9 x10) (x8 x9 x10))∀ x9 : ι → ο . (∀ x10 . x10x1iff (x5 x10) (x9 x10))x0 x1 x6 x7 x8 x9 = x0 x1 x2 x3 x4 x5)unpack_b_u_r_p_o (pack_b_u_r_p x1 x2 x3 x4 x5) x0 = x0 x1 x2 x3 x4 x5 (proof)
Definition pack_b_u_r_e := λ x0 . λ x1 : ι → ι → ι . λ x2 : ι → ι . λ x3 : ι → ι → ο . λ x4 . lam 5 (λ x5 . If_i (x5 = 0) x0 (If_i (x5 = 1) (encode_b x0 x1) (If_i (x5 = 2) (lam x0 x2) (If_i (x5 = 3) (encode_r x0 x3) x4))))
Theorem pack_b_u_r_e_0_eq : ∀ x0 x1 . ∀ x2 : ι → ι → ι . ∀ x3 : ι → ι . ∀ x4 : ι → ι → ο . ∀ x5 . x0 = pack_b_u_r_e x1 x2 x3 x4 x5x1 = ap x0 0 (proof)
Theorem pack_b_u_r_e_0_eq2 : ∀ x0 . ∀ x1 : ι → ι → ι . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ο . ∀ x4 . x0 = ap (pack_b_u_r_e x0 x1 x2 x3 x4) 0 (proof)
Theorem pack_b_u_r_e_1_eq : ∀ x0 x1 . ∀ x2 : ι → ι → ι . ∀ x3 : ι → ι . ∀ x4 : ι → ι → ο . ∀ x5 . x0 = pack_b_u_r_e x1 x2 x3 x4 x5∀ x6 . x6x1∀ x7 . x7x1x2 x6 x7 = decode_b (ap x0 1) x6 x7 (proof)
Theorem pack_b_u_r_e_1_eq2 : ∀ x0 . ∀ x1 : ι → ι → ι . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ο . ∀ x4 x5 . x5x0∀ x6 . x6x0x1 x5 x6 = decode_b (ap (pack_b_u_r_e x0 x1 x2 x3 x4) 1) x5 x6 (proof)
Theorem pack_b_u_r_e_2_eq : ∀ x0 x1 . ∀ x2 : ι → ι → ι . ∀ x3 : ι → ι . ∀ x4 : ι → ι → ο . ∀ x5 . x0 = pack_b_u_r_e x1 x2 x3 x4 x5∀ x6 . x6x1x3 x6 = ap (ap x0 2) x6 (proof)
Theorem pack_b_u_r_e_2_eq2 : ∀ x0 . ∀ x1 : ι → ι → ι . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ο . ∀ x4 x5 . x5x0x2 x5 = ap (ap (pack_b_u_r_e x0 x1 x2 x3 x4) 2) x5 (proof)
Theorem pack_b_u_r_e_3_eq : ∀ x0 x1 . ∀ x2 : ι → ι → ι . ∀ x3 : ι → ι . ∀ x4 : ι → ι → ο . ∀ x5 . x0 = pack_b_u_r_e x1 x2 x3 x4 x5∀ x6 . x6x1∀ x7 . x7x1x4 x6 x7 = decode_r (ap x0 3) x6 x7 (proof)
Theorem pack_b_u_r_e_3_eq2 : ∀ x0 . ∀ x1 : ι → ι → ι . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ο . ∀ x4 x5 . x5x0∀ x6 . x6x0x3 x5 x6 = decode_r (ap (pack_b_u_r_e x0 x1 x2 x3 x4) 3) x5 x6 (proof)
Theorem pack_b_u_r_e_4_eq : ∀ x0 x1 . ∀ x2 : ι → ι → ι . ∀ x3 : ι → ι . ∀ x4 : ι → ι → ο . ∀ x5 . x0 = pack_b_u_r_e x1 x2 x3 x4 x5x5 = ap x0 4 (proof)
Theorem pack_b_u_r_e_4_eq2 : ∀ x0 . ∀ x1 : ι → ι → ι . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ο . ∀ x4 . x4 = ap (pack_b_u_r_e x0 x1 x2 x3 x4) 4 (proof)
Theorem pack_b_u_r_e_inj : ∀ x0 x1 . ∀ x2 x3 : ι → ι → ι . ∀ x4 x5 : ι → ι . ∀ x6 x7 : ι → ι → ο . ∀ x8 x9 . pack_b_u_r_e x0 x2 x4 x6 x8 = pack_b_u_r_e x1 x3 x5 x7 x9and (and (and (and (x0 = x1) (∀ x10 . x10x0∀ x11 . x11x0x2 x10 x11 = x3 x10 x11)) (∀ x10 . x10x0x4 x10 = x5 x10)) (∀ x10 . x10x0∀ x11 . x11x0x6 x10 x11 = x7 x10 x11)) (x8 = x9) (proof)
Theorem pack_b_u_r_e_ext : ∀ x0 . ∀ x1 x2 : ι → ι → ι . ∀ x3 x4 : ι → ι . ∀ x5 x6 : ι → ι → ο . ∀ x7 . (∀ x8 . x8x0∀ x9 . x9x0x1 x8 x9 = x2 x8 x9)(∀ x8 . x8x0x3 x8 = x4 x8)(∀ x8 . x8x0∀ x9 . x9x0iff (x5 x8 x9) (x6 x8 x9))pack_b_u_r_e x0 x1 x3 x5 x7 = pack_b_u_r_e x0 x2 x4 x6 x7 (proof)
Definition struct_b_u_r_e := λ x0 . ∀ x1 : ι → ο . (∀ x2 . ∀ x3 : ι → ι → ι . (∀ x4 . x4x2∀ x5 . x5x2x3 x4 x5x2)∀ x4 : ι → ι . (∀ x5 . x5x2x4 x5x2)∀ x5 : ι → ι → ο . ∀ x6 . x6x2x1 (pack_b_u_r_e x2 x3 x4 x5 x6))x1 x0
Theorem pack_struct_b_u_r_e_I : ∀ x0 . ∀ x1 : ι → ι → ι . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x0)∀ x2 : ι → ι . (∀ x3 . x3x0x2 x3x0)∀ x3 : ι → ι → ο . ∀ x4 . x4x0struct_b_u_r_e (pack_b_u_r_e x0 x1 x2 x3 x4) (proof)
Theorem pack_struct_b_u_r_e_E1 : ∀ x0 . ∀ x1 : ι → ι → ι . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ο . ∀ x4 . struct_b_u_r_e (pack_b_u_r_e x0 x1 x2 x3 x4)∀ x5 . x5x0∀ x6 . x6x0x1 x5 x6x0 (proof)
Theorem pack_struct_b_u_r_e_E2 : ∀ x0 . ∀ x1 : ι → ι → ι . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ο . ∀ x4 . struct_b_u_r_e (pack_b_u_r_e x0 x1 x2 x3 x4)∀ x5 . x5x0x2 x5x0 (proof)
Theorem pack_struct_b_u_r_e_E4 : ∀ x0 . ∀ x1 : ι → ι → ι . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ο . ∀ x4 . struct_b_u_r_e (pack_b_u_r_e x0 x1 x2 x3 x4)x4x0 (proof)
Theorem struct_b_u_r_e_eta : ∀ x0 . struct_b_u_r_e x0x0 = pack_b_u_r_e (ap x0 0) (decode_b (ap x0 1)) (ap (ap x0 2)) (decode_r (ap x0 3)) (ap x0 4) (proof)
Definition unpack_b_u_r_e_i := λ x0 . λ x1 : ι → (ι → ι → ι)(ι → ι)(ι → ι → ο)ι → ι . x1 (ap x0 0) (decode_b (ap x0 1)) (ap (ap x0 2)) (decode_r (ap x0 3)) (ap x0 4)
Theorem unpack_b_u_r_e_i_eq : ∀ x0 : ι → (ι → ι → ι)(ι → ι)(ι → ι → ο)ι → ι . ∀ x1 . ∀ x2 : ι → ι → ι . ∀ x3 : ι → ι . ∀ x4 : ι → ι → ο . ∀ x5 . (∀ x6 : ι → ι → ι . (∀ x7 . x7x1∀ x8 . x8x1x2 x7 x8 = x6 x7 x8)∀ x7 : ι → ι . (∀ x8 . x8x1x3 x8 = x7 x8)∀ x8 : ι → ι → ο . (∀ x9 . x9x1∀ x10 . x10x1iff (x4 x9 x10) (x8 x9 x10))x0 x1 x6 x7 x8 x5 = x0 x1 x2 x3 x4 x5)unpack_b_u_r_e_i (pack_b_u_r_e x1 x2 x3 x4 x5) x0 = x0 x1 x2 x3 x4 x5 (proof)
Definition unpack_b_u_r_e_o := λ x0 . λ x1 : ι → (ι → ι → ι)(ι → ι)(ι → ι → ο)ι → ο . x1 (ap x0 0) (decode_b (ap x0 1)) (ap (ap x0 2)) (decode_r (ap x0 3)) (ap x0 4)
Theorem unpack_b_u_r_e_o_eq : ∀ x0 : ι → (ι → ι → ι)(ι → ι)(ι → ι → ο)ι → ο . ∀ x1 . ∀ x2 : ι → ι → ι . ∀ x3 : ι → ι . ∀ x4 : ι → ι → ο . ∀ x5 . (∀ x6 : ι → ι → ι . (∀ x7 . x7x1∀ x8 . x8x1x2 x7 x8 = x6 x7 x8)∀ x7 : ι → ι . (∀ x8 . x8x1x3 x8 = x7 x8)∀ x8 : ι → ι → ο . (∀ x9 . x9x1∀ x10 . x10x1iff (x4 x9 x10) (x8 x9 x10))x0 x1 x6 x7 x8 x5 = x0 x1 x2 x3 x4 x5)unpack_b_u_r_e_o (pack_b_u_r_e x1 x2 x3 x4 x5) x0 = x0 x1 x2 x3 x4 x5 (proof)
Definition pack_b_u_p_p := λ x0 . λ x1 : ι → ι → ι . λ x2 : ι → ι . λ x3 x4 : ι → ο . lam 5 (λ x5 . If_i (x5 = 0) x0 (If_i (x5 = 1) (encode_b x0 x1) (If_i (x5 = 2) (lam x0 x2) (If_i (x5 = 3) (Sep x0 x3) (Sep x0 x4)))))
Theorem pack_b_u_p_p_0_eq : ∀ x0 x1 . ∀ x2 : ι → ι → ι . ∀ x3 : ι → ι . ∀ x4 x5 : ι → ο . x0 = pack_b_u_p_p x1 x2 x3 x4 x5x1 = ap x0 0 (proof)
Theorem pack_b_u_p_p_0_eq2 : ∀ x0 . ∀ x1 : ι → ι → ι . ∀ x2 : ι → ι . ∀ x3 x4 : ι → ο . x0 = ap (pack_b_u_p_p x0 x1 x2 x3 x4) 0 (proof)
Theorem pack_b_u_p_p_1_eq : ∀ x0 x1 . ∀ x2 : ι → ι → ι . ∀ x3 : ι → ι . ∀ x4 x5 : ι → ο . x0 = pack_b_u_p_p x1 x2 x3 x4 x5∀ x6 . x6x1∀ x7 . x7x1x2 x6 x7 = decode_b (ap x0 1) x6 x7 (proof)
Theorem pack_b_u_p_p_1_eq2 : ∀ x0 . ∀ x1 : ι → ι → ι . ∀ x2 : ι → ι . ∀ x3 x4 : ι → ο . ∀ x5 . x5x0∀ x6 . x6x0x1 x5 x6 = decode_b (ap (pack_b_u_p_p x0 x1 x2 x3 x4) 1) x5 x6 (proof)
Theorem pack_b_u_p_p_2_eq : ∀ x0 x1 . ∀ x2 : ι → ι → ι . ∀ x3 : ι → ι . ∀ x4 x5 : ι → ο . x0 = pack_b_u_p_p x1 x2 x3 x4 x5∀ x6 . x6x1x3 x6 = ap (ap x0 2) x6 (proof)
Theorem pack_b_u_p_p_2_eq2 : ∀ x0 . ∀ x1 : ι → ι → ι . ∀ x2 : ι → ι . ∀ x3 x4 : ι → ο . ∀ x5 . x5x0x2 x5 = ap (ap (pack_b_u_p_p x0 x1 x2 x3 x4) 2) x5 (proof)
Theorem pack_b_u_p_p_3_eq : ∀ x0 x1 . ∀ x2 : ι → ι → ι . ∀ x3 : ι → ι . ∀ x4 x5 : ι → ο . x0 = pack_b_u_p_p x1 x2 x3 x4 x5∀ x6 . x6x1x4 x6 = decode_p (ap x0 3) x6 (proof)
Theorem pack_b_u_p_p_3_eq2 : ∀ x0 . ∀ x1 : ι → ι → ι . ∀ x2 : ι → ι . ∀ x3 x4 : ι → ο . ∀ x5 . x5x0x3 x5 = decode_p (ap (pack_b_u_p_p x0 x1 x2 x3 x4) 3) x5 (proof)
Theorem pack_b_u_p_p_4_eq : ∀ x0 x1 . ∀ x2 : ι → ι → ι . ∀ x3 : ι → ι . ∀ x4 x5 : ι → ο . x0 = pack_b_u_p_p x1 x2 x3 x4 x5∀ x6 . x6x1x5 x6 = decode_p (ap x0 4) x6 (proof)
Theorem pack_b_u_p_p_4_eq2 : ∀ x0 . ∀ x1 : ι → ι → ι . ∀ x2 : ι → ι . ∀ x3 x4 : ι → ο . ∀ x5 . x5x0x4 x5 = decode_p (ap (pack_b_u_p_p x0 x1 x2 x3 x4) 4) x5 (proof)
Theorem pack_b_u_p_p_inj : ∀ x0 x1 . ∀ x2 x3 : ι → ι → ι . ∀ x4 x5 : ι → ι . ∀ x6 x7 x8 x9 : ι → ο . pack_b_u_p_p x0 x2 x4 x6 x8 = pack_b_u_p_p x1 x3 x5 x7 x9and (and (and (and (x0 = x1) (∀ x10 . x10x0∀ x11 . x11x0x2 x10 x11 = x3 x10 x11)) (∀ x10 . x10x0x4 x10 = x5 x10)) (∀ x10 . x10x0x6 x10 = x7 x10)) (∀ x10 . x10x0x8 x10 = x9 x10) (proof)
Theorem pack_b_u_p_p_ext : ∀ x0 . ∀ x1 x2 : ι → ι → ι . ∀ x3 x4 : ι → ι . ∀ x5 x6 x7 x8 : ι → ο . (∀ x9 . x9x0∀ x10 . x10x0x1 x9 x10 = x2 x9 x10)(∀ x9 . x9x0x3 x9 = x4 x9)(∀ x9 . x9x0iff (x5 x9) (x6 x9))(∀ x9 . x9x0iff (x7 x9) (x8 x9))pack_b_u_p_p x0 x1 x3 x5 x7 = pack_b_u_p_p x0 x2 x4 x6 x8 (proof)
Definition struct_b_u_p_p := λ x0 . ∀ x1 : ι → ο . (∀ x2 . ∀ x3 : ι → ι → ι . (∀ x4 . x4x2∀ x5 . x5x2x3 x4 x5x2)∀ x4 : ι → ι . (∀ x5 . x5x2x4 x5x2)∀ x5 x6 : ι → ο . x1 (pack_b_u_p_p x2 x3 x4 x5 x6))x1 x0
Theorem pack_struct_b_u_p_p_I : ∀ x0 . ∀ x1 : ι → ι → ι . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x0)∀ x2 : ι → ι . (∀ x3 . x3x0x2 x3x0)∀ x3 x4 : ι → ο . struct_b_u_p_p (pack_b_u_p_p x0 x1 x2 x3 x4) (proof)
Theorem pack_struct_b_u_p_p_E1 : ∀ x0 . ∀ x1 : ι → ι → ι . ∀ x2 : ι → ι . ∀ x3 x4 : ι → ο . struct_b_u_p_p (pack_b_u_p_p x0 x1 x2 x3 x4)∀ x5 . x5x0∀ x6 . x6x0x1 x5 x6x0 (proof)
Theorem pack_struct_b_u_p_p_E2 : ∀ x0 . ∀ x1 : ι → ι → ι . ∀ x2 : ι → ι . ∀ x3 x4 : ι → ο . struct_b_u_p_p (pack_b_u_p_p x0 x1 x2 x3 x4)∀ x5 . x5x0x2 x5x0 (proof)
Theorem struct_b_u_p_p_eta : ∀ x0 . struct_b_u_p_p x0x0 = pack_b_u_p_p (ap x0 0) (decode_b (ap x0 1)) (ap (ap x0 2)) (decode_p (ap x0 3)) (decode_p (ap x0 4)) (proof)
Definition unpack_b_u_p_p_i := λ x0 . λ x1 : ι → (ι → ι → ι)(ι → ι)(ι → ο)(ι → ο) → ι . x1 (ap x0 0) (decode_b (ap x0 1)) (ap (ap x0 2)) (decode_p (ap x0 3)) (decode_p (ap x0 4))
Theorem unpack_b_u_p_p_i_eq : ∀ x0 : ι → (ι → ι → ι)(ι → ι)(ι → ο)(ι → ο) → ι . ∀ x1 . ∀ x2 : ι → ι → ι . ∀ x3 : ι → ι . ∀ x4 x5 : ι → ο . (∀ x6 : ι → ι → ι . (∀ x7 . x7x1∀ x8 . x8x1x2 x7 x8 = x6 x7 x8)∀ x7 : ι → ι . (∀ x8 . x8x1x3 x8 = x7 x8)∀ x8 : ι → ο . (∀ x9 . x9x1iff (x4 x9) (x8 x9))∀ x9 : ι → ο . (∀ x10 . x10x1iff (x5 x10) (x9 x10))x0 x1 x6 x7 x8 x9 = x0 x1 x2 x3 x4 x5)unpack_b_u_p_p_i (pack_b_u_p_p x1 x2 x3 x4 x5) x0 = x0 x1 x2 x3 x4 x5 (proof)
Definition unpack_b_u_p_p_o := λ x0 . λ x1 : ι → (ι → ι → ι)(ι → ι)(ι → ο)(ι → ο) → ο . x1 (ap x0 0) (decode_b (ap x0 1)) (ap (ap x0 2)) (decode_p (ap x0 3)) (decode_p (ap x0 4))
Theorem unpack_b_u_p_p_o_eq : ∀ x0 : ι → (ι → ι → ι)(ι → ι)(ι → ο)(ι → ο) → ο . ∀ x1 . ∀ x2 : ι → ι → ι . ∀ x3 : ι → ι . ∀ x4 x5 : ι → ο . (∀ x6 : ι → ι → ι . (∀ x7 . x7x1∀ x8 . x8x1x2 x7 x8 = x6 x7 x8)∀ x7 : ι → ι . (∀ x8 . x8x1x3 x8 = x7 x8)∀ x8 : ι → ο . (∀ x9 . x9x1iff (x4 x9) (x8 x9))∀ x9 : ι → ο . (∀ x10 . x10x1iff (x5 x10) (x9 x10))x0 x1 x6 x7 x8 x9 = x0 x1 x2 x3 x4 x5)unpack_b_u_p_p_o (pack_b_u_p_p x1 x2 x3 x4 x5) x0 = x0 x1 x2 x3 x4 x5 (proof)
Definition pack_b_u_p_e := λ x0 . λ x1 : ι → ι → ι . λ x2 : ι → ι . λ x3 : ι → ο . λ x4 . lam 5 (λ x5 . If_i (x5 = 0) x0 (If_i (x5 = 1) (encode_b x0 x1) (If_i (x5 = 2) (lam x0 x2) (If_i (x5 = 3) (Sep x0 x3) x4))))
Theorem pack_b_u_p_e_0_eq : ∀ x0 x1 . ∀ x2 : ι → ι → ι . ∀ x3 : ι → ι . ∀ x4 : ι → ο . ∀ x5 . x0 = pack_b_u_p_e x1 x2 x3 x4 x5x1 = ap x0 0 (proof)
Theorem pack_b_u_p_e_0_eq2 : ∀ x0 . ∀ x1 : ι → ι → ι . ∀ x2 : ι → ι . ∀ x3 : ι → ο . ∀ x4 . x0 = ap (pack_b_u_p_e x0 x1 x2 x3 x4) 0 (proof)
Theorem pack_b_u_p_e_1_eq : ∀ x0 x1 . ∀ x2 : ι → ι → ι . ∀ x3 : ι → ι . ∀ x4 : ι → ο . ∀ x5 . x0 = pack_b_u_p_e x1 x2 x3 x4 x5∀ x6 . x6x1∀ x7 . x7x1x2 x6 x7 = decode_b (ap x0 1) x6 x7 (proof)
Theorem pack_b_u_p_e_1_eq2 : ∀ x0 . ∀ x1 : ι → ι → ι . ∀ x2 : ι → ι . ∀ x3 : ι → ο . ∀ x4 x5 . x5x0∀ x6 . x6x0x1 x5 x6 = decode_b (ap (pack_b_u_p_e x0 x1 x2 x3 x4) 1) x5 x6 (proof)
Theorem pack_b_u_p_e_2_eq : ∀ x0 x1 . ∀ x2 : ι → ι → ι . ∀ x3 : ι → ι . ∀ x4 : ι → ο . ∀ x5 . x0 = pack_b_u_p_e x1 x2 x3 x4 x5∀ x6 . x6x1x3 x6 = ap (ap x0 2) x6 (proof)
Theorem pack_b_u_p_e_2_eq2 : ∀ x0 . ∀ x1 : ι → ι → ι . ∀ x2 : ι → ι . ∀ x3 : ι → ο . ∀ x4 x5 . x5x0x2 x5 = ap (ap (pack_b_u_p_e x0 x1 x2 x3 x4) 2) x5 (proof)
Theorem pack_b_u_p_e_3_eq : ∀ x0 x1 . ∀ x2 : ι → ι → ι . ∀ x3 : ι → ι . ∀ x4 : ι → ο . ∀ x5 . x0 = pack_b_u_p_e x1 x2 x3 x4 x5∀ x6 . x6x1x4 x6 = decode_p (ap x0 3) x6 (proof)
Theorem pack_b_u_p_e_3_eq2 : ∀ x0 . ∀ x1 : ι → ι → ι . ∀ x2 : ι → ι . ∀ x3 : ι → ο . ∀ x4 x5 . x5x0x3 x5 = decode_p (ap (pack_b_u_p_e x0 x1 x2 x3 x4) 3) x5 (proof)
Theorem pack_b_u_p_e_4_eq : ∀ x0 x1 . ∀ x2 : ι → ι → ι . ∀ x3 : ι → ι . ∀ x4 : ι → ο . ∀ x5 . x0 = pack_b_u_p_e x1 x2 x3 x4 x5x5 = ap x0 4 (proof)
Theorem pack_b_u_p_e_4_eq2 : ∀ x0 . ∀ x1 : ι → ι → ι . ∀ x2 : ι → ι . ∀ x3 : ι → ο . ∀ x4 . x4 = ap (pack_b_u_p_e x0 x1 x2 x3 x4) 4 (proof)
Theorem pack_b_u_p_e_inj : ∀ x0 x1 . ∀ x2 x3 : ι → ι → ι . ∀ x4 x5 : ι → ι . ∀ x6 x7 : ι → ο . ∀ x8 x9 . pack_b_u_p_e x0 x2 x4 x6 x8 = pack_b_u_p_e x1 x3 x5 x7 x9and (and (and (and (x0 = x1) (∀ x10 . x10x0∀ x11 . x11x0x2 x10 x11 = x3 x10 x11)) (∀ x10 . x10x0x4 x10 = x5 x10)) (∀ x10 . x10x0x6 x10 = x7 x10)) (x8 = x9) (proof)
Theorem pack_b_u_p_e_ext : ∀ x0 . ∀ x1 x2 : ι → ι → ι . ∀ x3 x4 : ι → ι . ∀ x5 x6 : ι → ο . ∀ x7 . (∀ x8 . x8x0∀ x9 . x9x0x1 x8 x9 = x2 x8 x9)(∀ x8 . x8x0x3 x8 = x4 x8)(∀ x8 . x8x0iff (x5 x8) (x6 x8))pack_b_u_p_e x0 x1 x3 x5 x7 = pack_b_u_p_e x0 x2 x4 x6 x7 (proof)
Definition struct_b_u_p_e := λ x0 . ∀ x1 : ι → ο . (∀ x2 . ∀ x3 : ι → ι → ι . (∀ x4 . x4x2∀ x5 . x5x2x3 x4 x5x2)∀ x4 : ι → ι . (∀ x5 . x5x2x4 x5x2)∀ x5 : ι → ο . ∀ x6 . x6x2x1 (pack_b_u_p_e x2 x3 x4 x5 x6))x1 x0
Theorem pack_struct_b_u_p_e_I : ∀ x0 . ∀ x1 : ι → ι → ι . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x0)∀ x2 : ι → ι . (∀ x3 . x3x0x2 x3x0)∀ x3 : ι → ο . ∀ x4 . x4x0struct_b_u_p_e (pack_b_u_p_e x0 x1 x2 x3 x4) (proof)
Theorem pack_struct_b_u_p_e_E1 : ∀ x0 . ∀ x1 : ι → ι → ι . ∀ x2 : ι → ι . ∀ x3 : ι → ο . ∀ x4 . struct_b_u_p_e (pack_b_u_p_e x0 x1 x2 x3 x4)∀ x5 . x5x0∀ x6 . x6x0x1 x5 x6x0 (proof)
Theorem pack_struct_b_u_p_e_E2 : ∀ x0 . ∀ x1 : ι → ι → ι . ∀ x2 : ι → ι . ∀ x3 : ι → ο . ∀ x4 . struct_b_u_p_e (pack_b_u_p_e x0 x1 x2 x3 x4)∀ x5 . x5x0x2 x5x0 (proof)
Theorem pack_struct_b_u_p_e_E4 : ∀ x0 . ∀ x1 : ι → ι → ι . ∀ x2 : ι → ι . ∀ x3 : ι → ο . ∀ x4 . struct_b_u_p_e (pack_b_u_p_e x0 x1 x2 x3 x4)x4x0 (proof)
Theorem struct_b_u_p_e_eta : ∀ x0 . struct_b_u_p_e x0x0 = pack_b_u_p_e (ap x0 0) (decode_b (ap x0 1)) (ap (ap x0 2)) (decode_p (ap x0 3)) (ap x0 4) (proof)
Definition unpack_b_u_p_e_i := λ x0 . λ x1 : ι → (ι → ι → ι)(ι → ι)(ι → ο)ι → ι . x1 (ap x0 0) (decode_b (ap x0 1)) (ap (ap x0 2)) (decode_p (ap x0 3)) (ap x0 4)
Theorem unpack_b_u_p_e_i_eq : ∀ x0 : ι → (ι → ι → ι)(ι → ι)(ι → ο)ι → ι . ∀ x1 . ∀ x2 : ι → ι → ι . ∀ x3 : ι → ι . ∀ x4 : ι → ο . ∀ x5 . (∀ x6 : ι → ι → ι . (∀ x7 . x7x1∀ x8 . x8x1x2 x7 x8 = x6 x7 x8)∀ x7 : ι → ι . (∀ x8 . x8x1x3 x8 = x7 x8)∀ x8 : ι → ο . (∀ x9 . x9x1iff (x4 x9) (x8 x9))x0 x1 x6 x7 x8 x5 = x0 x1 x2 x3 x4 x5)unpack_b_u_p_e_i (pack_b_u_p_e x1 x2 x3 x4 x5) x0 = x0 x1 x2 x3 x4 x5 (proof)
Definition unpack_b_u_p_e_o := λ x0 . λ x1 : ι → (ι → ι → ι)(ι → ι)(ι → ο)ι → ο . x1 (ap x0 0) (decode_b (ap x0 1)) (ap (ap x0 2)) (decode_p (ap x0 3)) (ap x0 4)
Theorem unpack_b_u_p_e_o_eq : ∀ x0 : ι → (ι → ι → ι)(ι → ι)(ι → ο)ι → ο . ∀ x1 . ∀ x2 : ι → ι → ι . ∀ x3 : ι → ι . ∀ x4 : ι → ο . ∀ x5 . (∀ x6 : ι → ι → ι . (∀ x7 . x7x1∀ x8 . x8x1x2 x7 x8 = x6 x7 x8)∀ x7 : ι → ι . (∀ x8 . x8x1x3 x8 = x7 x8)∀ x8 : ι → ο . (∀ x9 . x9x1iff (x4 x9) (x8 x9))x0 x1 x6 x7 x8 x5 = x0 x1 x2 x3 x4 x5)unpack_b_u_p_e_o (pack_b_u_p_e x1 x2 x3 x4 x5) x0 = x0 x1 x2 x3 x4 x5 (proof)