:: MSUALG_3 semantic presentation begin definitionlet "I" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "A", "B" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); let "F" be ($#m2_pboole :::"ManySortedFunction"::: ) "of" (Set (Const "A")) "," (Set (Const "B")); let "i" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "I")); :: original: :::"."::: redefine func "F" :::"."::: "i" -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" "A" ($#k1_funct_1 :::"."::: ) "i" ")" ) "," (Set "(" "B" ($#k1_funct_1 :::"."::: ) "i" ")" ); end; definitionlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; let "U1", "U2" be ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Const "S")); mode ManySortedFunction of "U1" "," "U2" is ($#m2_pboole :::"ManySortedFunction"::: ) "of" (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" "U1") "," (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" "U2"); end; definitionlet "I" be ($#m1_hidden :::"set"::: ) ; let "A" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); func :::"id"::: "A" -> ($#m2_pboole :::"ManySortedFunction"::: ) "of" "A" "," "A" means :: MSUALG_3: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 ($#k6_partfun1 :::"id"::: ) (Set "(" "A" ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" )))); end; :: deftheorem defines :::"id"::: MSUALG_3:def 1 : (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "b3")) "being" ($#m2_pboole :::"ManySortedFunction"::: ) "of" (Set (Var "A")) "," (Set (Var "A")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k2_msualg_3 :::"id"::: ) (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 "b3")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k6_partfun1 :::"id"::: ) (Set "(" (Set (Var "A")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" )))) ")" )))); definitionlet "IT" be ($#m1_hidden :::"Function":::); attr "IT" is :::""1-1""::: means :: MSUALG_3:def 2 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "IT")) & (Bool (Set "IT" ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Var "f")))) "holds" (Bool (Set (Var "f")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ))); end; :: deftheorem defines :::""1-1""::: MSUALG_3:def 2 : (Bool "for" (Set (Var "IT")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v1_msualg_3 :::""1-1""::: ) ) "iff" (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "IT")))) & (Bool (Set (Set (Var "IT")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Var "f")))) "holds" (Bool (Set (Var "f")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ))) ")" )); registrationlet "I" be ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) "I" ($#v4_relat_1 :::"-defined"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_partfun1 :::"total"::: ) bbbadV1_FUNCOP_1() bbbadV2_FUNCOP_1() ($#v1_msualg_3 :::""1-1""::: ) for ($#m1_hidden :::"set"::: ) ; end; theorem :: MSUALG_3:1 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_hidden :::"ManySortedFunction":::) "of" (Set (Var "I")) "holds" (Bool "(" (Bool (Set (Var "F")) "is" ($#v1_msualg_3 :::""1-1""::: ) ) "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 "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) "is" ($#v2_funct_1 :::"one-to-one"::: ) )) ")" ))) ; definitionlet "I" be ($#m1_hidden :::"set"::: ) ; let "A", "B" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); let "IT" be ($#m2_pboole :::"ManySortedFunction"::: ) "of" (Set (Const "A")) "," (Set (Const "B")); attr "IT" is :::""onto""::: means :: MSUALG_3:def 3 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) "I")) "holds" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" "IT" ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" )) ($#r1_hidden :::"="::: ) (Set "B" ($#k1_funct_1 :::"."::: ) (Set (Var "i"))))); end; :: deftheorem defines :::""onto""::: MSUALG_3:def 3 : (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 "IT")) "being" ($#m2_pboole :::"ManySortedFunction"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v2_msualg_3 :::""onto""::: ) ) "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 ($#k10_xtuple_0 :::"rng"::: ) (Set "(" (Set (Var "IT")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "B")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))))) ")" )))); theorem :: MSUALG_3:2 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "F")) "being" ($#m2_pboole :::"ManySortedFunction"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) (Bool "for" (Set (Var "G")) "being" ($#m2_pboole :::"ManySortedFunction"::: ) "of" (Set (Var "B")) "," (Set (Var "C")) "holds" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set (Var "G")) ($#k8_pboole :::"**"::: ) (Set (Var "F")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "I"))) & (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 "(" (Set (Var "G")) ($#k8_pboole :::"**"::: ) (Set (Var "F")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "G")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ))) ")" ) ")" ))))) ; definitionlet "I" be ($#m1_hidden :::"set"::: ) ; let "A" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); let "B", "C" be bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); let "F" be ($#m2_pboole :::"ManySortedFunction"::: ) "of" (Set (Const "A")) "," (Set (Const "B")); let "G" be ($#m2_pboole :::"ManySortedFunction"::: ) "of" (Set (Const "B")) "," (Set (Const "C")); :: original: :::"**"::: redefine func "G" :::"**"::: "F" -> ($#m2_pboole :::"ManySortedFunction"::: ) "of" "A" "," "C"; end; theorem :: MSUALG_3:3 (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")) "being" ($#m2_pboole :::"ManySortedFunction"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) "holds" (Bool (Set (Set (Var "F")) ($#k8_pboole :::"**"::: ) (Set "(" ($#k2_msualg_3 :::"id"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "F")))))) ; theorem :: MSUALG_3:4 (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")) "being" ($#m2_pboole :::"ManySortedFunction"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) "holds" (Bool (Set (Set "(" ($#k2_msualg_3 :::"id"::: ) (Set (Var "B")) ")" ) ($#k8_pboole :::"**"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set (Var "F")))))) ; definitionlet "I" be ($#m1_hidden :::"set"::: ) ; let "A", "B" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); let "F" be ($#m2_pboole :::"ManySortedFunction"::: ) "of" (Set (Const "A")) "," (Set (Const "B")); assume that (Bool (Set (Const "F")) "is" ($#v1_msualg_3 :::""1-1""::: ) ) and (Bool (Set (Const "F")) "is" ($#v2_msualg_3 :::""onto""::: ) ) ; func "F" :::""""::: -> ($#m2_pboole :::"ManySortedFunction"::: ) "of" "B" "," "A" means :: MSUALG_3:def 4 (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 (Set "(" "F" ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k2_funct_1 :::"""::: ) ))); end; :: deftheorem defines :::""""::: MSUALG_3:def 4 : (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")) "being" ($#m2_pboole :::"ManySortedFunction"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_msualg_3 :::""1-1""::: ) ) & (Bool (Set (Var "F")) "is" ($#v2_msualg_3 :::""onto""::: ) )) "holds" (Bool "for" (Set (Var "b5")) "being" ($#m2_pboole :::"ManySortedFunction"::: ) "of" (Set (Var "B")) "," (Set (Var "A")) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k4_msualg_3 :::""""::: ) )) "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 "b5")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k2_funct_1 :::"""::: ) ))) ")" ))))); theorem :: MSUALG_3:5 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "H")) "being" ($#m2_pboole :::"ManySortedFunction"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) (Bool "for" (Set (Var "H1")) "being" ($#m2_pboole :::"ManySortedFunction"::: ) "of" (Set (Var "B")) "," (Set (Var "A")) "st" (Bool (Bool (Set (Var "H")) "is" ($#v1_msualg_3 :::""1-1""::: ) ) & (Bool (Set (Var "H")) "is" ($#v2_msualg_3 :::""onto""::: ) ) & (Bool (Set (Var "H1")) ($#r6_pboole :::"="::: ) (Set (Set (Var "H")) ($#k4_msualg_3 :::""""::: ) ))) "holds" (Bool "(" (Bool (Set (Set (Var "H")) ($#k3_msualg_3 :::"**"::: ) (Set (Var "H1"))) ($#r6_pboole :::"="::: ) (Set ($#k2_msualg_3 :::"id"::: ) (Set (Var "B")))) & (Bool (Set (Set (Var "H1")) ($#k3_msualg_3 :::"**"::: ) (Set (Var "H"))) ($#r6_pboole :::"="::: ) (Set ($#k2_msualg_3 :::"id"::: ) (Set (Var "A")))) ")" ))))) ; registrationlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; let "U1" be ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Const "S")); let "o" be ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Const "S")); cluster (Set ($#k3_msualg_1 :::"Args"::: ) "(" "o" "," "U1" ")" ) -> ($#v4_funct_1 :::"functional"::: ) ; end; begin theorem :: MSUALG_3:6 (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "U1")) "being" ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k3_msualg_1 :::"Args"::: ) "(" (Set (Var "o")) "," (Set (Var "U1")) ")" ))) "holds" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set "(" ($#k1_msualg_1 :::"the_arity_of"::: ) (Set (Var "o")) ")" ))) & (Bool "(" "for" (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "U1"))) ($#k3_relat_1 :::"*"::: ) (Set "(" ($#k1_msualg_1 :::"the_arity_of"::: ) (Set (Var "o")) ")" ) ")" )))) "holds" (Bool (Set (Set (Var "x")) ($#k1_funct_1 :::"."::: ) (Set (Var "y"))) ($#r2_hidden :::"in"::: ) (Set (Set "(" (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "U1"))) ($#k3_relat_1 :::"*"::: ) (Set "(" ($#k1_msualg_1 :::"the_arity_of"::: ) (Set (Var "o")) ")" ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "y")))) ")" ) ")" ))))) ; definitionlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; let "U1", "U2" be ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Const "S")); let "o" be ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Const "S")); let "F" be ($#m2_pboole :::"ManySortedFunction":::) "of" (Set (Const "U1")) "," (Set (Const "U2")); let "x" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_msualg_1 :::"Args"::: ) "(" (Set (Const "o")) "," (Set (Const "U1")) ")" ); assume that (Bool (Set ($#k3_msualg_1 :::"Args"::: ) "(" (Set (Const "o")) "," (Set (Const "U1")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) and (Bool (Set ($#k3_msualg_1 :::"Args"::: ) "(" (Set (Const "o")) "," (Set (Const "U2")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ; func "F" :::"#"::: "x" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_msualg_1 :::"Args"::: ) "(" "o" "," "U2" ")" ) equals :: MSUALG_3:def 5 (Set (Set "(" ($#k2_pralg_2 :::"Frege"::: ) (Set "(" "F" ($#k3_relat_1 :::"*"::: ) (Set "(" ($#k1_msualg_1 :::"the_arity_of"::: ) "o" ")" ) ")" ) ")" ) ($#k1_funct_1 :::"."::: ) "x"); end; :: deftheorem defines :::"#"::: MSUALG_3:def 5 : (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "U1")) "," (Set (Var "U2")) "being" ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "F")) "being" ($#m2_pboole :::"ManySortedFunction":::) "of" (Set (Var "U1")) "," (Set (Var "U2")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_msualg_1 :::"Args"::: ) "(" (Set (Var "o")) "," (Set (Var "U1")) ")" ) "st" (Bool (Bool (Set ($#k3_msualg_1 :::"Args"::: ) "(" (Set (Var "o")) "," (Set (Var "U1")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k3_msualg_1 :::"Args"::: ) "(" (Set (Var "o")) "," (Set (Var "U2")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set (Set (Var "F")) ($#k5_msualg_3 :::"#"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_pralg_2 :::"Frege"::: ) (Set "(" (Set (Var "F")) ($#k3_relat_1 :::"*"::: ) (Set "(" ($#k1_msualg_1 :::"the_arity_of"::: ) (Set (Var "o")) ")" ) ")" ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))))))))); definitionlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; let "U1", "U2" be ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Const "S")); let "o" be ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Const "S")); let "F" be ($#m2_pboole :::"ManySortedFunction":::) "of" (Set (Const "U1")) "," (Set (Const "U2")); let "x" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_msualg_1 :::"Args"::: ) "(" (Set (Const "o")) "," (Set (Const "U1")) ")" ); redefine func "F" :::"#"::: "x" means :: MSUALG_3:def 6 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "x"))) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" "F" ($#k1_msualg_3 :::"."::: ) (Set "(" (Set "(" ($#k1_msualg_1 :::"the_arity_of"::: ) "o" ")" ) ($#k7_partfun1 :::"/."::: ) (Set (Var "n")) ")" ) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" "x" ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" )))); end; :: deftheorem defines :::"#"::: MSUALG_3:def 6 : (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "U1")) "," (Set (Var "U2")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "F")) "being" ($#m2_pboole :::"ManySortedFunction":::) "of" (Set (Var "U1")) "," (Set (Var "U2")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_msualg_1 :::"Args"::: ) "(" (Set (Var "o")) "," (Set (Var "U1")) ")" ) (Bool "for" (Set (Var "b7")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_msualg_1 :::"Args"::: ) "(" (Set (Var "o")) "," (Set (Var "U2")) ")" ) "holds" (Bool "(" (Bool (Set (Var "b7")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k5_msualg_3 :::"#"::: ) (Set (Var "x")))) "iff" (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "x"))))) "holds" (Bool (Set (Set (Var "b7")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "F")) ($#k1_msualg_3 :::"."::: ) (Set "(" (Set "(" ($#k1_msualg_1 :::"the_arity_of"::: ) (Set (Var "o")) ")" ) ($#k7_partfun1 :::"/."::: ) (Set (Var "n")) ")" ) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "x")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" )))) ")" ))))))); theorem :: MSUALG_3:7 (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "U1")) "being" ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) "st" (Bool (Bool (Set ($#k3_msualg_1 :::"Args"::: ) "(" (Set (Var "o")) "," (Set (Var "U1")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_msualg_1 :::"Args"::: ) "(" (Set (Var "o")) "," (Set (Var "U1")) ")" ) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_msualg_3 :::"id"::: ) (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "U1"))) ")" ) ($#k5_msualg_3 :::"#"::: ) (Set (Var "x")))))))) ; theorem :: MSUALG_3:8 (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "U1")) "," (Set (Var "U2")) "," (Set (Var "U3")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "H1")) "being" ($#m2_pboole :::"ManySortedFunction":::) "of" (Set (Var "U1")) "," (Set (Var "U2")) (Bool "for" (Set (Var "H2")) "being" ($#m2_pboole :::"ManySortedFunction":::) "of" (Set (Var "U2")) "," (Set (Var "U3")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_msualg_1 :::"Args"::: ) "(" (Set (Var "o")) "," (Set (Var "U1")) ")" ) "holds" (Bool (Set (Set "(" (Set (Var "H2")) ($#k3_msualg_3 :::"**"::: ) (Set (Var "H1")) ")" ) ($#k5_msualg_3 :::"#"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "H2")) ($#k5_msualg_3 :::"#"::: ) (Set "(" (Set (Var "H1")) ($#k5_msualg_3 :::"#"::: ) (Set (Var "x")) ")" ))))))))) ; definitionlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; let "U1", "U2" be ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Const "S")); let "F" be ($#m2_pboole :::"ManySortedFunction":::) "of" (Set (Const "U1")) "," (Set (Const "U2")); pred "F" :::"is_homomorphism"::: "U1" "," "U2" means :: MSUALG_3:def 7 (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" "S" "st" (Bool (Bool (Set ($#k3_msualg_1 :::"Args"::: ) "(" (Set (Var "o")) "," "U1" ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_msualg_1 :::"Args"::: ) "(" (Set (Var "o")) "," "U1" ")" ) "holds" (Bool (Set (Set "(" "F" ($#k1_msualg_3 :::"."::: ) (Set "(" ($#k2_msualg_1 :::"the_result_sort_of"::: ) (Set (Var "o")) ")" ) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" ($#k5_msualg_1 :::"Den"::: ) "(" (Set (Var "o")) "," "U1" ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_msualg_1 :::"Den"::: ) "(" (Set (Var "o")) "," "U2" ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" "F" ($#k5_msualg_3 :::"#"::: ) (Set (Var "x")) ")" ))))); end; :: deftheorem defines :::"is_homomorphism"::: MSUALG_3:def 7 : (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "U1")) "," (Set (Var "U2")) "being" ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "F")) "being" ($#m2_pboole :::"ManySortedFunction":::) "of" (Set (Var "U1")) "," (Set (Var "U2")) "holds" (Bool "(" (Bool (Set (Var "F")) ($#r1_msualg_3 :::"is_homomorphism"::: ) (Set (Var "U1")) "," (Set (Var "U2"))) "iff" (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set ($#k3_msualg_1 :::"Args"::: ) "(" (Set (Var "o")) "," (Set (Var "U1")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_msualg_1 :::"Args"::: ) "(" (Set (Var "o")) "," (Set (Var "U1")) ")" ) "holds" (Bool (Set (Set "(" (Set (Var "F")) ($#k1_msualg_3 :::"."::: ) (Set "(" ($#k2_msualg_1 :::"the_result_sort_of"::: ) (Set (Var "o")) ")" ) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" ($#k5_msualg_1 :::"Den"::: ) "(" (Set (Var "o")) "," (Set (Var "U1")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_msualg_1 :::"Den"::: ) "(" (Set (Var "o")) "," (Set (Var "U2")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "F")) ($#k5_msualg_3 :::"#"::: ) (Set (Var "x")) ")" ))))) ")" )))); theorem :: MSUALG_3:9 (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "U1")) "being" ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) "holds" (Bool (Set ($#k2_msualg_3 :::"id"::: ) (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "U1")))) ($#r1_msualg_3 :::"is_homomorphism"::: ) (Set (Var "U1")) "," (Set (Var "U1"))))) ; theorem :: MSUALG_3:10 (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "U1")) "," (Set (Var "U2")) "," (Set (Var "U3")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "H1")) "being" ($#m2_pboole :::"ManySortedFunction":::) "of" (Set (Var "U1")) "," (Set (Var "U2")) (Bool "for" (Set (Var "H2")) "being" ($#m2_pboole :::"ManySortedFunction":::) "of" (Set (Var "U2")) "," (Set (Var "U3")) "st" (Bool (Bool (Set (Var "H1")) ($#r1_msualg_3 :::"is_homomorphism"::: ) (Set (Var "U1")) "," (Set (Var "U2"))) & (Bool (Set (Var "H2")) ($#r1_msualg_3 :::"is_homomorphism"::: ) (Set (Var "U2")) "," (Set (Var "U3")))) "holds" (Bool (Set (Set (Var "H2")) ($#k3_msualg_3 :::"**"::: ) (Set (Var "H1"))) ($#r1_msualg_3 :::"is_homomorphism"::: ) (Set (Var "U1")) "," (Set (Var "U3"))))))) ; definitionlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; let "U1", "U2" be ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Const "S")); let "F" be ($#m2_pboole :::"ManySortedFunction":::) "of" (Set (Const "U1")) "," (Set (Const "U2")); pred "F" :::"is_epimorphism"::: "U1" "," "U2" means :: MSUALG_3:def 8 (Bool "(" (Bool "F" ($#r1_msualg_3 :::"is_homomorphism"::: ) "U1" "," "U2") & (Bool "F" "is" ($#v2_msualg_3 :::""onto""::: ) ) ")" ); end; :: deftheorem defines :::"is_epimorphism"::: MSUALG_3:def 8 : (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "U1")) "," (Set (Var "U2")) "being" ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "F")) "being" ($#m2_pboole :::"ManySortedFunction":::) "of" (Set (Var "U1")) "," (Set (Var "U2")) "holds" (Bool "(" (Bool (Set (Var "F")) ($#r2_msualg_3 :::"is_epimorphism"::: ) (Set (Var "U1")) "," (Set (Var "U2"))) "iff" (Bool "(" (Bool (Set (Var "F")) ($#r1_msualg_3 :::"is_homomorphism"::: ) (Set (Var "U1")) "," (Set (Var "U2"))) & (Bool (Set (Var "F")) "is" ($#v2_msualg_3 :::""onto""::: ) ) ")" ) ")" )))); theorem :: MSUALG_3:11 (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "U1")) "," (Set (Var "U2")) "," (Set (Var "U3")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "F")) "being" ($#m2_pboole :::"ManySortedFunction":::) "of" (Set (Var "U1")) "," (Set (Var "U2")) (Bool "for" (Set (Var "G")) "being" ($#m2_pboole :::"ManySortedFunction":::) "of" (Set (Var "U2")) "," (Set (Var "U3")) "st" (Bool (Bool (Set (Var "F")) ($#r2_msualg_3 :::"is_epimorphism"::: ) (Set (Var "U1")) "," (Set (Var "U2"))) & (Bool (Set (Var "G")) ($#r2_msualg_3 :::"is_epimorphism"::: ) (Set (Var "U2")) "," (Set (Var "U3")))) "holds" (Bool (Set (Set (Var "G")) ($#k3_msualg_3 :::"**"::: ) (Set (Var "F"))) ($#r2_msualg_3 :::"is_epimorphism"::: ) (Set (Var "U1")) "," (Set (Var "U3"))))))) ; definitionlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; let "U1", "U2" be ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Const "S")); let "F" be ($#m2_pboole :::"ManySortedFunction":::) "of" (Set (Const "U1")) "," (Set (Const "U2")); pred "F" :::"is_monomorphism"::: "U1" "," "U2" means :: MSUALG_3:def 9 (Bool "(" (Bool "F" ($#r1_msualg_3 :::"is_homomorphism"::: ) "U1" "," "U2") & (Bool "F" "is" ($#v1_msualg_3 :::""1-1""::: ) ) ")" ); end; :: deftheorem defines :::"is_monomorphism"::: MSUALG_3:def 9 : (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "U1")) "," (Set (Var "U2")) "being" ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "F")) "being" ($#m2_pboole :::"ManySortedFunction":::) "of" (Set (Var "U1")) "," (Set (Var "U2")) "holds" (Bool "(" (Bool (Set (Var "F")) ($#r3_msualg_3 :::"is_monomorphism"::: ) (Set (Var "U1")) "," (Set (Var "U2"))) "iff" (Bool "(" (Bool (Set (Var "F")) ($#r1_msualg_3 :::"is_homomorphism"::: ) (Set (Var "U1")) "," (Set (Var "U2"))) & (Bool (Set (Var "F")) "is" ($#v1_msualg_3 :::""1-1""::: ) ) ")" ) ")" )))); theorem :: MSUALG_3:12 (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "U1")) "," (Set (Var "U2")) "," (Set (Var "U3")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "F")) "being" ($#m2_pboole :::"ManySortedFunction":::) "of" (Set (Var "U1")) "," (Set (Var "U2")) (Bool "for" (Set (Var "G")) "being" ($#m2_pboole :::"ManySortedFunction":::) "of" (Set (Var "U2")) "," (Set (Var "U3")) "st" (Bool (Bool (Set (Var "F")) ($#r3_msualg_3 :::"is_monomorphism"::: ) (Set (Var "U1")) "," (Set (Var "U2"))) & (Bool (Set (Var "G")) ($#r3_msualg_3 :::"is_monomorphism"::: ) (Set (Var "U2")) "," (Set (Var "U3")))) "holds" (Bool (Set (Set (Var "G")) ($#k3_msualg_3 :::"**"::: ) (Set (Var "F"))) ($#r3_msualg_3 :::"is_monomorphism"::: ) (Set (Var "U1")) "," (Set (Var "U3"))))))) ; definitionlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; let "U1", "U2" be ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Const "S")); let "F" be ($#m2_pboole :::"ManySortedFunction":::) "of" (Set (Const "U1")) "," (Set (Const "U2")); pred "F" :::"is_isomorphism"::: "U1" "," "U2" means :: MSUALG_3:def 10 (Bool "(" (Bool "F" ($#r2_msualg_3 :::"is_epimorphism"::: ) "U1" "," "U2") & (Bool "F" ($#r3_msualg_3 :::"is_monomorphism"::: ) "U1" "," "U2") ")" ); end; :: deftheorem defines :::"is_isomorphism"::: MSUALG_3:def 10 : (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "U1")) "," (Set (Var "U2")) "being" ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "F")) "being" ($#m2_pboole :::"ManySortedFunction":::) "of" (Set (Var "U1")) "," (Set (Var "U2")) "holds" (Bool "(" (Bool (Set (Var "F")) ($#r4_msualg_3 :::"is_isomorphism"::: ) (Set (Var "U1")) "," (Set (Var "U2"))) "iff" (Bool "(" (Bool (Set (Var "F")) ($#r2_msualg_3 :::"is_epimorphism"::: ) (Set (Var "U1")) "," (Set (Var "U2"))) & (Bool (Set (Var "F")) ($#r3_msualg_3 :::"is_monomorphism"::: ) (Set (Var "U1")) "," (Set (Var "U2"))) ")" ) ")" )))); theorem :: MSUALG_3:13 (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "U1")) "," (Set (Var "U2")) "being" ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "F")) "being" ($#m2_pboole :::"ManySortedFunction":::) "of" (Set (Var "U1")) "," (Set (Var "U2")) "holds" (Bool "(" (Bool (Set (Var "F")) ($#r4_msualg_3 :::"is_isomorphism"::: ) (Set (Var "U1")) "," (Set (Var "U2"))) "iff" (Bool "(" (Bool (Set (Var "F")) ($#r1_msualg_3 :::"is_homomorphism"::: ) (Set (Var "U1")) "," (Set (Var "U2"))) & (Bool (Set (Var "F")) "is" ($#v2_msualg_3 :::""onto""::: ) ) & (Bool (Set (Var "F")) "is" ($#v1_msualg_3 :::""1-1""::: ) ) ")" ) ")" )))) ; theorem :: MSUALG_3:14 (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "U1")) "," (Set (Var "U2")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "H")) "being" ($#m2_pboole :::"ManySortedFunction":::) "of" (Set (Var "U1")) "," (Set (Var "U2")) (Bool "for" (Set (Var "H1")) "being" ($#m2_pboole :::"ManySortedFunction":::) "of" (Set (Var "U2")) "," (Set (Var "U1")) "st" (Bool (Bool (Set (Var "H")) ($#r4_msualg_3 :::"is_isomorphism"::: ) (Set (Var "U1")) "," (Set (Var "U2"))) & (Bool (Set (Var "H1")) ($#r8_pboole :::"="::: ) (Set (Set (Var "H")) ($#k4_msualg_3 :::""""::: ) ))) "holds" (Bool (Set (Var "H1")) ($#r4_msualg_3 :::"is_isomorphism"::: ) (Set (Var "U2")) "," (Set (Var "U1"))))))) ; theorem :: MSUALG_3:15 (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "U1")) "," (Set (Var "U2")) "," (Set (Var "U3")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "H")) "being" ($#m2_pboole :::"ManySortedFunction":::) "of" (Set (Var "U1")) "," (Set (Var "U2")) (Bool "for" (Set (Var "H1")) "being" ($#m2_pboole :::"ManySortedFunction":::) "of" (Set (Var "U2")) "," (Set (Var "U3")) "st" (Bool (Bool (Set (Var "H")) ($#r4_msualg_3 :::"is_isomorphism"::: ) (Set (Var "U1")) "," (Set (Var "U2"))) & (Bool (Set (Var "H1")) ($#r4_msualg_3 :::"is_isomorphism"::: ) (Set (Var "U2")) "," (Set (Var "U3")))) "holds" (Bool (Set (Set (Var "H1")) ($#k3_msualg_3 :::"**"::: ) (Set (Var "H"))) ($#r4_msualg_3 :::"is_isomorphism"::: ) (Set (Var "U1")) "," (Set (Var "U3"))))))) ; definitionlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; let "U1", "U2" be ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Const "S")); pred "U1" "," "U2" :::"are_isomorphic"::: means :: MSUALG_3:def 11 (Bool "ex" (Set (Var "F")) "being" ($#m2_pboole :::"ManySortedFunction":::) "of" "U1" "," "U2" "st" (Bool (Set (Var "F")) ($#r4_msualg_3 :::"is_isomorphism"::: ) "U1" "," "U2")); end; :: deftheorem defines :::"are_isomorphic"::: MSUALG_3:def 11 : (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "U1")) "," (Set (Var "U2")) "being" ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "U1")) "," (Set (Var "U2")) ($#r5_msualg_3 :::"are_isomorphic"::: ) ) "iff" (Bool "ex" (Set (Var "F")) "being" ($#m2_pboole :::"ManySortedFunction":::) "of" (Set (Var "U1")) "," (Set (Var "U2")) "st" (Bool (Set (Var "F")) ($#r4_msualg_3 :::"is_isomorphism"::: ) (Set (Var "U1")) "," (Set (Var "U2")))) ")" ))); theorem :: MSUALG_3:16 (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "U1")) "being" ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) "holds" (Bool "(" (Bool (Set ($#k2_msualg_3 :::"id"::: ) (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "U1")))) ($#r4_msualg_3 :::"is_isomorphism"::: ) (Set (Var "U1")) "," (Set (Var "U1"))) & (Bool (Set (Var "U1")) "," (Set (Var "U1")) ($#r5_msualg_3 :::"are_isomorphic"::: ) ) ")" ))) ; definitionlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; let "U1", "U2" be ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Const "S")); :: original: :::"are_isomorphic"::: redefine pred "U1" "," "U2" :::"are_isomorphic"::: ; reflexivity (Bool "for" (Set (Var "U1")) "being" ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Const "S")) "holds" (Bool ((Set (Const "S")) "," (Set (Var "b1")) "," (Set (Var "b1"))))) ; end; theorem :: MSUALG_3:17 (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "U1")) "," (Set (Var "U2")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) "st" (Bool (Bool (Set (Var "U1")) "," (Set (Var "U2")) ($#r6_msualg_3 :::"are_isomorphic"::: ) )) "holds" (Bool (Set (Var "U2")) "," (Set (Var "U1")) ($#r6_msualg_3 :::"are_isomorphic"::: ) ))) ; theorem :: MSUALG_3:18 (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "U1")) "," (Set (Var "U2")) "," (Set (Var "U3")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) "st" (Bool (Bool (Set (Var "U1")) "," (Set (Var "U2")) ($#r6_msualg_3 :::"are_isomorphic"::: ) ) & (Bool (Set (Var "U2")) "," (Set (Var "U3")) ($#r6_msualg_3 :::"are_isomorphic"::: ) )) "holds" (Bool (Set (Var "U1")) "," (Set (Var "U3")) ($#r6_msualg_3 :::"are_isomorphic"::: ) ))) ; definitionlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; let "U1", "U2" be ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Const "S")); let "F" be ($#m2_pboole :::"ManySortedFunction":::) "of" (Set (Const "U1")) "," (Set (Const "U2")); assume (Bool (Set (Const "F")) ($#r1_msualg_3 :::"is_homomorphism"::: ) (Set (Const "U1")) "," (Set (Const "U2"))) ; func :::"Image"::: "F" -> ($#v3_msualg_1 :::"strict"::: ) ($#v4_msualg_1 :::"non-empty"::: ) ($#m1_msualg_2 :::"MSSubAlgebra"::: ) "of" "U2" means :: MSUALG_3:def 12 (Bool (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" it) ($#r8_pboole :::"="::: ) (Set "F" ($#k9_pboole :::".:.:"::: ) (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" "U1"))); end; :: deftheorem defines :::"Image"::: MSUALG_3:def 12 : (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "U1")) "," (Set (Var "U2")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "F")) "being" ($#m2_pboole :::"ManySortedFunction":::) "of" (Set (Var "U1")) "," (Set (Var "U2")) "st" (Bool (Bool (Set (Var "F")) ($#r1_msualg_3 :::"is_homomorphism"::: ) (Set (Var "U1")) "," (Set (Var "U2")))) "holds" (Bool "for" (Set (Var "b5")) "being" ($#v3_msualg_1 :::"strict"::: ) ($#v4_msualg_1 :::"non-empty"::: ) ($#m1_msualg_2 :::"MSSubAlgebra"::: ) "of" (Set (Var "U2")) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k6_msualg_3 :::"Image"::: ) (Set (Var "F")))) "iff" (Bool (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "b5"))) ($#r8_pboole :::"="::: ) (Set (Set (Var "F")) ($#k9_pboole :::".:.:"::: ) (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "U1"))))) ")" ))))); theorem :: MSUALG_3:19 (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "U1")) "," (Set (Var "U2")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "F")) "being" ($#m2_pboole :::"ManySortedFunction":::) "of" (Set (Var "U1")) "," (Set (Var "U2")) "st" (Bool (Bool (Set (Var "F")) ($#r1_msualg_3 :::"is_homomorphism"::: ) (Set (Var "U1")) "," (Set (Var "U2")))) "holds" (Bool "(" (Bool (Set (Var "F")) ($#r2_msualg_3 :::"is_epimorphism"::: ) (Set (Var "U1")) "," (Set (Var "U2"))) "iff" (Bool (Set ($#k6_msualg_3 :::"Image"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#g3_msualg_1 :::"MSAlgebra"::: ) "(#" (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "U2"))) "," (Set "the" ($#u4_msualg_1 :::"Charact"::: ) "of" (Set (Var "U2"))) "#)" )) ")" )))) ; theorem :: MSUALG_3:20 (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "U1")) "," (Set (Var "U2")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "F")) "being" ($#m2_pboole :::"ManySortedFunction":::) "of" (Set (Var "U1")) "," (Set (Var "U2")) (Bool "for" (Set (Var "G")) "being" ($#m2_pboole :::"ManySortedFunction":::) "of" (Set (Var "U1")) "," (Set "(" ($#k6_msualg_3 :::"Image"::: ) (Set (Var "F")) ")" ) "st" (Bool (Bool (Set (Var "F")) ($#r8_pboole :::"="::: ) (Set (Var "G"))) & (Bool (Set (Var "F")) ($#r1_msualg_3 :::"is_homomorphism"::: ) (Set (Var "U1")) "," (Set (Var "U2")))) "holds" (Bool (Set (Var "G")) ($#r2_msualg_3 :::"is_epimorphism"::: ) (Set (Var "U1")) "," (Set ($#k6_msualg_3 :::"Image"::: ) (Set (Var "F")))))))) ; theorem :: MSUALG_3:21 (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "U1")) "," (Set (Var "U2")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "F")) "being" ($#m2_pboole :::"ManySortedFunction":::) "of" (Set (Var "U1")) "," (Set (Var "U2")) "st" (Bool (Bool (Set (Var "F")) ($#r1_msualg_3 :::"is_homomorphism"::: ) (Set (Var "U1")) "," (Set (Var "U2")))) "holds" (Bool "ex" (Set (Var "G")) "being" ($#m2_pboole :::"ManySortedFunction":::) "of" (Set (Var "U1")) "," (Set "(" ($#k6_msualg_3 :::"Image"::: ) (Set (Var "F")) ")" ) "st" (Bool "(" (Bool (Set (Var "F")) ($#r8_pboole :::"="::: ) (Set (Var "G"))) & (Bool (Set (Var "G")) ($#r2_msualg_3 :::"is_epimorphism"::: ) (Set (Var "U1")) "," (Set ($#k6_msualg_3 :::"Image"::: ) (Set (Var "F")))) ")" ))))) ; theorem :: MSUALG_3:22 (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "U1")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "U2")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#m1_msualg_2 :::"MSSubAlgebra"::: ) "of" (Set (Var "U1")) (Bool "for" (Set (Var "G")) "being" ($#m2_pboole :::"ManySortedFunction":::) "of" (Set (Var "U2")) "," (Set (Var "U1")) "st" (Bool (Bool (Set (Var "G")) ($#r8_pboole :::"="::: ) (Set ($#k2_msualg_3 :::"id"::: ) (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "U2")))))) "holds" (Bool (Set (Var "G")) ($#r3_msualg_3 :::"is_monomorphism"::: ) (Set (Var "U2")) "," (Set (Var "U1"))))))) ; theorem :: MSUALG_3:23 (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "U1")) "," (Set (Var "U2")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "F")) "being" ($#m2_pboole :::"ManySortedFunction":::) "of" (Set (Var "U1")) "," (Set (Var "U2")) "st" (Bool (Bool (Set (Var "F")) ($#r1_msualg_3 :::"is_homomorphism"::: ) (Set (Var "U1")) "," (Set (Var "U2")))) "holds" (Bool "ex" (Set (Var "F1")) "being" ($#m2_pboole :::"ManySortedFunction":::) "of" (Set (Var "U1")) "," (Set "(" ($#k6_msualg_3 :::"Image"::: ) (Set (Var "F")) ")" )(Bool "ex" (Set (Var "F2")) "being" ($#m2_pboole :::"ManySortedFunction":::) "of" (Set "(" ($#k6_msualg_3 :::"Image"::: ) (Set (Var "F")) ")" ) "," (Set (Var "U2")) "st" (Bool "(" (Bool (Set (Var "F1")) ($#r2_msualg_3 :::"is_epimorphism"::: ) (Set (Var "U1")) "," (Set ($#k6_msualg_3 :::"Image"::: ) (Set (Var "F")))) & (Bool (Set (Var "F2")) ($#r3_msualg_3 :::"is_monomorphism"::: ) (Set ($#k6_msualg_3 :::"Image"::: ) (Set (Var "F"))) "," (Set (Var "U2"))) & (Bool (Set (Var "F")) ($#r8_pboole :::"="::: ) (Set (Set (Var "F2")) ($#k3_msualg_3 :::"**"::: ) (Set (Var "F1")))) ")" )))))) ; theorem :: MSUALG_3:24 (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "U1")) "," (Set (Var "U2")) "being" ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "F")) "being" ($#m2_pboole :::"ManySortedFunction":::) "of" (Set (Var "U1")) "," (Set (Var "U2")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_msualg_1 :::"Args"::: ) "(" (Set (Var "o")) "," (Set (Var "U1")) ")" ) (Bool "for" (Set (Var "f")) "," (Set (Var "u")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "f"))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k3_msualg_1 :::"Args"::: ) "(" (Set (Var "o")) "," (Set (Var "U1")) ")" )) & (Bool (Set (Var "u")) ($#r2_hidden :::"in"::: ) (Set ($#k3_msualg_1 :::"Args"::: ) "(" (Set (Var "o")) "," (Set (Var "U2")) ")" ))) "holds" (Bool "(" (Bool (Set (Var "u")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k5_msualg_3 :::"#"::: ) (Set (Var "x")))) "iff" (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "u")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "F")) ($#k1_msualg_3 :::"."::: ) (Set "(" (Set "(" ($#k1_msualg_1 :::"the_arity_of"::: ) (Set (Var "o")) ")" ) ($#k7_partfun1 :::"/."::: ) (Set (Var "n")) ")" ) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" )))) ")" ))))))) ;