:: CATALG_1 semantic presentation begin definitionlet "I" be ($#m1_hidden :::"set"::: ) ; let "A", "f" be ($#m1_hidden :::"Function":::); func "f" :::"-MSF"::: "(" "I" "," "A" ")" -> ($#m1_hidden :::"ManySortedFunction":::) "of" "I" means :: CATALG_1:def 1 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) "I")) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set "f" ($#k5_relat_1 :::"|"::: ) (Set "(" "A" ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" )))); end; :: deftheorem defines :::"-MSF"::: CATALG_1:def 1 : (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "b4")) "being" ($#m1_hidden :::"ManySortedFunction":::) "of" (Set (Var "I")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_catalg_1 :::"-MSF"::: ) "(" (Set (Var "I")) "," (Set (Var "A")) ")" )) "iff" (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set (Var "I")))) "holds" (Bool (Set (Set (Var "b4")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k5_relat_1 :::"|"::: ) (Set "(" (Set (Var "A")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" )))) ")" )))); theorem :: CATALG_1:1 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool (Set (Set "(" ($#k6_partfun1 :::"id"::: ) (Set "(" ($#k3_card_3 :::"Union"::: ) (Set (Var "A")) ")" ) ")" ) ($#k1_catalg_1 :::"-MSF"::: ) "(" (Set (Var "I")) "," (Set (Var "A")) ")" ) ($#r6_pboole :::"="::: ) (Set ($#k2_msualg_3 :::"id"::: ) (Set (Var "A")))))) ; theorem :: CATALG_1:2 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set ($#k3_funct_6 :::"rngs"::: ) (Set "(" (Set (Var "f")) ($#k1_catalg_1 :::"-MSF"::: ) "(" (Set (Var "I")) "," (Set (Var "A")) ")" ")" )) ($#r2_pboole :::"c="::: ) (Set (Var "B")))) "holds" (Bool (Set (Set "(" (Set (Var "g")) ($#k3_relat_1 :::"*"::: ) (Set (Var "f")) ")" ) ($#k1_catalg_1 :::"-MSF"::: ) "(" (Set (Var "I")) "," (Set (Var "A")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "g")) ($#k1_catalg_1 :::"-MSF"::: ) "(" (Set (Var "I")) "," (Set (Var "B")) ")" ")" ) ($#k8_pboole :::"**"::: ) (Set "(" (Set (Var "f")) ($#k1_catalg_1 :::"-MSF"::: ) "(" (Set (Var "I")) "," (Set (Var "A")) ")" ")" )))))) ; theorem :: CATALG_1:3 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set (Var "I")))) "holds" (Bool "(" (Bool (Set (Set (Var "A")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_tarski :::"c="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Set (Var "f")) ($#k7_relat_1 :::".:"::: ) (Set "(" (Set (Var "A")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set (Var "B")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) ")" ) ")" )) "holds" (Bool (Set (Set (Var "f")) ($#k1_catalg_1 :::"-MSF"::: ) "(" (Set (Var "I")) "," (Set (Var "A")) ")" ) "is" ($#m2_pboole :::"ManySortedFunction"::: ) "of" (Set (Var "A")) "," (Set (Var "B")))))) ; definitionlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; let "A" be ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Const "S")); attr "A" is :::"empty"::: means :: CATALG_1:def 2 (Bool (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" "A") "is" bbbadV3_RELAT_1()); end; :: deftheorem defines :::"empty"::: CATALG_1:def 2 : (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "A")) "being" ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v1_catalg_1 :::"empty"::: ) ) "iff" (Bool (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "A"))) "is" bbbadV3_RELAT_1()) ")" ))); registrationlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; cluster ($#v4_msualg_1 :::"non-empty"::: ) -> ($#~v1_catalg_1 "non" ($#v1_catalg_1 :::"empty"::: ) ) for ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" "S"; end; registrationlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; cluster ($#v3_msualg_1 :::"strict"::: ) ($#v4_msualg_1 :::"non-empty"::: ) ($#v1_msafree1 :::"disjoint_valued"::: ) for ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" "S"; end; registrationlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; let "A" be ($#~v1_catalg_1 "non" ($#v1_catalg_1 :::"empty"::: ) ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Const "S")); cluster (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" "A") -> bbbadV3_RELAT_1() ; end; registration cluster ($#v1_relat_1 :::"Relation-like"::: ) ($#~v3_relat_1 "non" ($#v3_relat_1 :::"empty-yielding"::: ) ) ($#v1_funct_1 :::"Function-like"::: ) for ($#m1_hidden :::"set"::: ) ; end; begin definitionlet "A" be ($#m1_hidden :::"set"::: ) ; func :::"CatSign"::: "A" -> ($#v1_msualg_1 :::"strict"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) means :: CATALG_1:def 3 (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k1_tarski :::"}"::: ) ) "," (Set "(" (Num 2) ($#k4_finseq_2 :::"-tuples_on"::: ) "A" ")" ) ($#k2_zfmisc_1 :::":]"::: ) )) & (Bool (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_tarski :::"{"::: ) (Num 1) ($#k1_tarski :::"}"::: ) ) "," (Set "(" (Num 1) ($#k4_finseq_2 :::"-tuples_on"::: ) "A" ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_tarski :::"{"::: ) (Num 2) ($#k1_tarski :::"}"::: ) ) "," (Set "(" (Num 3) ($#k4_finseq_2 :::"-tuples_on"::: ) "A" ")" ) ($#k2_zfmisc_1 :::":]"::: ) ))) & (Bool "(" "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) "A")) "holds" (Bool "(" (Bool (Set (Set "the" ($#u1_msualg_1 :::"Arity"::: ) "of" it) ($#k1_funct_1 :::"."::: ) (Set ($#k4_tarski :::"["::: ) (Num 1) "," (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "a")) ($#k9_finseq_1 :::"*>"::: ) ) ($#k4_tarski :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Set "the" ($#u2_msualg_1 :::"ResultSort"::: ) "of" it) ($#k1_funct_1 :::"."::: ) (Set ($#k4_tarski :::"["::: ) (Num 1) "," (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "a")) ($#k9_finseq_1 :::"*>"::: ) ) ($#k4_tarski :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "a")) "," (Set (Var "a")) ($#k10_finseq_1 :::"*>"::: ) ) ($#k4_tarski :::"]"::: ) )) ")" ) ")" ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) "A") & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) "A") & (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) "A")) "holds" (Bool "(" (Bool (Set (Set "the" ($#u1_msualg_1 :::"Arity"::: ) "of" it) ($#k1_funct_1 :::"."::: ) (Set ($#k4_tarski :::"["::: ) (Num 2) "," (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ($#k11_finseq_1 :::"*>"::: ) ) ($#k4_tarski :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "b")) "," (Set (Var "c")) ($#k10_finseq_1 :::"*>"::: ) ) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k10_finseq_1 :::"*>"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#k10_finseq_1 :::"*>"::: ) )) & (Bool (Set (Set "the" ($#u2_msualg_1 :::"ResultSort"::: ) "of" it) ($#k1_funct_1 :::"."::: ) (Set ($#k4_tarski :::"["::: ) (Num 2) "," (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ($#k11_finseq_1 :::"*>"::: ) ) ($#k4_tarski :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "a")) "," (Set (Var "c")) ($#k10_finseq_1 :::"*>"::: ) ) ($#k4_tarski :::"]"::: ) )) ")" ) ")" ) ")" ); end; :: deftheorem defines :::"CatSign"::: CATALG_1:def 3 : (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b2")) "being" ($#v1_msualg_1 :::"strict"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k2_catalg_1 :::"CatSign"::: ) (Set (Var "A")))) "iff" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k1_tarski :::"}"::: ) ) "," (Set "(" (Num 2) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Var "A")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) )) & (Bool (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_tarski :::"{"::: ) (Num 1) ($#k1_tarski :::"}"::: ) ) "," (Set "(" (Num 1) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Var "A")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_tarski :::"{"::: ) (Num 2) ($#k1_tarski :::"}"::: ) ) "," (Set "(" (Num 3) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Var "A")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ))) & (Bool "(" "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool "(" (Bool (Set (Set "the" ($#u1_msualg_1 :::"Arity"::: ) "of" (Set (Var "b2"))) ($#k1_funct_1 :::"."::: ) (Set ($#k4_tarski :::"["::: ) (Num 1) "," (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "a")) ($#k9_finseq_1 :::"*>"::: ) ) ($#k4_tarski :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Set "the" ($#u2_msualg_1 :::"ResultSort"::: ) "of" (Set (Var "b2"))) ($#k1_funct_1 :::"."::: ) (Set ($#k4_tarski :::"["::: ) (Num 1) "," (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "a")) ($#k9_finseq_1 :::"*>"::: ) ) ($#k4_tarski :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "a")) "," (Set (Var "a")) ($#k10_finseq_1 :::"*>"::: ) ) ($#k4_tarski :::"]"::: ) )) ")" ) ")" ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool "(" (Bool (Set (Set "the" ($#u1_msualg_1 :::"Arity"::: ) "of" (Set (Var "b2"))) ($#k1_funct_1 :::"."::: ) (Set ($#k4_tarski :::"["::: ) (Num 2) "," (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ($#k11_finseq_1 :::"*>"::: ) ) ($#k4_tarski :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "b")) "," (Set (Var "c")) ($#k10_finseq_1 :::"*>"::: ) ) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k10_finseq_1 :::"*>"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#k10_finseq_1 :::"*>"::: ) )) & (Bool (Set (Set "the" ($#u2_msualg_1 :::"ResultSort"::: ) "of" (Set (Var "b2"))) ($#k1_funct_1 :::"."::: ) (Set ($#k4_tarski :::"["::: ) (Num 2) "," (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ($#k11_finseq_1 :::"*>"::: ) ) ($#k4_tarski :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "a")) "," (Set (Var "c")) ($#k10_finseq_1 :::"*>"::: ) ) ($#k4_tarski :::"]"::: ) )) ")" ) ")" ) ")" ) ")" ))); registrationlet "A" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k2_catalg_1 :::"CatSign"::: ) "A") -> ($#v1_msualg_1 :::"strict"::: ) ($#v1_instalg1 :::"feasible"::: ) ; end; registrationlet "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k2_catalg_1 :::"CatSign"::: ) "A") -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v1_msualg_1 :::"strict"::: ) ; end; definitionmode Signature is ($#v1_instalg1 :::"feasible"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; end; definitionlet "S" be ($#l1_msualg_1 :::"Signature":::); attr "S" is :::"Categorial"::: means :: CATALG_1:def 4 (Bool "ex" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set ($#k2_catalg_1 :::"CatSign"::: ) (Set (Var "A"))) "is" ($#m1_instalg1 :::"Subsignature"::: ) "of" "S") & (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S") ($#r1_hidden :::"="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k1_tarski :::"}"::: ) ) "," (Set "(" (Num 2) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Var "A")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) )) ")" )); end; :: deftheorem defines :::"Categorial"::: CATALG_1:def 4 : (Bool "for" (Set (Var "S")) "being" ($#l1_msualg_1 :::"Signature":::) "holds" (Bool "(" (Bool (Set (Var "S")) "is" ($#v2_catalg_1 :::"Categorial"::: ) ) "iff" (Bool "ex" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set ($#k2_catalg_1 :::"CatSign"::: ) (Set (Var "A"))) "is" ($#m1_instalg1 :::"Subsignature"::: ) "of" (Set (Var "S"))) & (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) ($#r1_hidden :::"="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k1_tarski :::"}"::: ) ) "," (Set "(" (Num 2) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Var "A")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) )) ")" )) ")" )); registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_instalg1 :::"feasible"::: ) ($#v2_catalg_1 :::"Categorial"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) for ($#l1_msualg_1 :::"ManySortedSign"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_msualg_1 :::"strict"::: ) ($#v1_instalg1 :::"feasible"::: ) ($#v2_catalg_1 :::"Categorial"::: ) for ($#l1_msualg_1 :::"ManySortedSign"::: ) ; end; definitionmode CatSignature is ($#v2_catalg_1 :::"Categorial"::: ) ($#l1_msualg_1 :::"Signature":::); end; definitionlet "A" be ($#m1_hidden :::"set"::: ) ; mode :::"CatSignature"::: "of" "A" -> ($#l1_msualg_1 :::"Signature":::) means :: CATALG_1:def 5 (Bool "(" (Bool (Set ($#k2_catalg_1 :::"CatSign"::: ) "A") "is" ($#m1_instalg1 :::"Subsignature"::: ) "of" it) & (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k1_tarski :::"}"::: ) ) "," (Set "(" (Num 2) ($#k4_finseq_2 :::"-tuples_on"::: ) "A" ")" ) ($#k2_zfmisc_1 :::":]"::: ) )) ")" ); end; :: deftheorem defines :::"CatSignature"::: CATALG_1:def 5 : (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b2")) "being" ($#l1_msualg_1 :::"Signature":::) "holds" (Bool "(" (Bool (Set (Var "b2")) "is" ($#m1_catalg_1 :::"CatSignature"::: ) "of" (Set (Var "A"))) "iff" (Bool "(" (Bool (Set ($#k2_catalg_1 :::"CatSign"::: ) (Set (Var "A"))) "is" ($#m1_instalg1 :::"Subsignature"::: ) "of" (Set (Var "b2"))) & (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k1_tarski :::"}"::: ) ) "," (Set "(" (Num 2) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Var "A")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) )) ")" ) ")" ))); theorem :: CATALG_1:4 (Bool "for" (Set (Var "A1")) "," (Set (Var "A2")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_catalg_1 :::"CatSignature"::: ) "of" (Set (Var "A1")) "st" (Bool (Bool (Set (Var "S")) "is" ($#m1_catalg_1 :::"CatSignature"::: ) "of" (Set (Var "A2")))) "holds" (Bool (Set (Var "A1")) ($#r1_hidden :::"="::: ) (Set (Var "A2"))))) ; registrationlet "A" be ($#m1_hidden :::"set"::: ) ; cluster -> ($#v2_catalg_1 :::"Categorial"::: ) for ($#m1_catalg_1 :::"CatSignature"::: ) "of" "A"; end; registrationlet "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) for ($#m1_catalg_1 :::"CatSignature"::: ) "of" "A"; end; registrationlet "A" be ($#m1_hidden :::"set"::: ) ; cluster ($#v1_msualg_1 :::"strict"::: ) ($#v1_instalg1 :::"feasible"::: ) ($#v2_catalg_1 :::"Categorial"::: ) for ($#m1_catalg_1 :::"CatSignature"::: ) "of" "A"; end; definitionlet "A" be ($#m1_hidden :::"set"::: ) ; :: original: :::"CatSign"::: redefine func :::"CatSign"::: "A" -> ($#v1_msualg_1 :::"strict"::: ) ($#m1_catalg_1 :::"CatSignature"::: ) "of" "A"; end; definitionlet "S" be ($#l1_msualg_1 :::"ManySortedSign"::: ) ; func :::"underlay"::: "S" -> ($#m1_hidden :::"set"::: ) means :: CATALG_1:def 6 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "ex" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) (Bool "ex" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "st" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "f")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S") ($#k2_xboole_0 :::"\/"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "S"))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f")))) ")" ))) ")" )); end; :: deftheorem defines :::"underlay"::: CATALG_1:def 6 : (Bool "for" (Set (Var "S")) "being" ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "b2")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k4_catalg_1 :::"underlay"::: ) (Set (Var "S")))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "b2"))) "iff" (Bool "ex" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) (Bool "ex" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "st" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "f")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) ($#k2_xboole_0 :::"\/"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "S"))))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f")))) ")" ))) ")" )) ")" ))); theorem :: CATALG_1:5 (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k4_catalg_1 :::"underlay"::: ) (Set "(" ($#k3_catalg_1 :::"CatSign"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "A")))) ; definitionlet "S" be ($#l1_msualg_1 :::"ManySortedSign"::: ) ; attr "S" is :::"delta-concrete"::: means :: CATALG_1:def 7 (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool "(" "for" (Set (Var "s")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "s")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S"))) "holds" (Bool "ex" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) )(Bool "ex" (Set (Var "p")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool "(" (Bool (Set (Var "s")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "p")) ($#k4_tarski :::"]"::: ) )) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "i")))) & (Bool (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "i")) ($#k1_tarski :::"}"::: ) ) "," (Set "(" (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "i")) ")" ) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set "(" ($#k4_catalg_1 :::"underlay"::: ) "S" ")" ) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S")) ")" ))) ")" ) & (Bool "(" "for" (Set (Var "o")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "o")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "S"))) "holds" (Bool "ex" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) )(Bool "ex" (Set (Var "p")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool "(" (Bool (Set (Var "o")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "p")) ($#k4_tarski :::"]"::: ) )) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "i")))) & (Bool (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "i")) ($#k1_tarski :::"}"::: ) ) "," (Set "(" (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "i")) ")" ) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set "(" ($#k4_catalg_1 :::"underlay"::: ) "S" ")" ) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) ($#r1_tarski :::"c="::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "S")) ")" ))) ")" ) ")" )); end; :: deftheorem defines :::"delta-concrete"::: CATALG_1:def 7 : (Bool "for" (Set (Var "S")) "being" ($#l1_msualg_1 :::"ManySortedSign"::: ) "holds" (Bool "(" (Bool (Set (Var "S")) "is" ($#v3_catalg_1 :::"delta-concrete"::: ) ) "iff" (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool "(" "for" (Set (Var "s")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "s")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))))) "holds" (Bool "ex" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) )(Bool "ex" (Set (Var "p")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool "(" (Bool (Set (Var "s")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "p")) ($#k4_tarski :::"]"::: ) )) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "i")))) & (Bool (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "i")) ($#k1_tarski :::"}"::: ) ) "," (Set "(" (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "i")) ")" ) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set "(" ($#k4_catalg_1 :::"underlay"::: ) (Set (Var "S")) ")" ) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S")))) ")" ))) ")" ) & (Bool "(" "for" (Set (Var "o")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "o")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "S"))))) "holds" (Bool "ex" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) )(Bool "ex" (Set (Var "p")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool "(" (Bool (Set (Var "o")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "p")) ($#k4_tarski :::"]"::: ) )) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "i")))) & (Bool (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "i")) ($#k1_tarski :::"}"::: ) ) "," (Set "(" (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "i")) ")" ) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set "(" ($#k4_catalg_1 :::"underlay"::: ) (Set (Var "S")) ")" ) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) ($#r1_tarski :::"c="::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "S")))) ")" ))) ")" ) ")" )) ")" )); registrationlet "A" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k2_catalg_1 :::"CatSign"::: ) "A") -> ($#v1_msualg_1 :::"strict"::: ) ($#v3_catalg_1 :::"delta-concrete"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_msualg_1 :::"strict"::: ) ($#v1_instalg1 :::"feasible"::: ) ($#v2_catalg_1 :::"Categorial"::: ) ($#v3_catalg_1 :::"delta-concrete"::: ) for ($#l1_msualg_1 :::"ManySortedSign"::: ) ; let "A" be ($#m1_hidden :::"set"::: ) ; cluster ($#v1_msualg_1 :::"strict"::: ) ($#v1_instalg1 :::"feasible"::: ) ($#v2_catalg_1 :::"Categorial"::: ) ($#v3_catalg_1 :::"delta-concrete"::: ) for ($#m1_catalg_1 :::"CatSignature"::: ) "of" "A"; end; theorem :: CATALG_1:6 (Bool "for" (Set (Var "S")) "being" ($#v3_catalg_1 :::"delta-concrete"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S")))) "or" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "S")))) ")" )) "holds" (Bool "ex" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) )(Bool "ex" (Set (Var "p")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "p")) ($#k4_tarski :::"]"::: ) )) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "p"))) ($#r1_tarski :::"c="::: ) (Set ($#k4_catalg_1 :::"underlay"::: ) (Set (Var "S")))) ")" ))))) ; theorem :: CATALG_1:7 (Bool "for" (Set (Var "S")) "being" ($#v3_catalg_1 :::"delta-concrete"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool "(" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "p1")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S")))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "p2")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S")))) ")" ) "or" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "p1")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "S")))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "p2")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "S")))) ")" ) ")" )) "holds" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p2"))))))) ; theorem :: CATALG_1:8 (Bool "for" (Set (Var "S")) "being" ($#v3_catalg_1 :::"delta-concrete"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p2"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1")))) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "p2"))) ($#r1_tarski :::"c="::: ) (Set ($#k4_catalg_1 :::"underlay"::: ) (Set (Var "S"))))) "holds" (Bool "(" "(" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "p1")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))))) "implies" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "p2")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S")))) ")" & "(" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "p1")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "S"))))) "implies" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "p2")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "S")))) ")" ")" )))) ; theorem :: CATALG_1:9 (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_catalg_1 :::"Categorial"::: ) ($#v3_catalg_1 :::"delta-concrete"::: ) ($#l1_msualg_1 :::"Signature":::) "holds" (Bool (Set (Var "S")) "is" ($#m1_catalg_1 :::"CatSignature"::: ) "of" (Set ($#k4_catalg_1 :::"underlay"::: ) (Set (Var "S"))))) ; begin registrationlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"CatSignature":::); let "s" be ($#m1_subset_1 :::"SortSymbol":::) "of" (Set (Const "S")); cluster (Set "s" ($#k2_xtuple_0 :::"`2"::: ) ) -> ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_funct_1 :::"Function-like"::: ) ; end; registrationlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_catalg_1 :::"delta-concrete"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; let "s" be ($#m1_subset_1 :::"SortSymbol":::) "of" (Set (Const "S")); cluster (Set "s" ($#k2_xtuple_0 :::"`2"::: ) ) -> ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_funct_1 :::"Function-like"::: ) ; end; registrationlet "S" be ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v3_catalg_1 :::"delta-concrete"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; let "o" be ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Const "S"))); cluster (Set "o" ($#k2_xtuple_0 :::"`2"::: ) ) -> ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_funct_1 :::"Function-like"::: ) ; end; registrationlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"CatSignature":::); let "s" be ($#m1_subset_1 :::"SortSymbol":::) "of" (Set (Const "S")); cluster (Set "s" ($#k2_xtuple_0 :::"`2"::: ) ) -> ($#v1_finseq_1 :::"FinSequence-like"::: ) ; end; registrationlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_catalg_1 :::"delta-concrete"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; let "s" be ($#m1_subset_1 :::"SortSymbol":::) "of" (Set (Const "S")); cluster (Set "s" ($#k2_xtuple_0 :::"`2"::: ) ) -> ($#v1_finseq_1 :::"FinSequence-like"::: ) ; end; registrationlet "S" be ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v3_catalg_1 :::"delta-concrete"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; let "o" be ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Const "S"))); cluster (Set "o" ($#k2_xtuple_0 :::"`2"::: ) ) -> ($#v1_finseq_1 :::"FinSequence-like"::: ) ; end; definitionlet "a" be ($#m1_hidden :::"set"::: ) ; func :::"idsym"::: "a" -> ($#m1_hidden :::"set"::: ) equals :: CATALG_1:def 8 (Set ($#k4_tarski :::"["::: ) (Num 1) "," (Set ($#k9_finseq_1 :::"<*"::: ) "a" ($#k9_finseq_1 :::"*>"::: ) ) ($#k4_tarski :::"]"::: ) ); let "b" be ($#m1_hidden :::"set"::: ) ; func :::"homsym"::: "(" "a" "," "b" ")" -> ($#m1_hidden :::"set"::: ) equals :: CATALG_1:def 9 (Set ($#k4_tarski :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k10_finseq_1 :::"<*"::: ) "a" "," "b" ($#k10_finseq_1 :::"*>"::: ) ) ($#k4_tarski :::"]"::: ) ); let "c" be ($#m1_hidden :::"set"::: ) ; func :::"compsym"::: "(" "a" "," "b" "," "c" ")" -> ($#m1_hidden :::"set"::: ) equals :: CATALG_1:def 10 (Set ($#k4_tarski :::"["::: ) (Num 2) "," (Set ($#k11_finseq_1 :::"<*"::: ) "a" "," "b" "," "c" ($#k11_finseq_1 :::"*>"::: ) ) ($#k4_tarski :::"]"::: ) ); end; :: deftheorem defines :::"idsym"::: CATALG_1:def 8 : (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k5_catalg_1 :::"idsym"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Num 1) "," (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "a")) ($#k9_finseq_1 :::"*>"::: ) ) ($#k4_tarski :::"]"::: ) ))); :: deftheorem defines :::"homsym"::: CATALG_1:def 9 : (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k6_catalg_1 :::"homsym"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k10_finseq_1 :::"*>"::: ) ) ($#k4_tarski :::"]"::: ) ))); :: deftheorem defines :::"compsym"::: CATALG_1:def 10 : (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k7_catalg_1 :::"compsym"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Num 2) "," (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ($#k11_finseq_1 :::"*>"::: ) ) ($#k4_tarski :::"]"::: ) ))); theorem :: CATALG_1:10 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_catalg_1 :::"CatSignature"::: ) "of" (Set (Var "A")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) "holds" (Bool "(" (Bool (Set ($#k5_catalg_1 :::"idsym"::: ) (Set (Var "a"))) ($#r2_hidden :::"in"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "S")))) & (Bool "(" "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) "holds" (Bool "(" (Bool (Set ($#k6_catalg_1 :::"homsym"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S")))) & (Bool "(" "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) "holds" (Bool (Set ($#k7_catalg_1 :::"compsym"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "S")))) ")" ) ")" ) ")" ) ")" )))) ; definitionlet "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "a" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "A")); :: original: :::"idsym"::: redefine func :::"idsym"::: "a" -> ($#m1_subset_1 :::"OperSymbol":::) "of" (Set "(" ($#k3_catalg_1 :::"CatSign"::: ) "A" ")" ); let "b" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "A")); :: original: :::"homsym"::: redefine func :::"homsym"::: "(" "a" "," "b" ")" -> ($#m1_subset_1 :::"SortSymbol":::) "of" (Set "(" ($#k3_catalg_1 :::"CatSign"::: ) "A" ")" ); let "c" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "A")); :: original: :::"compsym"::: redefine func :::"compsym"::: "(" "a" "," "b" "," "c" ")" -> ($#m1_subset_1 :::"OperSymbol":::) "of" (Set "(" ($#k3_catalg_1 :::"CatSign"::: ) "A" ")" ); end; theorem :: CATALG_1:11 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k5_catalg_1 :::"idsym"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k5_catalg_1 :::"idsym"::: ) (Set (Var "b"))))) "holds" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "b")))) ; theorem :: CATALG_1:12 (Bool "for" (Set (Var "a1")) "," (Set (Var "b1")) "," (Set (Var "a2")) "," (Set (Var "b2")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k6_catalg_1 :::"homsym"::: ) "(" (Set (Var "a1")) "," (Set (Var "a2")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_catalg_1 :::"homsym"::: ) "(" (Set (Var "b1")) "," (Set (Var "b2")) ")" ))) "holds" (Bool "(" (Bool (Set (Var "a1")) ($#r1_hidden :::"="::: ) (Set (Var "b1"))) & (Bool (Set (Var "a2")) ($#r1_hidden :::"="::: ) (Set (Var "b2"))) ")" )) ; theorem :: CATALG_1:13 (Bool "for" (Set (Var "a1")) "," (Set (Var "b1")) "," (Set (Var "a2")) "," (Set (Var "b2")) "," (Set (Var "a3")) "," (Set (Var "b3")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k7_catalg_1 :::"compsym"::: ) "(" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k7_catalg_1 :::"compsym"::: ) "(" (Set (Var "b1")) "," (Set (Var "b2")) "," (Set (Var "b3")) ")" ))) "holds" (Bool "(" (Bool (Set (Var "a1")) ($#r1_hidden :::"="::: ) (Set (Var "b1"))) & (Bool (Set (Var "a2")) ($#r1_hidden :::"="::: ) (Set (Var "b2"))) & (Bool (Set (Var "a3")) ($#r1_hidden :::"="::: ) (Set (Var "b3"))) ")" )) ; theorem :: CATALG_1:14 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_catalg_1 :::"CatSignature"::: ) "of" (Set (Var "A")) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"SortSymbol":::) "of" (Set (Var "S")) (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) "st" (Bool (Set (Var "s")) ($#r1_hidden :::"="::: ) (Set ($#k9_catalg_1 :::"homsym"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" )))))) ; theorem :: CATALG_1:15 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set "(" ($#k3_catalg_1 :::"CatSign"::: ) (Set (Var "A")) ")" ) "holds" (Bool "(" (Bool "(" (Bool (Set (Set (Var "o")) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" (Set (Var "o")) ($#k2_xtuple_0 :::"`2"::: ) ")" )) ($#r1_hidden :::"="::: ) (Num 1)) ")" ) "or" (Bool "(" (Bool (Set (Set (Var "o")) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Num 2)) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" (Set (Var "o")) ($#k2_xtuple_0 :::"`2"::: ) ")" )) ($#r1_hidden :::"="::: ) (Num 3)) ")" ) ")" ))) ; theorem :: CATALG_1:16 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set "(" ($#k3_catalg_1 :::"CatSign"::: ) (Set (Var "A")) ")" ) "st" (Bool (Bool "(" (Bool (Set (Set (Var "o")) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Num 1)) "or" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" (Set (Var "o")) ($#k2_xtuple_0 :::"`2"::: ) ")" )) ($#r1_hidden :::"="::: ) (Num 1)) ")" )) "holds" (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) "st" (Bool (Set (Var "o")) ($#r1_hidden :::"="::: ) (Set ($#k8_catalg_1 :::"idsym"::: ) (Set (Var "a"))))))) ; theorem :: CATALG_1:17 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set "(" ($#k3_catalg_1 :::"CatSign"::: ) (Set (Var "A")) ")" ) "st" (Bool (Bool "(" (Bool (Set (Set (Var "o")) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Num 2)) "or" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" (Set (Var "o")) ($#k2_xtuple_0 :::"`2"::: ) ")" )) ($#r1_hidden :::"="::: ) (Num 3)) ")" )) "holds" (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) "st" (Bool (Set (Var "o")) ($#r1_hidden :::"="::: ) (Set ($#k10_catalg_1 :::"compsym"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" ))))) ; theorem :: CATALG_1:18 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) "holds" (Bool "(" (Bool (Set ($#k1_msualg_1 :::"the_arity_of"::: ) (Set "(" ($#k8_catalg_1 :::"idsym"::: ) (Set (Var "a")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k2_msualg_1 :::"the_result_sort_of"::: ) (Set "(" ($#k8_catalg_1 :::"idsym"::: ) (Set (Var "a")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k9_catalg_1 :::"homsym"::: ) "(" (Set (Var "a")) "," (Set (Var "a")) ")" )) ")" ))) ; theorem :: CATALG_1:19 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) "holds" (Bool "(" (Bool (Set ($#k1_msualg_1 :::"the_arity_of"::: ) (Set "(" ($#k10_catalg_1 :::"compsym"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_finseq_4 :::"<*"::: ) (Set "(" ($#k9_catalg_1 :::"homsym"::: ) "(" (Set (Var "b")) "," (Set (Var "c")) ")" ")" ) "," (Set "(" ($#k9_catalg_1 :::"homsym"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) ($#k2_finseq_4 :::"*>"::: ) )) & (Bool (Set ($#k2_msualg_1 :::"the_result_sort_of"::: ) (Set "(" ($#k10_catalg_1 :::"compsym"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k9_catalg_1 :::"homsym"::: ) "(" (Set (Var "a")) "," (Set (Var "c")) ")" )) ")" ))) ; begin definitionlet "C1", "C2" be ($#l1_cat_1 :::"Category":::); let "F" be ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Const "C1")) "," (Set (Const "C2")); func :::"Upsilon"::: "F" -> ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k3_catalg_1 :::"CatSign"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "C1") ")" )) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k3_catalg_1 :::"CatSign"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "C2") ")" )) means :: CATALG_1:def 11 (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"SortSymbol":::) "of" (Set "(" ($#k3_catalg_1 :::"CatSign"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "C1") ")" ) "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" (Set "(" ($#k7_cat_1 :::"Obj"::: ) "F" ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" (Set (Var "s")) ($#k2_xtuple_0 :::"`2"::: ) ")" ) ")" ) ($#k4_tarski :::"]"::: ) ))); func :::"Psi"::: "F" -> ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set "(" ($#k3_catalg_1 :::"CatSign"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "C1") ")" )) "," (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set "(" ($#k3_catalg_1 :::"CatSign"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "C2") ")" )) means :: CATALG_1:def 12 (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set "(" ($#k3_catalg_1 :::"CatSign"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "C1") ")" ) "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "o"))) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set "(" (Set (Var "o")) ($#k1_xtuple_0 :::"`1"::: ) ")" ) "," (Set "(" (Set "(" ($#k7_cat_1 :::"Obj"::: ) "F" ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" (Set (Var "o")) ($#k2_xtuple_0 :::"`2"::: ) ")" ) ")" ) ($#k4_tarski :::"]"::: ) ))); end; :: deftheorem defines :::"Upsilon"::: CATALG_1:def 11 : (Bool "for" (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "C1")) "," (Set (Var "C2")) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k3_catalg_1 :::"CatSign"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "C1"))) ")" )) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k3_catalg_1 :::"CatSign"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "C2"))) ")" )) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k11_catalg_1 :::"Upsilon"::: ) (Set (Var "F")))) "iff" (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"SortSymbol":::) "of" (Set "(" ($#k3_catalg_1 :::"CatSign"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "C1"))) ")" ) "holds" (Bool (Set (Set (Var "b4")) ($#k3_funct_2 :::"."::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" (Set "(" ($#k7_cat_1 :::"Obj"::: ) (Set (Var "F")) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" (Set (Var "s")) ($#k2_xtuple_0 :::"`2"::: ) ")" ) ")" ) ($#k4_tarski :::"]"::: ) ))) ")" )))); :: deftheorem defines :::"Psi"::: CATALG_1:def 12 : (Bool "for" (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "C1")) "," (Set (Var "C2")) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set "(" ($#k3_catalg_1 :::"CatSign"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "C1"))) ")" )) "," (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set "(" ($#k3_catalg_1 :::"CatSign"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "C2"))) ")" )) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k12_catalg_1 :::"Psi"::: ) (Set (Var "F")))) "iff" (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set "(" ($#k3_catalg_1 :::"CatSign"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "C1"))) ")" ) "holds" (Bool (Set (Set (Var "b4")) ($#k3_funct_2 :::"."::: ) (Set (Var "o"))) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set "(" (Set (Var "o")) ($#k1_xtuple_0 :::"`1"::: ) ")" ) "," (Set "(" (Set "(" ($#k7_cat_1 :::"Obj"::: ) (Set (Var "F")) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" (Set (Var "o")) ($#k2_xtuple_0 :::"`2"::: ) ")" ) ")" ) ($#k4_tarski :::"]"::: ) ))) ")" )))); theorem :: CATALG_1:20 (Bool "for" (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "C1")) "," (Set (Var "C2")) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C1")) "holds" (Bool (Set (Set "(" ($#k11_catalg_1 :::"Upsilon"::: ) (Set (Var "F")) ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k9_catalg_1 :::"homsym"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k9_catalg_1 :::"homsym"::: ) "(" (Set "(" (Set (Var "F")) ($#k8_cat_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set "(" (Set (Var "F")) ($#k8_cat_1 :::"."::: ) (Set (Var "b")) ")" ) ")" ))))) ; theorem :: CATALG_1:21 (Bool "for" (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "C1")) "," (Set (Var "C2")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C1")) "holds" (Bool (Set (Set "(" ($#k12_catalg_1 :::"Psi"::: ) (Set (Var "F")) ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k8_catalg_1 :::"idsym"::: ) (Set (Var "a")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k8_catalg_1 :::"idsym"::: ) (Set "(" (Set (Var "F")) ($#k8_cat_1 :::"."::: ) (Set (Var "a")) ")" )))))) ; theorem :: CATALG_1:22 (Bool "for" (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "C1")) "," (Set (Var "C2")) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C1")) "holds" (Bool (Set (Set "(" ($#k12_catalg_1 :::"Psi"::: ) (Set (Var "F")) ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k10_catalg_1 :::"compsym"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k10_catalg_1 :::"compsym"::: ) "(" (Set "(" (Set (Var "F")) ($#k8_cat_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set "(" (Set (Var "F")) ($#k8_cat_1 :::"."::: ) (Set (Var "b")) ")" ) "," (Set "(" (Set (Var "F")) ($#k8_cat_1 :::"."::: ) (Set (Var "c")) ")" ) ")" ))))) ; theorem :: CATALG_1:23 (Bool "for" (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "C1")) "," (Set (Var "C2")) "holds" (Bool (Set ($#k11_catalg_1 :::"Upsilon"::: ) (Set (Var "F"))) "," (Set ($#k12_catalg_1 :::"Psi"::: ) (Set (Var "F"))) ($#r3_pua2mss1 :::"form_morphism_between"::: ) (Set ($#k3_catalg_1 :::"CatSign"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "C1")))) "," (Set ($#k3_catalg_1 :::"CatSign"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "C2"))))))) ; begin theorem :: CATALG_1:24 (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set ($#k3_catalg_1 :::"CatSign"::: ) (Set (Var "C"))) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "C")) "holds" (Bool (Set ($#k3_msualg_1 :::"Args"::: ) "(" (Set "(" ($#k8_catalg_1 :::"idsym"::: ) (Set (Var "a")) ")" ) "," (Set (Var "A")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) ))))) ; scheme :: CATALG_1:sch 1 CatAlgEx{ F1() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F2() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F3( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) , F4( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) , F5( ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) } : (Bool "ex" (Set (Var "A")) "being" ($#v3_msualg_1 :::"strict"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set ($#k3_catalg_1 :::"CatSign"::: ) (Set F1 "(" ")" )) "st" (Bool "(" (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "holds" (Bool (Set (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "A"))) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k9_catalg_1 :::"homsym"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set F3 "(" (Set (Var "a")) "," (Set (Var "b")) ")" )) ")" ) & (Bool "(" "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "holds" (Bool (Set (Set "(" ($#k5_msualg_1 :::"Den"::: ) "(" (Set "(" ($#k8_catalg_1 :::"idsym"::: ) (Set (Var "a")) ")" ) "," (Set (Var "A")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ($#r1_hidden :::"="::: ) (Set F5 "(" (Set (Var "a")) ")" )) ")" ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) "st" (Bool (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set F3 "(" (Set (Var "a")) "," (Set (Var "b")) ")" )) & (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set F3 "(" (Set (Var "b")) "," (Set (Var "c")) ")" ))) "holds" (Bool (Set (Set "(" ($#k5_msualg_1 :::"Den"::: ) "(" (Set "(" ($#k10_catalg_1 :::"compsym"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" ")" ) "," (Set (Var "A")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k2_finseq_4 :::"<*"::: ) (Set (Var "g")) "," (Set (Var "f")) ($#k2_finseq_4 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set F4 "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "g")) "," (Set (Var "f")) ")" ))) ")" ) ")" )) provided (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "holds" (Bool (Set F3 "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_tarski :::"c="::: ) (Set F2 "(" ")" ))) and (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "holds" (Bool (Set F5 "(" (Set (Var "a")) ")" ) ($#r2_hidden :::"in"::: ) (Set F3 "(" (Set (Var "a")) "," (Set (Var "a")) ")" ))) and (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) "st" (Bool (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set F3 "(" (Set (Var "a")) "," (Set (Var "b")) ")" )) & (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set F3 "(" (Set (Var "b")) "," (Set (Var "c")) ")" ))) "holds" (Bool (Set F4 "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "g")) "," (Set (Var "f")) ")" ) ($#r2_hidden :::"in"::: ) (Set F3 "(" (Set (Var "a")) "," (Set (Var "c")) ")" )))) proof end; definitionlet "C" be ($#l1_cat_1 :::"Category":::); func :::"MSAlg"::: "C" -> ($#v3_msualg_1 :::"strict"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set ($#k3_catalg_1 :::"CatSign"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "C")) means :: CATALG_1:def 13 (Bool "(" (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Object":::) "of" "C" "holds" (Bool (Set (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" it) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k9_catalg_1 :::"homsym"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" )) ")" ) & (Bool "(" "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" "C" "holds" (Bool (Set (Set "(" ($#k5_msualg_1 :::"Den"::: ) "(" (Set "(" ($#k8_catalg_1 :::"idsym"::: ) (Set (Var "a")) ")" ) "," it ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k4_cat_1 :::"id"::: ) (Set (Var "a")))) ")" ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Object":::) "of" "C" (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Morphism":::) "of" "C" "st" (Bool (Bool (Set ($#k3_graph_1 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool (Set ($#k4_graph_1 :::"cod"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "b"))) & (Bool (Set ($#k3_graph_1 :::"dom"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set (Var "b"))) & (Bool (Set ($#k4_graph_1 :::"cod"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set (Var "c")))) "holds" (Bool (Set (Set "(" ($#k5_msualg_1 :::"Den"::: ) "(" (Set "(" ($#k10_catalg_1 :::"compsym"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" ")" ) "," it ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k2_finseq_4 :::"<*"::: ) (Set (Var "g")) "," (Set (Var "f")) ($#k2_finseq_4 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k1_cat_1 :::"(*)"::: ) (Set (Var "f"))))) ")" ) ")" ); end; :: deftheorem defines :::"MSAlg"::: CATALG_1:def 13 : (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "b2")) "being" ($#v3_msualg_1 :::"strict"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set ($#k3_catalg_1 :::"CatSign"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "C")))) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k13_catalg_1 :::"MSAlg"::: ) (Set (Var "C")))) "iff" (Bool "(" (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "holds" (Bool (Set (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "b2"))) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k9_catalg_1 :::"homsym"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" )) ")" ) & (Bool "(" "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "holds" (Bool (Set (Set "(" ($#k5_msualg_1 :::"Den"::: ) "(" (Set "(" ($#k8_catalg_1 :::"idsym"::: ) (Set (Var "a")) ")" ) "," (Set (Var "b2")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k4_cat_1 :::"id"::: ) (Set (Var "a")))) ")" ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set ($#k3_graph_1 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool (Set ($#k4_graph_1 :::"cod"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "b"))) & (Bool (Set ($#k3_graph_1 :::"dom"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set (Var "b"))) & (Bool (Set ($#k4_graph_1 :::"cod"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set (Var "c")))) "holds" (Bool (Set (Set "(" ($#k5_msualg_1 :::"Den"::: ) "(" (Set "(" ($#k10_catalg_1 :::"compsym"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" ")" ) "," (Set (Var "b2")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k2_finseq_4 :::"<*"::: ) (Set (Var "g")) "," (Set (Var "f")) ($#k2_finseq_4 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k1_cat_1 :::"(*)"::: ) (Set (Var "f"))))) ")" ) ")" ) ")" ))); theorem :: CATALG_1:25 (Bool "for" (Set (Var "A")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "A")) "holds" (Bool (Set ($#k4_msualg_1 :::"Result"::: ) "(" (Set "(" ($#k8_catalg_1 :::"idsym"::: ) (Set (Var "a")) ")" ) "," (Set "(" ($#k13_catalg_1 :::"MSAlg"::: ) (Set (Var "A")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "a")) "," (Set (Var "a")) ")" )))) ; theorem :: CATALG_1:26 (Bool "for" (Set (Var "A")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "A")) "holds" (Bool "(" (Bool (Set ($#k3_msualg_1 :::"Args"::: ) "(" (Set "(" ($#k10_catalg_1 :::"compsym"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" ")" ) "," (Set "(" ($#k13_catalg_1 :::"MSAlg"::: ) (Set (Var "A")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_card_3 :::"product"::: ) (Set ($#k2_finseq_4 :::"<*"::: ) (Set "(" ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "b")) "," (Set (Var "c")) ")" ")" ) "," (Set "(" ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) ($#k2_finseq_4 :::"*>"::: ) ))) & (Bool (Set ($#k4_msualg_1 :::"Result"::: ) "(" (Set "(" ($#k10_catalg_1 :::"compsym"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" ")" ) "," (Set "(" ($#k13_catalg_1 :::"MSAlg"::: ) (Set (Var "A")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "a")) "," (Set (Var "c")) ")" )) ")" ))) ; registrationlet "C" be ($#l1_cat_1 :::"Category":::); cluster (Set ($#k13_catalg_1 :::"MSAlg"::: ) "C") -> ($#v3_msualg_1 :::"strict"::: ) ($#v1_msafree1 :::"disjoint_valued"::: ) ($#v1_msualg_6 :::"feasible"::: ) ; end; theorem :: CATALG_1:27 (Bool "for" (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "C1")) "," (Set (Var "C2")) "holds" (Bool (Set (Set (Var "F")) ($#k1_catalg_1 :::"-MSF"::: ) "(" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k3_catalg_1 :::"CatSign"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "C1"))) ")" )) "," (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set "(" ($#k13_catalg_1 :::"MSAlg"::: ) (Set (Var "C1")) ")" )) ")" ) "is" ($#m2_pboole :::"ManySortedFunction":::) "of" (Set "(" ($#k13_catalg_1 :::"MSAlg"::: ) (Set (Var "C1")) ")" ) "," (Set "(" (Set "(" ($#k13_catalg_1 :::"MSAlg"::: ) (Set (Var "C2")) ")" ) ($#k1_instalg1 :::"|"::: ) "(" (Set "(" ($#k3_catalg_1 :::"CatSign"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "C1"))) ")" ) "," (Set "(" ($#k11_catalg_1 :::"Upsilon"::: ) (Set (Var "F")) ")" ) "," (Set "(" ($#k12_catalg_1 :::"Psi"::: ) (Set (Var "F")) ")" ) ")" ")" )))) ; theorem :: CATALG_1:28 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k3_msualg_1 :::"Args"::: ) "(" (Set "(" ($#k10_catalg_1 :::"compsym"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" ")" ) "," (Set "(" ($#k13_catalg_1 :::"MSAlg"::: ) (Set (Var "C")) ")" ) ")" )) "iff" (Bool "ex" (Set (Var "g")) "," (Set (Var "f")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C")) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k2_finseq_4 :::"<*"::: ) (Set (Var "g")) "," (Set (Var "f")) ($#k2_finseq_4 :::"*>"::: ) )) & (Bool (Set ($#k3_graph_1 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool (Set ($#k4_graph_1 :::"cod"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "b"))) & (Bool (Set ($#k3_graph_1 :::"dom"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set (Var "b"))) & (Bool (Set ($#k4_graph_1 :::"cod"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set (Var "c"))) ")" )) ")" )))) ; theorem :: CATALG_1:29 (Bool "for" (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "C1")) "," (Set (Var "C2")) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C1")) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C1")) "st" (Bool (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" )) & (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "b")) "," (Set (Var "c")) ")" ))) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_msualg_1 :::"Args"::: ) "(" (Set "(" ($#k10_catalg_1 :::"compsym"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" ")" ) "," (Set "(" ($#k13_catalg_1 :::"MSAlg"::: ) (Set (Var "C1")) ")" ) ")" ) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k2_finseq_4 :::"<*"::: ) (Set (Var "g")) "," (Set (Var "f")) ($#k2_finseq_4 :::"*>"::: ) ))) "holds" (Bool "for" (Set (Var "H")) "being" ($#m2_pboole :::"ManySortedFunction":::) "of" (Set "(" ($#k13_catalg_1 :::"MSAlg"::: ) (Set (Var "C1")) ")" ) "," (Set "(" (Set "(" ($#k13_catalg_1 :::"MSAlg"::: ) (Set (Var "C2")) ")" ) ($#k1_instalg1 :::"|"::: ) "(" (Set "(" ($#k3_catalg_1 :::"CatSign"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "C1"))) ")" ) "," (Set "(" ($#k11_catalg_1 :::"Upsilon"::: ) (Set (Var "F")) ")" ) "," (Set "(" ($#k12_catalg_1 :::"Psi"::: ) (Set (Var "F")) ")" ) ")" ")" ) "st" (Bool (Bool (Set (Var "H")) ($#r8_pboole :::"="::: ) (Set (Set (Var "F")) ($#k1_catalg_1 :::"-MSF"::: ) "(" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k3_catalg_1 :::"CatSign"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "C1"))) ")" )) "," (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set "(" ($#k13_catalg_1 :::"MSAlg"::: ) (Set (Var "C1")) ")" )) ")" ))) "holds" (Bool (Set (Set (Var "H")) ($#k5_msualg_3 :::"#"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k2_finseq_4 :::"<*"::: ) (Set "(" (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "g")) ")" ) "," (Set "(" (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "f")) ")" ) ($#k2_finseq_4 :::"*>"::: ) )))))))) ; theorem :: CATALG_1:30 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" )) & (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "b")) "," (Set (Var "c")) ")" ))) "holds" (Bool (Set (Set "(" ($#k5_msualg_1 :::"Den"::: ) "(" (Set "(" ($#k10_catalg_1 :::"compsym"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" ")" ) "," (Set "(" ($#k13_catalg_1 :::"MSAlg"::: ) (Set (Var "C")) ")" ) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k2_finseq_4 :::"<*"::: ) (Set (Var "g")) "," (Set (Var "f")) ($#k2_finseq_4 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k1_cat_1 :::"(*)"::: ) (Set (Var "f"))))))) ; theorem :: CATALG_1:31 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" )) & (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "b")) "," (Set (Var "c")) ")" )) & (Bool (Set (Var "h")) ($#r2_hidden :::"in"::: ) (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "c")) "," (Set (Var "d")) ")" ))) "holds" (Bool (Set (Set "(" ($#k5_msualg_1 :::"Den"::: ) "(" (Set "(" ($#k10_catalg_1 :::"compsym"::: ) "(" (Set (Var "a")) "," (Set (Var "c")) "," (Set (Var "d")) ")" ")" ) "," (Set "(" ($#k13_catalg_1 :::"MSAlg"::: ) (Set (Var "C")) ")" ) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "h")) "," (Set "(" (Set "(" ($#k5_msualg_1 :::"Den"::: ) "(" (Set "(" ($#k10_catalg_1 :::"compsym"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" ")" ) "," (Set "(" ($#k13_catalg_1 :::"MSAlg"::: ) (Set (Var "C")) ")" ) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k2_finseq_4 :::"<*"::: ) (Set (Var "g")) "," (Set (Var "f")) ($#k2_finseq_4 :::"*>"::: ) ) ")" ) ($#k10_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_msualg_1 :::"Den"::: ) "(" (Set "(" ($#k10_catalg_1 :::"compsym"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "d")) ")" ")" ) "," (Set "(" ($#k13_catalg_1 :::"MSAlg"::: ) (Set (Var "C")) ")" ) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set "(" (Set "(" ($#k5_msualg_1 :::"Den"::: ) "(" (Set "(" ($#k10_catalg_1 :::"compsym"::: ) "(" (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) ")" ")" ) "," (Set "(" ($#k13_catalg_1 :::"MSAlg"::: ) (Set (Var "C")) ")" ) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k2_finseq_4 :::"<*"::: ) (Set (Var "h")) "," (Set (Var "g")) ($#k2_finseq_4 :::"*>"::: ) ) ")" ) "," (Set (Var "f")) ($#k10_finseq_1 :::"*>"::: ) )))))) ; theorem :: CATALG_1:32 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ))) "holds" (Bool "(" (Bool (Set (Set "(" ($#k5_msualg_1 :::"Den"::: ) "(" (Set "(" ($#k10_catalg_1 :::"compsym"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "b")) ")" ")" ) "," (Set "(" ($#k13_catalg_1 :::"MSAlg"::: ) (Set (Var "C")) ")" ) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k2_finseq_4 :::"<*"::: ) (Set "(" ($#k4_cat_1 :::"id"::: ) (Set (Var "b")) ")" ) "," (Set (Var "f")) ($#k2_finseq_4 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "f"))) & (Bool (Set (Set "(" ($#k5_msualg_1 :::"Den"::: ) "(" (Set "(" ($#k10_catalg_1 :::"compsym"::: ) "(" (Set (Var "a")) "," (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) "," (Set "(" ($#k13_catalg_1 :::"MSAlg"::: ) (Set (Var "C")) ")" ) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k2_finseq_4 :::"<*"::: ) (Set (Var "f")) "," (Set "(" ($#k4_cat_1 :::"id"::: ) (Set (Var "a")) ")" ) ($#k2_finseq_4 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "f"))) ")" )))) ; theorem :: CATALG_1:33 (Bool "for" (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "C1")) "," (Set (Var "C2")) (Bool "ex" (Set (Var "H")) "being" ($#m2_pboole :::"ManySortedFunction":::) "of" (Set "(" ($#k13_catalg_1 :::"MSAlg"::: ) (Set (Var "C1")) ")" ) "," (Set "(" (Set "(" ($#k13_catalg_1 :::"MSAlg"::: ) (Set (Var "C2")) ")" ) ($#k1_instalg1 :::"|"::: ) "(" (Set "(" ($#k3_catalg_1 :::"CatSign"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "C1"))) ")" ) "," (Set "(" ($#k11_catalg_1 :::"Upsilon"::: ) (Set (Var "F")) ")" ) "," (Set "(" ($#k12_catalg_1 :::"Psi"::: ) (Set (Var "F")) ")" ) ")" ")" ) "st" (Bool "(" (Bool (Set (Var "H")) ($#r8_pboole :::"="::: ) (Set (Set (Var "F")) ($#k1_catalg_1 :::"-MSF"::: ) "(" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k3_catalg_1 :::"CatSign"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "C1"))) ")" )) "," (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set "(" ($#k13_catalg_1 :::"MSAlg"::: ) (Set (Var "C1")) ")" )) ")" )) & (Bool (Set (Var "H")) ($#r1_msualg_3 :::"is_homomorphism"::: ) (Set ($#k13_catalg_1 :::"MSAlg"::: ) (Set (Var "C1"))) "," (Set (Set "(" ($#k13_catalg_1 :::"MSAlg"::: ) (Set (Var "C2")) ")" ) ($#k1_instalg1 :::"|"::: ) "(" (Set "(" ($#k3_catalg_1 :::"CatSign"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "C1"))) ")" ) "," (Set "(" ($#k11_catalg_1 :::"Upsilon"::: ) (Set (Var "F")) ")" ) "," (Set "(" ($#k12_catalg_1 :::"Psi"::: ) (Set (Var "F")) ")" ) ")" )) ")" )))) ;