Search for blocks/addresses/...

Proofgold Address

address
PUKcr8ESJ8jY6Sf9DsMiTB2sbGALorNbCLc
total
0
mg
-
conjpub
-
current assets
6864c../f5ca9.. bday: 11519 doc published by PrEBh..
Param unpack_r_iunpack_r_i : ι(ι(ιιο) → ι) → ι
Param pack_rpack_r : ι(ιιο) → ι
Param lamSigma : ι(ιι) → ι
Definition setprodsetprod := λ x0 x1 . lam x0 (λ x2 . x1)
Definition andand := λ x0 x1 : ο . ∀ x2 : ο . (x0x1x2)x2
Param apap : ιιι
Param ordsuccordsucc : ιι
Definition BinReln_product := λ x0 x1 . unpack_r_i x0 (λ x2 . λ x3 : ι → ι → ο . unpack_r_i x1 (λ x4 . λ x5 : ι → ι → ο . pack_r (setprod x2 x4) (λ x6 x7 . and (x3 (ap x6 0) (ap x7 0)) (x5 (ap x6 1) (ap x7 1)))))
Definition iffiff := λ x0 x1 : ο . and (x0x1) (x1x0)
Known unpack_r_i_equnpack_r_i_eq : ∀ x0 : ι → (ι → ι → ο) → ι . ∀ x1 . ∀ x2 : ι → ι → ο . (∀ x3 : ι → ι → ο . (∀ x4 . x4x1∀ x5 . x5x1iff (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_extpack_r_ext : ∀ x0 . ∀ x1 x2 : ι → ι → ο . (∀ x3 . x3x0∀ x4 . x4x0iff (x1 x3 x4) (x2 x3 x4))pack_r x0 x1 = pack_r x0 x2
Known iffIiffI : ∀ x0 x1 : ο . (x0x1)(x1x0)iff x0 x1
Known andIandI : ∀ x0 x1 : ο . x0x1and x0 x1
Known ap0_Sigmaap0_Sigma : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2lam x0 x1ap x2 0x0
Known ap1_Sigmaap1_Sigma : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2lam x0 x1ap x2 1x1 (ap x2 0)
Theorem 433d4.. : ∀ x0 . ∀ x1 : ι → ι → ο . ∀ x2 . ∀ x3 x4 : ι → ι → ο . x4 (BinReln_product (pack_r x0 x1) (pack_r x2 x3)) (pack_r (setprod x0 x2) (λ x5 x6 . and (x1 (ap x5 0) (ap x6 0)) (x3 (ap x5 1) (ap x6 1))))x4 (pack_r (setprod x0 x2) (λ x5 x6 . and (x1 (ap x5 0) (ap x6 0)) (x3 (ap x5 1) (ap x6 1)))) (BinReln_product (pack_r x0 x1) (pack_r x2 x3)) (proof)
Definition struct_rstruct_r := λ x0 . ∀ x1 : ι → ο . (∀ x2 . ∀ x3 : ι → ι → ο . x1 (pack_r x2 x3))x1 x0
Known pack_struct_r_Ipack_struct_r_I : ∀ x0 . ∀ x1 : ι → ι → ο . struct_r (pack_r x0 x1)
Theorem 08ab7.. : ∀ x0 x1 . struct_r x0struct_r x1struct_r (BinReln_product x0 x1) (proof)
Definition MetaCat_product_pproduct_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 x11x1 x10 x5 x12and (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 x13x3 x10 x6 x4 x7 x13 = x11x3 x10 x6 x5 x8 x13 = x12x13 = x9 x10 x11 x12))
Definition MetaCat_product_constr_pproduct_constr_p := λ x0 : ι → ο . λ x1 : ι → ι → ι → ο . λ x2 : ι → ι . λ x3 : ι → ι → ι → ι → ι → ι . λ x4 x5 x6 : ι → ι → ι . λ x7 : ι → ι → ι → ι → ι → ι . ∀ x8 x9 . x0 x8x0 x9MetaCat_product_p x0 x1 x2 x3 x8 x9 (x4 x8 x9) (x5 x8 x9) (x6 x8 x9) (x7 x8 x9)
Param BinRelnHomHom_struct_r : ιιιο
Param struct_idstruct_id : ιι
Definition lam_complam_comp := λ x0 x1 x2 . lam x0 (λ x3 . ap x1 (ap x2 x3))
Definition struct_compstruct_comp := λ x0 x1 x2 . lam_comp (ap x0 0)
Param If_iIf_i : οιιι
Known and6Iand6I : ∀ x0 x1 x2 x3 x4 x5 : ο . x0x1x2x3x4x5and (and (and (and (and x0 x1) x2) x3) x4) x5
Known pack_r_0_eq2pack_r_0_eq2 : ∀ x0 . ∀ x1 x2 : ι → ι → ο . x2 x0 (ap (pack_r x0 x1) 0)x2 (ap (pack_r x0 x1) 0) x0
Known and3Iand3I : ∀ x0 x1 x2 : ο . x0x1x2and (and x0 x1) x2
Param PiPi : ι(ιι) → ι
Definition setexpsetexp := λ x0 x1 . Pi x1 (λ x2 . x0)
Known c84ab..Hom_struct_r_pack : ∀ x0 x1 . ∀ x2 x3 : ι → ι → ο . ∀ x4 . BinRelnHom (pack_r x0 x2) (pack_r x1 x3) x4 = and (x4setexp x1 x0) (∀ x6 . x6x0∀ x7 . x7x0x2 x6 x7x3 (ap x4 x6) (ap x4 x7))
Known lam_Pilam_Pi : ∀ x0 . ∀ x1 x2 : ι → ι . (∀ x3 . x3x0x2 x3x1 x3)lam x0 x2Pi x0 x1
Known betabeta : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2x0ap (lam x0 x1) x2 = x1 x2
Known and4Iand4I : ∀ x0 x1 x2 x3 : ο . x0x1x2x3and (and (and x0 x1) x2) x3
Known encode_u_extencode_u_ext : ∀ x0 . ∀ x1 x2 : ι → ι . (∀ x3 . x3x0x1 x3 = x2 x3)lam x0 x1 = lam x0 x2
Known ap_Piap_Pi : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 x3 . x2Pi x0 x1x3x0ap x2 x3x1 x3
Known Pi_etaPi_eta : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2Pi x0 x1lam x0 (ap x2) = x2
Known tuple_Sigma_etatuple_Sigma_eta : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2lam x0 x1lam 2 (λ x4 . If_i (x4 = 0) (ap x2 0) (ap x2 1)) = x2
Known tuple_2_1_eqtuple_2_1_eq : ∀ x0 x1 . ap (lam 2 (λ x3 . If_i (x3 = 0) x0 x1)) 1 = x1
Known tuple_2_0_eqtuple_2_0_eq : ∀ x0 x1 . ap (lam 2 (λ x3 . If_i (x3 = 0) x0 x1)) 0 = x0
Known tuple_2_Sigmatuple_2_Sigma : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2x0∀ x3 . x3x1 x2lam 2 (λ x4 . If_i (x4 = 0) x2 x3)lam x0 x1
Theorem 10126.. : ∀ x0 : ι → ο . (∀ x1 . x0 x1struct_r x1)(∀ x1 x2 . x0 x1x0 x2x0 (BinReln_product x1 x2))MetaCat_product_constr_p x0 BinRelnHom struct_id struct_comp BinReln_product (λ 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 060a4.. : MetaCat_product_constr_p struct_r BinRelnHom struct_id struct_comp BinReln_product (λ 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 ece68..MetaCat_struct_r_product_constr : ∀ x0 : ο . (∀ x1 : ι → ι → ι . (∀ x2 : ο . (∀ x3 : ι → ι → ι . (∀ x4 : ο . (∀ x5 : ι → ι → ι . (∀ x6 : ο . (∀ x7 : ι → ι → ι → ι → ι → ι . MetaCat_product_constr_p struct_r BinRelnHom struct_id struct_comp x1 x3 x5 x7x6)x6)x4)x4)x2)x2)x0)x0 (proof)
Definition BinReln_exp := λ x0 x1 . unpack_r_i x0 (λ x2 . λ x3 : ι → ι → ο . unpack_r_i x1 (λ x4 . λ x5 : ι → ι → ο . pack_r (setexp x4 x2) (λ x6 x7 . ∀ x8 . x8x2∀ x9 . x9x2x3 x8 x9x5 (ap x6 x8) (ap x7 x9))))
Theorem 5ade7.. : ∀ x0 . ∀ x1 : ι → ι → ο . ∀ x2 . ∀ x3 x4 : ι → ι → ο . x4 (BinReln_exp (pack_r x0 x1) (pack_r x2 x3)) (pack_r (setexp x2 x0) (λ x5 x6 . ∀ x7 . x7x0∀ x8 . x8x0x1 x7 x8x3 (ap x5 x7) (ap x6 x8)))x4 (pack_r (setexp x2 x0) (λ x5 x6 . ∀ x7 . x7x0∀ x8 . x8x0x1 x7 x8x3 (ap x5 x7) (ap x6 x8))) (BinReln_exp (pack_r x0 x1) (pack_r x2 x3)) (proof)
Theorem 89edf.. : ∀ x0 x1 . struct_r x0struct_r x1struct_r (BinReln_exp x0 x1) (proof)
Definition MetaCat_exp_pexponent_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 x14and (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 x15x3 (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)) = x14x15 = x12 x13 x14))
Definition MetaCat_exp_constr_pproduct_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 x11x0 x12MetaCat_exp_p x0 x1 x2 x3 x4 x5 x6 x7 x11 x12 (x8 x11 x12) (x9 x11 x12) (x10 x11 x12))
Known and5Iand5I : ∀ x0 x1 x2 x3 x4 : ο . x0x1x2x3x4and (and (and (and x0 x1) x2) x3) x4
Known tuple_2_setprodtuple_2_setprod : ∀ x0 x1 x2 . x2x0∀ x3 . x3x1lam 2 (λ x4 . If_i (x4 = 0) x2 x3)setprod x0 x1
Theorem 2450d.. : ∀ x0 : ι → ο . (∀ x1 . x0 x1struct_r x1)(∀ x1 x2 . x0 x1x0 x2x0 (BinReln_product x1 x2))(∀ x1 x2 . x0 x1x0 x2x0 (BinReln_exp x1 x2))MetaCat_exp_constr_p x0 BinRelnHom struct_id struct_comp BinReln_product (λ 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)))) BinReln_exp (λ 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 4f1fe.. : MetaCat_exp_constr_p struct_r BinRelnHom struct_id struct_comp BinReln_product (λ 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)))) BinReln_exp (λ 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 7f417..MetaCat_struct_r_product_exponent : ∀ x0 : ο . (∀ x1 : ι → ι → ι . (∀ x2 : ο . (∀ x3 : ι → ι → ι . (∀ x4 : ο . (∀ x5 : ι → ι → ι . (∀ x6 : ο . (∀ x7 : ι → ι → ι → ι → ι → ι . (∀ x8 : ο . (∀ x9 : ι → ι → ι . (∀ x10 : ο . (∀ x11 : ι → ι → ι . (∀ x12 : ο . (∀ x13 : ι → ι → ι → ι → ι . MetaCat_exp_constr_p struct_r BinRelnHom struct_id struct_comp x1 x3 x5 x7 x9 x11 x13x12)x12)x10)x10)x8)x8)x6)x6)x4)x4)x2)x2)x0)x0 (proof)
Param unpack_r_ounpack_r_o : ι(ι(ιιο) → ο) → ο
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0False
Definition IrreflexiveSymmetricRelnstruct_r_graph := λ x0 . and (struct_r x0) (unpack_r_o x0 (λ x1 . λ x2 : ι → ι → ο . and (∀ x3 . x3x1not (x2 x3 x3)) (∀ x3 . x3x1∀ x4 . x4x1x2 x3 x4x2 x4 x3)))
Known 5344f.. : ∀ x0 . ∀ x1 : ι → ι → ο . unpack_r_o (pack_r x0 x1) (λ x3 . λ x4 : ι → ι → ο . and (∀ x5 . x5x3not (x4 x5 x5)) (∀ x5 . x5x3∀ x6 . x6x3x4 x5 x6x4 x6 x5)) = and (∀ x3 . x3x0not (x1 x3 x3)) (∀ x3 . x3x0∀ x4 . x4x0x1 x3 x4x1 x4 x3)
Known 36176.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0not (x1 x2 x2))(∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)IrreflexiveSymmetricReln (pack_r x0 x1)
Theorem 96ca7.. : ∀ x0 . IrreflexiveSymmetricReln x0∀ x1 : ι → ο . (∀ x2 . ∀ x3 : ι → ι → ο . (∀ x4 . x4x2not (x3 x4 x4))(∀ x4 . x4x2∀ x5 . x5x2x3 x4 x5x3 x5 x4)x1 (pack_r x2 x3))x1 x0 (proof)
Theorem e7d0d.. : ∀ x0 . IrreflexiveSymmetricReln x0struct_r x0 (proof)
Theorem 49c4f.. : ∀ x0 x1 . IrreflexiveSymmetricReln x0IrreflexiveSymmetricReln x1IrreflexiveSymmetricReln (BinReln_product x0 x1) (proof)
Theorem 709ef..MetaCat_struct_r_graph_product_constr : ∀ x0 : ο . (∀ x1 : ι → ι → ι . (∀ x2 : ο . (∀ x3 : ι → ι → ι . (∀ x4 : ο . (∀ x5 : ι → ι → ι . (∀ x6 : ο . (∀ x7 : ι → ι → ι → ι → ι → ι . MetaCat_product_constr_p IrreflexiveSymmetricReln BinRelnHom struct_id struct_comp x1 x3 x5 x7x6)x6)x4)x4)x2)x2)x0)x0 (proof)
Definition PERstruct_r_per := λ x0 . and (struct_r x0) (unpack_r_o x0 (λ x1 . λ x2 : ι → ι → ο . and (∀ x3 . x3x1∀ x4 . x4x1x2 x3 x4x2 x4 x3) (∀ x3 . x3x1∀ x4 . x4x1∀ x5 . x5x1x2 x3 x4x2 x4 x5x2 x3 x5)))
Known a3466.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)(∀ x2 . x2x0∀ x3 . x3x0∀ x4 . x4x0x1 x2 x3x1 x3 x4x1 x2 x4)PER (pack_r x0 x1)
Known 0bd5c.. : ∀ x0 . PER x0∀ x1 : ι → ο . (∀ x2 . ∀ x3 : ι → ι → ο . (∀ x4 . x4x2∀ x5 . x5x2x3 x4 x5x3 x5 x4)(∀ x4 . x4x2∀ x5 . x5x2∀ x6 . x6x2x3 x4 x5x3 x5 x6x3 x4 x6)x1 (pack_r x2 x3))x1 x0
Theorem 1b5dd.. : ∀ x0 . PER x0struct_r x0 (proof)
Theorem a9f70.. : ∀ x0 x1 . PER x0PER x1PER (BinReln_product x0 x1) (proof)
Theorem b370d..MetaCat_struct_r_per_product_constr : ∀ x0 : ο . (∀ x1 : ι → ι → ι . (∀ x2 : ο . (∀ x3 : ι → ι → ι . (∀ x4 : ο . (∀ x5 : ι → ι → ι . (∀ x6 : ο . (∀ x7 : ι → ι → ι → ι → ι → ι . MetaCat_product_constr_p PER BinRelnHom struct_id struct_comp x1 x3 x5 x7x6)x6)x4)x4)x2)x2)x0)x0 (proof)
Theorem 310d5.. : ∀ x0 x1 . PER x0PER x1PER (BinReln_exp x0 x1) (proof)
Theorem 97ee8..MetaCat_struct_r_per_product_exponent : ∀ x0 : ο . (∀ x1 : ι → ι → ι . (∀ x2 : ο . (∀ x3 : ι → ι → ι . (∀ x4 : ο . (∀ x5 : ι → ι → ι . (∀ x6 : ο . (∀ x7 : ι → ι → ι → ι → ι → ι . (∀ x8 : ο . (∀ x9 : ι → ι → ι . (∀ x10 : ο . (∀ x11 : ι → ι → ι . (∀ x12 : ο . (∀ x13 : ι → ι → ι → ι → ι . MetaCat_exp_constr_p PER BinRelnHom struct_id struct_comp x1 x3 x5 x7 x9 x11 x13x12)x12)x10)x10)x8)x8)x6)x6)x4)x4)x2)x2)x0)x0 (proof)
Definition EquivRelnstruct_r_equivreln := λ x0 . and (struct_r x0) (unpack_r_o x0 (λ x1 . λ x2 : ι → ι → ο . and (and (∀ x3 . x3x1x2 x3 x3) (∀ x3 . x3x1∀ x4 . x4x1x2 x3 x4x2 x4 x3)) (∀ x3 . x3x1∀ x4 . x4x1∀ x5 . x5x1x2 x3 x4x2 x4 x5x2 x3 x5)))
Known 517b3.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0x1 x2 x2)(∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)(∀ x2 . x2x0∀ x3 . x3x0∀ x4 . x4x0x1 x2 x3x1 x3 x4x1 x2 x4)EquivReln (pack_r x0 x1)
Known 909a7.. : ∀ x0 . EquivReln x0∀ x1 : ι → ο . (∀ x2 . ∀ x3 : ι → ι → ο . (∀ x4 . x4x2x3 x4 x4)(∀ x4 . x4x2∀ x5 . x5x2x3 x4 x5x3 x5 x4)(∀ x4 . x4x2∀ x5 . x5x2∀ x6 . x6x2x3 x4 x5x3 x5 x6x3 x4 x6)x1 (pack_r x2 x3))x1 x0
Theorem 2effc.. : ∀ x0 . EquivReln x0struct_r x0 (proof)
Theorem 7da0d.. : ∀ x0 x1 . EquivReln x0EquivReln x1EquivReln (BinReln_product x0 x1) (proof)
Theorem 4d1df..MetaCat_struct_r_equivreln_product_constr : ∀ x0 : ο . (∀ x1 : ι → ι → ι . (∀ x2 : ο . (∀ x3 : ι → ι → ι . (∀ x4 : ο . (∀ x5 : ι → ι → ι . (∀ x6 : ο . (∀ x7 : ι → ι → ι → ι → ι → ι . MetaCat_product_constr_p EquivReln BinRelnHom struct_id struct_comp x1 x3 x5 x7x6)x6)x4)x4)x2)x2)x0)x0 (proof)
Definition IrreflexiveTransitiveRelnstruct_r_partialord := λ x0 . and (struct_r x0) (unpack_r_o x0 (λ x1 . λ x2 : ι → ι → ο . and (∀ x3 . x3x1not (x2 x3 x3)) (∀ x3 . x3x1∀ x4 . x4x1∀ x5 . x5x1x2 x3 x4x2 x4 x5x2 x3 x5)))
Known b25e7.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0not (x1 x2 x2))(∀ x2 . x2x0∀ x3 . x3x0∀ x4 . x4x0x1 x2 x3x1 x3 x4x1 x2 x4)IrreflexiveTransitiveReln (pack_r x0 x1)
Known af4aa.. : ∀ x0 . IrreflexiveTransitiveReln x0∀ x1 : ι → ο . (∀ x2 . ∀ x3 : ι → ι → ο . (∀ x4 . x4x2not (x3 x4 x4))(∀ x4 . x4x2∀ x5 . x5x2∀ x6 . x6x2x3 x4 x5x3 x5 x6x3 x4 x6)x1 (pack_r x2 x3))x1 x0
Theorem 294e6.. : ∀ x0 . IrreflexiveTransitiveReln x0struct_r x0 (proof)
Theorem e27aa.. : ∀ x0 x1 . IrreflexiveTransitiveReln x0IrreflexiveTransitiveReln x1IrreflexiveTransitiveReln (BinReln_product x0 x1) (proof)
Theorem 42715..MetaCat_struct_r_partialord_product_constr : ∀ x0 : ο . (∀ x1 : ι → ι → ι . (∀ x2 : ο . (∀ x3 : ι → ι → ι . (∀ x4 : ο . (∀ x5 : ι → ι → ι . (∀ x6 : ο . (∀ x7 : ι → ι → ι → ι → ι → ι . MetaCat_product_constr_p IrreflexiveTransitiveReln BinRelnHom struct_id struct_comp x1 x3 x5 x7x6)x6)x4)x4)x2)x2)x0)x0 (proof)

previous assets