:: MSINST_1  semantic presentation begin  








definitionlet "A" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; func  :::"MSSCat"::: "A" ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v6_altcat_1 :::"strict"::: )     ($#l2_altcat_1 :::"AltCatStr"::: )   means :: MSINST_1:def 1 (Bool  "("  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" it)  ($#r1_hidden :::"="::: )  (Set   ($#k5_msalimit :::"MSS_set"::: )  "A")) & (Bool  "("   "for" (Set (Var "i")) "," (Set (Var "j")) "being"    ($#m3_msalimit :::"Element"::: )   "of" (Set   ($#k5_msalimit :::"MSS_set"::: )  "A") "holds"  (Bool (Set (Set  "the"  ($#u1_altcat_1 :::"Arrows"::: )  "of" it)  ($#k1_binop_1 :::"."::: )   "(" (Set (Var "i")) "," (Set (Var "j")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k6_msalimit :::"MSS_morph"::: )   "(" (Set (Var "i")) "," (Set (Var "j")) ")" ))  ")" ) & (Bool  "("   "for" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "k")) "being"   ($#m1_subset_1 :::"object":::) "of" it  "st" (Bool (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k5_msalimit :::"MSS_set"::: )  "A")) & (Bool (Set (Var "j"))  ($#r2_hidden :::"in"::: )  (Set   ($#k5_msalimit :::"MSS_set"::: )  "A")) & (Bool (Set (Var "k"))  ($#r2_hidden :::"in"::: )  (Set   ($#k5_msalimit :::"MSS_set"::: )  "A"))) "holds"  (Bool  "for" (Set (Var "f1")) "," (Set (Var "f2")) "," (Set (Var "g1")) "," (Set (Var "g2")) "being"   ($#m1_hidden :::"Function":::)  "st" (Bool (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "f1")) "," (Set (Var "f2")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set (Set  "the"  ($#u1_altcat_1 :::"Arrows"::: )  "of" it)  ($#k1_binop_1 :::"."::: )   "(" (Set (Var "i")) "," (Set (Var "j")) ")" )) & (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "g1")) "," (Set (Var "g2")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set (Set  "the"  ($#u1_altcat_1 :::"Arrows"::: )  "of" it)  ($#k1_binop_1 :::"."::: )   "(" (Set (Var "j")) "," (Set (Var "k")) ")" ))) "holds"  (Bool (Set (Set  "(" (Set  "the"  ($#u2_altcat_1 :::"Comp"::: )  "of" it)  ($#k4_altcat_1 :::"."::: )   "(" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "k")) ")"  ")" )  ($#k1_binop_1 :::"."::: )   "(" (Set  ($#k4_tarski :::"["::: ) (Set (Var "g1")) "," (Set (Var "g2")) ($#k4_tarski :::"]"::: ) ) "," (Set  ($#k4_tarski :::"["::: ) (Set (Var "f1")) "," (Set (Var "f2")) ($#k4_tarski :::"]"::: ) ) ")" )  ($#r1_hidden :::"="::: )  (Set  ($#k4_tarski :::"["::: ) (Set  "(" (Set (Var "g1"))  ($#k3_relat_1 :::"*"::: )  (Set (Var "f1")) ")" ) "," (Set  "(" (Set (Var "g2"))  ($#k3_relat_1 :::"*"::: )  (Set (Var "f2")) ")" ) ($#k4_tarski :::"]"::: ) )))  ")" )  ")" ); end; 





:: deftheorem    defines :::"MSSCat"::: MSINST_1:def 1 :  (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "b2")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v6_altcat_1 :::"strict"::: )     ($#l2_altcat_1 :::"AltCatStr"::: )   "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_msinst_1 :::"MSSCat"::: )  (Set (Var "A")))) "iff" (Bool  "("  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "b2")))  ($#r1_hidden :::"="::: )  (Set   ($#k5_msalimit :::"MSS_set"::: )  (Set (Var "A")))) & (Bool  "("   "for" (Set (Var "i")) "," (Set (Var "j")) "being"    ($#m3_msalimit :::"Element"::: )   "of" (Set   ($#k5_msalimit :::"MSS_set"::: )  (Set (Var "A"))) "holds"  (Bool (Set (Set  "the"  ($#u1_altcat_1 :::"Arrows"::: )  "of" (Set (Var "b2")))  ($#k1_binop_1 :::"."::: )   "(" (Set (Var "i")) "," (Set (Var "j")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k6_msalimit :::"MSS_morph"::: )   "(" (Set (Var "i")) "," (Set (Var "j")) ")" ))  ")" ) & (Bool  "("   "for" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "k")) "being"   ($#m1_subset_1 :::"object":::) "of" (Set (Var "b2"))  "st" (Bool (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k5_msalimit :::"MSS_set"::: )  (Set (Var "A")))) & (Bool (Set (Var "j"))  ($#r2_hidden :::"in"::: )  (Set   ($#k5_msalimit :::"MSS_set"::: )  (Set (Var "A")))) & (Bool (Set (Var "k"))  ($#r2_hidden :::"in"::: )  (Set   ($#k5_msalimit :::"MSS_set"::: )  (Set (Var "A"))))) "holds"  (Bool  "for" (Set (Var "f1")) "," (Set (Var "f2")) "," (Set (Var "g1")) "," (Set (Var "g2")) "being"   ($#m1_hidden :::"Function":::)  "st" (Bool (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "f1")) "," (Set (Var "f2")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set (Set  "the"  ($#u1_altcat_1 :::"Arrows"::: )  "of" (Set (Var "b2")))  ($#k1_binop_1 :::"."::: )   "(" (Set (Var "i")) "," (Set (Var "j")) ")" )) & (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "g1")) "," (Set (Var "g2")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set (Set  "the"  ($#u1_altcat_1 :::"Arrows"::: )  "of" (Set (Var "b2")))  ($#k1_binop_1 :::"."::: )   "(" (Set (Var "j")) "," (Set (Var "k")) ")" ))) "holds"  (Bool (Set (Set  "(" (Set  "the"  ($#u2_altcat_1 :::"Comp"::: )  "of" (Set (Var "b2")))  ($#k4_altcat_1 :::"."::: )   "(" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "k")) ")"  ")" )  ($#k1_binop_1 :::"."::: )   "(" (Set  ($#k4_tarski :::"["::: ) (Set (Var "g1")) "," (Set (Var "g2")) ($#k4_tarski :::"]"::: ) ) "," (Set  ($#k4_tarski :::"["::: ) (Set (Var "f1")) "," (Set (Var "f2")) ($#k4_tarski :::"]"::: ) ) ")" )  ($#r1_hidden :::"="::: )  (Set  ($#k4_tarski :::"["::: ) (Set  "(" (Set (Var "g1"))  ($#k3_relat_1 :::"*"::: )  (Set (Var "f1")) ")" ) "," (Set  "(" (Set (Var "g2"))  ($#k3_relat_1 :::"*"::: )  (Set (Var "f2")) ")" ) ($#k4_tarski :::"]"::: ) )))  ")" )  ")" )  ")" ))); 
 registrationlet "A" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; 
cluster (Set   ($#k1_msinst_1 :::"MSSCat"::: )  "A") ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v2_altcat_1 :::"transitive"::: )     ($#v6_altcat_1 :::"strict"::: )     ($#v11_altcat_1 :::"associative"::: )     ($#v12_altcat_1 :::"with_units"::: )   ; 
end; 
theorem :: MSINST_1:1 (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "C")) "being"   ($#l2_altcat_1 :::"category":::)  "st" (Bool (Bool (Set (Var "C"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_msinst_1 :::"MSSCat"::: )  (Set (Var "A"))))) "holds"  (Bool  "for" (Set (Var "o")) "being"   ($#m1_subset_1 :::"object":::) "of" (Set (Var "C")) "holds"  (Bool (Set (Var "o")) "is"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )    ($#l1_msualg_1 :::"ManySortedSign"::: )  )))) ; 
 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"::: )     ($#v1_msualg_6 :::"feasible"::: )    for    ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" "S"; 
end; definitionlet "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_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; func  :::"MSAlg_set":::  "(" "S" "," "A" ")"  ->    ($#m1_hidden :::"set"::: )   means :: MSINST_1:def 2 (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  it) "iff" (Bool  "ex" (Set (Var "M")) "being"   ($#v3_msualg_1 :::"strict"::: )     ($#v1_msualg_6 :::"feasible"::: )     ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" "S" "st"  (Bool  "("  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Var "M"))) & (Bool  "("   "for" (Set (Var "C")) "being"   ($#m1_subset_1 :::"Component":::) "of" (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" (Set (Var "M"))) "holds"  (Bool (Set (Var "C"))  ($#r1_tarski :::"c="::: )  "A")  ")" )  ")" ))  ")" )); end; 






:: deftheorem    defines :::"MSAlg_set"::: MSINST_1:def 2 :  (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 "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "b3")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_msinst_1 :::"MSAlg_set"::: )   "(" (Set (Var "S")) "," (Set (Var "A")) ")" )) "iff" (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "b3"))) "iff" (Bool  "ex" (Set (Var "M")) "being"   ($#v3_msualg_1 :::"strict"::: )     ($#v1_msualg_6 :::"feasible"::: )     ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Var "S")) "st"  (Bool  "("  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Var "M"))) & (Bool  "("   "for" (Set (Var "C")) "being"   ($#m1_subset_1 :::"Component":::) "of" (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" (Set (Var "M"))) "holds"  (Bool (Set (Var "C"))  ($#r1_tarski :::"c="::: )  (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 "A" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; 
cluster (Set   ($#k2_msinst_1 :::"MSAlg_set"::: )   "(" "S" "," "A" ")" ) ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )  ; 
end; begin  



theorem :: MSINST_1:2 (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (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 "x")) "being"    ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Var "S"))  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_msinst_1 :::"MSAlg_set"::: )   "(" (Set (Var "S")) "," (Set (Var "A")) ")" ))) "holds"  (Bool  "("  (Bool (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" (Set (Var "x")))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_funct_2 :::"Funcs"::: )   "(" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S"))) "," (Set  "("  ($#k1_zfmisc_1 :::"bool"::: )  (Set (Var "A")) ")" ) ")" )) & (Bool (Set  "the"  ($#u4_msualg_1 :::"Charact"::: )  "of" (Set (Var "x")))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_funct_2 :::"Funcs"::: )   "(" (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set (Var "S"))) "," (Set  "("  ($#k4_partfun1 :::"PFuncs"::: )   "(" (Set  "("  ($#k4_partfun1 :::"PFuncs"::: )   "(" (Set  ($#k5_numbers :::"NAT"::: ) ) "," (Set (Var "A")) ")"  ")" ) "," (Set (Var "A")) ")"  ")" ) ")" ))  ")" )))) ; 
 
theorem :: MSINST_1:3 (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")) "being"    ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Var "S"))  "st" (Bool (Bool (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" (Set (Var "U1")))  ($#r1_pzfmisc1 :::"is_transformable_to"::: )  (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" (Set (Var "U2")))) & (Bool (Set   ($#k3_msualg_1 :::"Args"::: )   "(" (Set (Var "o")) "," (Set (Var "U1")) ")" )  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) "holds"  (Bool (Set   ($#k3_msualg_1 :::"Args"::: )   "(" (Set (Var "o")) "," (Set (Var "U2")) ")" )  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))))) ; 
 
theorem :: MSINST_1:4 (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"   ($#v1_msualg_6 :::"feasible"::: )     ($#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"))  (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  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" (Set (Var "U1")))  ($#r1_pzfmisc1 :::"is_transformable_to"::: )  (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" (Set (Var "U2")))) & (Bool (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" (Set (Var "U2")))  ($#r1_pzfmisc1 :::"is_transformable_to"::: )  (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" (Set (Var "U3"))))) "holds"  (Bool  "ex" (Set (Var "GF")) "being"   ($#m2_pboole :::"ManySortedFunction":::) "of" (Set (Var "U1")) "," (Set (Var "U3")) "st"  (Bool  "("  (Bool (Set (Var "GF"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "G"))  ($#k8_pboole :::"**"::: )  (Set (Var "F")))) & (Bool (Set (Set (Var "GF"))  ($#k5_msualg_3 :::"#"::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "G"))  ($#k5_msualg_3 :::"#"::: )  (Set  "(" (Set (Var "F"))  ($#k5_msualg_3 :::"#"::: )  (Set (Var "x")) ")" )))  ")" )))))))) ; 
 
theorem :: MSINST_1: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")) "," (Set (Var "U3")) "being"   ($#v1_msualg_6 :::"feasible"::: )     ($#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  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" (Set (Var "U1")))  ($#r1_pzfmisc1 :::"is_transformable_to"::: )  (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" (Set (Var "U2")))) & (Bool (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" (Set (Var "U2")))  ($#r1_pzfmisc1 :::"is_transformable_to"::: )  (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" (Set (Var "U3")))) & (Bool (Set (Var "F"))  ($#r1_msualg_3 :::"is_homomorphism"::: )  (Set (Var "U1")) "," (Set (Var "U2"))) & (Bool (Set (Var "G"))  ($#r1_msualg_3 :::"is_homomorphism"::: )  (Set (Var "U2")) "," (Set (Var "U3")))) "holds"  (Bool  "ex" (Set (Var "GF")) "being"   ($#m2_pboole :::"ManySortedFunction":::) "of" (Set (Var "U1")) "," (Set (Var "U3")) "st"  (Bool  "("  (Bool (Set (Var "GF"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "G"))  ($#k8_pboole :::"**"::: )  (Set (Var "F")))) & (Bool (Set (Var "GF"))  ($#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 "A" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; let "i", "j" be    ($#m1_hidden :::"set"::: )  ; assume that  
(Bool (Set (Const "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_msinst_1 :::"MSAlg_set"::: )   "(" (Set (Const "S")) "," (Set (Const "A")) ")" ))
 and  
(Bool (Set (Const "j"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_msinst_1 :::"MSAlg_set"::: )   "(" (Set (Const "S")) "," (Set (Const "A")) ")" ))
 ; func  :::"MSAlg_morph":::  "(" "S" "," "A" "," "i" "," "j" ")"  ->    ($#m1_hidden :::"set"::: )   means :: MSINST_1:def 3 (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  it) "iff" (Bool  "ex" (Set (Var "M")) "," (Set (Var "N")) "being"   ($#v3_msualg_1 :::"strict"::: )     ($#v1_msualg_6 :::"feasible"::: )     ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" "S"(Bool  "ex" (Set (Var "f")) "being"   ($#m2_pboole :::"ManySortedFunction":::) "of" (Set (Var "M")) "," (Set (Var "N")) "st"  (Bool  "("  (Bool (Set (Var "M"))  ($#r1_hidden :::"="::: )  "i") & (Bool (Set (Var "N"))  ($#r1_hidden :::"="::: )  "j") & (Bool (Set (Var "f"))  ($#r1_hidden :::"="::: )  (Set (Var "x"))) & (Bool (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" (Set (Var "M")))  ($#r1_pzfmisc1 :::"is_transformable_to"::: )  (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" (Set (Var "N")))) & (Bool (Set (Var "f"))  ($#r1_msualg_3 :::"is_homomorphism"::: )  (Set (Var "M")) "," (Set (Var "N")))  ")" )))  ")" )); end; 









:: deftheorem    defines :::"MSAlg_morph"::: MSINST_1:def 3 :  (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 "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "i")) "," (Set (Var "j")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_msinst_1 :::"MSAlg_set"::: )   "(" (Set (Var "S")) "," (Set (Var "A")) ")" )) & (Bool (Set (Var "j"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_msinst_1 :::"MSAlg_set"::: )   "(" (Set (Var "S")) "," (Set (Var "A")) ")" ))) "holds"  (Bool  "for" (Set (Var "b5")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "b5"))  ($#r1_hidden :::"="::: )  (Set   ($#k3_msinst_1 :::"MSAlg_morph"::: )   "(" (Set (Var "S")) "," (Set (Var "A")) "," (Set (Var "i")) "," (Set (Var "j")) ")" )) "iff" (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "b5"))) "iff" (Bool  "ex" (Set (Var "M")) "," (Set (Var "N")) "being"   ($#v3_msualg_1 :::"strict"::: )     ($#v1_msualg_6 :::"feasible"::: )     ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Var "S"))(Bool  "ex" (Set (Var "f")) "being"   ($#m2_pboole :::"ManySortedFunction":::) "of" (Set (Var "M")) "," (Set (Var "N")) "st"  (Bool  "("  (Bool (Set (Var "M"))  ($#r1_hidden :::"="::: )  (Set (Var "i"))) & (Bool (Set (Var "N"))  ($#r1_hidden :::"="::: )  (Set (Var "j"))) & (Bool (Set (Var "f"))  ($#r1_hidden :::"="::: )  (Set (Var "x"))) & (Bool (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" (Set (Var "M")))  ($#r1_pzfmisc1 :::"is_transformable_to"::: )  (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" (Set (Var "N")))) & (Bool (Set (Var "f"))  ($#r1_msualg_3 :::"is_homomorphism"::: )  (Set (Var "M")) "," (Set (Var "N")))  ")" )))  ")" ))  ")" ))))); 
 definitionlet "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_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; func  :::"MSAlgCat":::  "(" "S" "," "A" ")"  ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v6_altcat_1 :::"strict"::: )     ($#l2_altcat_1 :::"AltCatStr"::: )   means :: MSINST_1:def 4 (Bool  "("  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" it)  ($#r1_hidden :::"="::: )  (Set   ($#k2_msinst_1 :::"MSAlg_set"::: )   "(" "S" "," "A" ")" )) & (Bool  "("   "for" (Set (Var "i")) "," (Set (Var "j")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_msinst_1 :::"MSAlg_set"::: )   "(" "S" "," "A" ")" ) "holds"  (Bool (Set (Set  "the"  ($#u1_altcat_1 :::"Arrows"::: )  "of" it)  ($#k1_binop_1 :::"."::: )   "(" (Set (Var "i")) "," (Set (Var "j")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k3_msinst_1 :::"MSAlg_morph"::: )   "(" "S" "," "A" "," (Set (Var "i")) "," (Set (Var "j")) ")" ))  ")" ) & (Bool  "("   "for" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "k")) "being"   ($#m1_subset_1 :::"object":::) "of" it  (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#v1_funcop_1 :::"Function-yielding"::: )    ($#m1_hidden :::"Function":::)  "st" (Bool (Bool (Set (Var "f"))  ($#r2_hidden :::"in"::: )  (Set (Set  "the"  ($#u1_altcat_1 :::"Arrows"::: )  "of" it)  ($#k1_binop_1 :::"."::: )   "(" (Set (Var "i")) "," (Set (Var "j")) ")" )) & (Bool (Set (Var "g"))  ($#r2_hidden :::"in"::: )  (Set (Set  "the"  ($#u1_altcat_1 :::"Arrows"::: )  "of" it)  ($#k1_binop_1 :::"."::: )   "(" (Set (Var "j")) "," (Set (Var "k")) ")" ))) "holds"  (Bool (Set (Set  "(" (Set  "the"  ($#u2_altcat_1 :::"Comp"::: )  "of" it)  ($#k4_altcat_1 :::"."::: )   "(" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "k")) ")"  ")" )  ($#k1_binop_1 :::"."::: )   "(" (Set (Var "g")) "," (Set (Var "f")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "g"))  ($#k8_pboole :::"**"::: )  (Set (Var "f")))))  ")" )  ")" ); end; 






:: deftheorem    defines :::"MSAlgCat"::: MSINST_1:def 4 :  (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 "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "b3")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v6_altcat_1 :::"strict"::: )     ($#l2_altcat_1 :::"AltCatStr"::: )   "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_msinst_1 :::"MSAlgCat"::: )   "(" (Set (Var "S")) "," (Set (Var "A")) ")" )) "iff" (Bool  "("  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "b3")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_msinst_1 :::"MSAlg_set"::: )   "(" (Set (Var "S")) "," (Set (Var "A")) ")" )) & (Bool  "("   "for" (Set (Var "i")) "," (Set (Var "j")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_msinst_1 :::"MSAlg_set"::: )   "(" (Set (Var "S")) "," (Set (Var "A")) ")" ) "holds"  (Bool (Set (Set  "the"  ($#u1_altcat_1 :::"Arrows"::: )  "of" (Set (Var "b3")))  ($#k1_binop_1 :::"."::: )   "(" (Set (Var "i")) "," (Set (Var "j")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k3_msinst_1 :::"MSAlg_morph"::: )   "(" (Set (Var "S")) "," (Set (Var "A")) "," (Set (Var "i")) "," (Set (Var "j")) ")" ))  ")" ) & (Bool  "("   "for" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "k")) "being"   ($#m1_subset_1 :::"object":::) "of" (Set (Var "b3"))  (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#v1_funcop_1 :::"Function-yielding"::: )    ($#m1_hidden :::"Function":::)  "st" (Bool (Bool (Set (Var "f"))  ($#r2_hidden :::"in"::: )  (Set (Set  "the"  ($#u1_altcat_1 :::"Arrows"::: )  "of" (Set (Var "b3")))  ($#k1_binop_1 :::"."::: )   "(" (Set (Var "i")) "," (Set (Var "j")) ")" )) & (Bool (Set (Var "g"))  ($#r2_hidden :::"in"::: )  (Set (Set  "the"  ($#u1_altcat_1 :::"Arrows"::: )  "of" (Set (Var "b3")))  ($#k1_binop_1 :::"."::: )   "(" (Set (Var "j")) "," (Set (Var "k")) ")" ))) "holds"  (Bool (Set (Set  "(" (Set  "the"  ($#u2_altcat_1 :::"Comp"::: )  "of" (Set (Var "b3")))  ($#k4_altcat_1 :::"."::: )   "(" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "k")) ")"  ")" )  ($#k1_binop_1 :::"."::: )   "(" (Set (Var "g")) "," (Set (Var "f")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "g"))  ($#k8_pboole :::"**"::: )  (Set (Var "f")))))  ")" )  ")" )  ")" )))); 
 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_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; 
cluster (Set   ($#k4_msinst_1 :::"MSAlgCat"::: )   "(" "S" "," "A" ")" ) ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v2_altcat_1 :::"transitive"::: )     ($#v6_altcat_1 :::"strict"::: )     ($#v11_altcat_1 :::"associative"::: )     ($#v12_altcat_1 :::"with_units"::: )   ; 
end; 
theorem :: MSINST_1:6 (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (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 "C")) "being"   ($#l2_altcat_1 :::"category":::)  "st" (Bool (Bool (Set (Var "C"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_msinst_1 :::"MSAlgCat"::: )   "(" (Set (Var "S")) "," (Set (Var "A")) ")" ))) "holds"  (Bool  "for" (Set (Var "o")) "being"   ($#m1_subset_1 :::"object":::) "of" (Set (Var "C")) "holds"  (Bool (Set (Var "o")) "is"   ($#v3_msualg_1 :::"strict"::: )     ($#v1_msualg_6 :::"feasible"::: )     ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Var "S"))))))) ;