Proofgold Signed Transaction

Param setsum^setsum : ι → ι → ι
Param Inj0^Inj0 : ι → ι
Param Unj^Unj : ι → ι
Definition or^or := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x2) ⟶ (x1 ⟶ x2) ⟶ x2
Definition and^and := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Param Inj1^Inj1 : ι → ι
Known setsum_Inj_inv^{setsum_Inj_inv} : ∀ x0 x1 x2 . x2 ∈ setsum x0 x1 ⟶ or (∀ x3 : ο . (∀ x4 . and (x4 ∈ x0) (x2 = Inj0 x4) ⟶ x3) ⟶ x3) (∀ x3 : ο . (∀ x4 . and (x4 ∈ x1) (x2 = Inj1 x4) ⟶ x3) ⟶ x3)
Known Unj_Inj0_eq^Unj_Inj0_eq : ∀ x0 . Unj (Inj0 x0) = x0
Definition False^False := ∀ x0 : ο . x0
Known FalseE^FalseE : False ⟶ ∀ x0 : ο . x0
Known Inj0_Inj1_neq^{Inj0_Inj1_neq} : ∀ x0 x1 . Inj0 x0 = Inj1 x1 ⟶ ∀ x2 : ο . x2
Theorem 88ba3.. : ∀ x0 x1 x2 . x2 ∈ setsum x0 x1 ⟶ x2 = Inj0 (Unj x2) ⟶ Unj x2 ∈ x0 (proof)
Known Unj_Inj1_eq^Unj_Inj1_eq : ∀ x0 . Unj (Inj1 x0) = x0
Theorem 7d886.. : ∀ x0 x1 x2 . x2 ∈ setsum x0 x1 ⟶ x2 = Inj1 (Unj x2) ⟶ Unj x2 ∈ x1 (proof)
Param unpack_p_i^unpack_p_i : ι → (ι → (ι → ο) → ι) → ι
Param pack_p^pack_p : ι → (ι → ο) → ι
Definition 20e9b.. := λ x0 x1 . unpack_p_i x0 (λ x2 . λ x3 : ι → ο . unpack_p_i x1 (λ x4 . λ x5 : ι → ο . pack_p (setsum x2 x4) (λ x6 . or (and (x6 = Inj0 (Unj x6)) (x3 (Unj x6))) (and (x6 = Inj1 (Unj x6)) (x5 (Unj x6))))))
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 orIL^orIL : ∀ x0 x1 : ο . x0 ⟶ or x0 x1
Known andI^andI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1
Known orIR^orIR : ∀ x0 x1 : ο . x1 ⟶ or x0 x1
Theorem afc07.. : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . ∀ x3 : ι → ο . 20e9b.. (pack_p x0 x1) (pack_p x2 x3) = pack_p (setsum x0 x2) (λ x5 . or (and (x5 = Inj0 (Unj x5)) (x1 (Unj x5))) (and (x5 = Inj1 (Unj x5)) (x3 (Unj x5)))) (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 b6b31.. : ∀ x0 x1 . struct_p x0 ⟶ struct_p x1 ⟶ struct_p (20e9b.. x0 x1) (proof)
Definition MetaCat_coproduct_p^coproduct_p := λ x0 : ι → ο . λ x1 : ι → ι → ι → ο . λ x2 : ι → ι . λ x3 : ι → ι → ι → ι → ι → ι . λ x4 x5 x6 x7 x8 . λ x9 : ι → ι → ι → ι . and (and (and (and (and (x0 x4) (x0 x5)) (x0 x6)) (x1 x4 x6 x7)) (x1 x5 x6 x8)) (∀ x10 . x0 x10 ⟶ ∀ x11 x12 . x1 x4 x10 x11 ⟶ x1 x5 x10 x12 ⟶ and (and (and (x1 x6 x10 (x9 x10 x11 x12)) (x3 x4 x6 x10 (x9 x10 x11 x12) x7 = x11)) (x3 x5 x6 x10 (x9 x10 x11 x12) x8 = x12)) (∀ x13 . x1 x6 x10 x13 ⟶ x3 x4 x6 x10 x13 x7 = x11 ⟶ x3 x5 x6 x10 x13 x8 = x12 ⟶ x13 = x9 x10 x11 x12))
Definition MetaCat_coproduct_constr_p^{coproduct_constr_p} := λ x0 : ι → ο . λ x1 : ι → ι → ι → ο . λ x2 : ι → ι . λ x3 : ι → ι → ι → ι → ι → ι . λ x4 x5 x6 : ι → ι → ι . λ x7 : ι → ι → ι → ι → ι → ι . ∀ x8 x9 . x0 x8 ⟶ x0 x9 ⟶ MetaCat_coproduct_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 : ι → ι
Param lam^Sigma : ι → (ι → ι) → ι
Param ap^ap : ι → ι → ι
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 combine_funcs^{combine_funcs} : ι → ι → (ι → ι) → (ι → ι) → ι → ι
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 Inj0_setsum^Inj0_setsum : ∀ x0 x1 x2 . x2 ∈ x0 ⟶ Inj0 x2 ∈ setsum x0 x1
Known beta^beta : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ x0 ⟶ ap (lam x0 x1) x2 = x1 x2
Known Inj1_setsum^Inj1_setsum : ∀ x0 x1 x2 . x2 ∈ x1 ⟶ Inj1 x2 ∈ setsum x0 x1
Known and4I^and4I : ∀ x0 x1 x2 x3 : ο . x0 ⟶ x1 ⟶ x2 ⟶ x3 ⟶ and (and (and x0 x1) x2) x3
Known combine_funcs_eq1^{combine_funcs_eq1} : ∀ x0 x1 . ∀ x2 x3 : ι → ι . ∀ x4 . combine_funcs x0 x1 x2 x3 (Inj0 x4) = x2 x4
Known ap_Pi^ap_Pi : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 x3 . x2 ∈ Pi x0 x1 ⟶ x3 ∈ x0 ⟶ ap x2 x3 ∈ x1 x3
Known combine_funcs_eq2^{combine_funcs_eq2} : ∀ x0 x1 . ∀ x2 x3 : ι → ι . ∀ x4 . combine_funcs x0 x1 x2 x3 (Inj1 x4) = x3 x4
Known encode_u_ext^encode_u_ext : ∀ x0 . ∀ x1 x2 : ι → ι . (∀ x3 . x3 ∈ x0 ⟶ x1 x3 = x2 x3) ⟶ lam x0 x1 = lam x0 x2
Known Pi_eta^Pi_eta : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ Pi x0 x1 ⟶ lam x0 (ap x2) = x2
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
Theorem e93b0.. : ∀ x0 : ι → ο . (∀ x1 . x0 x1 ⟶ struct_p x1) ⟶ (∀ x1 x2 . x0 x1 ⟶ x0 x2 ⟶ x0 (20e9b.. x1 x2)) ⟶ MetaCat_coproduct_constr_p x0 UnaryPredHom struct_id struct_comp 20e9b.. (λ x1 x2 . lam (ap x1 0) Inj0) (λ x1 x2 . lam (ap x2 0) Inj1) (λ x1 x2 x3 x4 x5 . lam (setsum (ap x1 0) (ap x2 0)) (combine_funcs (ap x1 0) (ap x2 0) (ap x4) (ap x5))) (proof)
Theorem 09ba2..^{MetaCat_struct_p_coproduct_constr} : ∀ x0 : ο . (∀ x1 : ι → ι → ι . (∀ x2 : ο . (∀ x3 : ι → ι → ι . (∀ x4 : ο . (∀ x5 : ι → ι → ι . (∀ x6 : ο . (∀ x7 : ι → ι → ι → ι → ι → ι . MetaCat_coproduct_constr_p struct_p UnaryPredHom struct_id struct_comp x1 x3 x5 x7 ⟶ 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 d8d91.. : ∀ x0 . PtdPred x0 ⟶ ∀ x1 : ι → ο . (∀ x2 . ∀ x3 : ι → ο . ∀ x4 . x4 ∈ x2 ⟶ x3 x4 ⟶ x1 (pack_p x2 x3)) ⟶ x1 x0
Known 93af6.. : ∀ x0 . ∀ x1 : ι → ο . (∀ x2 : ο . (∀ x3 . and (x3 ∈ x0) (x1 x3) ⟶ x2) ⟶ x2) ⟶ PtdPred (pack_p x0 x1)
Theorem 0e807..^{MetaCat_struct_p_nonempty_coproduct_constr} : ∀ x0 : ο . (∀ x1 : ι → ι → ι . (∀ x2 : ο . (∀ x3 : ι → ι → ι . (∀ x4 : ο . (∀ x5 : ι → ι → ι . (∀ x6 : ο . (∀ x7 : ι → ι → ι → ι → ι → ι . MetaCat_coproduct_constr_p PtdPred UnaryPredHom struct_id struct_comp x1 x3 x5 x7 ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4) ⟶ x2) ⟶ x2) ⟶ x0) ⟶ x0 (proof)
Param unpack_r_i^unpack_r_i : ι → (ι → (ι → ι → ο) → ι) → ι
Param pack_r^pack_r : ι → (ι → ι → ο) → ι
Definition 3fa3a.. := λ x0 x1 . unpack_r_i x0 (λ x2 . λ x3 : ι → ι → ο . unpack_r_i x1 (λ x4 . λ x5 : ι → ι → ο . pack_r (setsum x2 x4) (λ x6 x7 . or (and (and (x6 = Inj0 (Unj x6)) (x7 = Inj0 (Unj x7))) (x3 (Unj x6) (Unj x7))) (and (and (x6 = Inj1 (Unj x6)) (x7 = Inj1 (Unj x7))) (x5 (Unj x6) (Unj x7))))))
Known unpack_r_i_eq^{unpack_r_i_eq} : ∀ x0 : ι → (ι → ι → ο) → ι . ∀ x1 . ∀ x2 : ι → ι → ο . (∀ x3 : ι → ι → ο . (∀ x4 . x4 ∈ x1 ⟶ ∀ x5 . x5 ∈ x1 ⟶ iff (x2 x4 x5) (x3 x4 x5)) ⟶ x0 x1 x3 = x0 x1 x2) ⟶ unpack_r_i (pack_r x1 x2) x0 = x0 x1 x2
Known pack_r_ext^pack_r_ext : ∀ x0 . ∀ x1 x2 : ι → ι → ο . (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ iff (x1 x3 x4) (x2 x3 x4)) ⟶ pack_r x0 x1 = pack_r x0 x2
Theorem b86ce.. : ∀ x0 . ∀ x1 : ι → ι → ο . ∀ x2 . ∀ x3 x4 : ι → ι → ο . x4 (3fa3a.. (pack_r x0 x1) (pack_r x2 x3)) (pack_r (setsum x0 x2) (λ x5 x6 . or (and (and (x5 = Inj0 (Unj x5)) (x6 = Inj0 (Unj x6))) (x1 (Unj x5) (Unj x6))) (and (and (x5 = Inj1 (Unj x5)) (x6 = Inj1 (Unj x6))) (x3 (Unj x5) (Unj x6))))) ⟶ x4 (pack_r (setsum x0 x2) (λ x5 x6 . or (and (and (x5 = Inj0 (Unj x5)) (x6 = Inj0 (Unj x6))) (x1 (Unj x5) (Unj x6))) (and (and (x5 = Inj1 (Unj x5)) (x6 = Inj1 (Unj x6))) (x3 (Unj x5) (Unj x6))))) (3fa3a.. (pack_r x0 x1) (pack_r x2 x3)) (proof)
Definition struct_r^struct_r := λ x0 . ∀ x1 : ι → ο . (∀ x2 . ∀ x3 : ι → ι → ο . x1 (pack_r x2 x3)) ⟶ x1 x0
Known pack_struct_r_I^{pack_struct_r_I} : ∀ x0 . ∀ x1 : ι → ι → ο . struct_r (pack_r x0 x1)
Theorem db146.. : ∀ x0 x1 . struct_r x0 ⟶ struct_r x1 ⟶ struct_r (3fa3a.. x0 x1) (proof)
Param BinRelnHom^Hom_struct_r : ι → ι → ι → ο
Known pack_r_0_eq2^pack_r_0_eq2 : ∀ x0 . ∀ x1 x2 : ι → ι → ο . x2 x0 (ap (pack_r x0 x1) 0) ⟶ x2 (ap (pack_r x0 x1) 0) x0
Known c84ab..^{Hom_struct_r_pack} : ∀ x0 x1 . ∀ x2 x3 : ι → ι → ο . ∀ x4 . BinRelnHom (pack_r x0 x2) (pack_r x1 x3) x4 = and (x4 ∈ setexp x1 x0) (∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ x2 x6 x7 ⟶ x3 (ap x4 x6) (ap x4 x7))
Theorem 85bf3.. : ∀ x0 : ι → ο . (∀ x1 . x0 x1 ⟶ struct_r x1) ⟶ (∀ x1 x2 . x0 x1 ⟶ x0 x2 ⟶ x0 (3fa3a.. x1 x2)) ⟶ MetaCat_coproduct_constr_p x0 BinRelnHom struct_id struct_comp 3fa3a.. (λ x1 x2 . lam (ap x1 0) Inj0) (λ x1 x2 . lam (ap x2 0) Inj1) (λ x1 x2 x3 x4 x5 . lam (setsum (ap x1 0) (ap x2 0)) (combine_funcs (ap x1 0) (ap x2 0) (ap x4) (ap x5))) (proof)
Theorem 9a2fc..^{MetaCat_struct_r_coproduct_constr} : ∀ x0 : ο . (∀ x1 : ι → ι → ι . (∀ x2 : ο . (∀ x3 : ι → ι → ι . (∀ x4 : ο . (∀ x5 : ι → ι → ι . (∀ x6 : ο . (∀ x7 : ι → ι → ι → ι → ι → ι . MetaCat_coproduct_constr_p struct_r BinRelnHom struct_id struct_comp x1 x3 x5 x7 ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4) ⟶ x2) ⟶ x2) ⟶ x0) ⟶ x0 (proof)
Param unpack_r_o^unpack_r_o : ι → (ι → (ι → ι → ο) → ο) → ο
Definition not^not := λ x0 : ο . x0 ⟶ False
Definition IrreflexiveSymmetricReln^{struct_r_graph} := λ x0 . and (struct_r x0) (unpack_r_o x0 (λ x1 . λ x2 : ι → ι → ο . and (∀ x3 . x3 ∈ x1 ⟶ not (x2 x3 x3)) (∀ x3 . x3 ∈ x1 ⟶ ∀ x4 . x4 ∈ x1 ⟶ x2 x3 x4 ⟶ x2 x4 x3)))
Known 96ca7.. : ∀ x0 . IrreflexiveSymmetricReln x0 ⟶ ∀ x1 : ι → ο . (∀ x2 . ∀ x3 : ι → ι → ο . (∀ x4 . x4 ∈ x2 ⟶ not (x3 x4 x4)) ⟶ (∀ x4 . x4 ∈ x2 ⟶ ∀ x5 . x5 ∈ x2 ⟶ x3 x4 x5 ⟶ x3 x5 x4) ⟶ x1 (pack_r x2 x3)) ⟶ x1 x0
Known 36176.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2 ∈ x0 ⟶ not (x1 x2 x2)) ⟶ (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2) ⟶ IrreflexiveSymmetricReln (pack_r x0 x1)
Theorem ad517..^{MetaCat_struct_r_graph_coproduct_constr} : ∀ x0 : ο . (∀ x1 : ι → ι → ι . (∀ x2 : ο . (∀ x3 : ι → ι → ι . (∀ x4 : ο . (∀ x5 : ι → ι → ι . (∀ x6 : ο . (∀ x7 : ι → ι → ι → ι → ι → ι . MetaCat_coproduct_constr_p IrreflexiveSymmetricReln BinRelnHom struct_id struct_comp x1 x3 x5 x7 ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4) ⟶ x2) ⟶ x2) ⟶ x0) ⟶ x0 (proof)
Definition PER^struct_r_per := λ x0 . and (struct_r x0) (unpack_r_o x0 (λ x1 . λ x2 : ι → ι → ο . and (∀ x3 . x3 ∈ x1 ⟶ ∀ x4 . x4 ∈ x1 ⟶ x2 x3 x4 ⟶ x2 x4 x3) (∀ x3 . x3 ∈ x1 ⟶ ∀ x4 . x4 ∈ x1 ⟶ ∀ x5 . x5 ∈ x1 ⟶ x2 x3 x4 ⟶ x2 x4 x5 ⟶ x2 x3 x5)))
Known 0bd5c.. : ∀ x0 . PER x0 ⟶ ∀ x1 : ι → ο . (∀ x2 . ∀ x3 : ι → ι → ο . (∀ x4 . x4 ∈ x2 ⟶ ∀ x5 . x5 ∈ x2 ⟶ x3 x4 x5 ⟶ x3 x5 x4) ⟶ (∀ x4 . x4 ∈ x2 ⟶ ∀ x5 . x5 ∈ x2 ⟶ ∀ x6 . x6 ∈ x2 ⟶ x3 x4 x5 ⟶ x3 x5 x6 ⟶ x3 x4 x6) ⟶ x1 (pack_r x2 x3)) ⟶ x1 x0
Known a3466.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2) ⟶ (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x4 ⟶ x1 x2 x4) ⟶ PER (pack_r x0 x1)
Theorem 5de9f..^{MetaCat_struct_r_per_coproduct_constr} : ∀ x0 : ο . (∀ x1 : ι → ι → ι . (∀ x2 : ο . (∀ x3 : ι → ι → ι . (∀ x4 : ο . (∀ x5 : ι → ι → ι . (∀ x6 : ο . (∀ x7 : ι → ι → ι → ι → ι → ι . MetaCat_coproduct_constr_p PER BinRelnHom struct_id struct_comp x1 x3 x5 x7 ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4) ⟶ x2) ⟶ x2) ⟶ x0) ⟶ x0 (proof)
Definition EquivReln^{struct_r_equivreln} := λ x0 . and (struct_r x0) (unpack_r_o x0 (λ x1 . λ x2 : ι → ι → ο . and (and (∀ x3 . x3 ∈ x1 ⟶ x2 x3 x3) (∀ x3 . x3 ∈ x1 ⟶ ∀ x4 . x4 ∈ x1 ⟶ x2 x3 x4 ⟶ x2 x4 x3)) (∀ x3 . x3 ∈ x1 ⟶ ∀ x4 . x4 ∈ x1 ⟶ ∀ x5 . x5 ∈ x1 ⟶ x2 x3 x4 ⟶ x2 x4 x5 ⟶ x2 x3 x5)))
Known 909a7.. : ∀ x0 . EquivReln x0 ⟶ ∀ x1 : ι → ο . (∀ x2 . ∀ x3 : ι → ι → ο . (∀ x4 . x4 ∈ x2 ⟶ x3 x4 x4) ⟶ (∀ x4 . x4 ∈ x2 ⟶ ∀ x5 . x5 ∈ x2 ⟶ x3 x4 x5 ⟶ x3 x5 x4) ⟶ (∀ x4 . x4 ∈ x2 ⟶ ∀ x5 . x5 ∈ x2 ⟶ ∀ x6 . x6 ∈ x2 ⟶ x3 x4 x5 ⟶ x3 x5 x6 ⟶ x3 x4 x6) ⟶ x1 (pack_r x2 x3)) ⟶ x1 x0
Known 517b3.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2 ∈ x0 ⟶ x1 x2 x2) ⟶ (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2) ⟶ (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x4 ⟶ x1 x2 x4) ⟶ EquivReln (pack_r x0 x1)
Theorem ec184..^{MetaCat_struct_r_equivreln_coproduct_constr} : ∀ x0 : ο . (∀ x1 : ι → ι → ι . (∀ x2 : ο . (∀ x3 : ι → ι → ι . (∀ x4 : ο . (∀ x5 : ι → ι → ι . (∀ x6 : ο . (∀ x7 : ι → ι → ι → ι → ι → ι . MetaCat_coproduct_constr_p EquivReln BinRelnHom struct_id struct_comp x1 x3 x5 x7 ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4) ⟶ x2) ⟶ x2) ⟶ x0) ⟶ x0 (proof)
Definition IrreflexiveTransitiveReln^{struct_r_partialord} := λ x0 . and (struct_r x0) (unpack_r_o x0 (λ x1 . λ x2 : ι → ι → ο . and (∀ x3 . x3 ∈ x1 ⟶ not (x2 x3 x3)) (∀ x3 . x3 ∈ x1 ⟶ ∀ x4 . x4 ∈ x1 ⟶ ∀ x5 . x5 ∈ x1 ⟶ x2 x3 x4 ⟶ x2 x4 x5 ⟶ x2 x3 x5)))
Known af4aa.. : ∀ x0 . IrreflexiveTransitiveReln x0 ⟶ ∀ x1 : ι → ο . (∀ x2 . ∀ x3 : ι → ι → ο . (∀ x4 . x4 ∈ x2 ⟶ not (x3 x4 x4)) ⟶ (∀ x4 . x4 ∈ x2 ⟶ ∀ x5 . x5 ∈ x2 ⟶ ∀ x6 . x6 ∈ x2 ⟶ x3 x4 x5 ⟶ x3 x5 x6 ⟶ x3 x4 x6) ⟶ x1 (pack_r x2 x3)) ⟶ x1 x0
Known b25e7.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2 ∈ x0 ⟶ not (x1 x2 x2)) ⟶ (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x4 ⟶ x1 x2 x4) ⟶ IrreflexiveTransitiveReln (pack_r x0 x1)
Theorem 8a2ce..^{MetaCat_struct_r_partialord_coproduct_constr} : ∀ x0 : ο . (∀ x1 : ι → ι → ι . (∀ x2 : ο . (∀ x3 : ι → ι → ι . (∀ x4 : ο . (∀ x5 : ι → ι → ι . (∀ x6 : ο . (∀ x7 : ι → ι → ι → ι → ι → ι . MetaCat_coproduct_constr_p IrreflexiveTransitiveReln BinRelnHom struct_id struct_comp x1 x3 x5 x7 ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4) ⟶ x2) ⟶ x2) ⟶ x0) ⟶ x0 (proof)