Search for blocks/addresses/...

Proofgold Asset

asset id
66eb4a1903985f0d86c1002238feb0a1c35aa2ea669e549c2f95ab02cc1fb7d8
asset hash
2562a361cfd291ffb7293bba6d6ab12e1c65537171571e88760bb1d0cbccfec3
bday / block
11551
tx
6c47c..
preasset
doc published by PrEBh..
Param unpack_r_iunpack_r_i : ι(ι(ιιο) → ι) → ι
Param pack_rpack_r : ι(ιιο) → ι
Param SepSep : ι(ιο) → ι
Param apap : ιιι
Definition 05907.. := λ x0 x1 x2 x3 . unpack_r_i x0 (λ x4 . pack_r {x5 ∈ x4|ap x2 x5 = ap x3 x5})
Definition andand := λ x0 x1 : ο . ∀ x2 : ο . (x0x1x2)x2
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 SepE1SepE1 : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . x2Sep x0 x1x2x0
Known iffIiffI : ∀ x0 x1 : ο . (x0x1)(x1x0)iff x0 x1
Theorem 08d58.. : ∀ x0 . ∀ x1 : ι → ι → ο . ∀ x2 x3 x4 . 05907.. (pack_r x0 x1) x2 x3 x4 = pack_r {x6 ∈ x0|ap x3 x6 = ap x4 x6} x1 (proof)
Definition struct_rstruct_r := λ x0 . ∀ x1 : ι → ο . (∀ x2 . ∀ x3 : ι → ι → ο . x1 (pack_r x2 x3))x1 x0
Param BinRelnHomHom_struct_r : ιιιο
Definition MetaCat_equalizer_pequalizer_p := λ x0 : ι → ο . λ x1 : ι → ι → ι → ο . λ x2 : ι → ι . λ x3 : ι → ι → ι → ι → ι → ι . λ x4 x5 x6 x7 x8 x9 . λ x10 : ι → ι → ι . and (and (and (and (and (and (and (x0 x4) (x0 x5)) (x1 x4 x5 x6)) (x1 x4 x5 x7)) (x0 x8)) (x1 x8 x4 x9)) (x3 x8 x4 x5 x6 x9 = x3 x8 x4 x5 x7 x9)) (∀ x11 . x0 x11∀ x12 . x1 x11 x4 x12x3 x11 x4 x5 x6 x12 = x3 x11 x4 x5 x7 x12and (and (x1 x11 x8 (x10 x11 x12)) (x3 x11 x8 x4 x9 (x10 x11 x12) = x12)) (∀ x13 . x1 x11 x8 x13x3 x11 x8 x4 x9 x13 = x12x13 = x10 x11 x12))
Definition MetaCat_equalizer_struct_pequalizer_constr_p := λ x0 : ι → ο . λ x1 : ι → ι → ι → ο . λ x2 : ι → ι . λ x3 : ι → ι → ι → ι → ι → ι . λ x4 x5 : ι → ι → ι → ι → ι . λ x6 : ι → ι → ι → ι → ι → ι → ι . ∀ x7 x8 . x0 x7x0 x8∀ x9 x10 . x1 x7 x8 x9x1 x7 x8 x10MetaCat_equalizer_p x0 x1 x2 x3 x7 x8 x9 x10 (x4 x7 x8 x9 x10) (x5 x7 x8 x9 x10) (x6 x7 x8 x9 x10)
Param struct_idstruct_id : ιι
Param lamSigma : ι(ιι) → ι
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)
Known 41253..and8I : ∀ x0 x1 x2 x3 x4 x5 x6 x7 : ο . x0x1x2x3x4x5x6x7and (and (and (and (and (and (and x0 x1) x2) x3) x4) x5) x6) x7
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 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 andIandI : ∀ x0 x1 : ο . x0x1and x0 x1
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 encode_u_extencode_u_ext : ∀ x0 . ∀ x1 x2 : ι → ι . (∀ x3 . x3x0x1 x3 = x2 x3)lam x0 x1 = lam x0 x2
Known SepE2SepE2 : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . x2Sep x0 x1x1 x2
Known and3Iand3I : ∀ x0 x1 x2 : ο . x0x1x2and (and x0 x1) x2
Known Pi_etaPi_eta : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2Pi x0 x1lam x0 (ap x2) = x2
Known ap_Piap_Pi : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 x3 . x2Pi x0 x1x3x0ap x2 x3x1 x3
Known SepISepI : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . x2x0x1 x2x2Sep x0 x1
Theorem 3d2c4.. : ∀ x0 : ι → ο . (∀ x1 . x0 x1struct_r x1)(∀ x1 x2 x3 x4 . x0 x1x0 x2BinRelnHom x1 x2 x3BinRelnHom x1 x2 x4x0 (05907.. x1 x2 x3 x4))∀ x1 : ο . (∀ x2 : ι → ι → ι → ι → ι . (∀ x3 : ο . (∀ x4 : ι → ι → ι → ι → ι . (∀ x5 : ο . (∀ x6 : ι → ι → ι → ι → ι → ι → ι . MetaCat_equalizer_struct_p x0 BinRelnHom struct_id struct_comp x2 x4 x6x5)x5)x3)x3)x1)x1 (proof)
Known pack_struct_r_Ipack_struct_r_I : ∀ x0 . ∀ x1 : ι → ι → ο . struct_r (pack_r x0 x1)
Theorem 1d8ba..MetaCat_struct_r_equalizer_constr : ∀ x0 : ο . (∀ x1 : ι → ι → ι → ι → ι . (∀ x2 : ο . (∀ x3 : ι → ι → ι → ι → ι . (∀ x4 : ο . (∀ x5 : ι → ι → ι → ι → ι → ι → ι . MetaCat_equalizer_struct_p struct_r BinRelnHom struct_id struct_comp x1 x3 x5x4)x4)x2)x2)x0)x0 (proof)
Param MetaCatMetaCat : (ιο) → (ιιιο) → (ιι) → (ιιιιιι) → ο
Known 6955f..MetaCat_struct_r : MetaCat struct_r BinRelnHom struct_id struct_comp
Param MetaCat_pullback_struct_ppullback_constr_p : (ιο) → (ιιιο) → (ιι) → (ιιιιιι) → (ιιιιιι) → (ιιιιιι) → (ιιιιιι) → (ιιιιιιιιι) → ο
Param MetaCat_product_constr_pproduct_constr_p : (ιο) → (ιιιο) → (ιι) → (ιιιιιι) → (ιιι) → (ιιι) → (ιιι) → (ιιιιιι) → ο
Known ed2b0..product_equalizer_pullback_constr_ex : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι → ο . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ι → ι → ι → ι . MetaCat x0 x1 x2 x3(∀ x4 : ο . (∀ x5 : ι → ι → ι → ι → ι . (∀ x6 : ο . (∀ x7 : ι → ι → ι → ι → ι . (∀ x8 : ο . (∀ x9 : ι → ι → ι → ι → ι → ι → ι . MetaCat_equalizer_struct_p x0 x1 x2 x3 x5 x7 x9x8)x8)x6)x6)x4)x4)(∀ x4 : ο . (∀ x5 : ι → ι → ι . (∀ x6 : ο . (∀ x7 : ι → ι → ι . (∀ x8 : ο . (∀ x9 : ι → ι → ι . (∀ x10 : ο . (∀ x11 : ι → ι → ι → ι → ι → ι . MetaCat_product_constr_p x0 x1 x2 x3 x5 x7 x9 x11x10)x10)x8)x8)x6)x6)x4)x4)∀ x4 : ο . (∀ x5 : ι → ι → ι → ι → ι → ι . (∀ x6 : ο . (∀ x7 : ι → ι → ι → ι → ι → ι . (∀ x8 : ο . (∀ x9 : ι → ι → ι → ι → ι → ι . (∀ x10 : ο . (∀ x11 : ι → ι → ι → ι → ι → ι → ι → ι → ι . MetaCat_pullback_struct_p x0 x1 x2 x3 x5 x7 x9 x11x10)x10)x8)x8)x6)x6)x4)x4
Known 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
Theorem 97f16..MetaCat_struct_r_pullback_constr : ∀ x0 : ο . (∀ x1 : ι → ι → ι → ι → ι → ι . (∀ x2 : ο . (∀ x3 : ι → ι → ι → ι → ι → ι . (∀ x4 : ο . (∀ x5 : ι → ι → ι → ι → ι → ι . (∀ x6 : ο . (∀ x7 : ι → ι → ι → ι → ι → ι → ι → ι → ι . MetaCat_pullback_struct_p struct_r BinRelnHom struct_id struct_comp x1 x3 x5 x7x6)x6)x4)x4)x2)x2)x0)x0 (proof)
Param unpack_r_ounpack_r_o : ι(ι(ιιο) → ο) → ο
Param notnot : οο
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 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
Known 36176.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0not (x1 x2 x2))(∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)IrreflexiveSymmetricReln (pack_r x0 x1)
Theorem 06b27..MetaCat_struct_r_graph_equalizer_constr : ∀ x0 : ο . (∀ x1 : ι → ι → ι → ι → ι . (∀ x2 : ο . (∀ x3 : ι → ι → ι → ι → ι . (∀ x4 : ο . (∀ x5 : ι → ι → ι → ι → ι → ι → ι . MetaCat_equalizer_struct_p IrreflexiveSymmetricReln BinRelnHom struct_id struct_comp x1 x3 x5x4)x4)x2)x2)x0)x0 (proof)
Known 71675..MetaCat_struct_r_graph : MetaCat IrreflexiveSymmetricReln BinRelnHom struct_id struct_comp
Known 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
Theorem c2d12..MetaCat_struct_r_graph_pullback_constr : ∀ x0 : ο . (∀ x1 : ι → ι → ι → ι → ι → ι . (∀ x2 : ο . (∀ x3 : ι → ι → ι → ι → ι → ι . (∀ x4 : ο . (∀ x5 : ι → ι → ι → ι → ι → ι . (∀ x6 : ο . (∀ x7 : ι → ι → ι → ι → ι → ι → ι → ι → ι . MetaCat_pullback_struct_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 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
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)
Theorem 57f50..MetaCat_struct_r_per_equalizer_constr : ∀ x0 : ο . (∀ x1 : ι → ι → ι → ι → ι . (∀ x2 : ο . (∀ x3 : ι → ι → ι → ι → ι . (∀ x4 : ο . (∀ x5 : ι → ι → ι → ι → ι → ι → ι . MetaCat_equalizer_struct_p PER BinRelnHom struct_id struct_comp x1 x3 x5x4)x4)x2)x2)x0)x0 (proof)
Known 259fb..MetaCat_struct_r_per : MetaCat PER BinRelnHom struct_id struct_comp
Known 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
Theorem 44067..MetaCat_struct_r_per_pullback_constr : ∀ x0 : ο . (∀ x1 : ι → ι → ι → ι → ι → ι . (∀ x2 : ο . (∀ x3 : ι → ι → ι → ι → ι → ι . (∀ x4 : ο . (∀ x5 : ι → ι → ι → ι → ι → ι . (∀ x6 : ο . (∀ x7 : ι → ι → ι → ι → ι → ι → ι → ι → ι . MetaCat_pullback_struct_p PER BinRelnHom struct_id struct_comp x1 x3 x5 x7x6)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 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
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)
Theorem 99d06..MetaCat_struct_r_equivreln_equalizer_constr : ∀ x0 : ο . (∀ x1 : ι → ι → ι → ι → ι . (∀ x2 : ο . (∀ x3 : ι → ι → ι → ι → ι . (∀ x4 : ο . (∀ x5 : ι → ι → ι → ι → ι → ι → ι . MetaCat_equalizer_struct_p EquivReln BinRelnHom struct_id struct_comp x1 x3 x5x4)x4)x2)x2)x0)x0 (proof)
Known ca919..MetaCat_struct_r_equivreln : MetaCat EquivReln BinRelnHom struct_id struct_comp
Known 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
Theorem e7f7d..MetaCat_struct_r_equivreln_pullback_constr : ∀ x0 : ο . (∀ x1 : ι → ι → ι → ι → ι → ι . (∀ x2 : ο . (∀ x3 : ι → ι → ι → ι → ι → ι . (∀ x4 : ο . (∀ x5 : ι → ι → ι → ι → ι → ι . (∀ x6 : ο . (∀ x7 : ι → ι → ι → ι → ι → ι → ι → ι → ι . MetaCat_pullback_struct_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 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
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)
Theorem 3d0dd..MetaCat_struct_r_partialord_equalizer_constr : ∀ x0 : ο . (∀ x1 : ι → ι → ι → ι → ι . (∀ x2 : ο . (∀ x3 : ι → ι → ι → ι → ι . (∀ x4 : ο . (∀ x5 : ι → ι → ι → ι → ι → ι → ι . MetaCat_equalizer_struct_p IrreflexiveTransitiveReln BinRelnHom struct_id struct_comp x1 x3 x5x4)x4)x2)x2)x0)x0 (proof)
Known c6620..MetaCat_struct_r_partialord : MetaCat IrreflexiveTransitiveReln BinRelnHom struct_id struct_comp
Known 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
Theorem d1a34..MetaCat_struct_r_partialord_pullback_constr : ∀ x0 : ο . (∀ x1 : ι → ι → ι → ι → ι → ι . (∀ x2 : ο . (∀ x3 : ι → ι → ι → ι → ι → ι . (∀ x4 : ο . (∀ x5 : ι → ι → ι → ι → ι → ι . (∀ x6 : ο . (∀ x7 : ι → ι → ι → ι → ι → ι → ι → ι → ι . MetaCat_pullback_struct_p IrreflexiveTransitiveReln BinRelnHom struct_id struct_comp x1 x3 x5 x7x6)x6)x4)x4)x2)x2)x0)x0 (proof)