Proofgold Address

Param unpack_p_i^unpack_p_i : ι → (ι → (ι → ο) → ι) → ι
Param pack_p^pack_p : ι → (ι → ο) → ι
Param lam^Sigma : ι → (ι → ι) → ι
Definition setprod^setprod := λ x0 x1 . lam x0 (λ x2 . x1)
Definition and^and := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Param ap^ap : ι → ι → ι
Param ordsucc^ordsucc : ι → ι
Definition b0670.. := λ x0 x1 . unpack_p_i x0 (λ x2 . λ x3 : ι → ο . unpack_p_i x1 (λ x4 . λ x5 : ι → ο . pack_p (setprod x2 x4) (λ x6 . and (x3 (ap x6 0)) (x5 (ap x6 1)))))
Definition iff^iff := λ x0 x1 : ο . and (x0 ⟶ x1) (x1 ⟶ x0)
Known unpack_p_i_eq^{unpack_p_i_eq} : ∀ x0 : ι → (ι → ο) → ι . ∀ x1 . ∀ x2 : ι → ο . (∀ x3 : ι → ο . (∀ x4 . x4 ∈ x1 ⟶ iff (x2 x4) (x3 x4)) ⟶ x0 x1 x3 = x0 x1 x2) ⟶ unpack_p_i (pack_p x1 x2) x0 = x0 x1 x2
Known pack_p_ext^pack_p_ext : ∀ x0 . ∀ x1 x2 : ι → ο . (∀ x3 . x3 ∈ x0 ⟶ iff (x1 x3) (x2 x3)) ⟶ pack_p x0 x1 = pack_p x0 x2
Known iffI^iffI : ∀ x0 x1 : ο . (x0 ⟶ x1) ⟶ (x1 ⟶ x0) ⟶ iff x0 x1
Known andI^andI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1
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 9b8cf.. : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . ∀ x3 : ι → ο . b0670.. (pack_p x0 x1) (pack_p x2 x3) = pack_p (setprod x0 x2) (λ x5 . and (x1 (ap x5 0)) (x3 (ap x5 1))) (proof)
Definition struct_p^struct_p := λ x0 . ∀ x1 : ι → ο . (∀ x2 . ∀ x3 : ι → ο . x1 (pack_p x2 x3)) ⟶ x1 x0
Known pack_struct_p_I^{pack_struct_p_I} : ∀ x0 . ∀ x1 : ι → ο . struct_p (pack_p x0 x1)
Theorem 07788.. : ∀ x0 x1 . struct_p x0 ⟶ struct_p x1 ⟶ struct_p (b0670.. x0 x1) (proof)
Definition MetaCat_product_p^product_p := λ x0 : ι → ο . λ x1 : ι → ι → ι → ο . λ x2 : ι → ι . λ x3 : ι → ι → ι → ι → ι → ι . λ x4 x5 x6 x7 x8 . λ x9 : ι → ι → ι → ι . and (and (and (and (and (x0 x4) (x0 x5)) (x0 x6)) (x1 x6 x4 x7)) (x1 x6 x5 x8)) (∀ x10 . x0 x10 ⟶ ∀ x11 x12 . x1 x10 x4 x11 ⟶ x1 x10 x5 x12 ⟶ and (and (and (x1 x10 x6 (x9 x10 x11 x12)) (x3 x10 x6 x4 x7 (x9 x10 x11 x12) = x11)) (x3 x10 x6 x5 x8 (x9 x10 x11 x12) = x12)) (∀ x13 . x1 x10 x6 x13 ⟶ x3 x10 x6 x4 x7 x13 = x11 ⟶ x3 x10 x6 x5 x8 x13 = x12 ⟶ x13 = x9 x10 x11 x12))
Definition MetaCat_product_constr_p^{product_constr_p} := λ x0 : ι → ο . λ x1 : ι → ι → ι → ο . λ x2 : ι → ι . λ x3 : ι → ι → ι → ι → ι → ι . λ x4 x5 x6 : ι → ι → ι . λ x7 : ι → ι → ι → ι → ι → ι . ∀ x8 x9 . x0 x8 ⟶ x0 x9 ⟶ MetaCat_product_p x0 x1 x2 x3 x8 x9 (x4 x8 x9) (x5 x8 x9) (x6 x8 x9) (x7 x8 x9)
Param UnaryPredHom^Hom_struct_p : ι → ι → ι → ο
Param struct_id^struct_id : ι → ι
Definition lam_comp^lam_comp := λ x0 x1 x2 . lam x0 (λ x3 . ap x1 (ap x2 x3))
Definition struct_comp^struct_comp := λ x0 x1 x2 . lam_comp (ap x0 0)
Param If_i^If_i : ο → ι → ι → ι
Known and6I^and6I : ∀ x0 x1 x2 x3 x4 x5 : ο . x0 ⟶ x1 ⟶ x2 ⟶ x3 ⟶ x4 ⟶ x5 ⟶ and (and (and (and (and x0 x1) x2) x3) x4) x5
Known pack_p_0_eq2^pack_p_0_eq2 : ∀ x0 . ∀ x1 : ι → ο . x0 = ap (pack_p x0 x1) 0
Known and3I^and3I : ∀ x0 x1 x2 : ο . x0 ⟶ x1 ⟶ x2 ⟶ and (and x0 x1) x2
Param Pi^Pi : ι → (ι → ι) → ι
Definition setexp^setexp := λ x0 x1 . Pi x1 (λ x2 . x0)
Known 55fb5..^{Hom_struct_p_pack} : ∀ x0 x1 . ∀ x2 x3 : ι → ο . ∀ x4 . UnaryPredHom (pack_p x0 x2) (pack_p x1 x3) x4 = and (x4 ∈ setexp x1 x0) (∀ x6 . x6 ∈ x0 ⟶ x2 x6 ⟶ x3 (ap x4 x6))
Known lam_Pi^lam_Pi : ∀ x0 . ∀ x1 x2 : ι → ι . (∀ x3 . x3 ∈ x0 ⟶ x2 x3 ∈ x1 x3) ⟶ lam x0 x2 ∈ Pi x0 x1
Known beta^beta : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ x0 ⟶ ap (lam x0 x1) x2 = x1 x2
Known and4I^and4I : ∀ x0 x1 x2 x3 : ο . x0 ⟶ x1 ⟶ x2 ⟶ x3 ⟶ and (and (and x0 x1) x2) x3
Known encode_u_ext^encode_u_ext : ∀ x0 . ∀ x1 x2 : ι → ι . (∀ x3 . x3 ∈ x0 ⟶ x1 x3 = x2 x3) ⟶ lam x0 x1 = lam x0 x2
Known ap_Pi^ap_Pi : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 x3 . x2 ∈ Pi x0 x1 ⟶ x3 ∈ x0 ⟶ ap x2 x3 ∈ x1 x3
Known Pi_eta^Pi_eta : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ Pi x0 x1 ⟶ lam x0 (ap x2) = x2
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
Known tuple_2_1_eq^tuple_2_1_eq : ∀ x0 x1 . ap (lam 2 (λ x3 . If_i (x3 = 0) x0 x1)) 1 = x1
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_Sigma^{tuple_2_Sigma} : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x1 x2 ⟶ lam 2 (λ x4 . If_i (x4 = 0) x2 x3) ∈ lam x0 x1
Theorem a9f63.. : ∀ x0 : ι → ο . (∀ x1 . x0 x1 ⟶ struct_p x1) ⟶ (∀ x1 x2 . x0 x1 ⟶ x0 x2 ⟶ x0 (b0670.. x1 x2)) ⟶ MetaCat_product_constr_p x0 UnaryPredHom struct_id struct_comp b0670.. (λ x1 x2 . lam (setprod (ap x1 0) (ap x2 0)) (λ x3 . ap x3 0)) (λ x1 x2 . lam (setprod (ap x1 0) (ap x2 0)) (λ x3 . ap x3 1)) (λ x1 x2 x3 x4 x5 . lam (ap x3 0) (λ x6 . lam 2 (λ x7 . If_i (x7 = 0) (ap x4 x6) (ap x5 x6)))) (proof)
Theorem 83624.. : MetaCat_product_constr_p struct_p UnaryPredHom struct_id struct_comp b0670.. (λ x0 x1 . lam (setprod (ap x0 0) (ap x1 0)) (λ x2 . ap x2 0)) (λ x0 x1 . lam (setprod (ap x0 0) (ap x1 0)) (λ x2 . ap x2 1)) (λ x0 x1 x2 x3 x4 . lam (ap x2 0) (λ x5 . lam 2 (λ x6 . If_i (x6 = 0) (ap x3 x5) (ap x4 x5)))) (proof)
Theorem 4f9ac..^{MetaCat_struct_p_product_constr} : ∀ x0 : ο . (∀ x1 : ι → ι → ι . (∀ x2 : ο . (∀ x3 : ι → ι → ι . (∀ x4 : ο . (∀ x5 : ι → ι → ι . (∀ x6 : ο . (∀ x7 : ι → ι → ι → ι → ι → ι . MetaCat_product_constr_p struct_p UnaryPredHom struct_id struct_comp x1 x3 x5 x7 ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4) ⟶ x2) ⟶ x2) ⟶ x0) ⟶ x0 (proof)
Definition f5637.. := λ x0 x1 . unpack_p_i x0 (λ x2 . λ x3 : ι → ο . unpack_p_i x1 (λ x4 . λ x5 : ι → ο . pack_p (setexp x4 x2) (λ x6 . ∀ x7 . x7 ∈ x2 ⟶ x3 x7 ⟶ x5 (ap x6 x7))))
Theorem 742d0.. : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . ∀ x3 : ι → ο . f5637.. (pack_p x0 x1) (pack_p x2 x3) = pack_p (setexp x2 x0) (λ x5 . ∀ x6 . x6 ∈ x0 ⟶ x1 x6 ⟶ x3 (ap x5 x6)) (proof)
Theorem 92911.. : ∀ x0 x1 . struct_p x0 ⟶ struct_p x1 ⟶ struct_p (f5637.. x0 x1) (proof)
Definition MetaCat_exp_p^exponent_p := λ x0 : ι → ο . λ x1 : ι → ι → ι → ο . λ x2 : ι → ι . λ x3 : ι → ι → ι → ι → ι → ι . λ x4 x5 x6 : ι → ι → ι . λ x7 : ι → ι → ι → ι → ι → ι . λ x8 x9 x10 x11 . λ x12 : ι → ι → ι . and (and (and (and (x0 x8) (x0 x9)) (x0 x10)) (x1 (x4 x10 x8) x9 x11)) (∀ x13 . x0 x13 ⟶ ∀ x14 . x1 (x4 x13 x8) x9 x14 ⟶ and (and (x1 x13 x10 (x12 x13 x14)) (x3 (x4 x13 x8) (x4 x10 x8) x9 x11 (x7 x10 x8 (x4 x13 x8) (x3 (x4 x13 x8) x13 x10 (x12 x13 x14) (x5 x13 x8)) (x6 x13 x8)) = x14)) (∀ x15 . x1 x13 x10 x15 ⟶ x3 (x4 x13 x8) (x4 x10 x8) x9 x11 (x7 x10 x8 (x4 x13 x8) (x3 (x4 x13 x8) x13 x10 x15 (x5 x13 x8)) (x6 x13 x8)) = x14 ⟶ x15 = x12 x13 x14))
Definition MetaCat_exp_constr_p^{product_exponent_constr_p} := λ x0 : ι → ο . λ x1 : ι → ι → ι → ο . λ x2 : ι → ι . λ x3 : ι → ι → ι → ι → ι → ι . λ x4 x5 x6 : ι → ι → ι . λ x7 : ι → ι → ι → ι → ι → ι . λ x8 x9 : ι → ι → ι . λ x10 : ι → ι → ι → ι → ι . and (MetaCat_product_constr_p x0 x1 x2 x3 x4 x5 x6 x7) (∀ x11 x12 . x0 x11 ⟶ x0 x12 ⟶ MetaCat_exp_p x0 x1 x2 x3 x4 x5 x6 x7 x11 x12 (x8 x11 x12) (x9 x11 x12) (x10 x11 x12))
Known and5I^and5I : ∀ x0 x1 x2 x3 x4 : ο . x0 ⟶ x1 ⟶ x2 ⟶ x3 ⟶ x4 ⟶ and (and (and (and x0 x1) x2) x3) x4
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 a0a6c.. : ∀ x0 : ι → ο . (∀ x1 . x0 x1 ⟶ struct_p x1) ⟶ (∀ x1 x2 . x0 x1 ⟶ x0 x2 ⟶ x0 (b0670.. x1 x2)) ⟶ (∀ x1 x2 . x0 x1 ⟶ x0 x2 ⟶ x0 (f5637.. x1 x2)) ⟶ MetaCat_exp_constr_p x0 UnaryPredHom struct_id struct_comp b0670.. (λ x1 x2 . lam (setprod (ap x1 0) (ap x2 0)) (λ x3 . ap x3 0)) (λ x1 x2 . lam (setprod (ap x1 0) (ap x2 0)) (λ x3 . ap x3 1)) (λ x1 x2 x3 x4 x5 . lam (ap x3 0) (λ x6 . lam 2 (λ x7 . If_i (x7 = 0) (ap x4 x6) (ap x5 x6)))) f5637.. (λ x1 x2 . lam (setprod (setexp (ap x2 0) (ap x1 0)) (ap x1 0)) (λ x3 . ap (ap x3 0) (ap x3 1))) (λ x1 x2 x3 x4 . lam (ap x3 0) (λ x5 . lam (ap x1 0) (λ x6 . ap x4 (lam 2 (λ x7 . If_i (x7 = 0) x5 x6))))) (proof)
Theorem 25e85.. : MetaCat_exp_constr_p struct_p UnaryPredHom struct_id struct_comp b0670.. (λ x0 x1 . lam (setprod (ap x0 0) (ap x1 0)) (λ x2 . ap x2 0)) (λ x0 x1 . lam (setprod (ap x0 0) (ap x1 0)) (λ x2 . ap x2 1)) (λ x0 x1 x2 x3 x4 . lam (ap x2 0) (λ x5 . lam 2 (λ x6 . If_i (x6 = 0) (ap x3 x5) (ap x4 x5)))) f5637.. (λ x0 x1 . lam (setprod (setexp (ap x1 0) (ap x0 0)) (ap x0 0)) (λ x2 . ap (ap x2 0) (ap x2 1))) (λ x0 x1 x2 x3 . lam (ap x2 0) (λ x4 . lam (ap x0 0) (λ x5 . ap x3 (lam 2 (λ x6 . If_i (x6 = 0) x4 x5))))) (proof)
Theorem 592be..^{MetaCat_struct_p_product_exponent} : ∀ x0 : ο . (∀ x1 : ι → ι → ι . (∀ x2 : ο . (∀ x3 : ι → ι → ι . (∀ x4 : ο . (∀ x5 : ι → ι → ι . (∀ x6 : ο . (∀ x7 : ι → ι → ι → ι → ι → ι . (∀ x8 : ο . (∀ x9 : ι → ι → ι . (∀ x10 : ο . (∀ x11 : ι → ι → ι . (∀ x12 : ο . (∀ x13 : ι → ι → ι → ι → ι . MetaCat_exp_constr_p struct_p UnaryPredHom struct_id struct_comp x1 x3 x5 x7 x9 x11 x13 ⟶ x12) ⟶ x12) ⟶ x10) ⟶ x10) ⟶ x8) ⟶ x8) ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4) ⟶ x2) ⟶ x2) ⟶ x0) ⟶ x0 (proof)
Param unpack_p_o^unpack_p_o : ι → (ι → (ι → ο) → ο) → ο
Definition PtdPred^{struct_p_nonempty} := λ x0 . and (struct_p x0) (unpack_p_o x0 (λ x1 . λ x2 : ι → ο . ∀ x3 : ο . (∀ x4 . and (x4 ∈ x1) (x2 x4) ⟶ x3) ⟶ x3))
Known 93af6.. : ∀ x0 . ∀ x1 : ι → ο . (∀ x2 : ο . (∀ x3 . and (x3 ∈ x0) (x1 x3) ⟶ x2) ⟶ x2) ⟶ PtdPred (pack_p x0 x1)
Known d8d91.. : ∀ x0 . PtdPred x0 ⟶ ∀ x1 : ι → ο . (∀ x2 . ∀ x3 : ι → ο . ∀ x4 . x4 ∈ x2 ⟶ x3 x4 ⟶ x1 (pack_p x2 x3)) ⟶ x1 x0
Theorem 7633a.. : ∀ x0 . PtdPred x0 ⟶ struct_p x0 (proof)
Theorem e558d.. : ∀ x0 x1 . PtdPred x0 ⟶ PtdPred x1 ⟶ PtdPred (b0670.. x0 x1) (proof)
Theorem 45658..^{MetaCat_struct_p_nonempty_product_constr} : ∀ x0 : ο . (∀ x1 : ι → ι → ι . (∀ x2 : ο . (∀ x3 : ι → ι → ι . (∀ x4 : ο . (∀ x5 : ι → ι → ι . (∀ x6 : ο . (∀ x7 : ι → ι → ι → ι → ι → ι . MetaCat_product_constr_p PtdPred UnaryPredHom struct_id struct_comp x1 x3 x5 x7 ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4) ⟶ x2) ⟶ x2) ⟶ x0) ⟶ x0 (proof)
Theorem 77cc4.. : ∀ x0 x1 . PtdPred x0 ⟶ PtdPred x1 ⟶ PtdPred (f5637.. x0 x1) (proof)
Theorem e25fa..^{MetaCat_struct_p_nonempty_product_exponent} : ∀ x0 : ο . (∀ x1 : ι → ι → ι . (∀ x2 : ο . (∀ x3 : ι → ι → ι . (∀ x4 : ο . (∀ x5 : ι → ι → ι . (∀ x6 : ο . (∀ x7 : ι → ι → ι → ι → ι → ι . (∀ x8 : ο . (∀ x9 : ι → ι → ι . (∀ x10 : ο . (∀ x11 : ι → ι → ι . (∀ x12 : ο . (∀ x13 : ι → ι → ι → ι → ι . MetaCat_exp_constr_p PtdPred UnaryPredHom struct_id struct_comp x1 x3 x5 x7 x9 x11 x13 ⟶ x12) ⟶ x12) ⟶ x10) ⟶ x10) ⟶ x8) ⟶ x8) ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4) ⟶ x2) ⟶ x2) ⟶ x0) ⟶ x0 (proof)