:: INSTALG1 semantic presentation begin theorem :: INSTALG1:1 (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 "V")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) "is" ($#m1_msaterm :::"ArgumentSeq"::: ) "of" (Set ($#k2_msaterm :::"Sym"::: ) "(" (Set (Var "o")) "," (Set (Var "V")) ")" )) "iff" (Bool (Set (Var "x")) "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_msualg_1 :::"Args"::: ) "(" (Set (Var "o")) "," (Set "(" ($#k11_msafree :::"FreeMSA"::: ) (Set (Var "V")) ")" ) ")" )) ")" ))))) ; registrationlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; let "V" be bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "S"))); let "o" be ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Const "S")); cluster -> ($#v6_trees_3 :::"DTree-yielding"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_msualg_1 :::"Args"::: ) "(" "o" "," (Set "(" ($#k11_msafree :::"FreeMSA"::: ) "V" ")" ) ")" ); end; theorem :: INSTALG1: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 "A1")) "," (Set (Var "A2")) "being" ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) "st" (Bool (Bool (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "A1"))) ($#r1_pzfmisc1 :::"is_transformable_to"::: ) (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "A2"))))) "holds" (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set ($#k3_msualg_1 :::"Args"::: ) "(" (Set (Var "o")) "," (Set (Var "A1")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set ($#k3_msualg_1 :::"Args"::: ) "(" (Set (Var "o")) "," (Set (Var "A2")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))))) ; theorem :: INSTALG1: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 "V")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_msualg_1 :::"Args"::: ) "(" (Set (Var "o")) "," (Set "(" ($#k11_msafree :::"FreeMSA"::: ) (Set (Var "V")) ")" ) ")" ) "holds" (Bool (Set (Set "(" ($#k5_msualg_1 :::"Den"::: ) "(" (Set (Var "o")) "," (Set "(" ($#k11_msafree :::"FreeMSA"::: ) (Set (Var "V")) ")" ) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k4_tarski :::"["::: ) (Set (Var "o")) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) ($#k4_tarski :::"]"::: ) ) ($#k4_trees_4 :::"-tree"::: ) (Set (Var "x")))))))) ; theorem :: INSTALG1: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")) "," (Set (Var "B")) "being" ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) "st" (Bool (Bool (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"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g3_msualg_1 :::"MSAlgebra"::: ) "(#" (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "B"))) "," (Set "the" ($#u4_msualg_1 :::"Charact"::: ) "of" (Set (Var "B"))) "#)" ))) "holds" (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S")) "holds" (Bool (Set ($#k5_msualg_1 :::"Den"::: ) "(" (Set (Var "o")) "," (Set (Var "A")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_msualg_1 :::"Den"::: ) "(" (Set (Var "o")) "," (Set (Var "B")) ")" ))))) ; theorem :: INSTALG1: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 "A1")) "," (Set (Var "A2")) "," (Set (Var "B1")) "," (Set (Var "B2")) "being" ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) "st" (Bool (Bool (Set ($#g3_msualg_1 :::"MSAlgebra"::: ) "(#" (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "A1"))) "," (Set "the" ($#u4_msualg_1 :::"Charact"::: ) "of" (Set (Var "A1"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g3_msualg_1 :::"MSAlgebra"::: ) "(#" (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "B1"))) "," (Set "the" ($#u4_msualg_1 :::"Charact"::: ) "of" (Set (Var "B1"))) "#)" )) & (Bool (Set ($#g3_msualg_1 :::"MSAlgebra"::: ) "(#" (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "A2"))) "," (Set "the" ($#u4_msualg_1 :::"Charact"::: ) "of" (Set (Var "A2"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g3_msualg_1 :::"MSAlgebra"::: ) "(#" (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "B2"))) "," (Set "the" ($#u4_msualg_1 :::"Charact"::: ) "of" (Set (Var "B2"))) "#)" ))) "holds" (Bool "for" (Set (Var "f")) "being" ($#m2_pboole :::"ManySortedFunction":::) "of" (Set (Var "A1")) "," (Set (Var "A2")) (Bool "for" (Set (Var "g")) "being" ($#m2_pboole :::"ManySortedFunction":::) "of" (Set (Var "B1")) "," (Set (Var "B2")) "st" (Bool (Bool (Set (Var "f")) ($#r8_pboole :::"="::: ) (Set (Var "g")))) "holds" (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set ($#k3_msualg_1 :::"Args"::: ) "(" (Set (Var "o")) "," (Set (Var "A1")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k3_msualg_1 :::"Args"::: ) "(" (Set (Var "o")) "," (Set (Var "A2")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_msualg_1 :::"Args"::: ) "(" (Set (Var "o")) "," (Set (Var "A1")) ")" ) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_msualg_1 :::"Args"::: ) "(" (Set (Var "o")) "," (Set (Var "B1")) ")" ) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y")))) "holds" (Bool (Set (Set (Var "f")) ($#k5_msualg_3 :::"#"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k5_msualg_3 :::"#"::: ) (Set (Var "y"))))))))))) ; theorem :: INSTALG1: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 "A1")) "," (Set (Var "A2")) "," (Set (Var "B1")) "," (Set (Var "B2")) "being" ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) "st" (Bool (Bool (Set ($#g3_msualg_1 :::"MSAlgebra"::: ) "(#" (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "A1"))) "," (Set "the" ($#u4_msualg_1 :::"Charact"::: ) "of" (Set (Var "A1"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g3_msualg_1 :::"MSAlgebra"::: ) "(#" (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "B1"))) "," (Set "the" ($#u4_msualg_1 :::"Charact"::: ) "of" (Set (Var "B1"))) "#)" )) & (Bool (Set ($#g3_msualg_1 :::"MSAlgebra"::: ) "(#" (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "A2"))) "," (Set "the" ($#u4_msualg_1 :::"Charact"::: ) "of" (Set (Var "A2"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g3_msualg_1 :::"MSAlgebra"::: ) "(#" (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "B2"))) "," (Set "the" ($#u4_msualg_1 :::"Charact"::: ) "of" (Set (Var "B2"))) "#)" )) & (Bool (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "A1"))) ($#r1_pzfmisc1 :::"is_transformable_to"::: ) (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "A2"))))) "holds" (Bool "for" (Set (Var "h")) "being" ($#m2_pboole :::"ManySortedFunction":::) "of" (Set (Var "A1")) "," (Set (Var "A2")) "st" (Bool (Bool (Set (Var "h")) ($#r1_msualg_3 :::"is_homomorphism"::: ) (Set (Var "A1")) "," (Set (Var "A2")))) "holds" (Bool "ex" (Set (Var "h9")) "being" ($#m2_pboole :::"ManySortedFunction":::) "of" (Set (Var "B1")) "," (Set (Var "B2")) "st" (Bool "(" (Bool (Set (Var "h9")) ($#r8_pboole :::"="::: ) (Set (Var "h"))) & (Bool (Set (Var "h9")) ($#r1_msualg_3 :::"is_homomorphism"::: ) (Set (Var "B1")) "," (Set (Var "B2"))) ")" ))))) ; definitionlet "S" be ($#l1_msualg_1 :::"ManySortedSign"::: ) ; attr "S" is :::"feasible"::: means :: INSTALG1:def 1 "(" (Bool (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S") ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "implies" (Bool (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "S") ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ; end; :: deftheorem defines :::"feasible"::: INSTALG1:def 1 : (Bool "for" (Set (Var "S")) "being" ($#l1_msualg_1 :::"ManySortedSign"::: ) "holds" (Bool "(" (Bool (Set (Var "S")) "is" ($#v1_instalg1 :::"feasible"::: ) ) "iff" "(" (Bool (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "implies" (Bool (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "S"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ")" )); theorem :: INSTALG1:7 (Bool "for" (Set (Var "S")) "being" ($#l1_msualg_1 :::"ManySortedSign"::: ) "holds" (Bool "(" (Bool (Set (Var "S")) "is" ($#v1_instalg1 :::"feasible"::: ) ) "iff" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "the" ($#u2_msualg_1 :::"ResultSort"::: ) "of" (Set (Var "S")))) ($#r1_hidden :::"="::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "S")))) ")" )) ; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) -> ($#v1_instalg1 :::"feasible"::: ) for ($#l1_msualg_1 :::"ManySortedSign"::: ) ; cluster ($#v11_struct_0 :::"void"::: ) -> ($#v1_instalg1 :::"feasible"::: ) for ($#l1_msualg_1 :::"ManySortedSign"::: ) ; cluster ($#v2_struct_0 :::"empty"::: ) ($#v1_instalg1 :::"feasible"::: ) -> ($#v11_struct_0 :::"void"::: ) for ($#l1_msualg_1 :::"ManySortedSign"::: ) ; cluster ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v1_instalg1 :::"feasible"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) for ($#l1_msualg_1 :::"ManySortedSign"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) for ($#l1_msualg_1 :::"ManySortedSign"::: ) ; end; theorem :: INSTALG1:8 (Bool "for" (Set (Var "S")) "being" ($#v1_instalg1 :::"feasible"::: ) ($#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")))) ; theorem :: INSTALG1:9 (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "being" ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "f")) "," (Set (Var "g")) ($#r3_pua2mss1 :::"form_morphism_between"::: ) (Set (Var "S1")) "," (Set (Var "S2")))) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S1"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S2")))) & (Bool (Set (Var "g")) "is" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "S1"))) "," (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "S2")))) ")" ))) ; begin definitionlet "S" be ($#v1_instalg1 :::"feasible"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; mode :::"Subsignature"::: "of" "S" -> ($#l1_msualg_1 :::"ManySortedSign"::: ) means :: INSTALG1:def 2 (Bool (Set ($#k6_partfun1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it)) "," (Set ($#k6_partfun1 :::"id"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" it)) ($#r3_pua2mss1 :::"form_morphism_between"::: ) it "," "S"); end; :: deftheorem defines :::"Subsignature"::: INSTALG1:def 2 : (Bool "for" (Set (Var "S")) "being" ($#v1_instalg1 :::"feasible"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "b2")) "being" ($#l1_msualg_1 :::"ManySortedSign"::: ) "holds" (Bool "(" (Bool (Set (Var "b2")) "is" ($#m1_instalg1 :::"Subsignature"::: ) "of" (Set (Var "S"))) "iff" (Bool (Set ($#k6_partfun1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b2")))) "," (Set ($#k6_partfun1 :::"id"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "b2")))) ($#r3_pua2mss1 :::"form_morphism_between"::: ) (Set (Var "b2")) "," (Set (Var "S"))) ")" ))); theorem :: INSTALG1:10 (Bool "for" (Set (Var "S")) "being" ($#v1_instalg1 :::"feasible"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "T")) "being" ($#m1_instalg1 :::"Subsignature"::: ) "of" (Set (Var "S")) "holds" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T"))) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S")))) & (Bool (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "T"))) ($#r1_tarski :::"c="::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "S")))) ")" ))) ; registrationlet "S" be ($#v1_instalg1 :::"feasible"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; cluster -> ($#v1_instalg1 :::"feasible"::: ) for ($#m1_instalg1 :::"Subsignature"::: ) "of" "S"; end; theorem :: INSTALG1:11 (Bool "for" (Set (Var "S")) "being" ($#v1_instalg1 :::"feasible"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "T")) "being" ($#m1_instalg1 :::"Subsignature"::: ) "of" (Set (Var "S")) "holds" (Bool "(" (Bool (Set "the" ($#u2_msualg_1 :::"ResultSort"::: ) "of" (Set (Var "T"))) ($#r1_tarski :::"c="::: ) (Set "the" ($#u2_msualg_1 :::"ResultSort"::: ) "of" (Set (Var "S")))) & (Bool (Set "the" ($#u1_msualg_1 :::"Arity"::: ) "of" (Set (Var "T"))) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_msualg_1 :::"Arity"::: ) "of" (Set (Var "S")))) ")" ))) ; theorem :: INSTALG1:12 (Bool "for" (Set (Var "S")) "being" ($#v1_instalg1 :::"feasible"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "T")) "being" ($#m1_instalg1 :::"Subsignature"::: ) "of" (Set (Var "S")) "holds" (Bool "(" (Bool (Set "the" ($#u1_msualg_1 :::"Arity"::: ) "of" (Set (Var "T"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_msualg_1 :::"Arity"::: ) "of" (Set (Var "S"))) ($#k2_partfun1 :::"|"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "T"))))) & (Bool (Set "the" ($#u2_msualg_1 :::"ResultSort"::: ) "of" (Set (Var "T"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u2_msualg_1 :::"ResultSort"::: ) "of" (Set (Var "S"))) ($#k2_partfun1 :::"|"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "T"))))) ")" ))) ; theorem :: INSTALG1:13 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#v1_instalg1 :::"feasible"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) "st" (Bool (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T"))) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S")))) & (Bool (Set "the" ($#u1_msualg_1 :::"Arity"::: ) "of" (Set (Var "T"))) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_msualg_1 :::"Arity"::: ) "of" (Set (Var "S")))) & (Bool (Set "the" ($#u2_msualg_1 :::"ResultSort"::: ) "of" (Set (Var "T"))) ($#r1_tarski :::"c="::: ) (Set "the" ($#u2_msualg_1 :::"ResultSort"::: ) "of" (Set (Var "S"))))) "holds" (Bool (Set (Var "T")) "is" ($#m1_instalg1 :::"Subsignature"::: ) "of" (Set (Var "S")))) ; theorem :: INSTALG1:14 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#v1_instalg1 :::"feasible"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) "st" (Bool (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T"))) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S")))) & (Bool (Set "the" ($#u1_msualg_1 :::"Arity"::: ) "of" (Set (Var "T"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_msualg_1 :::"Arity"::: ) "of" (Set (Var "S"))) ($#k2_partfun1 :::"|"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "T"))))) & (Bool (Set "the" ($#u2_msualg_1 :::"ResultSort"::: ) "of" (Set (Var "T"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u2_msualg_1 :::"ResultSort"::: ) "of" (Set (Var "S"))) ($#k2_partfun1 :::"|"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "T")))))) "holds" (Bool (Set (Var "T")) "is" ($#m1_instalg1 :::"Subsignature"::: ) "of" (Set (Var "S")))) ; theorem :: INSTALG1:15 (Bool "for" (Set (Var "S")) "being" ($#v1_instalg1 :::"feasible"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) "holds" (Bool (Set (Var "S")) "is" ($#m1_instalg1 :::"Subsignature"::: ) "of" (Set (Var "S")))) ; theorem :: INSTALG1:16 (Bool "for" (Set (Var "S1")) "being" ($#v1_instalg1 :::"feasible"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "S2")) "being" ($#m1_instalg1 :::"Subsignature"::: ) "of" (Set (Var "S1")) (Bool "for" (Set (Var "S3")) "being" ($#m1_instalg1 :::"Subsignature"::: ) "of" (Set (Var "S2")) "holds" (Bool (Set (Var "S3")) "is" ($#m1_instalg1 :::"Subsignature"::: ) "of" (Set (Var "S1")))))) ; theorem :: INSTALG1:17 (Bool "for" (Set (Var "S1")) "being" ($#v1_instalg1 :::"feasible"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "S2")) "being" ($#m1_instalg1 :::"Subsignature"::: ) "of" (Set (Var "S1")) "st" (Bool (Bool (Set (Var "S1")) "is" ($#m1_instalg1 :::"Subsignature"::: ) "of" (Set (Var "S2")))) "holds" (Bool (Set ($#g1_msualg_1 :::"ManySortedSign"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S1"))) "," (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "S1"))) "," (Set "the" ($#u1_msualg_1 :::"Arity"::: ) "of" (Set (Var "S1"))) "," (Set "the" ($#u2_msualg_1 :::"ResultSort"::: ) "of" (Set (Var "S1"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g1_msualg_1 :::"ManySortedSign"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S2"))) "," (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "S2"))) "," (Set "the" ($#u1_msualg_1 :::"Arity"::: ) "of" (Set (Var "S2"))) "," (Set "the" ($#u2_msualg_1 :::"ResultSort"::: ) "of" (Set (Var "S2"))) "#)" )))) ; registrationlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_instalg1 :::"feasible"::: ) for ($#m1_instalg1 :::"Subsignature"::: ) "of" "S"; end; registrationlet "S" be ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v1_instalg1 :::"feasible"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; cluster ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v1_instalg1 :::"feasible"::: ) for ($#m1_instalg1 :::"Subsignature"::: ) "of" "S"; end; theorem :: INSTALG1:18 (Bool "for" (Set (Var "S")) "being" ($#v1_instalg1 :::"feasible"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "S9")) "being" ($#m1_instalg1 :::"Subsignature"::: ) "of" (Set (Var "S")) (Bool "for" (Set (Var "T")) "being" ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "f")) "," (Set (Var "g")) ($#r3_pua2mss1 :::"form_morphism_between"::: ) (Set (Var "S")) "," (Set (Var "T")))) "holds" (Bool (Set (Set (Var "f")) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S9")))) "," (Set (Set (Var "g")) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "S9")))) ($#r3_pua2mss1 :::"form_morphism_between"::: ) (Set (Var "S9")) "," (Set (Var "T"))))))) ; theorem :: INSTALG1:19 (Bool "for" (Set (Var "S")) "being" ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "T")) "being" ($#v1_instalg1 :::"feasible"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "T9")) "being" ($#m1_instalg1 :::"Subsignature"::: ) "of" (Set (Var "T")) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "f")) "," (Set (Var "g")) ($#r3_pua2mss1 :::"form_morphism_between"::: ) (Set (Var "S")) "," (Set (Var "T9")))) "holds" (Bool (Set (Var "f")) "," (Set (Var "g")) ($#r3_pua2mss1 :::"form_morphism_between"::: ) (Set (Var "S")) "," (Set (Var "T"))))))) ; theorem :: INSTALG1:20 (Bool "for" (Set (Var "S")) "being" ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "T")) "being" ($#v1_instalg1 :::"feasible"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "T9")) "being" ($#m1_instalg1 :::"Subsignature"::: ) "of" (Set (Var "T")) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "f")) "," (Set (Var "g")) ($#r3_pua2mss1 :::"form_morphism_between"::: ) (Set (Var "S")) "," (Set (Var "T"))) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f"))) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T9")))) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "g"))) ($#r1_tarski :::"c="::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "T9"))))) "holds" (Bool (Set (Var "f")) "," (Set (Var "g")) ($#r3_pua2mss1 :::"form_morphism_between"::: ) (Set (Var "S")) "," (Set (Var "T9"))))))) ; begin definitionlet "S1", "S2" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; let "A" be ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Const "S2")); let "f", "g" be ($#m1_hidden :::"Function":::); assume (Bool (Set (Const "f")) "," (Set (Const "g")) ($#r3_pua2mss1 :::"form_morphism_between"::: ) (Set (Const "S1")) "," (Set (Const "S2"))) ; func "A" :::"|"::: "(" "S1" "," "f" "," "g" ")" -> ($#v3_msualg_1 :::"strict"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" "S1" means :: INSTALG1:def 3 (Bool "(" (Bool (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" "A") ($#k3_relat_1 :::"*"::: ) "f")) & (Bool (Set "the" ($#u4_msualg_1 :::"Charact"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u4_msualg_1 :::"Charact"::: ) "of" "A") ($#k3_relat_1 :::"*"::: ) "g")) ")" ); end; :: deftheorem defines :::"|"::: INSTALG1:def 3 : (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "A")) "being" ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S2")) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "f")) "," (Set (Var "g")) ($#r3_pua2mss1 :::"form_morphism_between"::: ) (Set (Var "S1")) "," (Set (Var "S2")))) "holds" (Bool "for" (Set (Var "b6")) "being" ($#v3_msualg_1 :::"strict"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S1")) "holds" (Bool "(" (Bool (Set (Var "b6")) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k1_instalg1 :::"|"::: ) "(" (Set (Var "S1")) "," (Set (Var "f")) "," (Set (Var "g")) ")" )) "iff" (Bool "(" (Bool (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "b6"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "A"))) ($#k3_relat_1 :::"*"::: ) (Set (Var "f")))) & (Bool (Set "the" ($#u4_msualg_1 :::"Charact"::: ) "of" (Set (Var "b6"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u4_msualg_1 :::"Charact"::: ) "of" (Set (Var "A"))) ($#k3_relat_1 :::"*"::: ) (Set (Var "g")))) ")" ) ")" ))))); definitionlet "S2", "S1" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; let "A" be ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Const "S2")); func "A" :::"|"::: "S1" -> ($#v3_msualg_1 :::"strict"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" "S1" equals :: INSTALG1:def 4 (Set "A" ($#k1_instalg1 :::"|"::: ) "(" "S1" "," (Set "(" ($#k6_partfun1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S1") ")" ) "," (Set "(" ($#k6_partfun1 :::"id"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "S1") ")" ) ")" ); end; :: deftheorem defines :::"|"::: INSTALG1:def 4 : (Bool "for" (Set (Var "S2")) "," (Set (Var "S1")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "A")) "being" ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S2")) "holds" (Bool (Set (Set (Var "A")) ($#k2_instalg1 :::"|"::: ) (Set (Var "S1"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k1_instalg1 :::"|"::: ) "(" (Set (Var "S1")) "," (Set "(" ($#k6_partfun1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S1"))) ")" ) "," (Set "(" ($#k6_partfun1 :::"id"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "S1"))) ")" ) ")" )))); theorem :: INSTALG1:21 (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S2")) "st" (Bool (Bool (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"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g3_msualg_1 :::"MSAlgebra"::: ) "(#" (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "B"))) "," (Set "the" ($#u4_msualg_1 :::"Charact"::: ) "of" (Set (Var "B"))) "#)" ))) "holds" (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "f")) "," (Set (Var "g")) ($#r3_pua2mss1 :::"form_morphism_between"::: ) (Set (Var "S1")) "," (Set (Var "S2")))) "holds" (Bool (Set (Set (Var "A")) ($#k1_instalg1 :::"|"::: ) "(" (Set (Var "S1")) "," (Set (Var "f")) "," (Set (Var "g")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "B")) ($#k1_instalg1 :::"|"::: ) "(" (Set (Var "S1")) "," (Set (Var "f")) "," (Set (Var "g")) ")" ))))) ; theorem :: INSTALG1:22 (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "A")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S2")) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "f")) "," (Set (Var "g")) ($#r3_pua2mss1 :::"form_morphism_between"::: ) (Set (Var "S1")) "," (Set (Var "S2")))) "holds" (Bool (Set (Set (Var "A")) ($#k1_instalg1 :::"|"::: ) "(" (Set (Var "S1")) "," (Set (Var "f")) "," (Set (Var "g")) ")" ) "is" ($#v4_msualg_1 :::"non-empty"::: ) )))) ; registrationlet "S2" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; let "S1" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_instalg1 :::"Subsignature"::: ) "of" (Set (Const "S2")); let "A" be ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Const "S2")); cluster (Set "A" ($#k2_instalg1 :::"|"::: ) "S1") -> ($#v3_msualg_1 :::"strict"::: ) ($#v4_msualg_1 :::"non-empty"::: ) ; end; theorem :: INSTALG1:23 (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "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")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "f")) "," (Set (Var "g")) ($#r3_pua2mss1 :::"form_morphism_between"::: ) (Set (Var "S1")) "," (Set (Var "S2")))) "holds" (Bool "for" (Set (Var "A")) "being" ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S2")) (Bool "for" (Set (Var "o1")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S1")) (Bool "for" (Set (Var "o2")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S2")) "st" (Bool (Bool (Set (Var "o2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "o1"))))) "holds" (Bool (Set ($#k5_msualg_1 :::"Den"::: ) "(" (Set (Var "o1")) "," (Set "(" (Set (Var "A")) ($#k1_instalg1 :::"|"::: ) "(" (Set (Var "S1")) "," (Set (Var "f")) "," (Set (Var "g")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_msualg_1 :::"Den"::: ) "(" (Set (Var "o2")) "," (Set (Var "A")) ")" ))))))) ; theorem :: INSTALG1:24 (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "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")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "f")) "," (Set (Var "g")) ($#r3_pua2mss1 :::"form_morphism_between"::: ) (Set (Var "S1")) "," (Set (Var "S2")))) "holds" (Bool "for" (Set (Var "A")) "being" ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S2")) (Bool "for" (Set (Var "o1")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S1")) (Bool "for" (Set (Var "o2")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S2")) "st" (Bool (Bool (Set (Var "o2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "o1"))))) "holds" (Bool "(" (Bool (Set ($#k3_msualg_1 :::"Args"::: ) "(" (Set (Var "o2")) "," (Set (Var "A")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_msualg_1 :::"Args"::: ) "(" (Set (Var "o1")) "," (Set "(" (Set (Var "A")) ($#k1_instalg1 :::"|"::: ) "(" (Set (Var "S1")) "," (Set (Var "f")) "," (Set (Var "g")) ")" ")" ) ")" )) & (Bool (Set ($#k4_msualg_1 :::"Result"::: ) "(" (Set (Var "o1")) "," (Set "(" (Set (Var "A")) ($#k1_instalg1 :::"|"::: ) "(" (Set (Var "S1")) "," (Set (Var "f")) "," (Set (Var "g")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_msualg_1 :::"Result"::: ) "(" (Set (Var "o2")) "," (Set (Var "A")) ")" )) ")" )))))) ; theorem :: INSTALG1:25 (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "A")) "being" ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) "holds" (Bool (Set (Set (Var "A")) ($#k1_instalg1 :::"|"::: ) "(" (Set (Var "S")) "," (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"))) ")" ) ")" ) ($#r1_hidden :::"="::: ) (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 :: INSTALG1:26 (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "A")) "being" ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) "holds" (Bool (Set (Set (Var "A")) ($#k2_instalg1 :::"|"::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) (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 :: INSTALG1:27 (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "," (Set (Var "S3")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "f1")) "," (Set (Var "g1")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "f1")) "," (Set (Var "g1")) ($#r3_pua2mss1 :::"form_morphism_between"::: ) (Set (Var "S1")) "," (Set (Var "S2")))) "holds" (Bool "for" (Set (Var "f2")) "," (Set (Var "g2")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "f2")) "," (Set (Var "g2")) ($#r3_pua2mss1 :::"form_morphism_between"::: ) (Set (Var "S2")) "," (Set (Var "S3")))) "holds" (Bool "for" (Set (Var "A")) "being" ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S3")) "holds" (Bool (Set (Set (Var "A")) ($#k1_instalg1 :::"|"::: ) "(" (Set (Var "S1")) "," (Set "(" (Set (Var "f2")) ($#k3_relat_1 :::"*"::: ) (Set (Var "f1")) ")" ) "," (Set "(" (Set (Var "g2")) ($#k3_relat_1 :::"*"::: ) (Set (Var "g1")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "A")) ($#k1_instalg1 :::"|"::: ) "(" (Set (Var "S2")) "," (Set (Var "f2")) "," (Set (Var "g2")) ")" ")" ) ($#k1_instalg1 :::"|"::: ) "(" (Set (Var "S1")) "," (Set (Var "f1")) "," (Set (Var "g1")) ")" )))))) ; theorem :: INSTALG1:28 (Bool "for" (Set (Var "S1")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_instalg1 :::"feasible"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "S2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_instalg1 :::"Subsignature"::: ) "of" (Set (Var "S1")) (Bool "for" (Set (Var "S3")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_instalg1 :::"Subsignature"::: ) "of" (Set (Var "S2")) (Bool "for" (Set (Var "A")) "being" ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S1")) "holds" (Bool (Set (Set (Var "A")) ($#k2_instalg1 :::"|"::: ) (Set (Var "S3"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "A")) ($#k2_instalg1 :::"|"::: ) (Set (Var "S2")) ")" ) ($#k2_instalg1 :::"|"::: ) (Set (Var "S3")))))))) ; theorem :: INSTALG1:29 (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S1"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S2"))) (Bool "for" (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "f")) "," (Set (Var "g")) ($#r3_pua2mss1 :::"form_morphism_between"::: ) (Set (Var "S1")) "," (Set (Var "S2")))) "holds" (Bool "for" (Set (Var "A1")) "," (Set (Var "A2")) "being" ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S2")) (Bool "for" (Set (Var "h")) "being" ($#m2_pboole :::"ManySortedFunction"::: ) "of" (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "A1"))) "," (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "A2"))) "holds" (Bool (Set (Set (Var "h")) ($#k3_relat_1 :::"*"::: ) (Set (Var "f"))) "is" ($#m2_pboole :::"ManySortedFunction"::: ) "of" (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set "(" (Set (Var "A1")) ($#k1_instalg1 :::"|"::: ) "(" (Set (Var "S1")) "," (Set (Var "f")) "," (Set (Var "g")) ")" ")" )) "," (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set "(" (Set (Var "A2")) ($#k1_instalg1 :::"|"::: ) "(" (Set (Var "S1")) "," (Set (Var "f")) "," (Set (Var "g")) ")" ")" )))))))) ; theorem :: INSTALG1:30 (Bool "for" (Set (Var "S1")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "S2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_instalg1 :::"Subsignature"::: ) "of" (Set (Var "S1")) (Bool "for" (Set (Var "A1")) "," (Set (Var "A2")) "being" ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S1")) (Bool "for" (Set (Var "h")) "being" ($#m2_pboole :::"ManySortedFunction"::: ) "of" (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "A1"))) "," (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "A2"))) "holds" (Bool (Set (Set (Var "h")) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S2")))) "is" ($#m2_pboole :::"ManySortedFunction"::: ) "of" (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set "(" (Set (Var "A1")) ($#k2_instalg1 :::"|"::: ) (Set (Var "S2")) ")" )) "," (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set "(" (Set (Var "A2")) ($#k2_instalg1 :::"|"::: ) (Set (Var "S2")) ")" ))))))) ; theorem :: INSTALG1:31 (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "f")) "," (Set (Var "g")) ($#r3_pua2mss1 :::"form_morphism_between"::: ) (Set (Var "S1")) "," (Set (Var "S2")))) "holds" (Bool "for" (Set (Var "A")) "being" ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S2")) "holds" (Bool (Set (Set "(" ($#k2_msualg_3 :::"id"::: ) (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "A"))) ")" ) ($#k3_relat_1 :::"*"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k2_msualg_3 :::"id"::: ) (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set "(" (Set (Var "A")) ($#k1_instalg1 :::"|"::: ) "(" (Set (Var "S1")) "," (Set (Var "f")) "," (Set (Var "g")) ")" ")" ))))))) ; theorem :: INSTALG1:32 (Bool "for" (Set (Var "S1")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "S2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_instalg1 :::"Subsignature"::: ) "of" (Set (Var "S1")) (Bool "for" (Set (Var "A")) "being" ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S1")) "holds" (Bool (Set (Set "(" ($#k2_msualg_3 :::"id"::: ) (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "A"))) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S2")))) ($#r1_hidden :::"="::: ) (Set ($#k2_msualg_3 :::"id"::: ) (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set "(" (Set (Var "A")) ($#k2_instalg1 :::"|"::: ) (Set (Var "S2")) ")" ))))))) ; theorem :: INSTALG1:33 (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "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")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "f")) "," (Set (Var "g")) ($#r3_pua2mss1 :::"form_morphism_between"::: ) (Set (Var "S1")) "," (Set (Var "S2")))) "holds" (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S2")) (Bool "for" (Set (Var "h2")) "being" ($#m2_pboole :::"ManySortedFunction":::) "of" (Set (Var "A")) "," (Set (Var "B")) (Bool "for" (Set (Var "h1")) "being" ($#m2_pboole :::"ManySortedFunction":::) "of" (Set "(" (Set (Var "A")) ($#k1_instalg1 :::"|"::: ) "(" (Set (Var "S1")) "," (Set (Var "f")) "," (Set (Var "g")) ")" ")" ) "," (Set "(" (Set (Var "B")) ($#k1_instalg1 :::"|"::: ) "(" (Set (Var "S1")) "," (Set (Var "f")) "," (Set (Var "g")) ")" ")" ) "st" (Bool (Bool (Set (Var "h1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "h2")) ($#k3_relat_1 :::"*"::: ) (Set (Var "f"))))) "holds" (Bool "for" (Set (Var "o1")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S1")) (Bool "for" (Set (Var "o2")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S2")) "st" (Bool (Bool (Set (Var "o2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "o1")))) & (Bool (Set ($#k3_msualg_1 :::"Args"::: ) "(" (Set (Var "o2")) "," (Set (Var "A")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k3_msualg_1 :::"Args"::: ) "(" (Set (Var "o2")) "," (Set (Var "B")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "for" (Set (Var "x2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_msualg_1 :::"Args"::: ) "(" (Set (Var "o2")) "," (Set (Var "A")) ")" ) (Bool "for" (Set (Var "x1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_msualg_1 :::"Args"::: ) "(" (Set (Var "o1")) "," (Set "(" (Set (Var "A")) ($#k1_instalg1 :::"|"::: ) "(" (Set (Var "S1")) "," (Set (Var "f")) "," (Set (Var "g")) ")" ")" ) ")" ) "st" (Bool (Bool (Set (Var "x2")) ($#r1_hidden :::"="::: ) (Set (Var "x1")))) "holds" (Bool (Set (Set (Var "h1")) ($#k5_msualg_3 :::"#"::: ) (Set (Var "x1"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "h2")) ($#k5_msualg_3 :::"#"::: ) (Set (Var "x2"))))))))))))) ; theorem :: INSTALG1:34 (Bool "for" (Set (Var "S")) "," (Set (Var "S9")) "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 "A1")) "," (Set (Var "A2")) "being" ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) "st" (Bool (Bool (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "A1"))) ($#r1_pzfmisc1 :::"is_transformable_to"::: ) (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "A2"))))) "holds" (Bool "for" (Set (Var "h")) "being" ($#m2_pboole :::"ManySortedFunction":::) "of" (Set (Var "A1")) "," (Set (Var "A2")) "st" (Bool (Bool (Set (Var "h")) ($#r1_msualg_3 :::"is_homomorphism"::: ) (Set (Var "A1")) "," (Set (Var "A2")))) "holds" (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S9"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) (Bool "for" (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "f")) "," (Set (Var "g")) ($#r3_pua2mss1 :::"form_morphism_between"::: ) (Set (Var "S9")) "," (Set (Var "S")))) "holds" (Bool "ex" (Set (Var "h9")) "being" ($#m2_pboole :::"ManySortedFunction":::) "of" (Set "(" (Set (Var "A1")) ($#k1_instalg1 :::"|"::: ) "(" (Set (Var "S9")) "," (Set (Var "f")) "," (Set (Var "g")) ")" ")" ) "," (Set "(" (Set (Var "A2")) ($#k1_instalg1 :::"|"::: ) "(" (Set (Var "S9")) "," (Set (Var "f")) "," (Set (Var "g")) ")" ")" ) "st" (Bool "(" (Bool (Set (Var "h9")) ($#r8_pboole :::"="::: ) (Set (Set (Var "h")) ($#k3_relat_1 :::"*"::: ) (Set (Var "f")))) & (Bool (Set (Var "h9")) ($#r1_msualg_3 :::"is_homomorphism"::: ) (Set (Set (Var "A1")) ($#k1_instalg1 :::"|"::: ) "(" (Set (Var "S9")) "," (Set (Var "f")) "," (Set (Var "g")) ")" ) "," (Set (Set (Var "A2")) ($#k1_instalg1 :::"|"::: ) "(" (Set (Var "S9")) "," (Set (Var "f")) "," (Set (Var "g")) ")" )) ")" ))))))) ; theorem :: INSTALG1:35 (Bool "for" (Set (Var "S")) "being" ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v1_instalg1 :::"feasible"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "S9")) "being" ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#m1_instalg1 :::"Subsignature"::: ) "of" (Set (Var "S")) (Bool "for" (Set (Var "A1")) "," (Set (Var "A2")) "being" ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) "st" (Bool (Bool (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "A1"))) ($#r1_pzfmisc1 :::"is_transformable_to"::: ) (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "A2"))))) "holds" (Bool "for" (Set (Var "h")) "being" ($#m2_pboole :::"ManySortedFunction":::) "of" (Set (Var "A1")) "," (Set (Var "A2")) "st" (Bool (Bool (Set (Var "h")) ($#r1_msualg_3 :::"is_homomorphism"::: ) (Set (Var "A1")) "," (Set (Var "A2")))) "holds" (Bool "ex" (Set (Var "h9")) "being" ($#m2_pboole :::"ManySortedFunction":::) "of" (Set "(" (Set (Var "A1")) ($#k2_instalg1 :::"|"::: ) (Set (Var "S9")) ")" ) "," (Set "(" (Set (Var "A2")) ($#k2_instalg1 :::"|"::: ) (Set (Var "S9")) ")" ) "st" (Bool "(" (Bool (Set (Var "h9")) ($#r1_hidden :::"="::: ) (Set (Set (Var "h")) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S9"))))) & (Bool (Set (Var "h9")) ($#r1_msualg_3 :::"is_homomorphism"::: ) (Set (Set (Var "A1")) ($#k2_instalg1 :::"|"::: ) (Set (Var "S9"))) "," (Set (Set (Var "A2")) ($#k2_instalg1 :::"|"::: ) (Set (Var "S9")))) ")" )))))) ; theorem :: INSTALG1:36 (Bool "for" (Set (Var "S")) "," (Set (Var "S9")) "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" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S9"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) (Bool "for" (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "f")) "," (Set (Var "g")) ($#r3_pua2mss1 :::"form_morphism_between"::: ) (Set (Var "S9")) "," (Set (Var "S")))) "holds" (Bool "for" (Set (Var "B")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S9")) "st" (Bool (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k1_instalg1 :::"|"::: ) "(" (Set (Var "S9")) "," (Set (Var "f")) "," (Set (Var "g")) ")" ))) "holds" (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m1_subset_1 :::"SortSymbol":::) "of" (Set (Var "S9")) (Bool "for" (Set (Var "t")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "t")) ($#r1_msualg_6 :::"is_e.translation_of"::: ) (Set (Var "B")) "," (Set (Var "s1")) "," (Set (Var "s2")))) "holds" (Bool (Set (Var "t")) ($#r1_msualg_6 :::"is_e.translation_of"::: ) (Set (Var "A")) "," (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "s1"))) "," (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "s2"))))))))))) ; theorem :: INSTALG1:37 (Bool "for" (Set (Var "S")) "," (Set (Var "S9")) "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_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S9"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) (Bool "for" (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "f")) "," (Set (Var "g")) ($#r3_pua2mss1 :::"form_morphism_between"::: ) (Set (Var "S9")) "," (Set (Var "S")))) "holds" (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m1_subset_1 :::"SortSymbol":::) "of" (Set (Var "S9")) "st" (Bool (Bool (Set ($#k3_msualg_6 :::"TranslationRel"::: ) (Set (Var "S9"))) ($#r1_rewrite1 :::"reduces"::: ) (Set (Var "s1")) "," (Set (Var "s2")))) "holds" (Bool (Set ($#k3_msualg_6 :::"TranslationRel"::: ) (Set (Var "S"))) ($#r1_rewrite1 :::"reduces"::: ) (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "s1"))) "," (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "s2")))))))) ; theorem :: INSTALG1:38 (Bool "for" (Set (Var "S")) "," (Set (Var "S9")) "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" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S9"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) (Bool "for" (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "f")) "," (Set (Var "g")) ($#r3_pua2mss1 :::"form_morphism_between"::: ) (Set (Var "S9")) "," (Set (Var "S")))) "holds" (Bool "for" (Set (Var "B")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S9")) "st" (Bool (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k1_instalg1 :::"|"::: ) "(" (Set (Var "S9")) "," (Set (Var "f")) "," (Set (Var "g")) ")" ))) "holds" (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m1_subset_1 :::"SortSymbol":::) "of" (Set (Var "S9")) "st" (Bool (Bool (Set ($#k3_msualg_6 :::"TranslationRel"::: ) (Set (Var "S9"))) ($#r1_rewrite1 :::"reduces"::: ) (Set (Var "s1")) "," (Set (Var "s2")))) "holds" (Bool "for" (Set (Var "t")) "being" ($#m2_msualg_6 :::"Translation"::: ) "of" (Set (Var "B")) "," (Set (Var "s1")) "," (Set (Var "s2")) "holds" (Bool (Set (Var "t")) "is" ($#m2_msualg_6 :::"Translation"::: ) "of" (Set (Var "A")) "," (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "s1"))) "," (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "s2"))))))))))) ; begin scheme :: INSTALG1:sch 1 GenFuncEx{ F1() -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) , F2() -> ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set F1 "(" ")" ), F3() -> bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set F1 "(" ")" )), F4( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) } : (Bool "ex" (Set (Var "h")) "being" ($#m2_pboole :::"ManySortedFunction":::) "of" (Set "(" ($#k11_msafree :::"FreeMSA"::: ) (Set F3 "(" ")" ) ")" ) "," (Set F2 "(" ")" ) "st" (Bool "(" (Bool (Set (Var "h")) ($#r1_msualg_3 :::"is_homomorphism"::: ) (Set ($#k11_msafree :::"FreeMSA"::: ) (Set F3 "(" ")" )) "," (Set F2 "(" ")" )) & (Bool "(" "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"SortSymbol":::) "of" (Set F1 "(" ")" ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set F3 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "s"))) "holds" (Bool (Set (Set "(" (Set (Var "h")) ($#k1_msualg_3 :::"."::: ) (Set (Var "s")) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_trees_4 :::"root-tree"::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "s")) ($#k4_tarski :::"]"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set F4 "(" (Set (Var "x")) "," (Set (Var "s")) ")" ))) ")" ) ")" )) provided (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"SortSymbol":::) "of" (Set F1 "(" ")" ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set F3 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "s"))) "holds" (Bool (Set F4 "(" (Set (Var "x")) "," (Set (Var "s")) ")" ) ($#r2_hidden :::"in"::: ) (Set (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set F2 "(" ")" )) ($#k1_funct_1 :::"."::: ) (Set (Var "s")))))) proof end; theorem :: INSTALG1:39 (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 "C")) "being" ($#m3_pboole :::"ManySortedSubset"::: ) "of" (Set (Var "A")) (Bool "for" (Set (Var "F")) "being" ($#m2_pboole :::"ManySortedFunction"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set (Var "I")))) "holds" (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set (Var "g")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "F")) ($#k1_msafree :::"||"::: ) (Set (Var "C")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))))) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "C")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))))) "holds" (Bool (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))))))))))) ; registrationlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; let "X" be bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "S"))); cluster (Set ($#k13_msafree :::"FreeGen"::: ) "X") -> bbbadV2_RELAT_1() ; end; definitionlet "S1", "S2" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; let "X" be bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "S2"))); let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "S1"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "S2"))); let "g" be ($#m1_hidden :::"Function":::); assume (Bool (Set (Const "f")) "," (Set (Const "g")) ($#r3_pua2mss1 :::"form_morphism_between"::: ) (Set (Const "S1")) "," (Set (Const "S2"))) ; func :::"hom"::: "(" "f" "," "g" "," "X" "," "S1" "," "S2" ")" -> ($#m2_pboole :::"ManySortedFunction":::) "of" (Set "(" ($#k11_msafree :::"FreeMSA"::: ) (Set "(" "X" ($#k3_relat_1 :::"*"::: ) "f" ")" ) ")" ) "," (Set "(" (Set "(" ($#k11_msafree :::"FreeMSA"::: ) "X" ")" ) ($#k1_instalg1 :::"|"::: ) "(" "S1" "," "f" "," "g" ")" ")" ) means :: INSTALG1:def 5 (Bool "(" (Bool it ($#r1_msualg_3 :::"is_homomorphism"::: ) (Set ($#k11_msafree :::"FreeMSA"::: ) (Set "(" "X" ($#k3_relat_1 :::"*"::: ) "f" ")" )) "," (Set (Set "(" ($#k11_msafree :::"FreeMSA"::: ) "X" ")" ) ($#k1_instalg1 :::"|"::: ) "(" "S1" "," "f" "," "g" ")" )) & (Bool "(" "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"SortSymbol":::) "of" "S1" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set "(" "X" ($#k3_relat_1 :::"*"::: ) "f" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "s"))) "holds" (Bool (Set (Set "(" it ($#k1_msualg_3 :::"."::: ) (Set (Var "s")) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_trees_4 :::"root-tree"::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "s")) ($#k4_tarski :::"]"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_trees_4 :::"root-tree"::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set "(" "f" ($#k3_funct_2 :::"."::: ) (Set (Var "s")) ")" ) ($#k4_tarski :::"]"::: ) )))) ")" ) ")" ); end; :: deftheorem defines :::"hom"::: INSTALG1:def 5 : (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "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" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S2"))) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S1"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S2"))) (Bool "for" (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "f")) "," (Set (Var "g")) ($#r3_pua2mss1 :::"form_morphism_between"::: ) (Set (Var "S1")) "," (Set (Var "S2")))) "holds" (Bool "for" (Set (Var "b6")) "being" ($#m2_pboole :::"ManySortedFunction":::) "of" (Set "(" ($#k11_msafree :::"FreeMSA"::: ) (Set "(" (Set (Var "X")) ($#k3_relat_1 :::"*"::: ) (Set (Var "f")) ")" ) ")" ) "," (Set "(" (Set "(" ($#k11_msafree :::"FreeMSA"::: ) (Set (Var "X")) ")" ) ($#k1_instalg1 :::"|"::: ) "(" (Set (Var "S1")) "," (Set (Var "f")) "," (Set (Var "g")) ")" ")" ) "holds" (Bool "(" (Bool (Set (Var "b6")) ($#r1_hidden :::"="::: ) (Set ($#k3_instalg1 :::"hom"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "X")) "," (Set (Var "S1")) "," (Set (Var "S2")) ")" )) "iff" (Bool "(" (Bool (Set (Var "b6")) ($#r1_msualg_3 :::"is_homomorphism"::: ) (Set ($#k11_msafree :::"FreeMSA"::: ) (Set "(" (Set (Var "X")) ($#k3_relat_1 :::"*"::: ) (Set (Var "f")) ")" )) "," (Set (Set "(" ($#k11_msafree :::"FreeMSA"::: ) (Set (Var "X")) ")" ) ($#k1_instalg1 :::"|"::: ) "(" (Set (Var "S1")) "," (Set (Var "f")) "," (Set (Var "g")) ")" )) & (Bool "(" "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"SortSymbol":::) "of" (Set (Var "S1")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set "(" (Set (Var "X")) ($#k3_relat_1 :::"*"::: ) (Set (Var "f")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "s"))) "holds" (Bool (Set (Set "(" (Set (Var "b6")) ($#k1_msualg_3 :::"."::: ) (Set (Var "s")) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_trees_4 :::"root-tree"::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "s")) ($#k4_tarski :::"]"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_trees_4 :::"root-tree"::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "s")) ")" ) ($#k4_tarski :::"]"::: ) )))) ")" ) ")" ) ")" )))))); theorem :: INSTALG1:40 (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "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" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S2"))) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S1"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S2"))) (Bool "for" (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "f")) "," (Set (Var "g")) ($#r3_pua2mss1 :::"form_morphism_between"::: ) (Set (Var "S1")) "," (Set (Var "S2")))) "holds" (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S1")) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_msualg_1 :::"Args"::: ) "(" (Set (Var "o")) "," (Set "(" ($#k11_msafree :::"FreeMSA"::: ) (Set "(" (Set (Var "X")) ($#k3_relat_1 :::"*"::: ) (Set (Var "f")) ")" ) ")" ) ")" ) (Bool "for" (Set (Var "q")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set (Var "q")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_instalg1 :::"hom"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "X")) "," (Set (Var "S1")) "," (Set (Var "S2")) ")" ")" ) ($#k5_msualg_3 :::"#"::: ) (Set (Var "p"))))) "holds" (Bool (Set (Set "(" (Set "(" ($#k3_instalg1 :::"hom"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "X")) "," (Set (Var "S1")) "," (Set (Var "S2")) ")" ")" ) ($#k1_msualg_3 :::"."::: ) (Set "(" ($#k2_msualg_1 :::"the_result_sort_of"::: ) (Set (Var "o")) ")" ) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set ($#k4_tarski :::"["::: ) (Set (Var "o")) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S1"))) ($#k4_tarski :::"]"::: ) ) ($#k4_trees_4 :::"-tree"::: ) (Set (Var "p")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set ($#k4_tarski :::"["::: ) (Set "(" (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "o")) ")" ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S2"))) ($#k4_tarski :::"]"::: ) ) ($#k4_trees_4 :::"-tree"::: ) (Set (Var "q"))))))))))) ; theorem :: INSTALG1:41 (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "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" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S2"))) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S1"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S2"))) (Bool "for" (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "f")) "," (Set (Var "g")) ($#r3_pua2mss1 :::"form_morphism_between"::: ) (Set (Var "S1")) "," (Set (Var "S2")))) "holds" (Bool "for" (Set (Var "t")) "being" ($#m1_dtconstr :::"Term":::) "of" (Set (Var "S1")) "," (Set "(" (Set (Var "X")) ($#k3_relat_1 :::"*"::: ) (Set (Var "f")) ")" ) "holds" (Bool "(" (Bool (Set (Set "(" (Set "(" ($#k3_instalg1 :::"hom"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "X")) "," (Set (Var "S1")) "," (Set (Var "S2")) ")" ")" ) ($#k1_msualg_3 :::"."::: ) (Set "(" ($#k7_msaterm :::"the_sort_of"::: ) (Set (Var "t")) ")" ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "t"))) "is" ($#m2_msaterm :::"CompoundTerm"::: ) "of" (Set (Var "S2")) "," (Set (Var "X"))) "iff" (Bool (Set (Var "t")) "is" ($#m2_msaterm :::"CompoundTerm"::: ) "of" (Set (Var "S1")) "," (Set (Set (Var "X")) ($#k3_relat_1 :::"*"::: ) (Set (Var "f")))) ")" )))))) ; theorem :: INSTALG1:42 (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "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" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S2"))) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S1"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S2"))) (Bool "for" (Set (Var "g")) "being" ($#v2_funct_1 :::"one-to-one"::: ) ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "f")) "," (Set (Var "g")) ($#r3_pua2mss1 :::"form_morphism_between"::: ) (Set (Var "S1")) "," (Set (Var "S2")))) "holds" (Bool (Set ($#k3_instalg1 :::"hom"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "X")) "," (Set (Var "S1")) "," (Set (Var "S2")) ")" ) ($#r3_msualg_3 :::"is_monomorphism"::: ) (Set ($#k11_msafree :::"FreeMSA"::: ) (Set "(" (Set (Var "X")) ($#k3_relat_1 :::"*"::: ) (Set (Var "f")) ")" )) "," (Set (Set "(" ($#k11_msafree :::"FreeMSA"::: ) (Set (Var "X")) ")" ) ($#k1_instalg1 :::"|"::: ) "(" (Set (Var "S1")) "," (Set (Var "f")) "," (Set (Var "g")) ")" )))))) ; theorem :: INSTALG1:43 (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" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) "holds" (Bool (Set ($#k3_instalg1 :::"hom"::: ) "(" (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"))) ")" ) "," (Set (Var "X")) "," (Set (Var "S")) "," (Set (Var "S")) ")" ) ($#r8_pboole :::"="::: ) (Set ($#k2_msualg_3 :::"id"::: ) (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set "(" ($#k11_msafree :::"FreeMSA"::: ) (Set (Var "X")) ")" )))))) ; theorem :: INSTALG1:44 (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "," (Set (Var "S3")) "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" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S3"))) (Bool "for" (Set (Var "f1")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S1"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S2"))) (Bool "for" (Set (Var "g1")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "f1")) "," (Set (Var "g1")) ($#r3_pua2mss1 :::"form_morphism_between"::: ) (Set (Var "S1")) "," (Set (Var "S2")))) "holds" (Bool "for" (Set (Var "f2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S2"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S3"))) (Bool "for" (Set (Var "g2")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "f2")) "," (Set (Var "g2")) ($#r3_pua2mss1 :::"form_morphism_between"::: ) (Set (Var "S2")) "," (Set (Var "S3")))) "holds" (Bool (Set ($#k3_instalg1 :::"hom"::: ) "(" (Set "(" (Set (Var "f2")) ($#k1_partfun1 :::"*"::: ) (Set (Var "f1")) ")" ) "," (Set "(" (Set (Var "g2")) ($#k3_relat_1 :::"*"::: ) (Set (Var "g1")) ")" ) "," (Set (Var "X")) "," (Set (Var "S1")) "," (Set (Var "S3")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k3_instalg1 :::"hom"::: ) "(" (Set (Var "f2")) "," (Set (Var "g2")) "," (Set (Var "X")) "," (Set (Var "S2")) "," (Set (Var "S3")) ")" ")" ) ($#k3_relat_1 :::"*"::: ) (Set (Var "f1")) ")" ) ($#k8_pboole :::"**"::: ) (Set "(" ($#k3_instalg1 :::"hom"::: ) "(" (Set (Var "f1")) "," (Set (Var "g1")) "," (Set "(" (Set (Var "X")) ($#k3_relat_1 :::"*"::: ) (Set (Var "f2")) ")" ) "," (Set (Var "S1")) "," (Set (Var "S2")) ")" ")" ))))))))) ;