:: MSALIMIT semantic presentation begin registrationlet "I" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; let "AF" be ($#m1_pralg_2 :::"MSAlgebra-Family"::: ) "of" (Set (Const "I")) "," (Set (Const "S")); let "i" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "I")); let "o" be ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Const "S")); cluster (Set (Set "(" (Set "(" ($#k11_pralg_2 :::"OPER"::: ) "AF" ")" ) ($#k1_funct_1 :::"."::: ) "i" ")" ) ($#k1_funct_1 :::"."::: ) "o") -> ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_funct_1 :::"Function-like"::: ) ; end; registrationlet "I" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; let "AF" be ($#m1_pralg_2 :::"MSAlgebra-Family"::: ) "of" (Set (Const "I")) "," (Set (Const "S")); let "s" be ($#m1_subset_1 :::"SortSymbol":::) "of" (Set (Const "S")); cluster (Set (Set "(" ($#k10_pralg_2 :::"SORTS"::: ) "AF" ")" ) ($#k1_funct_1 :::"."::: ) "s") -> ($#v4_funct_1 :::"functional"::: ) ; end; definitionlet "P" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::); let "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; mode :::"OrderedAlgFam"::: "of" "P" "," "S" -> ($#m1_pralg_2 :::"MSAlgebra-Family"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "P") "," "S" means :: MSALIMIT:def 1 (Bool "ex" (Set (Var "F")) "being" ($#m1_hidden :::"ManySortedFunction":::) "of" (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" "P") "st" (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "k")) "being" ($#m1_subset_1 :::"Element":::) "of" "P" "st" (Bool (Bool (Set (Var "i")) ($#r1_orders_2 :::">="::: ) (Set (Var "j"))) & (Bool (Set (Var "j")) ($#r1_orders_2 :::">="::: ) (Set (Var "k")))) "holds" (Bool "ex" (Set (Var "f1")) "being" ($#m2_pboole :::"ManySortedFunction":::) "of" (Set "(" it ($#k5_pralg_2 :::"."::: ) (Set (Var "i")) ")" ) "," (Set "(" it ($#k5_pralg_2 :::"."::: ) (Set (Var "j")) ")" )(Bool "ex" (Set (Var "f2")) "being" ($#m2_pboole :::"ManySortedFunction":::) "of" (Set "(" it ($#k5_pralg_2 :::"."::: ) (Set (Var "j")) ")" ) "," (Set "(" it ($#k5_pralg_2 :::"."::: ) (Set (Var "k")) ")" ) "st" (Bool "(" (Bool (Set (Var "f1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "j")) "," (Set (Var "i")) ")" )) & (Bool (Set (Var "f2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "k")) "," (Set (Var "j")) ")" )) & (Bool (Set (Set (Var "F")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "k")) "," (Set (Var "i")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "f2")) ($#k3_msualg_3 :::"**"::: ) (Set (Var "f1")))) & (Bool (Set (Var "f1")) ($#r1_msualg_3 :::"is_homomorphism"::: ) (Set it ($#k5_pralg_2 :::"."::: ) (Set (Var "i"))) "," (Set it ($#k5_pralg_2 :::"."::: ) (Set (Var "j")))) ")" ))))); end; :: deftheorem defines :::"OrderedAlgFam"::: MSALIMIT:def 1 : (Bool "for" (Set (Var "P")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (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 "b3")) "being" ($#m1_pralg_2 :::"MSAlgebra-Family"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "P"))) "," (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "b3")) "is" ($#m1_msalimit :::"OrderedAlgFam"::: ) "of" (Set (Var "P")) "," (Set (Var "S"))) "iff" (Bool "ex" (Set (Var "F")) "being" ($#m1_hidden :::"ManySortedFunction":::) "of" (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "P"))) "st" (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "k")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "P")) "st" (Bool (Bool (Set (Var "i")) ($#r1_orders_2 :::">="::: ) (Set (Var "j"))) & (Bool (Set (Var "j")) ($#r1_orders_2 :::">="::: ) (Set (Var "k")))) "holds" (Bool "ex" (Set (Var "f1")) "being" ($#m2_pboole :::"ManySortedFunction":::) "of" (Set "(" (Set (Var "b3")) ($#k5_pralg_2 :::"."::: ) (Set (Var "i")) ")" ) "," (Set "(" (Set (Var "b3")) ($#k5_pralg_2 :::"."::: ) (Set (Var "j")) ")" )(Bool "ex" (Set (Var "f2")) "being" ($#m2_pboole :::"ManySortedFunction":::) "of" (Set "(" (Set (Var "b3")) ($#k5_pralg_2 :::"."::: ) (Set (Var "j")) ")" ) "," (Set "(" (Set (Var "b3")) ($#k5_pralg_2 :::"."::: ) (Set (Var "k")) ")" ) "st" (Bool "(" (Bool (Set (Var "f1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "j")) "," (Set (Var "i")) ")" )) & (Bool (Set (Var "f2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "k")) "," (Set (Var "j")) ")" )) & (Bool (Set (Set (Var "F")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "k")) "," (Set (Var "i")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "f2")) ($#k3_msualg_3 :::"**"::: ) (Set (Var "f1")))) & (Bool (Set (Var "f1")) ($#r1_msualg_3 :::"is_homomorphism"::: ) (Set (Set (Var "b3")) ($#k5_pralg_2 :::"."::: ) (Set (Var "i"))) "," (Set (Set (Var "b3")) ($#k5_pralg_2 :::"."::: ) (Set (Var "j")))) ")" ))))) ")" )))); definitionlet "P" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::); let "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; let "OAF" be ($#m1_msalimit :::"OrderedAlgFam"::: ) "of" (Set (Const "P")) "," (Set (Const "S")); mode :::"Binding"::: "of" "OAF" -> ($#m1_hidden :::"ManySortedFunction":::) "of" (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" "P") means :: MSALIMIT:def 2 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "k")) "being" ($#m1_subset_1 :::"Element":::) "of" "P" "st" (Bool (Bool (Set (Var "i")) ($#r1_orders_2 :::">="::: ) (Set (Var "j"))) & (Bool (Set (Var "j")) ($#r1_orders_2 :::">="::: ) (Set (Var "k")))) "holds" (Bool "ex" (Set (Var "f1")) "being" ($#m2_pboole :::"ManySortedFunction":::) "of" (Set "(" "OAF" ($#k5_pralg_2 :::"."::: ) (Set (Var "i")) ")" ) "," (Set "(" "OAF" ($#k5_pralg_2 :::"."::: ) (Set (Var "j")) ")" )(Bool "ex" (Set (Var "f2")) "being" ($#m2_pboole :::"ManySortedFunction":::) "of" (Set "(" "OAF" ($#k5_pralg_2 :::"."::: ) (Set (Var "j")) ")" ) "," (Set "(" "OAF" ($#k5_pralg_2 :::"."::: ) (Set (Var "k")) ")" ) "st" (Bool "(" (Bool (Set (Var "f1")) ($#r1_hidden :::"="::: ) (Set it ($#k1_binop_1 :::"."::: ) "(" (Set (Var "j")) "," (Set (Var "i")) ")" )) & (Bool (Set (Var "f2")) ($#r1_hidden :::"="::: ) (Set it ($#k1_binop_1 :::"."::: ) "(" (Set (Var "k")) "," (Set (Var "j")) ")" )) & (Bool (Set it ($#k1_binop_1 :::"."::: ) "(" (Set (Var "k")) "," (Set (Var "i")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "f2")) ($#k3_msualg_3 :::"**"::: ) (Set (Var "f1")))) & (Bool (Set (Var "f1")) ($#r1_msualg_3 :::"is_homomorphism"::: ) (Set "OAF" ($#k5_pralg_2 :::"."::: ) (Set (Var "i"))) "," (Set "OAF" ($#k5_pralg_2 :::"."::: ) (Set (Var "j")))) ")" )))); end; :: deftheorem defines :::"Binding"::: MSALIMIT:def 2 : (Bool "for" (Set (Var "P")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (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 "OAF")) "being" ($#m1_msalimit :::"OrderedAlgFam"::: ) "of" (Set (Var "P")) "," (Set (Var "S")) (Bool "for" (Set (Var "b4")) "being" ($#m1_hidden :::"ManySortedFunction":::) "of" (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "P"))) "holds" (Bool "(" (Bool (Set (Var "b4")) "is" ($#m2_msalimit :::"Binding"::: ) "of" (Set (Var "OAF"))) "iff" (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "k")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "P")) "st" (Bool (Bool (Set (Var "i")) ($#r1_orders_2 :::">="::: ) (Set (Var "j"))) & (Bool (Set (Var "j")) ($#r1_orders_2 :::">="::: ) (Set (Var "k")))) "holds" (Bool "ex" (Set (Var "f1")) "being" ($#m2_pboole :::"ManySortedFunction":::) "of" (Set "(" (Set (Var "OAF")) ($#k5_pralg_2 :::"."::: ) (Set (Var "i")) ")" ) "," (Set "(" (Set (Var "OAF")) ($#k5_pralg_2 :::"."::: ) (Set (Var "j")) ")" )(Bool "ex" (Set (Var "f2")) "being" ($#m2_pboole :::"ManySortedFunction":::) "of" (Set "(" (Set (Var "OAF")) ($#k5_pralg_2 :::"."::: ) (Set (Var "j")) ")" ) "," (Set "(" (Set (Var "OAF")) ($#k5_pralg_2 :::"."::: ) (Set (Var "k")) ")" ) "st" (Bool "(" (Bool (Set (Var "f1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "b4")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "j")) "," (Set (Var "i")) ")" )) & (Bool (Set (Var "f2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "b4")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "k")) "," (Set (Var "j")) ")" )) & (Bool (Set (Set (Var "b4")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "k")) "," (Set (Var "i")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "f2")) ($#k3_msualg_3 :::"**"::: ) (Set (Var "f1")))) & (Bool (Set (Var "f1")) ($#r1_msualg_3 :::"is_homomorphism"::: ) (Set (Set (Var "OAF")) ($#k5_pralg_2 :::"."::: ) (Set (Var "i"))) "," (Set (Set (Var "OAF")) ($#k5_pralg_2 :::"."::: ) (Set (Var "j")))) ")" )))) ")" ))))); definitionlet "P" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::); let "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; let "OAF" be ($#m1_msalimit :::"OrderedAlgFam"::: ) "of" (Set (Const "P")) "," (Set (Const "S")); let "B" be ($#m2_msalimit :::"Binding"::: ) "of" (Set (Const "OAF")); let "i", "j" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "P")); assume (Bool (Set (Const "i")) ($#r1_orders_2 :::">="::: ) (Set (Const "j"))) ; func :::"bind"::: "(" "B" "," "i" "," "j" ")" -> ($#m2_pboole :::"ManySortedFunction":::) "of" (Set "(" "OAF" ($#k5_pralg_2 :::"."::: ) "i" ")" ) "," (Set "(" "OAF" ($#k5_pralg_2 :::"."::: ) "j" ")" ) equals :: MSALIMIT:def 3 (Set "B" ($#k1_binop_1 :::"."::: ) "(" "j" "," "i" ")" ); end; :: deftheorem defines :::"bind"::: MSALIMIT:def 3 : (Bool "for" (Set (Var "P")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (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 "OAF")) "being" ($#m1_msalimit :::"OrderedAlgFam"::: ) "of" (Set (Var "P")) "," (Set (Var "S")) (Bool "for" (Set (Var "B")) "being" ($#m2_msalimit :::"Binding"::: ) "of" (Set (Var "OAF")) (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "P")) "st" (Bool (Bool (Set (Var "i")) ($#r1_orders_2 :::">="::: ) (Set (Var "j")))) "holds" (Bool (Set ($#k1_msalimit :::"bind"::: ) "(" (Set (Var "B")) "," (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "B")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "j")) "," (Set (Var "i")) ")" ))))))); theorem :: MSALIMIT:1 (Bool "for" (Set (Var "P")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "k")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "P")) (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 "OAF")) "being" ($#m1_msalimit :::"OrderedAlgFam"::: ) "of" (Set (Var "P")) "," (Set (Var "S")) (Bool "for" (Set (Var "B")) "being" ($#m2_msalimit :::"Binding"::: ) "of" (Set (Var "OAF")) "st" (Bool (Bool (Set (Var "i")) ($#r1_orders_2 :::">="::: ) (Set (Var "j"))) & (Bool (Set (Var "j")) ($#r1_orders_2 :::">="::: ) (Set (Var "k")))) "holds" (Bool (Set (Set "(" ($#k1_msalimit :::"bind"::: ) "(" (Set (Var "B")) "," (Set (Var "j")) "," (Set (Var "k")) ")" ")" ) ($#k3_msualg_3 :::"**"::: ) (Set "(" ($#k1_msalimit :::"bind"::: ) "(" (Set (Var "B")) "," (Set (Var "i")) "," (Set (Var "j")) ")" ")" )) ($#r8_pboole :::"="::: ) (Set ($#k1_msalimit :::"bind"::: ) "(" (Set (Var "B")) "," (Set (Var "i")) "," (Set (Var "k")) ")" ))))))) ; definitionlet "P" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::); let "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; let "OAF" be ($#m1_msalimit :::"OrderedAlgFam"::: ) "of" (Set (Const "P")) "," (Set (Const "S")); let "IT" be ($#m2_msalimit :::"Binding"::: ) "of" (Set (Const "OAF")); attr "IT" is :::"normalized"::: means :: MSALIMIT:def 4 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element":::) "of" "P" "holds" (Bool (Set "IT" ($#k1_binop_1 :::"."::: ) "(" (Set (Var "i")) "," (Set (Var "i")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_msualg_3 :::"id"::: ) (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set "(" "OAF" ($#k5_pralg_2 :::"."::: ) (Set (Var "i")) ")" ))))); end; :: deftheorem defines :::"normalized"::: MSALIMIT:def 4 : (Bool "for" (Set (Var "P")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (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 "OAF")) "being" ($#m1_msalimit :::"OrderedAlgFam"::: ) "of" (Set (Var "P")) "," (Set (Var "S")) (Bool "for" (Set (Var "IT")) "being" ($#m2_msalimit :::"Binding"::: ) "of" (Set (Var "OAF")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v1_msalimit :::"normalized"::: ) ) "iff" (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "P")) "holds" (Bool (Set (Set (Var "IT")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "i")) "," (Set (Var "i")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_msualg_3 :::"id"::: ) (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set "(" (Set (Var "OAF")) ($#k5_pralg_2 :::"."::: ) (Set (Var "i")) ")" ))))) ")" ))))); theorem :: MSALIMIT:2 (Bool "for" (Set (Var "P")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (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 "OAF")) "being" ($#m1_msalimit :::"OrderedAlgFam"::: ) "of" (Set (Var "P")) "," (Set (Var "S")) (Bool "for" (Set (Var "B")) "being" ($#m2_msalimit :::"Binding"::: ) "of" (Set (Var "OAF")) (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "P")) "st" (Bool (Bool (Set (Var "i")) ($#r1_orders_2 :::">="::: ) (Set (Var "j")))) "holds" (Bool "for" (Set (Var "f")) "being" ($#m2_pboole :::"ManySortedFunction":::) "of" (Set "(" (Set (Var "OAF")) ($#k5_pralg_2 :::"."::: ) (Set (Var "i")) ")" ) "," (Set "(" (Set (Var "OAF")) ($#k5_pralg_2 :::"."::: ) (Set (Var "j")) ")" ) "st" (Bool (Bool (Set (Var "f")) ($#r8_pboole :::"="::: ) (Set ($#k1_msalimit :::"bind"::: ) "(" (Set (Var "B")) "," (Set (Var "i")) "," (Set (Var "j")) ")" ))) "holds" (Bool (Set (Var "f")) ($#r1_msualg_3 :::"is_homomorphism"::: ) (Set (Set (Var "OAF")) ($#k5_pralg_2 :::"."::: ) (Set (Var "i"))) "," (Set (Set (Var "OAF")) ($#k5_pralg_2 :::"."::: ) (Set (Var "j")))))))))) ; definitionlet "P" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::); let "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; let "OAF" be ($#m1_msalimit :::"OrderedAlgFam"::: ) "of" (Set (Const "P")) "," (Set (Const "S")); let "B" be ($#m2_msalimit :::"Binding"::: ) "of" (Set (Const "OAF")); func :::"Normalized"::: "B" -> ($#m2_msalimit :::"Binding"::: ) "of" "OAF" means :: MSALIMIT:def 5 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_subset_1 :::"Element":::) "of" "P" "st" (Bool (Bool (Set (Var "i")) ($#r1_orders_2 :::">="::: ) (Set (Var "j")))) "holds" (Bool (Set it ($#k1_binop_1 :::"."::: ) "(" (Set (Var "j")) "," (Set (Var "i")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k14_funcop_1 :::"IFEQ"::: ) "(" (Set (Var "j")) "," (Set (Var "i")) "," (Set "(" ($#k2_msualg_3 :::"id"::: ) (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set "(" "OAF" ($#k5_pralg_2 :::"."::: ) (Set (Var "i")) ")" )) ")" ) "," (Set "(" (Set "(" ($#k1_msalimit :::"bind"::: ) "(" "B" "," (Set (Var "i")) "," (Set (Var "j")) ")" ")" ) ($#k3_msualg_3 :::"**"::: ) (Set "(" ($#k2_msualg_3 :::"id"::: ) (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set "(" "OAF" ($#k5_pralg_2 :::"."::: ) (Set (Var "i")) ")" )) ")" ) ")" ) ")" ))); end; :: deftheorem defines :::"Normalized"::: MSALIMIT:def 5 : (Bool "for" (Set (Var "P")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (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 "OAF")) "being" ($#m1_msalimit :::"OrderedAlgFam"::: ) "of" (Set (Var "P")) "," (Set (Var "S")) (Bool "for" (Set (Var "B")) "," (Set (Var "b5")) "being" ($#m2_msalimit :::"Binding"::: ) "of" (Set (Var "OAF")) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k2_msalimit :::"Normalized"::: ) (Set (Var "B")))) "iff" (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "P")) "st" (Bool (Bool (Set (Var "i")) ($#r1_orders_2 :::">="::: ) (Set (Var "j")))) "holds" (Bool (Set (Set (Var "b5")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "j")) "," (Set (Var "i")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k14_funcop_1 :::"IFEQ"::: ) "(" (Set (Var "j")) "," (Set (Var "i")) "," (Set "(" ($#k2_msualg_3 :::"id"::: ) (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set "(" (Set (Var "OAF")) ($#k5_pralg_2 :::"."::: ) (Set (Var "i")) ")" )) ")" ) "," (Set "(" (Set "(" ($#k1_msalimit :::"bind"::: ) "(" (Set (Var "B")) "," (Set (Var "i")) "," (Set (Var "j")) ")" ")" ) ($#k3_msualg_3 :::"**"::: ) (Set "(" ($#k2_msualg_3 :::"id"::: ) (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set "(" (Set (Var "OAF")) ($#k5_pralg_2 :::"."::: ) (Set (Var "i")) ")" )) ")" ) ")" ) ")" ))) ")" ))))); theorem :: MSALIMIT:3 (Bool "for" (Set (Var "P")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (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 "OAF")) "being" ($#m1_msalimit :::"OrderedAlgFam"::: ) "of" (Set (Var "P")) "," (Set (Var "S")) (Bool "for" (Set (Var "B")) "being" ($#m2_msalimit :::"Binding"::: ) "of" (Set (Var "OAF")) (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "P")) "st" (Bool (Bool (Set (Var "i")) ($#r1_orders_2 :::">="::: ) (Set (Var "j"))) & (Bool (Set (Var "i")) ($#r1_hidden :::"<>"::: ) (Set (Var "j")))) "holds" (Bool (Set (Set (Var "B")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "j")) "," (Set (Var "i")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_msalimit :::"Normalized"::: ) (Set (Var "B")) ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "j")) "," (Set (Var "i")) ")" ))))))) ; registrationlet "P" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::); let "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; let "OAF" be ($#m1_msalimit :::"OrderedAlgFam"::: ) "of" (Set (Const "P")) "," (Set (Const "S")); let "B" be ($#m2_msalimit :::"Binding"::: ) "of" (Set (Const "OAF")); cluster (Set ($#k2_msalimit :::"Normalized"::: ) "B") -> ($#v1_msalimit :::"normalized"::: ) ; end; registrationlet "P" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::); let "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; let "OAF" be ($#m1_msalimit :::"OrderedAlgFam"::: ) "of" (Set (Const "P")) "," (Set (Const "S")); cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" "P") ($#v4_relat_1 :::"-defined"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_partfun1 :::"total"::: ) ($#v1_funcop_1 :::"Function-yielding"::: ) bbbadV2_FUNCOP_1() ($#v1_msalimit :::"normalized"::: ) for ($#m2_msalimit :::"Binding"::: ) "of" "OAF"; end; theorem :: MSALIMIT:4 (Bool "for" (Set (Var "P")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (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 "OAF")) "being" ($#m1_msalimit :::"OrderedAlgFam"::: ) "of" (Set (Var "P")) "," (Set (Var "S")) (Bool "for" (Set (Var "NB")) "being" ($#v1_msalimit :::"normalized"::: ) ($#m2_msalimit :::"Binding"::: ) "of" (Set (Var "OAF")) (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "P")) "st" (Bool (Bool (Set (Var "i")) ($#r1_orders_2 :::">="::: ) (Set (Var "j")))) "holds" (Bool (Set (Set "(" ($#k2_msalimit :::"Normalized"::: ) (Set (Var "NB")) ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "j")) "," (Set (Var "i")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "NB")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "j")) "," (Set (Var "i")) ")" ))))))) ; definitionlet "P" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::); let "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; let "OAF" be ($#m1_msalimit :::"OrderedAlgFam"::: ) "of" (Set (Const "P")) "," (Set (Const "S")); let "B" be ($#m2_msalimit :::"Binding"::: ) "of" (Set (Const "OAF")); func :::"InvLim"::: "B" -> ($#v3_msualg_1 :::"strict"::: ) ($#m1_msualg_2 :::"MSSubAlgebra"::: ) "of" (Set ($#k14_pralg_2 :::"product"::: ) "OAF") means :: MSALIMIT:def 6 (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"SortSymbol":::) "of" "S" (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set "(" ($#k10_pralg_2 :::"SORTS"::: ) "OAF" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "s"))) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" it) ($#k1_funct_1 :::"."::: ) (Set (Var "s")))) "iff" (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_subset_1 :::"Element":::) "of" "P" "st" (Bool (Bool (Set (Var "i")) ($#r1_orders_2 :::">="::: ) (Set (Var "j")))) "holds" (Bool (Set (Set "(" (Set "(" ($#k1_msalimit :::"bind"::: ) "(" "B" "," (Set (Var "i")) "," (Set (Var "j")) ")" ")" ) ($#k1_msualg_3 :::"."::: ) (Set (Var "s")) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "j"))))) ")" ))); end; :: deftheorem defines :::"InvLim"::: MSALIMIT:def 6 : (Bool "for" (Set (Var "P")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (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 "OAF")) "being" ($#m1_msalimit :::"OrderedAlgFam"::: ) "of" (Set (Var "P")) "," (Set (Var "S")) (Bool "for" (Set (Var "B")) "being" ($#m2_msalimit :::"Binding"::: ) "of" (Set (Var "OAF")) (Bool "for" (Set (Var "b5")) "being" ($#v3_msualg_1 :::"strict"::: ) ($#m1_msualg_2 :::"MSSubAlgebra"::: ) "of" (Set ($#k14_pralg_2 :::"product"::: ) (Set (Var "OAF"))) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k3_msalimit :::"InvLim"::: ) (Set (Var "B")))) "iff" (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"SortSymbol":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set "(" ($#k10_pralg_2 :::"SORTS"::: ) (Set (Var "OAF")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "s"))) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "b5"))) ($#k1_funct_1 :::"."::: ) (Set (Var "s")))) "iff" (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "P")) "st" (Bool (Bool (Set (Var "i")) ($#r1_orders_2 :::">="::: ) (Set (Var "j")))) "holds" (Bool (Set (Set "(" (Set "(" ($#k1_msalimit :::"bind"::: ) "(" (Set (Var "B")) "," (Set (Var "i")) "," (Set (Var "j")) ")" ")" ) ($#k1_msualg_3 :::"."::: ) (Set (Var "s")) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "j"))))) ")" ))) ")" )))))); theorem :: MSALIMIT:5 (Bool "for" (Set (Var "DP")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_orders_3 :::"discrete"::: ) ($#l1_orders_2 :::"Poset":::) (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 "OAF")) "being" ($#m1_msalimit :::"OrderedAlgFam"::: ) "of" (Set (Var "DP")) "," (Set (Var "S")) (Bool "for" (Set (Var "B")) "being" ($#v1_msalimit :::"normalized"::: ) ($#m2_msalimit :::"Binding"::: ) "of" (Set (Var "OAF")) "holds" (Bool (Set ($#k3_msalimit :::"InvLim"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set ($#k14_pralg_2 :::"product"::: ) (Set (Var "OAF")))))))) ; begin definitionlet "X" be ($#m1_hidden :::"set"::: ) ; attr "X" is :::"MSS-membered"::: means :: MSALIMIT:def 7 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) "X")) "holds" (Bool (Set (Var "x")) "is" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v1_msualg_1 :::"strict"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) )); end; :: deftheorem defines :::"MSS-membered"::: MSALIMIT:def 7 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v2_msalimit :::"MSS-membered"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Var "x")) "is" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v1_msualg_1 :::"strict"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) )) ")" )); registration cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_msalimit :::"MSS-membered"::: ) for ($#m1_hidden :::"set"::: ) ; end; definitionfunc :::"TrivialMSSign"::: -> ($#v1_msualg_1 :::"strict"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) means :: MSALIMIT:def 8 (Bool "(" (Bool it "is" ($#v2_struct_0 :::"empty"::: ) ) & (Bool it "is" ($#v11_struct_0 :::"void"::: ) ) ")" ); end; :: deftheorem defines :::"TrivialMSSign"::: MSALIMIT:def 8 : (Bool "for" (Set (Var "b1")) "being" ($#v1_msualg_1 :::"strict"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k4_msalimit :::"TrivialMSSign"::: ) )) "iff" (Bool "(" (Bool (Set (Var "b1")) "is" ($#v2_struct_0 :::"empty"::: ) ) & (Bool (Set (Var "b1")) "is" ($#v11_struct_0 :::"void"::: ) ) ")" ) ")" )); registration cluster (Set ($#k4_msalimit :::"TrivialMSSign"::: ) ) -> ($#v2_struct_0 :::"empty"::: ) ($#v11_struct_0 :::"void"::: ) ($#v1_msualg_1 :::"strict"::: ) ; end; registration cluster ($#v2_struct_0 :::"empty"::: ) ($#v11_struct_0 :::"void"::: ) ($#v1_msualg_1 :::"strict"::: ) for ($#l1_msualg_1 :::"ManySortedSign"::: ) ; end; theorem :: MSALIMIT:6 (Bool "for" (Set (Var "S")) "being" ($#v11_struct_0 :::"void"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) "holds" (Bool (Set ($#k6_partfun1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S")))) "," (Set ($#k6_partfun1 :::"id"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "S")))) ($#r3_pua2mss1 :::"form_morphism_between"::: ) (Set (Var "S")) "," (Set (Var "S")))) ; definitionlet "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; func :::"MSS_set"::: "A" -> ($#m1_hidden :::"set"::: ) means :: MSALIMIT:def 9 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "ex" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v1_msualg_1 :::"strict"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "S"))) & (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) ($#r1_tarski :::"c="::: ) "A") & (Bool (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "S"))) ($#r1_tarski :::"c="::: ) "A") ")" )) ")" )); end; :: deftheorem defines :::"MSS_set"::: MSALIMIT:def 9 : (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b2")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k5_msalimit :::"MSS_set"::: ) (Set (Var "A")))) "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 "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v1_msualg_1 :::"strict"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "S"))) & (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) ($#r1_tarski :::"c="::: ) (Set (Var "A"))) & (Bool (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "S"))) ($#r1_tarski :::"c="::: ) (Set (Var "A"))) ")" )) ")" )) ")" ))); registrationlet "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k5_msalimit :::"MSS_set"::: ) "A") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_msalimit :::"MSS-membered"::: ) ; end; definitionlet "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_msalimit :::"MSS-membered"::: ) ($#m1_hidden :::"set"::: ) ; :: original: :::"Element"::: redefine mode :::"Element"::: "of" "A" -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v1_msualg_1 :::"strict"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; end; definitionlet "S1", "S2" be ($#l1_msualg_1 :::"ManySortedSign"::: ) ; func :::"MSS_morph"::: "(" "S1" "," "S2" ")" -> ($#m1_hidden :::"set"::: ) means :: MSALIMIT:def 10 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "ex" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "f")) "," (Set (Var "g")) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Var "f")) "," (Set (Var "g")) ($#r3_pua2mss1 :::"form_morphism_between"::: ) "S1" "," "S2") ")" )) ")" )); end; :: deftheorem defines :::"MSS_morph"::: MSALIMIT:def 10 : (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "being" ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "b3")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k6_msalimit :::"MSS_morph"::: ) "(" (Set (Var "S1")) "," (Set (Var "S2")) ")" )) "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 "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "f")) "," (Set (Var "g")) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Var "f")) "," (Set (Var "g")) ($#r3_pua2mss1 :::"form_morphism_between"::: ) (Set (Var "S1")) "," (Set (Var "S2"))) ")" )) ")" )) ")" )));