:: EQUATION semantic presentation begin theorem :: EQUATION:1 (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "B")) "," (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set (Var "B")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "B")) "," (Set (Var "C")) "st" (Bool (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set "(" (Set (Var "g")) ($#k1_partfun1 :::"*"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "C")))) "holds" (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set (Var "C"))))))) ; theorem :: EQUATION:2 (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 "B")) "," (Set (Var "C")) "being" bbbadV2_RELAT_1() ($#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")) "st" (Bool (Bool (Set (Set (Var "g")) ($#k3_msualg_3 :::"**"::: ) (Set (Var "f"))) "is" ($#v2_msualg_3 :::""onto""::: ) )) "holds" (Bool (Set (Var "g")) "is" ($#v2_msualg_3 :::""onto""::: ) )))))) ; theorem :: EQUATION:3 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k1_funct_2 :::"Funcs"::: ) "(" (Set (Var "A")) "," (Set "(" ($#k1_funct_2 :::"Funcs"::: ) "(" (Set (Var "B")) "," (Set (Var "C")) ")" ")" ) ")" )) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "B")))) "holds" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set "(" ($#k10_funct_6 :::"commute"::: ) (Set (Var "f")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "y")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "A"))) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" (Set "(" ($#k10_funct_6 :::"commute"::: ) (Set (Var "f")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "y")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Var "C"))) ")" )))) ; theorem :: EQUATION: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")) "st" (Bool (Bool (Set (Var "A")) ($#r1_pzfmisc1 :::"is_transformable_to"::: ) (Set (Var "B")))) "holds" (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"ManySortedFunction":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set ($#k2_funct_6 :::"doms"::: ) (Set (Var "f"))) ($#r6_pboole :::"="::: ) (Set (Var "A"))) & (Bool (Set ($#k3_funct_6 :::"rngs"::: ) (Set (Var "f"))) ($#r2_pboole :::"c="::: ) (Set (Var "B")))) "holds" (Bool (Set (Var "f")) "is" ($#m2_pboole :::"ManySortedFunction"::: ) "of" (Set (Var "A")) "," (Set (Var "B")))))) ; theorem :: EQUATION:5 (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")) (Bool "for" (Set (Var "C")) "," (Set (Var "E")) "being" ($#m3_pboole :::"ManySortedSubset"::: ) "of" (Set (Var "A")) (Bool "for" (Set (Var "D")) "being" ($#m3_pboole :::"ManySortedSubset"::: ) "of" (Set (Var "C")) "st" (Bool (Bool (Set (Var "E")) ($#r6_pboole :::"="::: ) (Set (Var "D")))) "holds" (Bool (Set (Set "(" (Set (Var "F")) ($#k1_msafree :::"||"::: ) (Set (Var "C")) ")" ) ($#k1_msafree :::"||"::: ) (Set (Var "D"))) ($#r6_pboole :::"="::: ) (Set (Set (Var "F")) ($#k1_msafree :::"||"::: ) (Set (Var "E"))))))))) ; theorem :: EQUATION:6 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "B")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "C")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "A")) "being" ($#m3_pboole :::"ManySortedSubset"::: ) "of" (Set (Var "C")) (Bool "for" (Set (Var "F")) "being" ($#m2_pboole :::"ManySortedFunction"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) (Bool "ex" (Set (Var "G")) "being" ($#m2_pboole :::"ManySortedFunction"::: ) "of" (Set (Var "C")) "," (Set (Var "B")) "st" (Bool (Set (Set (Var "G")) ($#k1_msafree :::"||"::: ) (Set (Var "A"))) ($#r6_pboole :::"="::: ) (Set (Var "F"))))))))) ; definitionlet "I" be ($#m1_hidden :::"set"::: ) ; let "A" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); let "F" be ($#m1_hidden :::"ManySortedFunction":::) "of" (Set (Const "I")); func "F" :::""""::: "A" -> ($#m1_hidden :::"ManySortedSet":::) "of" "I" means :: EQUATION: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 (Set "(" "F" ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k8_relat_1 :::"""::: ) (Set "(" "A" ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" )))); end; :: deftheorem defines :::""""::: EQUATION: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 "F")) "being" ($#m1_hidden :::"ManySortedFunction":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "b4")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_equation :::""""::: ) (Set (Var "A")))) "iff" (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set (Var "I")))) "holds" (Bool (Set (Set (Var "b4")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k8_relat_1 :::"""::: ) (Set "(" (Set (Var "A")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" )))) ")" ))))); theorem :: EQUATION:7 (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")) "holds" (Bool (Set (Set (Var "F")) ($#k9_pboole :::".:.:"::: ) (Set (Var "C"))) "is" ($#m3_pboole :::"ManySortedSubset"::: ) "of" (Set (Var "B")))))) ; theorem :: EQUATION:8 (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")) "holds" (Bool (Set (Set (Var "F")) ($#k1_equation :::""""::: ) (Set (Var "C"))) "is" ($#m3_pboole :::"ManySortedSubset"::: ) "of" (Set (Var "A")))))) ; theorem :: EQUATION:9 (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" ($#v2_msualg_3 :::""onto""::: ) )) "holds" (Bool (Set (Set (Var "F")) ($#k9_pboole :::".:.:"::: ) (Set (Var "A"))) ($#r6_pboole :::"="::: ) (Set (Var "B")))))) ; theorem :: EQUATION:10 (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 "A")) ($#r1_pzfmisc1 :::"is_transformable_to"::: ) (Set (Var "B")))) "holds" (Bool (Set (Set (Var "F")) ($#k1_equation :::""""::: ) (Set (Var "B"))) ($#r6_pboole :::"="::: ) (Set (Var "A")))))) ; theorem :: EQUATION:11 (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 "F")) "being" ($#m1_hidden :::"ManySortedFunction":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Var "A")) ($#r2_pboole :::"c="::: ) (Set ($#k3_funct_6 :::"rngs"::: ) (Set (Var "F"))))) "holds" (Bool (Set (Set (Var "F")) ($#k9_pboole :::".:.:"::: ) (Set "(" (Set (Var "F")) ($#k1_equation :::""""::: ) (Set (Var "A")) ")" )) ($#r6_pboole :::"="::: ) (Set (Var "A")))))) ; theorem :: EQUATION:12 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"ManySortedFunction":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool (Set (Set (Var "f")) ($#k9_pboole :::".:.:"::: ) (Set (Var "X"))) ($#r2_pboole :::"c="::: ) (Set ($#k3_funct_6 :::"rngs"::: ) (Set (Var "f"))))))) ; theorem :: EQUATION:13 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"ManySortedFunction":::) "of" (Set (Var "I")) "holds" (Bool (Set (Set (Var "f")) ($#k9_pboole :::".:.:"::: ) (Set "(" ($#k2_funct_6 :::"doms"::: ) (Set (Var "f")) ")" )) ($#r6_pboole :::"="::: ) (Set ($#k3_funct_6 :::"rngs"::: ) (Set (Var "f")))))) ; theorem :: EQUATION:14 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"ManySortedFunction":::) "of" (Set (Var "I")) "holds" (Bool (Set (Set (Var "f")) ($#k1_equation :::""""::: ) (Set "(" ($#k3_funct_6 :::"rngs"::: ) (Set (Var "f")) ")" )) ($#r6_pboole :::"="::: ) (Set ($#k2_funct_6 :::"doms"::: ) (Set (Var "f")))))) ; theorem :: EQUATION:15 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool (Set (Set "(" ($#k2_msualg_3 :::"id"::: ) (Set (Var "A")) ")" ) ($#k9_pboole :::".:.:"::: ) (Set (Var "A"))) ($#r6_pboole :::"="::: ) (Set (Var "A"))))) ; theorem :: EQUATION:16 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool (Set (Set "(" ($#k2_msualg_3 :::"id"::: ) (Set (Var "A")) ")" ) ($#k1_equation :::""""::: ) (Set (Var "A"))) ($#r6_pboole :::"="::: ) (Set (Var "A"))))) ; begin theorem :: EQUATION: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 "A")) "being" ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) "holds" (Bool (Set (Var "A")) "is" ($#m1_msualg_2 :::"MSSubAlgebra"::: ) "of" (Set ($#g3_msualg_1 :::"MSAlgebra"::: ) "(#" (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "A"))) "," (Set "the" ($#u4_msualg_1 :::"Charact"::: ) "of" (Set (Var "A"))) "#)" )))) ; theorem :: EQUATION: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 "U0")) "being" ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "A")) "being" ($#m1_msualg_2 :::"MSSubAlgebra"::: ) "of" (Set (Var "U0")) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k3_msualg_1 :::"Args"::: ) "(" (Set (Var "o")) "," (Set (Var "A")) ")" ))) "holds" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k3_msualg_1 :::"Args"::: ) "(" (Set (Var "o")) "," (Set (Var "U0")) ")" ))))))) ; theorem :: EQUATION: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 "U0")) "being" ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "A")) "being" ($#m1_msualg_2 :::"MSSubAlgebra"::: ) "of" (Set (Var "U0")) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k3_msualg_1 :::"Args"::: ) "(" (Set (Var "o")) "," (Set (Var "A")) ")" ))) "holds" (Bool (Set (Set "(" ($#k5_msualg_1 :::"Den"::: ) "(" (Set (Var "o")) "," (Set (Var "A")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_msualg_1 :::"Den"::: ) "(" (Set (Var "o")) "," (Set (Var "U0")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))))))))) ; theorem :: EQUATION:20 (Bool "for" (Set (Var "I")) "being" ($#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 "F")) "being" ($#m1_pralg_2 :::"MSAlgebra-Family"::: ) "of" (Set (Var "I")) "," (Set (Var "S")) (Bool "for" (Set (Var "B")) "being" ($#m1_msualg_2 :::"MSSubAlgebra"::: ) "of" (Set ($#k14_pralg_2 :::"product"::: ) (Set (Var "F"))) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k3_msualg_1 :::"Args"::: ) "(" (Set (Var "o")) "," (Set (Var "B")) ")" ))) "holds" (Bool "(" (Bool (Set (Set "(" ($#k5_msualg_1 :::"Den"::: ) "(" (Set (Var "o")) "," (Set (Var "B")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) "is" ($#m1_hidden :::"Function":::)) & (Bool (Set (Set "(" ($#k5_msualg_1 :::"Den"::: ) "(" (Set (Var "o")) "," (Set "(" ($#k14_pralg_2 :::"product"::: ) (Set (Var "F")) ")" ) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) "is" ($#m1_hidden :::"Function":::)) ")" ))))))) ; 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 ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Const "S")); let "B" be ($#m1_msualg_2 :::"MSSubAlgebra"::: ) "of" (Set (Const "A")); func :::"SuperAlgebraSet"::: "B" -> ($#m1_hidden :::"set"::: ) means :: EQUATION: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 "C")) "being" ($#v3_msualg_1 :::"strict"::: ) ($#m1_msualg_2 :::"MSSubAlgebra"::: ) "of" "A" "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "C"))) & (Bool "B" "is" ($#m1_msualg_2 :::"MSSubAlgebra"::: ) "of" (Set (Var "C"))) ")" )) ")" )); end; :: deftheorem defines :::"SuperAlgebraSet"::: EQUATION: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" ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "B")) "being" ($#m1_msualg_2 :::"MSSubAlgebra"::: ) "of" (Set (Var "A")) (Bool "for" (Set (Var "b4")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k2_equation :::"SuperAlgebraSet"::: ) (Set (Var "B")))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "b4"))) "iff" (Bool "ex" (Set (Var "C")) "being" ($#v3_msualg_1 :::"strict"::: ) ($#m1_msualg_2 :::"MSSubAlgebra"::: ) "of" (Set (Var "A")) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "C"))) & (Bool (Set (Var "B")) "is" ($#m1_msualg_2 :::"MSSubAlgebra"::: ) "of" (Set (Var "C"))) ")" )) ")" )) ")" ))))); 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 ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Const "S")); let "B" be ($#m1_msualg_2 :::"MSSubAlgebra"::: ) "of" (Set (Const "A")); cluster (Set ($#k2_equation :::"SuperAlgebraSet"::: ) "B") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; registrationlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; cluster ($#v3_msualg_1 :::"strict"::: ) ($#v4_msualg_1 :::"non-empty"::: ) ($#v2_msafree :::"free"::: ) for ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" "S"; end; registrationlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; let "A" be ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Const "S")); let "X" be bbbadV2_RELAT_1() bbbadV2_FINSET_1() ($#m3_pboole :::"MSSubset":::) "of" (Set (Const "A")); cluster (Set ($#k12_msualg_2 :::"GenMSAlg"::: ) "X") -> ($#v3_msafree2 :::"finitely-generated"::: ) ; end; registrationlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; let "A" be ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Const "S")); cluster ($#v3_msualg_1 :::"strict"::: ) ($#v4_msualg_1 :::"non-empty"::: ) ($#v3_msafree2 :::"finitely-generated"::: ) for ($#m1_msualg_2 :::"MSSubAlgebra"::: ) "of" "A"; end; registrationlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; let "A" be ($#v1_msualg_6 :::"feasible"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Const "S")); cluster ($#v1_msualg_6 :::"feasible"::: ) for ($#m1_msualg_2 :::"MSSubAlgebra"::: ) "of" "A"; end; theorem :: EQUATION: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 "U0")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "A")) "being" ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "C")) "being" ($#m1_msualg_2 :::"MSSubAlgebra"::: ) "of" (Set (Var "A")) (Bool "for" (Set (Var "D")) "being" ($#m3_pboole :::"ManySortedSubset"::: ) "of" (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "A"))) "st" (Bool (Bool (Set (Var "D")) ($#r8_pboole :::"="::: ) (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "C"))))) "holds" (Bool "for" (Set (Var "h")) "being" ($#m2_pboole :::"ManySortedFunction":::) "of" (Set (Var "A")) "," (Set (Var "U0")) (Bool "for" (Set (Var "g")) "being" ($#m2_pboole :::"ManySortedFunction":::) "of" (Set (Var "C")) "," (Set (Var "U0")) "st" (Bool (Bool (Set (Var "g")) ($#r8_pboole :::"="::: ) (Set (Set (Var "h")) ($#k1_msafree :::"||"::: ) (Set (Var "D"))))) "holds" (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_msualg_1 :::"Args"::: ) "(" (Set (Var "o")) "," (Set (Var "A")) ")" ) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_msualg_1 :::"Args"::: ) "(" (Set (Var "o")) "," (Set (Var "C")) ")" ) "st" (Bool (Bool (Set ($#k3_msualg_1 :::"Args"::: ) "(" (Set (Var "o")) "," (Set (Var "C")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y")))) "holds" (Bool (Set (Set (Var "h")) ($#k5_msualg_3 :::"#"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k5_msualg_3 :::"#"::: ) (Set (Var "y")))))))))))))) ; theorem :: EQUATION: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 "U0")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "A")) "being" ($#v1_msualg_6 :::"feasible"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "C")) "being" ($#v1_msualg_6 :::"feasible"::: ) ($#m1_msualg_2 :::"MSSubAlgebra"::: ) "of" (Set (Var "A")) (Bool "for" (Set (Var "D")) "being" ($#m3_pboole :::"ManySortedSubset"::: ) "of" (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "A"))) "st" (Bool (Bool (Set (Var "D")) ($#r8_pboole :::"="::: ) (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "C"))))) "holds" (Bool "for" (Set (Var "h")) "being" ($#m2_pboole :::"ManySortedFunction":::) "of" (Set (Var "A")) "," (Set (Var "U0")) "st" (Bool (Bool (Set (Var "h")) ($#r1_msualg_3 :::"is_homomorphism"::: ) (Set (Var "A")) "," (Set (Var "U0")))) "holds" (Bool "for" (Set (Var "g")) "being" ($#m2_pboole :::"ManySortedFunction":::) "of" (Set (Var "C")) "," (Set (Var "U0")) "st" (Bool (Bool (Set (Var "g")) ($#r8_pboole :::"="::: ) (Set (Set (Var "h")) ($#k1_msafree :::"||"::: ) (Set (Var "D"))))) "holds" (Bool (Set (Var "g")) ($#r1_msualg_3 :::"is_homomorphism"::: ) (Set (Var "C")) "," (Set (Var "U0")))))))))) ; theorem :: EQUATION: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 "U0")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "B")) "being" ($#v3_msualg_1 :::"strict"::: ) ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "G")) "being" ($#m1_msafree :::"GeneratorSet"::: ) "of" (Set (Var "U0")) (Bool "for" (Set (Var "H")) "being" bbbadV2_RELAT_1() ($#m1_msafree :::"GeneratorSet"::: ) "of" (Set (Var "B")) (Bool "for" (Set (Var "f")) "being" ($#m2_pboole :::"ManySortedFunction":::) "of" (Set (Var "U0")) "," (Set (Var "B")) "st" (Bool (Bool (Set (Var "H")) ($#r2_pboole :::"c="::: ) (Set (Set (Var "f")) ($#k9_pboole :::".:.:"::: ) (Set (Var "G")))) & (Bool (Set (Var "f")) ($#r1_msualg_3 :::"is_homomorphism"::: ) (Set (Var "U0")) "," (Set (Var "B")))) "holds" (Bool (Set (Var "f")) ($#r2_msualg_3 :::"is_epimorphism"::: ) (Set (Var "U0")) "," (Set (Var "B"))))))))) ; theorem :: EQUATION: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 "U0")) "," (Set (Var "U1")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "W")) "being" ($#v3_msualg_1 :::"strict"::: ) ($#v4_msualg_1 :::"non-empty"::: ) ($#v2_msafree :::"free"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "F")) "being" ($#m2_pboole :::"ManySortedFunction":::) "of" (Set (Var "U0")) "," (Set (Var "U1")) "st" (Bool (Bool (Set (Var "F")) ($#r2_msualg_3 :::"is_epimorphism"::: ) (Set (Var "U0")) "," (Set (Var "U1")))) "holds" (Bool "for" (Set (Var "G")) "being" ($#m2_pboole :::"ManySortedFunction":::) "of" (Set (Var "W")) "," (Set (Var "U1")) "st" (Bool (Bool (Set (Var "G")) ($#r1_msualg_3 :::"is_homomorphism"::: ) (Set (Var "W")) "," (Set (Var "U1")))) "holds" (Bool "ex" (Set (Var "H")) "being" ($#m2_pboole :::"ManySortedFunction":::) "of" (Set (Var "W")) "," (Set (Var "U0")) "st" (Bool "(" (Bool (Set (Var "H")) ($#r1_msualg_3 :::"is_homomorphism"::: ) (Set (Var "W")) "," (Set (Var "U0"))) & (Bool (Set (Var "G")) ($#r8_pboole :::"="::: ) (Set (Set (Var "F")) ($#k3_msualg_3 :::"**"::: ) (Set (Var "H")))) ")" ))))))) ; theorem :: EQUATION:25 (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 "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "F")) "being" ($#m1_pralg_2 :::"MSAlgebra-Family"::: ) "of" (Set (Var "I")) "," (Set (Var "S")) "st" (Bool (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "I")) (Bool "ex" (Set (Var "C")) "being" ($#v3_msualg_1 :::"strict"::: ) ($#v4_msualg_1 :::"non-empty"::: ) ($#v3_msafree2 :::"finitely-generated"::: ) ($#m1_msualg_2 :::"MSSubAlgebra"::: ) "of" (Set (Var "A")) "st" (Bool (Set (Var "C")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k5_pralg_2 :::"."::: ) (Set (Var "i"))))) ")" )) "holds" (Bool "ex" (Set (Var "B")) "being" ($#v3_msualg_1 :::"strict"::: ) ($#v4_msualg_1 :::"non-empty"::: ) ($#v3_msafree2 :::"finitely-generated"::: ) ($#m1_msualg_2 :::"MSSubAlgebra"::: ) "of" (Set (Var "A")) "st" (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "I")) "holds" (Bool (Set (Set (Var "F")) ($#k5_pralg_2 :::"."::: ) (Set (Var "i"))) "is" ($#m1_msualg_2 :::"MSSubAlgebra"::: ) "of" (Set (Var "B"))))))))) ; theorem :: EQUATION:26 (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 "U0")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#v3_msualg_1 :::"strict"::: ) ($#v4_msualg_1 :::"non-empty"::: ) ($#v3_msafree2 :::"finitely-generated"::: ) ($#m1_msualg_2 :::"MSSubAlgebra"::: ) "of" (Set (Var "U0")) (Bool "ex" (Set (Var "M")) "being" ($#v3_msualg_1 :::"strict"::: ) ($#v4_msualg_1 :::"non-empty"::: ) ($#v3_msafree2 :::"finitely-generated"::: ) ($#m1_msualg_2 :::"MSSubAlgebra"::: ) "of" (Set (Var "U0")) "st" (Bool "(" (Bool (Set (Var "A")) "is" ($#m1_msualg_2 :::"MSSubAlgebra"::: ) "of" (Set (Var "M"))) & (Bool (Set (Var "B")) "is" ($#m1_msualg_2 :::"MSSubAlgebra"::: ) "of" (Set (Var "M"))) ")" ))))) ; theorem :: EQUATION:27 (Bool "for" (Set (Var "SG")) "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 "AG")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "SG")) (Bool "for" (Set (Var "C")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "C")) ($#r1_hidden :::"="::: ) "{" (Set (Var "A")) where A "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k14_msualg_2 :::"MSSub"::: ) (Set (Var "AG"))) : (Bool "ex" (Set (Var "R")) "being" ($#v3_msualg_1 :::"strict"::: ) ($#v4_msualg_1 :::"non-empty"::: ) ($#v3_msafree2 :::"finitely-generated"::: ) ($#m1_msualg_2 :::"MSSubAlgebra"::: ) "of" (Set (Var "AG")) "st" (Bool (Set (Var "R")) ($#r1_hidden :::"="::: ) (Set (Var "A")))) "}" )) "holds" (Bool "for" (Set (Var "F")) "being" ($#m1_pralg_2 :::"MSAlgebra-Family"::: ) "of" (Set (Var "C")) "," (Set (Var "SG")) "st" (Bool (Bool "(" "for" (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set (Var "C")))) "holds" (Bool (Set (Var "c")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "c")))) ")" )) "holds" (Bool "ex" (Set (Var "PS")) "being" ($#v3_msualg_1 :::"strict"::: ) ($#v4_msualg_1 :::"non-empty"::: ) ($#m1_msualg_2 :::"MSSubAlgebra"::: ) "of" (Set ($#k14_pralg_2 :::"product"::: ) (Set (Var "F")))(Bool "ex" (Set (Var "BA")) "being" ($#m2_pboole :::"ManySortedFunction":::) "of" (Set (Var "PS")) "," (Set (Var "AG")) "st" (Bool (Set (Var "BA")) ($#r2_msualg_3 :::"is_epimorphism"::: ) (Set (Var "PS")) "," (Set (Var "AG"))))))))) ; theorem :: EQUATION:28 (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 "U0")) "being" ($#v2_msafree :::"free"::: ) ($#v1_msualg_6 :::"feasible"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "A")) "being" ($#v1_msafree :::"free"::: ) ($#m1_msafree :::"GeneratorSet"::: ) "of" (Set (Var "U0")) (Bool "for" (Set (Var "Z")) "being" ($#m3_pboole :::"MSSubset":::) "of" (Set (Var "U0")) "st" (Bool (Bool (Set (Var "Z")) ($#r2_pboole :::"c="::: ) (Set (Var "A"))) & (Bool (Set ($#k12_msualg_2 :::"GenMSAlg"::: ) (Set (Var "Z"))) "is" ($#v1_msualg_6 :::"feasible"::: ) )) "holds" (Bool (Set ($#k12_msualg_2 :::"GenMSAlg"::: ) (Set (Var "Z"))) "is" ($#v2_msafree :::"free"::: ) ))))) ; begin definitionlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; func :::"TermAlg"::: "S" -> ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" "S" equals :: EQUATION:def 3 (Set ($#k11_msafree :::"FreeMSA"::: ) (Set "(" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S") ($#k8_funcop_1 :::"-->"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ")" )); end; :: deftheorem defines :::"TermAlg"::: EQUATION: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"::: ) "holds" (Bool (Set ($#k3_equation :::"TermAlg"::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) (Set ($#k11_msafree :::"FreeMSA"::: ) (Set "(" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) ($#k8_funcop_1 :::"-->"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ")" )))); registrationlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; cluster (Set ($#k3_equation :::"TermAlg"::: ) "S") -> ($#v3_msualg_1 :::"strict"::: ) ($#v4_msualg_1 :::"non-empty"::: ) ($#v2_msafree :::"free"::: ) ; end; definitionlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; func :::"Equations"::: "S" -> ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S") equals :: EQUATION:def 4 (Set ($#k6_pboole :::"[|"::: ) (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set "(" ($#k3_equation :::"TermAlg"::: ) "S" ")" )) "," (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set "(" ($#k3_equation :::"TermAlg"::: ) "S" ")" )) ($#k6_pboole :::"|]"::: ) ); end; :: deftheorem defines :::"Equations"::: EQUATION: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"::: ) "holds" (Bool (Set ($#k4_equation :::"Equations"::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) (Set ($#k6_pboole :::"[|"::: ) (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set "(" ($#k3_equation :::"TermAlg"::: ) (Set (Var "S")) ")" )) "," (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set "(" ($#k3_equation :::"TermAlg"::: ) (Set (Var "S")) ")" )) ($#k6_pboole :::"|]"::: ) ))); registrationlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; cluster (Set ($#k4_equation :::"Equations"::: ) "S") -> bbbadV2_RELAT_1() ; end; definitionlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; mode EqualSet of "S" is ($#m3_pboole :::"ManySortedSubset"::: ) "of" (Set ($#k4_equation :::"Equations"::: ) "S"); end; notationlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; let "s" be ($#m1_subset_1 :::"SortSymbol":::) "of" (Set (Const "S")); let "x", "y" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set "(" ($#k3_equation :::"TermAlg"::: ) (Set (Const "S")) ")" )) ($#k1_funct_1 :::"."::: ) (Set (Const "s"))); synonym "x" :::"'='"::: "y" for :::"[":::"S" "," "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 "s" be ($#m1_subset_1 :::"SortSymbol":::) "of" (Set (Const "S")); let "x", "y" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set "(" ($#k3_equation :::"TermAlg"::: ) (Set (Const "S")) ")" )) ($#k1_funct_1 :::"."::: ) (Set (Const "s"))); :: original: :::"'='"::: redefine func "x" :::"'='"::: "y" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set "(" ($#k4_equation :::"Equations"::: ) "S" ")" ) ($#k1_funct_1 :::"."::: ) "s"); end; theorem :: EQUATION:29 (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 "s")) "being" ($#m1_subset_1 :::"SortSymbol":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set "(" ($#k4_equation :::"Equations"::: ) (Set (Var "S")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "s"))) "holds" (Bool (Set (Set (Var "e")) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set "(" ($#k3_equation :::"TermAlg"::: ) (Set (Var "S")) ")" )) ($#k1_funct_1 :::"."::: ) (Set (Var "s"))))))) ; theorem :: EQUATION:30 (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 "s")) "being" ($#m1_subset_1 :::"SortSymbol":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set "(" ($#k4_equation :::"Equations"::: ) (Set (Var "S")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "s"))) "holds" (Bool (Set (Set (Var "e")) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set "(" ($#k3_equation :::"TermAlg"::: ) (Set (Var "S")) ")" )) ($#k1_funct_1 :::"."::: ) (Set (Var "s"))))))) ; 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 ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Const "S")); let "s" be ($#m1_subset_1 :::"SortSymbol":::) "of" (Set (Const "S")); let "e" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set "(" ($#k4_equation :::"Equations"::: ) (Set (Const "S")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Const "s"))); pred "A" :::"|="::: "e" means :: EQUATION:def 5 (Bool "for" (Set (Var "h")) "being" ($#m2_pboole :::"ManySortedFunction":::) "of" (Set "(" ($#k3_equation :::"TermAlg"::: ) "S" ")" ) "," "A" "st" (Bool (Bool (Set (Var "h")) ($#r1_msualg_3 :::"is_homomorphism"::: ) (Set ($#k3_equation :::"TermAlg"::: ) "S") "," "A")) "holds" (Bool (Set (Set "(" (Set (Var "h")) ($#k1_msualg_3 :::"."::: ) "s" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" "e" ($#k1_xtuple_0 :::"`1"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "h")) ($#k1_msualg_3 :::"."::: ) "s" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" "e" ($#k2_xtuple_0 :::"`2"::: ) ")" )))); end; :: deftheorem defines :::"|="::: EQUATION: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 "A")) "being" ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"SortSymbol":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set "(" ($#k4_equation :::"Equations"::: ) (Set (Var "S")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "s"))) "holds" (Bool "(" (Bool (Set (Var "A")) ($#r1_equation :::"|="::: ) (Set (Var "e"))) "iff" (Bool "for" (Set (Var "h")) "being" ($#m2_pboole :::"ManySortedFunction":::) "of" (Set "(" ($#k3_equation :::"TermAlg"::: ) (Set (Var "S")) ")" ) "," (Set (Var "A")) "st" (Bool (Bool (Set (Var "h")) ($#r1_msualg_3 :::"is_homomorphism"::: ) (Set ($#k3_equation :::"TermAlg"::: ) (Set (Var "S"))) "," (Set (Var "A")))) "holds" (Bool (Set (Set "(" (Set (Var "h")) ($#k1_msualg_3 :::"."::: ) (Set (Var "s")) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "e")) ($#k1_xtuple_0 :::"`1"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "h")) ($#k1_msualg_3 :::"."::: ) (Set (Var "s")) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "e")) ($#k2_xtuple_0 :::"`2"::: ) ")" )))) ")" ))))); 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 ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Const "S")); let "E" be ($#m3_pboole :::"EqualSet":::) "of" (Set (Const "S")); pred "A" :::"|="::: "E" means :: EQUATION:def 6 (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"SortSymbol":::) "of" "S" (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set "(" ($#k4_equation :::"Equations"::: ) "S" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "s"))) "st" (Bool (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set "E" ($#k1_funct_1 :::"."::: ) (Set (Var "s"))))) "holds" (Bool "A" ($#r1_equation :::"|="::: ) (Set (Var "e"))))); end; :: deftheorem defines :::"|="::: EQUATION: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 "A")) "being" ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "E")) "being" ($#m3_pboole :::"EqualSet":::) "of" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "A")) ($#r2_equation :::"|="::: ) (Set (Var "E"))) "iff" (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"SortSymbol":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set "(" ($#k4_equation :::"Equations"::: ) (Set (Var "S")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "s"))) "st" (Bool (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "E")) ($#k1_funct_1 :::"."::: ) (Set (Var "s"))))) "holds" (Bool (Set (Var "A")) ($#r1_equation :::"|="::: ) (Set (Var "e"))))) ")" )))); theorem :: EQUATION:31 (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 "U0")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"SortSymbol":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set "(" ($#k4_equation :::"Equations"::: ) (Set (Var "S")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "s"))) (Bool "for" (Set (Var "U2")) "being" ($#v3_msualg_1 :::"strict"::: ) ($#v4_msualg_1 :::"non-empty"::: ) ($#m1_msualg_2 :::"MSSubAlgebra"::: ) "of" (Set (Var "U0")) "st" (Bool (Bool (Set (Var "U0")) ($#r1_equation :::"|="::: ) (Set (Var "e")))) "holds" (Bool (Set (Var "U2")) ($#r1_equation :::"|="::: ) (Set (Var "e")))))))) ; theorem :: EQUATION:32 (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 "U0")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "E")) "being" ($#m3_pboole :::"EqualSet":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "U2")) "being" ($#v3_msualg_1 :::"strict"::: ) ($#v4_msualg_1 :::"non-empty"::: ) ($#m1_msualg_2 :::"MSSubAlgebra"::: ) "of" (Set (Var "U0")) "st" (Bool (Bool (Set (Var "U0")) ($#r2_equation :::"|="::: ) (Set (Var "E")))) "holds" (Bool (Set (Var "U2")) ($#r2_equation :::"|="::: ) (Set (Var "E"))))))) ; theorem :: EQUATION:33 (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 "U0")) "," (Set (Var "U1")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"SortSymbol":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set "(" ($#k4_equation :::"Equations"::: ) (Set (Var "S")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "s"))) "st" (Bool (Bool (Set (Var "U0")) "," (Set (Var "U1")) ($#r6_msualg_3 :::"are_isomorphic"::: ) ) & (Bool (Set (Var "U0")) ($#r1_equation :::"|="::: ) (Set (Var "e")))) "holds" (Bool (Set (Var "U1")) ($#r1_equation :::"|="::: ) (Set (Var "e"))))))) ; theorem :: EQUATION:34 (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 "U0")) "," (Set (Var "U1")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "E")) "being" ($#m3_pboole :::"EqualSet":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "U0")) "," (Set (Var "U1")) ($#r6_msualg_3 :::"are_isomorphic"::: ) ) & (Bool (Set (Var "U0")) ($#r2_equation :::"|="::: ) (Set (Var "E")))) "holds" (Bool (Set (Var "U1")) ($#r2_equation :::"|="::: ) (Set (Var "E")))))) ; theorem :: EQUATION:35 (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 "U0")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"SortSymbol":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set "(" ($#k4_equation :::"Equations"::: ) (Set (Var "S")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "s"))) (Bool "for" (Set (Var "R")) "being" ($#m1_msualg_4 :::"MSCongruence":::) "of" (Set (Var "U0")) "st" (Bool (Bool (Set (Var "U0")) ($#r1_equation :::"|="::: ) (Set (Var "e")))) "holds" (Bool (Set ($#k13_msualg_4 :::"QuotMSAlg"::: ) "(" (Set (Var "U0")) "," (Set (Var "R")) ")" ) ($#r1_equation :::"|="::: ) (Set (Var "e")))))))) ; theorem :: EQUATION:36 (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 "U0")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "E")) "being" ($#m3_pboole :::"EqualSet":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "R")) "being" ($#m1_msualg_4 :::"MSCongruence":::) "of" (Set (Var "U0")) "st" (Bool (Bool (Set (Var "U0")) ($#r2_equation :::"|="::: ) (Set (Var "E")))) "holds" (Bool (Set ($#k13_msualg_4 :::"QuotMSAlg"::: ) "(" (Set (Var "U0")) "," (Set (Var "R")) ")" ) ($#r2_equation :::"|="::: ) (Set (Var "E"))))))) ; theorem :: EQUATION:37 (Bool "for" (Set (Var "I")) "being" ($#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 "s")) "being" ($#m1_subset_1 :::"SortSymbol":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set "(" ($#k4_equation :::"Equations"::: ) (Set (Var "S")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "s"))) (Bool "for" (Set (Var "F")) "being" ($#m1_pralg_2 :::"MSAlgebra-Family"::: ) "of" (Set (Var "I")) "," (Set (Var "S")) "st" (Bool (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set (Var "I")))) "holds" (Bool "ex" (Set (Var "A")) "being" ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) "st" (Bool "(" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set (Var "A")) ($#r1_equation :::"|="::: ) (Set (Var "e"))) ")" )) ")" )) "holds" (Bool (Set ($#k14_pralg_2 :::"product"::: ) (Set (Var "F"))) ($#r1_equation :::"|="::: ) (Set (Var "e")))))))) ; theorem :: EQUATION:38 (Bool "for" (Set (Var "I")) "being" ($#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 "E")) "being" ($#m3_pboole :::"EqualSet":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "F")) "being" ($#m1_pralg_2 :::"MSAlgebra-Family"::: ) "of" (Set (Var "I")) "," (Set (Var "S")) "st" (Bool (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set (Var "I")))) "holds" (Bool "ex" (Set (Var "A")) "being" ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) "st" (Bool "(" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set (Var "A")) ($#r2_equation :::"|="::: ) (Set (Var "E"))) ")" )) ")" )) "holds" (Bool (Set ($#k14_pralg_2 :::"product"::: ) (Set (Var "F"))) ($#r2_equation :::"|="::: ) (Set (Var "E"))))))) ;