:: EXTENS_1 semantic presentation begin begin theorem :: EXTENS_1: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 "B")) "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 "X")) "being" ($#m3_pboole :::"ManySortedSubset"::: ) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "A")) ($#r2_pboole :::"c="::: ) (Set (Var "X")))) "holds" (Bool (Set (Set (Var "F")) ($#k1_msafree :::"||"::: ) (Set (Var "X"))) ($#r6_pboole :::"="::: ) (Set (Var "F")))))))) ; theorem :: EXTENS_1:2 (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 "M")) "being" ($#m3_pboole :::"ManySortedSubset"::: ) "of" (Set (Var "A")) (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 "M"))) ($#r2_pboole :::"c="::: ) (Set (Set (Var "F")) ($#k9_pboole :::".:.:"::: ) (Set (Var "A")))))))) ; theorem :: EXTENS_1:3 (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")) "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 "M1")) "," (Set (Var "M2")) "being" ($#m3_pboole :::"ManySortedSubset"::: ) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "M1")) ($#r2_pboole :::"c="::: ) (Set (Var "M2")))) "holds" (Bool (Set (Set "(" (Set (Var "F")) ($#k1_msafree :::"||"::: ) (Set (Var "M2")) ")" ) ($#k9_pboole :::".:.:"::: ) (Set (Var "M1"))) ($#r6_pboole :::"="::: ) (Set (Set (Var "F")) ($#k9_pboole :::".:.:"::: ) (Set (Var "M1"))))))))) ; theorem :: EXTENS_1:4 (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")) (Bool "for" (Set (Var "X")) "being" ($#m3_pboole :::"ManySortedSubset"::: ) "of" (Set (Var "A")) "holds" (Bool (Set (Set "(" (Set (Var "G")) ($#k3_msualg_3 :::"**"::: ) (Set (Var "F")) ")" ) ($#k1_msafree :::"||"::: ) (Set (Var "X"))) ($#r6_pboole :::"="::: ) (Set (Set (Var "G")) ($#k3_msualg_3 :::"**"::: ) (Set "(" (Set (Var "F")) ($#k1_msafree :::"||"::: ) (Set (Var "X")) ")" ))))))))) ; theorem :: EXTENS_1: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")) "st" (Bool (Bool (Set (Var "A")) ($#r1_pzfmisc1 :::"is_transformable_to"::: ) (Set (Var "B")))) "holds" (Bool "for" (Set (Var "F")) "being" ($#m2_pboole :::"ManySortedFunction"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) (Bool "for" (Set (Var "C")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Var "B")) "is" ($#m3_pboole :::"ManySortedSubset"::: ) "of" (Set (Var "C")))) "holds" (Bool (Set (Var "F")) "is" ($#m2_pboole :::"ManySortedFunction"::: ) "of" (Set (Var "A")) "," (Set (Var "C"))))))) ; theorem :: EXTENS_1:6 (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")) "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 "X")) "being" ($#m3_pboole :::"ManySortedSubset"::: ) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_msualg_3 :::""1-1""::: ) )) "holds" (Bool (Set (Set (Var "F")) ($#k1_msafree :::"||"::: ) (Set (Var "X"))) "is" ($#v1_msualg_3 :::""1-1""::: ) )))))) ; begin theorem :: EXTENS_1:7 (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")) "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 "X")) "being" ($#m3_pboole :::"ManySortedSubset"::: ) "of" (Set (Var "A")) "holds" (Bool (Set ($#k2_funct_6 :::"doms"::: ) (Set "(" (Set (Var "F")) ($#k1_msafree :::"||"::: ) (Set (Var "X")) ")" )) ($#r2_pboole :::"c="::: ) (Set ($#k2_funct_6 :::"doms"::: ) (Set (Var "F"))))))))) ; theorem :: EXTENS_1:8 (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")) "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 "X")) "being" ($#m3_pboole :::"ManySortedSubset"::: ) "of" (Set (Var "A")) "holds" (Bool (Set ($#k3_funct_6 :::"rngs"::: ) (Set "(" (Set (Var "F")) ($#k1_msafree :::"||"::: ) (Set (Var "X")) ")" )) ($#r2_pboole :::"c="::: ) (Set ($#k3_funct_6 :::"rngs"::: ) (Set (Var "F"))))))))) ; theorem :: EXTENS_1: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")) "holds" (Bool "(" (Bool (Set (Var "F")) "is" ($#v2_msualg_3 :::""onto""::: ) ) "iff" (Bool (Set ($#k3_funct_6 :::"rngs"::: ) (Set (Var "F"))) ($#r6_pboole :::"="::: ) (Set (Var "B"))) ")" )))) ; theorem :: EXTENS_1:10 (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "X")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) "holds" (Bool (Set ($#k3_funct_6 :::"rngs"::: ) (Set "(" ($#k15_msafree :::"Reverse"::: ) (Set (Var "X")) ")" )) ($#r8_pboole :::"="::: ) (Set (Var "X"))))) ; theorem :: EXTENS_1: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 "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")) (Bool "for" (Set (Var "X")) "being" bbbadV2_RELAT_1() ($#m3_pboole :::"ManySortedSubset"::: ) "of" (Set (Var "B")) "st" (Bool (Bool (Set ($#k3_funct_6 :::"rngs"::: ) (Set (Var "F"))) ($#r2_pboole :::"c="::: ) (Set (Var "X")))) "holds" (Bool (Set (Set "(" (Set (Var "G")) ($#k1_msafree :::"||"::: ) (Set (Var "X")) ")" ) ($#k8_pboole :::"**"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k3_msualg_3 :::"**"::: ) (Set (Var "F")))))))))) ; begin theorem :: EXTENS_1:12 (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")) "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")) "holds" (Bool "(" (Bool (Set (Var "F")) "is" ($#v2_msualg_3 :::""onto""::: ) ) "iff" (Bool "for" (Set (Var "C")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "G")) "," (Set (Var "H")) "being" ($#m2_pboole :::"ManySortedFunction"::: ) "of" (Set (Var "B")) "," (Set (Var "C")) "st" (Bool (Bool (Set (Set (Var "G")) ($#k3_msualg_3 :::"**"::: ) (Set (Var "F"))) ($#r6_pboole :::"="::: ) (Set (Set (Var "H")) ($#k3_msualg_3 :::"**"::: ) (Set (Var "F"))))) "holds" (Bool (Set (Var "G")) ($#r6_pboole :::"="::: ) (Set (Var "H"))))) ")" ))))) ; theorem :: EXTENS_1:13 (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")) "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")) "st" (Bool (Bool (Set (Var "A")) "is" bbbadV2_RELAT_1())) "holds" (Bool "(" (Bool (Set (Var "F")) "is" ($#v1_msualg_3 :::""1-1""::: ) ) "iff" (Bool "for" (Set (Var "C")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "G")) "," (Set (Var "H")) "being" ($#m2_pboole :::"ManySortedFunction"::: ) "of" (Set (Var "C")) "," (Set (Var "A")) "st" (Bool (Bool (Set (Set (Var "F")) ($#k8_pboole :::"**"::: ) (Set (Var "G"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k8_pboole :::"**"::: ) (Set (Var "H"))))) "holds" (Bool (Set (Var "G")) ($#r6_pboole :::"="::: ) (Set (Var "H"))))) ")" ))))) ; begin theorem :: EXTENS_1:14 (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "U1")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "X")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) (Bool "for" (Set (Var "h1")) "," (Set (Var "h2")) "being" ($#m2_pboole :::"ManySortedFunction":::) "of" (Set "(" ($#k11_msafree :::"FreeMSA"::: ) (Set (Var "X")) ")" ) "," (Set (Var "U1")) "st" (Bool (Bool (Set (Var "h1")) ($#r1_msualg_3 :::"is_homomorphism"::: ) (Set ($#k11_msafree :::"FreeMSA"::: ) (Set (Var "X"))) "," (Set (Var "U1"))) & (Bool (Set (Var "h2")) ($#r1_msualg_3 :::"is_homomorphism"::: ) (Set ($#k11_msafree :::"FreeMSA"::: ) (Set (Var "X"))) "," (Set (Var "U1"))) & (Bool (Set (Set (Var "h1")) ($#k1_msafree :::"||"::: ) (Set "(" ($#k13_msafree :::"FreeGen"::: ) (Set (Var "X")) ")" )) ($#r8_pboole :::"="::: ) (Set (Set (Var "h2")) ($#k1_msafree :::"||"::: ) (Set "(" ($#k13_msafree :::"FreeGen"::: ) (Set (Var "X")) ")" )))) "holds" (Bool (Set (Var "h1")) ($#r8_pboole :::"="::: ) (Set (Var "h2"))))))) ; theorem :: EXTENS_1:15 (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "U1")) "," (Set (Var "U2")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "F")) "being" ($#m2_pboole :::"ManySortedFunction":::) "of" (Set (Var "U1")) "," (Set (Var "U2")) "st" (Bool (Bool (Set (Var "F")) ($#r2_msualg_3 :::"is_epimorphism"::: ) (Set (Var "U1")) "," (Set (Var "U2")))) "holds" (Bool "for" (Set (Var "U3")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "h1")) "," (Set (Var "h2")) "being" ($#m2_pboole :::"ManySortedFunction":::) "of" (Set (Var "U2")) "," (Set (Var "U3")) "st" (Bool (Bool (Set (Set (Var "h1")) ($#k3_msualg_3 :::"**"::: ) (Set (Var "F"))) ($#r8_pboole :::"="::: ) (Set (Set (Var "h2")) ($#k3_msualg_3 :::"**"::: ) (Set (Var "F"))))) "holds" (Bool (Set (Var "h1")) ($#r8_pboole :::"="::: ) (Set (Var "h2")))))))) ; theorem :: EXTENS_1:16 (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "U2")) "," (Set (Var "U3")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "F")) "being" ($#m2_pboole :::"ManySortedFunction":::) "of" (Set (Var "U2")) "," (Set (Var "U3")) "st" (Bool (Bool (Set (Var "F")) ($#r1_msualg_3 :::"is_homomorphism"::: ) (Set (Var "U2")) "," (Set (Var "U3")))) "holds" (Bool "(" (Bool (Set (Var "F")) ($#r3_msualg_3 :::"is_monomorphism"::: ) (Set (Var "U2")) "," (Set (Var "U3"))) "iff" (Bool "for" (Set (Var "U1")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "h1")) "," (Set (Var "h2")) "being" ($#m2_pboole :::"ManySortedFunction":::) "of" (Set (Var "U1")) "," (Set (Var "U2")) "st" (Bool (Bool (Set (Var "h1")) ($#r1_msualg_3 :::"is_homomorphism"::: ) (Set (Var "U1")) "," (Set (Var "U2"))) & (Bool (Set (Var "h2")) ($#r1_msualg_3 :::"is_homomorphism"::: ) (Set (Var "U1")) "," (Set (Var "U2"))) & (Bool (Set (Set (Var "F")) ($#k3_msualg_3 :::"**"::: ) (Set (Var "h1"))) ($#r8_pboole :::"="::: ) (Set (Set (Var "F")) ($#k3_msualg_3 :::"**"::: ) (Set (Var "h2"))))) "holds" (Bool (Set (Var "h1")) ($#r8_pboole :::"="::: ) (Set (Var "h2"))))) ")" )))) ; registrationlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; let "U1" be ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Const "S")); cluster ($#v1_relat_1 :::"Relation-like"::: ) bbbadV2_RELAT_1() (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S") ($#v4_relat_1 :::"-defined"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_partfun1 :::"total"::: ) for ($#m1_msafree :::"GeneratorSet"::: ) "of" "U1"; end; theorem :: EXTENS_1:17 (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "U1")) "being" ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m3_pboole :::"MSSubset":::) "of" (Set (Var "U1")) "st" (Bool (Bool (Set (Var "A")) "is" ($#m3_pboole :::"ManySortedSubset"::: ) "of" (Set (Var "B")))) "holds" (Bool (Set ($#k12_msualg_2 :::"GenMSAlg"::: ) (Set (Var "A"))) "is" ($#m1_msualg_2 :::"MSSubAlgebra"::: ) "of" (Set ($#k12_msualg_2 :::"GenMSAlg"::: ) (Set (Var "B"))))))) ; theorem :: EXTENS_1:18 (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "U1")) "being" ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "U2")) "being" ($#m1_msualg_2 :::"MSSubAlgebra"::: ) "of" (Set (Var "U1")) (Bool "for" (Set (Var "B1")) "being" ($#m3_pboole :::"MSSubset":::) "of" (Set (Var "U1")) (Bool "for" (Set (Var "B2")) "being" ($#m3_pboole :::"MSSubset":::) "of" (Set (Var "U2")) "st" (Bool (Bool (Set (Var "B1")) ($#r8_pboole :::"="::: ) (Set (Var "B2")))) "holds" (Bool (Set ($#k12_msualg_2 :::"GenMSAlg"::: ) (Set (Var "B1"))) ($#r1_hidden :::"="::: ) (Set ($#k12_msualg_2 :::"GenMSAlg"::: ) (Set (Var "B2"))))))))) ; theorem :: EXTENS_1:19 (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "U1")) "," (Set (Var "U2")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "Gen")) "being" ($#m1_msafree :::"GeneratorSet"::: ) "of" (Set (Var "U1")) (Bool "for" (Set (Var "h1")) "," (Set (Var "h2")) "being" ($#m2_pboole :::"ManySortedFunction":::) "of" (Set (Var "U1")) "," (Set (Var "U2")) "st" (Bool (Bool (Set (Var "h1")) ($#r1_msualg_3 :::"is_homomorphism"::: ) (Set (Var "U1")) "," (Set (Var "U2"))) & (Bool (Set (Var "h2")) ($#r1_msualg_3 :::"is_homomorphism"::: ) (Set (Var "U1")) "," (Set (Var "U2"))) & (Bool (Set (Set (Var "h1")) ($#k1_msafree :::"||"::: ) (Set (Var "Gen"))) ($#r8_pboole :::"="::: ) (Set (Set (Var "h2")) ($#k1_msafree :::"||"::: ) (Set (Var "Gen"))))) "holds" (Bool (Set (Var "h1")) ($#r8_pboole :::"="::: ) (Set (Var "h2"))))))) ;