:: MSUALG_2  semantic presentation begin  



registrationlet "I" be    ($#m1_hidden :::"set"::: )  ; let "X" be   ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); let "Y" be bbbadV2_RELAT_1()  ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); 
cluster (Set "X"  ($#k2_pboole :::"\/"::: )  "Y") -> bbbadV2_RELAT_1() ; 

cluster (Set "Y"  ($#k2_pboole :::"\/"::: )  "X") -> bbbadV2_RELAT_1() ; 
end; 
theorem :: MSUALG_2:1 (Bool  "for" (Set (Var "I")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"   ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I"))  (Bool  "for" (Set (Var "i")) "being"    ($#m2_finseq_2 :::"Element"::: )   "of" (Set (Set (Var "I"))  ($#k3_finseq_2 :::"*"::: )  ) "holds"  (Bool (Set   ($#k4_card_3 :::"product"::: )  (Set  "(" (Set  "(" (Set (Var "X"))  ($#k3_pboole :::"/\"::: )  (Set (Var "Y")) ")" )  ($#k3_relat_1 :::"*"::: )  (Set (Var "i")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k4_card_3 :::"product"::: )  (Set  "(" (Set (Var "X"))  ($#k3_relat_1 :::"*"::: )  (Set (Var "i")) ")" ) ")" )  ($#k3_xboole_0 :::"/\"::: )  (Set  "("  ($#k4_card_3 :::"product"::: )  (Set  "(" (Set (Var "Y"))  ($#k3_relat_1 :::"*"::: )  (Set (Var "i")) ")" ) ")" )))))) ; 
 begin  










definitionlet "S" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_msualg_1 :::"ManySortedSign"::: )  ; let "U0" be    ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Const "S")); mode MSSubset of "U0" is    ($#m3_pboole :::"ManySortedSubset"::: )   "of" (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" "U0"); end; definitionlet "S" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_msualg_1 :::"ManySortedSign"::: )  ; let "IT" be   ($#m1_subset_1 :::"SortSymbol":::) "of" (Set (Const "S")); attr "IT" is  :::"with_const_op":::  means :: MSUALG_2:def 1 (Bool  "ex" (Set (Var "o")) "being"   ($#m1_subset_1 :::"OperSymbol":::) "of" "S" "st"  (Bool  "("  (Bool (Set (Set  "the"  ($#u1_msualg_1 :::"Arity"::: )  "of" "S")  ($#k1_funct_1 :::"."::: )  (Set (Var "o")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) & (Bool (Set (Set  "the"  ($#u2_msualg_1 :::"ResultSort"::: )  "of" "S")  ($#k1_funct_1 :::"."::: )  (Set (Var "o")))  ($#r1_hidden :::"="::: )  "IT")  ")" )); end; 





:: deftheorem    defines :::"with_const_op"::: MSUALG_2:def 1 :  (Bool  "for" (Set (Var "S")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_msualg_1 :::"ManySortedSign"::: )    (Bool  "for" (Set (Var "IT")) "being"   ($#m1_subset_1 :::"SortSymbol":::) "of" (Set (Var "S")) "holds"   (Bool  "("  (Bool (Set (Var "IT")) "is"   ($#v1_msualg_2 :::"with_const_op"::: )  ) "iff" (Bool  "ex" (Set (Var "o")) "being"   ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S")) "st"  (Bool  "("  (Bool (Set (Set  "the"  ($#u1_msualg_1 :::"Arity"::: )  "of" (Set (Var "S")))  ($#k1_funct_1 :::"."::: )  (Set (Var "o")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) & (Bool (Set (Set  "the"  ($#u2_msualg_1 :::"ResultSort"::: )  "of" (Set (Var "S")))  ($#k1_funct_1 :::"."::: )  (Set (Var "o")))  ($#r1_hidden :::"="::: )  (Set (Var "IT")))  ")" ))  ")" ))); 
 definitionlet "IT" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_msualg_1 :::"ManySortedSign"::: )  ; attr "IT" is  :::"all-with_const_op":::  means :: MSUALG_2:def 2 (Bool  "for" (Set (Var "s")) "being"   ($#m1_subset_1 :::"SortSymbol":::) "of" "IT" "holds"  (Bool (Set (Var "s")) "is"   ($#v1_msualg_2 :::"with_const_op"::: )  )); end; 




:: deftheorem    defines :::"all-with_const_op"::: MSUALG_2:def 2 :  (Bool  "for" (Set (Var "IT")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_msualg_1 :::"ManySortedSign"::: )   "holds"   (Bool  "("  (Bool (Set (Var "IT")) "is"   ($#v2_msualg_2 :::"all-with_const_op"::: )  ) "iff" (Bool  "for" (Set (Var "s")) "being"   ($#m1_subset_1 :::"SortSymbol":::) "of" (Set (Var "IT")) "holds"  (Bool (Set (Var "s")) "is"   ($#v1_msualg_2 :::"with_const_op"::: )  ))  ")" )); 
 registrationlet "A" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; let "B" be    ($#m1_hidden :::"set"::: )  ; let "a" be   ($#m1_subset_1 :::"Function":::) "of" (Set (Const "B")) "," (Set  "(" (Set (Const "A"))  ($#k3_finseq_2 :::"*"::: )  ")" ); let "r" be   ($#m1_subset_1 :::"Function":::) "of" (Set (Const "B")) "," (Set (Const "A")); 
cluster (Set   ($#g1_msualg_1 :::"ManySortedSign"::: )  "(#"  "A" "," "B" "," "a" "," "r" "#)" ) ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )  ; 
end; registration
cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )  bbbadV14_STRUCT_0()   ($#v1_msualg_1 :::"strict"::: )     ($#v2_msualg_2 :::"all-with_const_op"::: )    for    ($#l1_msualg_1 :::"ManySortedSign"::: )  ; 
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 "U0" be    ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Const "S")); let "s" be   ($#m1_subset_1 :::"SortSymbol":::) "of" (Set (Const "S")); func  :::"Constants":::  "(" "U0" "," "s" ")"  ->   ($#m1_subset_1 :::"Subset":::) "of" (Set  "(" (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" "U0")  ($#k1_funct_1 :::"."::: )  "s" ")" ) means :: MSUALG_2:def 3 (Bool  "ex" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )   "st"  (Bool  "("  (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" "U0")  ($#k1_funct_1 :::"."::: )  "s")) & (Bool it  ($#r1_hidden :::"="::: )   "{"  (Set (Var "a")) where a "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "A")) : (Bool  "ex" (Set (Var "o")) "being"   ($#m1_subset_1 :::"OperSymbol":::) "of" "S" "st"  (Bool  "("  (Bool (Set (Set  "the"  ($#u1_msualg_1 :::"Arity"::: )  "of" "S")  ($#k3_funct_2 :::"."::: )  (Set (Var "o")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) & (Bool (Set (Set  "the"  ($#u2_msualg_1 :::"ResultSort"::: )  "of" "S")  ($#k3_funct_2 :::"."::: )  (Set (Var "o")))  ($#r1_hidden :::"="::: )  "s") & (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set  "("  ($#k5_msualg_1 :::"Den"::: )   "(" (Set (Var "o")) "," "U0" ")"  ")" )))  ")" ))  "}"  )  ")" )) if (Bool (Set (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" "U0")  ($#k1_funct_1 :::"."::: )  "s")  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))  otherwise (Bool it  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )); end; 







:: deftheorem    defines :::"Constants"::: MSUALG_2:def 3 :  (Bool  "for" (Set (Var "S")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )    ($#l1_msualg_1 :::"ManySortedSign"::: )    (Bool  "for" (Set (Var "U0")) "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 "b4")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "(" (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" (Set (Var "U0")))  ($#k1_funct_1 :::"."::: )  (Set (Var "s")) ")" ) "holds"   (Bool  "("   "("  (Bool (Bool (Set (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" (Set (Var "U0")))  ($#k1_funct_1 :::"."::: )  (Set (Var "s")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) "implies" (Bool  "("  (Bool (Set (Var "b4"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_msualg_2 :::"Constants"::: )   "(" (Set (Var "U0")) "," (Set (Var "s")) ")" )) "iff" (Bool  "ex" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )   "st"  (Bool  "("  (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" (Set (Var "U0")))  ($#k1_funct_1 :::"."::: )  (Set (Var "s")))) & (Bool (Set (Var "b4"))  ($#r1_hidden :::"="::: )   "{"  (Set (Var "a")) where a "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "A")) : (Bool  "ex" (Set (Var "o")) "being"   ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S")) "st"  (Bool  "("  (Bool (Set (Set  "the"  ($#u1_msualg_1 :::"Arity"::: )  "of" (Set (Var "S")))  ($#k3_funct_2 :::"."::: )  (Set (Var "o")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) & (Bool (Set (Set  "the"  ($#u2_msualg_1 :::"ResultSort"::: )  "of" (Set (Var "S")))  ($#k3_funct_2 :::"."::: )  (Set (Var "o")))  ($#r1_hidden :::"="::: )  (Set (Var "s"))) & (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set  "("  ($#k5_msualg_1 :::"Den"::: )   "(" (Set (Var "o")) "," (Set (Var "U0")) ")"  ")" )))  ")" ))  "}"  )  ")" ))  ")" )  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" (Set (Var "U0")))  ($#k1_funct_1 :::"."::: )  (Set (Var "s")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )))) "implies" (Bool  "("  (Bool (Set (Var "b4"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_msualg_2 :::"Constants"::: )   "(" (Set (Var "U0")) "," (Set (Var "s")) ")" )) "iff" (Bool (Set (Var "b4"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))  ")" )  ")"   ")" ))))); 
 definitionlet "S" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )    ($#l1_msualg_1 :::"ManySortedSign"::: )  ; let "U0" be    ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Const "S")); func  :::"Constants"::: "U0" ->   ($#m3_pboole :::"MSSubset":::) "of" "U0" means :: MSUALG_2:def 4 (Bool  "for" (Set (Var "s")) "being"   ($#m1_subset_1 :::"SortSymbol":::) "of" "S" "holds"  (Bool (Set it  ($#k1_funct_1 :::"."::: )  (Set (Var "s")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_msualg_2 :::"Constants"::: )   "(" "U0" "," (Set (Var "s")) ")" ))); end; 






:: deftheorem    defines :::"Constants"::: MSUALG_2:def 4 :  (Bool  "for" (Set (Var "S")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )    ($#l1_msualg_1 :::"ManySortedSign"::: )    (Bool  "for" (Set (Var "U0")) "being"    ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Var "S"))  (Bool  "for" (Set (Var "b3")) "being"   ($#m3_pboole :::"MSSubset":::) "of" (Set (Var "U0")) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_msualg_2 :::"Constants"::: )  (Set (Var "U0")))) "iff" (Bool  "for" (Set (Var "s")) "being"   ($#m1_subset_1 :::"SortSymbol":::) "of" (Set (Var "S")) "holds"  (Bool (Set (Set (Var "b3"))  ($#k1_funct_1 :::"."::: )  (Set (Var "s")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_msualg_2 :::"Constants"::: )   "(" (Set (Var "U0")) "," (Set (Var "s")) ")" )))  ")" )))); 
 registrationlet "S" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )    ($#v2_msualg_2 :::"all-with_const_op"::: )     ($#l1_msualg_1 :::"ManySortedSign"::: )  ; let "U0" be   ($#v4_msualg_1 :::"non-empty"::: )     ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Const "S")); let "s" be   ($#m1_subset_1 :::"SortSymbol":::) "of" (Set (Const "S")); 
cluster (Set   ($#k1_msualg_2 :::"Constants"::: )   "(" "U0" "," "s" ")" ) ->  ($#~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"::: )   )    ($#v2_msualg_2 :::"all-with_const_op"::: )     ($#l1_msualg_1 :::"ManySortedSign"::: )  ; let "U0" be   ($#v4_msualg_1 :::"non-empty"::: )     ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Const "S")); 
cluster (Set   ($#k2_msualg_2 :::"Constants"::: )  "U0") -> bbbadV2_RELAT_1() ; 
end; begin  definitionlet "S" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )    ($#l1_msualg_1 :::"ManySortedSign"::: )  ; let "U0" be    ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Const "S")); let "o" be   ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Const "S")); let "A" be   ($#m3_pboole :::"MSSubset":::) "of" (Set (Const "U0")); pred "A" :::"is_closed_on"::: "o" means :: MSUALG_2:def 5 (Bool (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set  "(" (Set  "("  ($#k5_msualg_1 :::"Den"::: )   "(" "o" "," "U0" ")"  ")" )  ($#k5_relat_1 :::"|"::: )  (Set  "(" (Set  "(" (Set  "(" "A"  ($#k6_finseq_2 :::"#"::: )  ")" )  ($#k3_relat_1 :::"*"::: )  (Set  "the"  ($#u1_msualg_1 :::"Arity"::: )  "of" "S") ")" )  ($#k1_funct_1 :::"."::: )  "o" ")" ) ")" ))  ($#r1_tarski :::"c="::: )  (Set (Set  "(" "A"  ($#k3_relat_1 :::"*"::: )  (Set  "the"  ($#u2_msualg_1 :::"ResultSort"::: )  "of" "S") ")" )  ($#k1_funct_1 :::"."::: )  "o")); end; 







:: deftheorem    defines :::"is_closed_on"::: MSUALG_2: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 "U0")) "being"    ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Var "S"))  (Bool  "for" (Set (Var "o")) "being"   ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S"))  (Bool  "for" (Set (Var "A")) "being"   ($#m3_pboole :::"MSSubset":::) "of" (Set (Var "U0")) "holds"   (Bool  "("  (Bool (Set (Var "A"))  ($#r1_msualg_2 :::"is_closed_on"::: )  (Set (Var "o"))) "iff" (Bool (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set  "(" (Set  "("  ($#k5_msualg_1 :::"Den"::: )   "(" (Set (Var "o")) "," (Set (Var "U0")) ")"  ")" )  ($#k5_relat_1 :::"|"::: )  (Set  "(" (Set  "(" (Set  "(" (Set (Var "A"))  ($#k6_finseq_2 :::"#"::: )  ")" )  ($#k3_relat_1 :::"*"::: )  (Set  "the"  ($#u1_msualg_1 :::"Arity"::: )  "of" (Set (Var "S"))) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "o")) ")" ) ")" ))  ($#r1_tarski :::"c="::: )  (Set (Set  "(" (Set (Var "A"))  ($#k3_relat_1 :::"*"::: )  (Set  "the"  ($#u2_msualg_1 :::"ResultSort"::: )  "of" (Set (Var "S"))) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "o"))))  ")" ))))); 
 definitionlet "S" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )    ($#l1_msualg_1 :::"ManySortedSign"::: )  ; let "U0" be    ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Const "S")); let "A" be   ($#m3_pboole :::"MSSubset":::) "of" (Set (Const "U0")); attr "A" is  :::"opers_closed":::  means :: MSUALG_2:def 6 (Bool  "for" (Set (Var "o")) "being"   ($#m1_subset_1 :::"OperSymbol":::) "of" "S" "holds"  (Bool "A"  ($#r1_msualg_2 :::"is_closed_on"::: )  (Set (Var "o")))); end; 






:: deftheorem    defines :::"opers_closed"::: MSUALG_2: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 "U0")) "being"    ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Var "S"))  (Bool  "for" (Set (Var "A")) "being"   ($#m3_pboole :::"MSSubset":::) "of" (Set (Var "U0")) "holds"   (Bool  "("  (Bool (Set (Var "A")) "is"   ($#v3_msualg_2 :::"opers_closed"::: )  ) "iff" (Bool  "for" (Set (Var "o")) "being"   ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S")) "holds"  (Bool (Set (Var "A"))  ($#r1_msualg_2 :::"is_closed_on"::: )  (Set (Var "o"))))  ")" )))); 
 
theorem :: MSUALG_2: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 "o")) "being"   ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S"))  (Bool  "for" (Set (Var "U0")) "being"    ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Var "S"))  (Bool  "for" (Set (Var "B0")) "," (Set (Var "B1")) "being"   ($#m3_pboole :::"MSSubset":::) "of" (Set (Var "U0"))  "st" (Bool (Bool (Set (Var "B0"))  ($#r2_pboole :::"c="::: )  (Set (Var "B1")))) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set (Var "B0"))  ($#k6_finseq_2 :::"#"::: )  ")" )  ($#k3_relat_1 :::"*"::: )  (Set  "the"  ($#u1_msualg_1 :::"Arity"::: )  "of" (Set (Var "S"))) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "o")))  ($#r1_tarski :::"c="::: )  (Set (Set  "(" (Set  "(" (Set (Var "B1"))  ($#k6_finseq_2 :::"#"::: )  ")" )  ($#k3_relat_1 :::"*"::: )  (Set  "the"  ($#u1_msualg_1 :::"Arity"::: )  "of" (Set (Var "S"))) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "o")))))))) ; 
 definitionlet "S" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )    ($#l1_msualg_1 :::"ManySortedSign"::: )  ; let "U0" be    ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Const "S")); let "o" be   ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Const "S")); let "A" be   ($#m3_pboole :::"MSSubset":::) "of" (Set (Const "U0")); assume 
(Bool (Set (Const "A"))  ($#r1_msualg_2 :::"is_closed_on"::: )  (Set (Const "o")))
 ; func "o" :::"/."::: "A" ->   ($#m1_subset_1 :::"Function":::) "of" (Set  "(" (Set  "(" (Set  "(" "A"  ($#k6_finseq_2 :::"#"::: )  ")" )  ($#k3_relat_1 :::"*"::: )  (Set  "the"  ($#u1_msualg_1 :::"Arity"::: )  "of" "S") ")" )  ($#k1_funct_1 :::"."::: )  "o" ")" ) "," (Set  "(" (Set  "(" "A"  ($#k3_relat_1 :::"*"::: )  (Set  "the"  ($#u2_msualg_1 :::"ResultSort"::: )  "of" "S") ")" )  ($#k1_funct_1 :::"."::: )  "o" ")" ) equals :: MSUALG_2:def 7 (Set (Set  "("  ($#k5_msualg_1 :::"Den"::: )   "(" "o" "," "U0" ")"  ")" )  ($#k5_relat_1 :::"|"::: )  (Set  "(" (Set  "(" (Set  "(" "A"  ($#k6_finseq_2 :::"#"::: )  ")" )  ($#k3_relat_1 :::"*"::: )  (Set  "the"  ($#u1_msualg_1 :::"Arity"::: )  "of" "S") ")" )  ($#k1_funct_1 :::"."::: )  "o" ")" )); end; 









:: deftheorem    defines :::"/."::: MSUALG_2:def 7 :  (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 "o")) "being"   ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S"))  (Bool  "for" (Set (Var "A")) "being"   ($#m3_pboole :::"MSSubset":::) "of" (Set (Var "U0"))  "st" (Bool (Bool (Set (Var "A"))  ($#r1_msualg_2 :::"is_closed_on"::: )  (Set (Var "o")))) "holds"  (Bool (Set (Set (Var "o"))  ($#k3_msualg_2 :::"/."::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k5_msualg_1 :::"Den"::: )   "(" (Set (Var "o")) "," (Set (Var "U0")) ")"  ")" )  ($#k5_relat_1 :::"|"::: )  (Set  "(" (Set  "(" (Set  "(" (Set (Var "A"))  ($#k6_finseq_2 :::"#"::: )  ")" )  ($#k3_relat_1 :::"*"::: )  (Set  "the"  ($#u1_msualg_1 :::"Arity"::: )  "of" (Set (Var "S"))) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "o")) ")" ))))))); 
 definitionlet "S" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )    ($#l1_msualg_1 :::"ManySortedSign"::: )  ; let "U0" be    ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Const "S")); let "A" be   ($#m3_pboole :::"MSSubset":::) "of" (Set (Const "U0")); func  :::"Opers":::  "(" "U0" "," "A" ")"  ->    ($#m2_pboole :::"ManySortedFunction"::: )   "of" (Set (Set  "(" "A"  ($#k6_finseq_2 :::"#"::: )  ")" )  ($#k3_relat_1 :::"*"::: )  (Set  "the"  ($#u1_msualg_1 :::"Arity"::: )  "of" "S")) "," (Set "A"  ($#k3_relat_1 :::"*"::: )  (Set  "the"  ($#u2_msualg_1 :::"ResultSort"::: )  "of" "S")) means :: MSUALG_2:def 8 (Bool  "for" (Set (Var "o")) "being"   ($#m1_subset_1 :::"OperSymbol":::) "of" "S" "holds"  (Bool (Set it  ($#k1_funct_1 :::"."::: )  (Set (Var "o")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "o"))  ($#k3_msualg_2 :::"/."::: )  "A"))); end; 







:: deftheorem    defines :::"Opers"::: MSUALG_2:def 8 :  (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"   ($#m3_pboole :::"MSSubset":::) "of" (Set (Var "U0"))  (Bool  "for" (Set (Var "b4")) "being"    ($#m2_pboole :::"ManySortedFunction"::: )   "of" (Set (Set  "(" (Set (Var "A"))  ($#k6_finseq_2 :::"#"::: )  ")" )  ($#k3_relat_1 :::"*"::: )  (Set  "the"  ($#u1_msualg_1 :::"Arity"::: )  "of" (Set (Var "S")))) "," (Set (Set (Var "A"))  ($#k3_relat_1 :::"*"::: )  (Set  "the"  ($#u2_msualg_1 :::"ResultSort"::: )  "of" (Set (Var "S")))) "holds"   (Bool  "("  (Bool (Set (Var "b4"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_msualg_2 :::"Opers"::: )   "(" (Set (Var "U0")) "," (Set (Var "A")) ")" )) "iff" (Bool  "for" (Set (Var "o")) "being"   ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S")) "holds"  (Bool (Set (Set (Var "b4"))  ($#k1_funct_1 :::"."::: )  (Set (Var "o")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "o"))  ($#k3_msualg_2 :::"/."::: )  (Set (Var "A")))))  ")" ))))); 
 
theorem :: MSUALG_2: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 "U0")) "being"    ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Var "S"))  (Bool  "for" (Set (Var "B")) "being"   ($#m3_pboole :::"MSSubset":::) "of" (Set (Var "U0"))  "st" (Bool (Bool (Set (Var "B"))  ($#r8_pboole :::"="::: )  (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" (Set (Var "U0"))))) "holds"  (Bool  "("  (Bool (Set (Var "B")) "is"   ($#v3_msualg_2 :::"opers_closed"::: )  ) & (Bool  "("   "for" (Set (Var "o")) "being"   ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S")) "holds"  (Bool (Set (Set (Var "o"))  ($#k3_msualg_2 :::"/."::: )  (Set (Var "B")))  ($#r1_hidden :::"="::: )  (Set   ($#k5_msualg_1 :::"Den"::: )   "(" (Set (Var "o")) "," (Set (Var "U0")) ")" ))  ")" )  ")" )))) ; 
 
theorem :: MSUALG_2: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 "U0")) "being"    ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Var "S"))  (Bool  "for" (Set (Var "B")) "being"   ($#m3_pboole :::"MSSubset":::) "of" (Set (Var "U0"))  "st" (Bool (Bool (Set (Var "B"))  ($#r8_pboole :::"="::: )  (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" (Set (Var "U0"))))) "holds"  (Bool (Set   ($#k4_msualg_2 :::"Opers"::: )   "(" (Set (Var "U0")) "," (Set (Var "B")) ")" )  ($#r8_pboole :::"="::: )  (Set  "the"  ($#u4_msualg_1 :::"Charact"::: )  "of" (Set (Var "U0"))))))) ; 
 definitionlet "S" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )    ($#l1_msualg_1 :::"ManySortedSign"::: )  ; let "U0" be    ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Const "S")); mode  :::"MSSubAlgebra":::  "of" "U0" ->    ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" "S" means :: MSUALG_2:def 9 (Bool  "("  (Bool (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" it) "is"   ($#m3_pboole :::"MSSubset":::) "of" "U0") & (Bool  "("   "for" (Set (Var "B")) "being"   ($#m3_pboole :::"MSSubset":::) "of" "U0"  "st" (Bool (Bool (Set (Var "B"))  ($#r8_pboole :::"="::: )  (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" it))) "holds"  (Bool  "("  (Bool (Set (Var "B")) "is"   ($#v3_msualg_2 :::"opers_closed"::: )  ) & (Bool (Set  "the"  ($#u4_msualg_1 :::"Charact"::: )  "of" it)  ($#r8_pboole :::"="::: )  (Set   ($#k4_msualg_2 :::"Opers"::: )   "(" "U0" "," (Set (Var "B")) ")" ))  ")" )  ")" )  ")" ); end; 






:: deftheorem    defines :::"MSSubAlgebra"::: MSUALG_2:def 9 :  (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 "b3")) "being"    ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Var "S")) "holds"   (Bool  "("  (Bool (Set (Var "b3")) "is"    ($#m1_msualg_2 :::"MSSubAlgebra"::: )   "of" (Set (Var "U0"))) "iff" (Bool  "("  (Bool (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" (Set (Var "b3"))) "is"   ($#m3_pboole :::"MSSubset":::) "of" (Set (Var "U0"))) & (Bool  "("   "for" (Set (Var "B")) "being"   ($#m3_pboole :::"MSSubset":::) "of" (Set (Var "U0"))  "st" (Bool (Bool (Set (Var "B"))  ($#r8_pboole :::"="::: )  (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" (Set (Var "b3"))))) "holds"  (Bool  "("  (Bool (Set (Var "B")) "is"   ($#v3_msualg_2 :::"opers_closed"::: )  ) & (Bool (Set  "the"  ($#u4_msualg_1 :::"Charact"::: )  "of" (Set (Var "b3")))  ($#r8_pboole :::"="::: )  (Set   ($#k4_msualg_2 :::"Opers"::: )   "(" (Set (Var "U0")) "," (Set (Var "B")) ")" ))  ")" )  ")" )  ")" )  ")" ))); 
 registrationlet "S" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )    ($#l1_msualg_1 :::"ManySortedSign"::: )  ; let "U0" be    ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Const "S")); 
cluster   ($#v3_msualg_1 :::"strict"::: )    for    ($#m1_msualg_2 :::"MSSubAlgebra"::: )   "of" "U0"; 
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 "U0" be   ($#v4_msualg_1 :::"non-empty"::: )     ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Const "S")); 
cluster (Set   ($#g3_msualg_1 :::"MSAlgebra"::: )  "(#"  (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" "U0") "," (Set  "the"  ($#u4_msualg_1 :::"Charact"::: )  "of" "U0") "#)" ) ->   ($#v4_msualg_1 :::"non-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"::: )  ; let "U0" be   ($#v4_msualg_1 :::"non-empty"::: )     ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Const "S")); 
cluster   ($#v3_msualg_1 :::"strict"::: )     ($#v4_msualg_1 :::"non-empty"::: )    for    ($#m1_msualg_2 :::"MSSubAlgebra"::: )   "of" "U0"; 
end; 
theorem :: MSUALG_2: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 "U0")) "," (Set (Var "U1")) "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 "U0"))) "," (Set  "the"  ($#u4_msualg_1 :::"Charact"::: )  "of" (Set (Var "U0"))) "#)" )  ($#r1_hidden :::"="::: )  (Set   ($#g3_msualg_1 :::"MSAlgebra"::: )  "(#"  (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" (Set (Var "U1"))) "," (Set  "the"  ($#u4_msualg_1 :::"Charact"::: )  "of" (Set (Var "U1"))) "#)" ))) "holds"  (Bool (Set (Var "U0")) "is"    ($#m1_msualg_2 :::"MSSubAlgebra"::: )   "of" (Set (Var "U1"))))) ; 
 
theorem :: MSUALG_2: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 "U0")) "," (Set (Var "U1")) "," (Set (Var "U2")) "being"    ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Var "S"))  "st" (Bool (Bool (Set (Var "U0")) "is"    ($#m1_msualg_2 :::"MSSubAlgebra"::: )   "of" (Set (Var "U1"))) & (Bool (Set (Var "U1")) "is"    ($#m1_msualg_2 :::"MSSubAlgebra"::: )   "of" (Set (Var "U2")))) "holds"  (Bool (Set (Var "U0")) "is"    ($#m1_msualg_2 :::"MSSubAlgebra"::: )   "of" (Set (Var "U2"))))) ; 
 
theorem :: MSUALG_2:7 (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"    ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Var "S"))  "st" (Bool (Bool (Set (Var "U1")) "is"    ($#m1_msualg_2 :::"MSSubAlgebra"::: )   "of" (Set (Var "U2"))) & (Bool (Set (Var "U2")) "is"    ($#m1_msualg_2 :::"MSSubAlgebra"::: )   "of" (Set (Var "U1")))) "holds"  (Bool (Set   ($#g3_msualg_1 :::"MSAlgebra"::: )  "(#"  (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" (Set (Var "U1"))) "," (Set  "the"  ($#u4_msualg_1 :::"Charact"::: )  "of" (Set (Var "U1"))) "#)" )  ($#r1_hidden :::"="::: )  (Set   ($#g3_msualg_1 :::"MSAlgebra"::: )  "(#"  (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" (Set (Var "U2"))) "," (Set  "the"  ($#u4_msualg_1 :::"Charact"::: )  "of" (Set (Var "U2"))) "#)" )))) ; 
 
theorem :: MSUALG_2:8 (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 "U1")) "," (Set (Var "U2")) "being"    ($#m1_msualg_2 :::"MSSubAlgebra"::: )   "of" (Set (Var "U0"))  "st" (Bool (Bool (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" (Set (Var "U1")))  ($#r2_pboole :::"c="::: )  (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" (Set (Var "U2"))))) "holds"  (Bool (Set (Var "U1")) "is"    ($#m1_msualg_2 :::"MSSubAlgebra"::: )   "of" (Set (Var "U2")))))) ; 
 
theorem :: MSUALG_2:9 (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 "U1")) "," (Set (Var "U2")) "being"    ($#m1_msualg_2 :::"MSSubAlgebra"::: )   "of" (Set (Var "U0"))  "st" (Bool (Bool (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" (Set (Var "U1")))  ($#r8_pboole :::"="::: )  (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" (Set (Var "U2"))))) "holds"  (Bool (Set   ($#g3_msualg_1 :::"MSAlgebra"::: )  "(#"  (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" (Set (Var "U1"))) "," (Set  "the"  ($#u4_msualg_1 :::"Charact"::: )  "of" (Set (Var "U1"))) "#)" )  ($#r1_hidden :::"="::: )  (Set   ($#g3_msualg_1 :::"MSAlgebra"::: )  "(#"  (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" (Set (Var "U2"))) "," (Set  "the"  ($#u4_msualg_1 :::"Charact"::: )  "of" (Set (Var "U2"))) "#)" ))))) ; 
 
theorem :: MSUALG_2: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 "U0")) "being"    ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Var "S"))  (Bool  "for" (Set (Var "U1")) "being"    ($#m1_msualg_2 :::"MSSubAlgebra"::: )   "of" (Set (Var "U0")) "holds"  (Bool (Set   ($#k2_msualg_2 :::"Constants"::: )  (Set (Var "U0"))) "is"   ($#m3_pboole :::"MSSubset":::) "of" (Set (Var "U1")))))) ; 
 
theorem :: MSUALG_2:11 (Bool  "for" (Set (Var "S")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )    ($#v2_msualg_2 :::"all-with_const_op"::: )     ($#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 "U1")) "being"   ($#v4_msualg_1 :::"non-empty"::: )     ($#m1_msualg_2 :::"MSSubAlgebra"::: )   "of" (Set (Var "U0")) "holds"  (Bool (Set   ($#k2_msualg_2 :::"Constants"::: )  (Set (Var "U0"))) "is" bbbadV2_RELAT_1()  ($#m3_pboole :::"MSSubset":::) "of" (Set (Var "U1")))))) ; 
 
theorem :: MSUALG_2:12 (Bool  "for" (Set (Var "S")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )    ($#v2_msualg_2 :::"all-with_const_op"::: )     ($#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 "U1")) "," (Set (Var "U2")) "being"   ($#v4_msualg_1 :::"non-empty"::: )     ($#m1_msualg_2 :::"MSSubAlgebra"::: )   "of" (Set (Var "U0")) "holds"  (Bool (Set (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" (Set (Var "U1")))  ($#k3_pboole :::"/\"::: )  (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" (Set (Var "U2")))) "is" bbbadV2_RELAT_1())))) ; 
 begin  definitionlet "S" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )    ($#l1_msualg_1 :::"ManySortedSign"::: )  ; let "U0" be    ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Const "S")); let "A" be   ($#m3_pboole :::"MSSubset":::) "of" (Set (Const "U0")); func  :::"SubSort"::: "A" ->    ($#m1_hidden :::"set"::: )   means :: MSUALG_2:def 10 (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  it) "iff" (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_funct_2 :::"Funcs"::: )   "(" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "S") "," (Set  "("  ($#k9_setfam_1 :::"bool"::: )  (Set  "("  ($#k3_card_3 :::"Union"::: )  (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" "U0") ")" ) ")" ) ")" )) & (Bool (Set (Var "x")) "is"   ($#m3_pboole :::"MSSubset":::) "of" "U0") & (Bool  "("   "for" (Set (Var "B")) "being"   ($#m3_pboole :::"MSSubset":::) "of" "U0"  "st" (Bool (Bool (Set (Var "B"))  ($#r1_hidden :::"="::: )  (Set (Var "x")))) "holds"  (Bool  "("  (Bool (Set (Var "B")) "is"   ($#v3_msualg_2 :::"opers_closed"::: )  ) & (Bool (Set   ($#k2_msualg_2 :::"Constants"::: )  "U0")  ($#r2_pboole :::"c="::: )  (Set (Var "B"))) & (Bool "A"  ($#r2_pboole :::"c="::: )  (Set (Var "B")))  ")" )  ")" )  ")" )  ")" )); end; 







:: deftheorem    defines :::"SubSort"::: MSUALG_2:def 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 "U0")) "being"    ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Var "S"))  (Bool  "for" (Set (Var "A")) "being"   ($#m3_pboole :::"MSSubset":::) "of" (Set (Var "U0"))  (Bool  "for" (Set (Var "b4")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "b4"))  ($#r1_hidden :::"="::: )  (Set   ($#k5_msualg_2 :::"SubSort"::: )  (Set (Var "A")))) "iff" (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "b4"))) "iff" (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_funct_2 :::"Funcs"::: )   "(" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S"))) "," (Set  "("  ($#k9_setfam_1 :::"bool"::: )  (Set  "("  ($#k3_card_3 :::"Union"::: )  (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" (Set (Var "U0"))) ")" ) ")" ) ")" )) & (Bool (Set (Var "x")) "is"   ($#m3_pboole :::"MSSubset":::) "of" (Set (Var "U0"))) & (Bool  "("   "for" (Set (Var "B")) "being"   ($#m3_pboole :::"MSSubset":::) "of" (Set (Var "U0"))  "st" (Bool (Bool (Set (Var "B"))  ($#r1_hidden :::"="::: )  (Set (Var "x")))) "holds"  (Bool  "("  (Bool (Set (Var "B")) "is"   ($#v3_msualg_2 :::"opers_closed"::: )  ) & (Bool (Set   ($#k2_msualg_2 :::"Constants"::: )  (Set (Var "U0")))  ($#r2_pboole :::"c="::: )  (Set (Var "B"))) & (Bool (Set (Var "A"))  ($#r2_pboole :::"c="::: )  (Set (Var "B")))  ")" )  ")" )  ")" )  ")" ))  ")" ))))); 
 registrationlet "S" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )    ($#l1_msualg_1 :::"ManySortedSign"::: )  ; let "U0" be    ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Const "S")); let "A" be   ($#m3_pboole :::"MSSubset":::) "of" (Set (Const "U0")); 
cluster (Set   ($#k5_msualg_2 :::"SubSort"::: )  "A") ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )  ; 
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 "U0" be    ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Const "S")); func  :::"SubSort"::: "U0" ->    ($#m1_hidden :::"set"::: )   means :: MSUALG_2:def 11 (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  it) "iff" (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_funct_2 :::"Funcs"::: )   "(" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "S") "," (Set  "("  ($#k9_setfam_1 :::"bool"::: )  (Set  "("  ($#k3_card_3 :::"Union"::: )  (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" "U0") ")" ) ")" ) ")" )) & (Bool (Set (Var "x")) "is"   ($#m3_pboole :::"MSSubset":::) "of" "U0") & (Bool  "("   "for" (Set (Var "B")) "being"   ($#m3_pboole :::"MSSubset":::) "of" "U0"  "st" (Bool (Bool (Set (Var "B"))  ($#r1_hidden :::"="::: )  (Set (Var "x")))) "holds"  (Bool (Set (Var "B")) "is"   ($#v3_msualg_2 :::"opers_closed"::: )  )  ")" )  ")" )  ")" )); end; 






:: deftheorem    defines :::"SubSort"::: MSUALG_2:def 11 :  (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 "b3")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_msualg_2 :::"SubSort"::: )  (Set (Var "U0")))) "iff" (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "b3"))) "iff" (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_funct_2 :::"Funcs"::: )   "(" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S"))) "," (Set  "("  ($#k9_setfam_1 :::"bool"::: )  (Set  "("  ($#k3_card_3 :::"Union"::: )  (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" (Set (Var "U0"))) ")" ) ")" ) ")" )) & (Bool (Set (Var "x")) "is"   ($#m3_pboole :::"MSSubset":::) "of" (Set (Var "U0"))) & (Bool  "("   "for" (Set (Var "B")) "being"   ($#m3_pboole :::"MSSubset":::) "of" (Set (Var "U0"))  "st" (Bool (Bool (Set (Var "B"))  ($#r1_hidden :::"="::: )  (Set (Var "x")))) "holds"  (Bool (Set (Var "B")) "is"   ($#v3_msualg_2 :::"opers_closed"::: )  )  ")" )  ")" )  ")" ))  ")" )))); 
 registrationlet "S" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )    ($#l1_msualg_1 :::"ManySortedSign"::: )  ; let "U0" be    ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Const "S")); 
cluster (Set   ($#k6_msualg_2 :::"SubSort"::: )  "U0") ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )  ; 
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 "U0" be    ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Const "S")); let "e" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k6_msualg_2 :::"SubSort"::: )  (Set (Const "U0"))); func  :::"@"::: "e" ->   ($#m3_pboole :::"MSSubset":::) "of" "U0" equals :: MSUALG_2:def 12 "e"; end; 







:: deftheorem    defines :::"@"::: MSUALG_2:def 12 :  (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 "e")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k6_msualg_2 :::"SubSort"::: )  (Set (Var "U0"))) "holds"  (Bool (Set   ($#k7_msualg_2 :::"@"::: )  (Set (Var "e")))  ($#r1_hidden :::"="::: )  (Set (Var "e")))))); 
 
theorem :: MSUALG_2:13 (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")) "," (Set (Var "B")) "being"   ($#m3_pboole :::"MSSubset":::) "of" (Set (Var "U0")) "holds"   (Bool  "("  (Bool (Set (Var "B"))  ($#r2_hidden :::"in"::: )  (Set   ($#k5_msualg_2 :::"SubSort"::: )  (Set (Var "A")))) "iff" (Bool  "("  (Bool (Set (Var "B")) "is"   ($#v3_msualg_2 :::"opers_closed"::: )  ) & (Bool (Set   ($#k2_msualg_2 :::"Constants"::: )  (Set (Var "U0")))  ($#r2_pboole :::"c="::: )  (Set (Var "B"))) & (Bool (Set (Var "A"))  ($#r2_pboole :::"c="::: )  (Set (Var "B")))  ")" )  ")" )))) ; 
 
theorem :: MSUALG_2: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 "U0")) "being"    ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Var "S"))  (Bool  "for" (Set (Var "B")) "being"   ($#m3_pboole :::"MSSubset":::) "of" (Set (Var "U0")) "holds"   (Bool  "("  (Bool (Set (Var "B"))  ($#r2_hidden :::"in"::: )  (Set   ($#k6_msualg_2 :::"SubSort"::: )  (Set (Var "U0")))) "iff" (Bool (Set (Var "B")) "is"   ($#v3_msualg_2 :::"opers_closed"::: )  )  ")" )))) ; 
 definitionlet "S" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )    ($#l1_msualg_1 :::"ManySortedSign"::: )  ; let "U0" be    ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Const "S")); let "A" be   ($#m3_pboole :::"MSSubset":::) "of" (Set (Const "U0")); let "s" be   ($#m1_subset_1 :::"SortSymbol":::) "of" (Set (Const "S")); func  :::"SubSort":::  "(" "A" "," "s" ")"  ->    ($#m1_hidden :::"set"::: )   means :: MSUALG_2:def 13 (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  it) "iff" (Bool  "ex" (Set (Var "B")) "being"   ($#m3_pboole :::"MSSubset":::) "of" "U0" "st"  (Bool  "("  (Bool (Set (Var "B"))  ($#r2_hidden :::"in"::: )  (Set   ($#k5_msualg_2 :::"SubSort"::: )  "A")) & (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "B"))  ($#k1_funct_1 :::"."::: )  "s"))  ")" ))  ")" )); end; 








:: deftheorem    defines :::"SubSort"::: MSUALG_2:def 13 :  (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"   ($#m3_pboole :::"MSSubset":::) "of" (Set (Var "U0"))  (Bool  "for" (Set (Var "s")) "being"   ($#m1_subset_1 :::"SortSymbol":::) "of" (Set (Var "S"))  (Bool  "for" (Set (Var "b5")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "b5"))  ($#r1_hidden :::"="::: )  (Set   ($#k8_msualg_2 :::"SubSort"::: )   "(" (Set (Var "A")) "," (Set (Var "s")) ")" )) "iff" (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "b5"))) "iff" (Bool  "ex" (Set (Var "B")) "being"   ($#m3_pboole :::"MSSubset":::) "of" (Set (Var "U0")) "st"  (Bool  "("  (Bool (Set (Var "B"))  ($#r2_hidden :::"in"::: )  (Set   ($#k5_msualg_2 :::"SubSort"::: )  (Set (Var "A")))) & (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "B"))  ($#k1_funct_1 :::"."::: )  (Set (Var "s"))))  ")" ))  ")" ))  ")" )))))); 
 registrationlet "S" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )    ($#l1_msualg_1 :::"ManySortedSign"::: )  ; let "U0" be    ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Const "S")); let "A" be   ($#m3_pboole :::"MSSubset":::) "of" (Set (Const "U0")); let "s" be   ($#m1_subset_1 :::"SortSymbol":::) "of" (Set (Const "S")); 
cluster (Set   ($#k8_msualg_2 :::"SubSort"::: )   "(" "A" "," "s" ")" ) ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )  ; 
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 "U0" be    ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Const "S")); let "A" be   ($#m3_pboole :::"MSSubset":::) "of" (Set (Const "U0")); func  :::"MSSubSort"::: "A" ->   ($#m3_pboole :::"MSSubset":::) "of" "U0" means :: MSUALG_2:def 14 (Bool  "for" (Set (Var "s")) "being"   ($#m1_subset_1 :::"SortSymbol":::) "of" "S" "holds"  (Bool (Set it  ($#k1_funct_1 :::"."::: )  (Set (Var "s")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_setfam_1 :::"meet"::: )  (Set  "("  ($#k8_msualg_2 :::"SubSort"::: )   "(" "A" "," (Set (Var "s")) ")"  ")" )))); end; 







:: deftheorem    defines :::"MSSubSort"::: MSUALG_2:def 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 "U0")) "being"    ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Var "S"))  (Bool  "for" (Set (Var "A")) "," (Set (Var "b4")) "being"   ($#m3_pboole :::"MSSubset":::) "of" (Set (Var "U0")) "holds"   (Bool  "("  (Bool (Set (Var "b4"))  ($#r1_hidden :::"="::: )  (Set   ($#k9_msualg_2 :::"MSSubSort"::: )  (Set (Var "A")))) "iff" (Bool  "for" (Set (Var "s")) "being"   ($#m1_subset_1 :::"SortSymbol":::) "of" (Set (Var "S")) "holds"  (Bool (Set (Set (Var "b4"))  ($#k1_funct_1 :::"."::: )  (Set (Var "s")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_setfam_1 :::"meet"::: )  (Set  "("  ($#k8_msualg_2 :::"SubSort"::: )   "(" (Set (Var "A")) "," (Set (Var "s")) ")"  ")" ))))  ")" )))); 
 
theorem :: MSUALG_2: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 "U0")) "being"    ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Var "S"))  (Bool  "for" (Set (Var "A")) "being"   ($#m3_pboole :::"MSSubset":::) "of" (Set (Var "U0")) "holds"  (Bool (Set (Set  "("  ($#k2_msualg_2 :::"Constants"::: )  (Set (Var "U0")) ")" )  ($#k2_pboole :::"\/"::: )  (Set (Var "A")))  ($#r2_pboole :::"c="::: )  (Set   ($#k9_msualg_2 :::"MSSubSort"::: )  (Set (Var "A"))))))) ; 
 
theorem :: MSUALG_2: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 "U0")) "being"    ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Var "S"))  (Bool  "for" (Set (Var "A")) "being"   ($#m3_pboole :::"MSSubset":::) "of" (Set (Var "U0"))  "st" (Bool (Bool (Set (Set  "("  ($#k2_msualg_2 :::"Constants"::: )  (Set (Var "U0")) ")" )  ($#k2_pboole :::"\/"::: )  (Set (Var "A"))) "is" bbbadV2_RELAT_1())) "holds"  (Bool (Set   ($#k9_msualg_2 :::"MSSubSort"::: )  (Set (Var "A"))) "is" bbbadV2_RELAT_1())))) ; 
 
theorem :: MSUALG_2: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 "o")) "being"   ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S"))  (Bool  "for" (Set (Var "U0")) "being"    ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Var "S"))  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m3_pboole :::"MSSubset":::) "of" (Set (Var "U0"))  "st" (Bool (Bool (Set (Var "B"))  ($#r2_hidden :::"in"::: )  (Set   ($#k5_msualg_2 :::"SubSort"::: )  (Set (Var "A"))))) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set  "("  ($#k9_msualg_2 :::"MSSubSort"::: )  (Set (Var "A")) ")" )  ($#k6_finseq_2 :::"#"::: )  ")" )  ($#k3_relat_1 :::"*"::: )  (Set  "the"  ($#u1_msualg_1 :::"Arity"::: )  "of" (Set (Var "S"))) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "o")))  ($#r1_tarski :::"c="::: )  (Set (Set  "(" (Set  "(" (Set (Var "B"))  ($#k6_finseq_2 :::"#"::: )  ")" )  ($#k3_relat_1 :::"*"::: )  (Set  "the"  ($#u1_msualg_1 :::"Arity"::: )  "of" (Set (Var "S"))) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "o")))))))) ; 
 
theorem :: MSUALG_2: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 "o")) "being"   ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S"))  (Bool  "for" (Set (Var "U0")) "being"    ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Var "S"))  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m3_pboole :::"MSSubset":::) "of" (Set (Var "U0"))  "st" (Bool (Bool (Set (Var "B"))  ($#r2_hidden :::"in"::: )  (Set   ($#k5_msualg_2 :::"SubSort"::: )  (Set (Var "A"))))) "holds"  (Bool (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set  "(" (Set  "("  ($#k5_msualg_1 :::"Den"::: )   "(" (Set (Var "o")) "," (Set (Var "U0")) ")"  ")" )  ($#k5_relat_1 :::"|"::: )  (Set  "(" (Set  "(" (Set  "(" (Set  "("  ($#k9_msualg_2 :::"MSSubSort"::: )  (Set (Var "A")) ")" )  ($#k6_finseq_2 :::"#"::: )  ")" )  ($#k3_relat_1 :::"*"::: )  (Set  "the"  ($#u1_msualg_1 :::"Arity"::: )  "of" (Set (Var "S"))) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "o")) ")" ) ")" ))  ($#r1_tarski :::"c="::: )  (Set (Set  "(" (Set (Var "B"))  ($#k3_relat_1 :::"*"::: )  (Set  "the"  ($#u2_msualg_1 :::"ResultSort"::: )  "of" (Set (Var "S"))) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "o")))))))) ; 
 
theorem :: MSUALG_2: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 "o")) "being"   ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S"))  (Bool  "for" (Set (Var "U0")) "being"    ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Var "S"))  (Bool  "for" (Set (Var "A")) "being"   ($#m3_pboole :::"MSSubset":::) "of" (Set (Var "U0")) "holds"  (Bool (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set  "(" (Set  "("  ($#k5_msualg_1 :::"Den"::: )   "(" (Set (Var "o")) "," (Set (Var "U0")) ")"  ")" )  ($#k5_relat_1 :::"|"::: )  (Set  "(" (Set  "(" (Set  "(" (Set  "("  ($#k9_msualg_2 :::"MSSubSort"::: )  (Set (Var "A")) ")" )  ($#k6_finseq_2 :::"#"::: )  ")" )  ($#k3_relat_1 :::"*"::: )  (Set  "the"  ($#u1_msualg_1 :::"Arity"::: )  "of" (Set (Var "S"))) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "o")) ")" ) ")" ))  ($#r1_tarski :::"c="::: )  (Set (Set  "(" (Set  "("  ($#k9_msualg_2 :::"MSSubSort"::: )  (Set (Var "A")) ")" )  ($#k3_relat_1 :::"*"::: )  (Set  "the"  ($#u2_msualg_1 :::"ResultSort"::: )  "of" (Set (Var "S"))) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "o")))))))) ; 
 
theorem :: MSUALG_2:20 (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"   ($#m3_pboole :::"MSSubset":::) "of" (Set (Var "U0")) "holds"   (Bool  "("  (Bool (Set   ($#k9_msualg_2 :::"MSSubSort"::: )  (Set (Var "A"))) "is"   ($#v3_msualg_2 :::"opers_closed"::: )  ) & (Bool (Set (Var "A"))  ($#r2_pboole :::"c="::: )  (Set   ($#k9_msualg_2 :::"MSSubSort"::: )  (Set (Var "A"))))  ")" )))) ; 
 begin  definitionlet "S" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )    ($#l1_msualg_1 :::"ManySortedSign"::: )  ; let "U0" be    ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Const "S")); let "A" be   ($#m3_pboole :::"MSSubset":::) "of" (Set (Const "U0")); assume 
(Bool (Set (Const "A")) "is"   ($#v3_msualg_2 :::"opers_closed"::: )  )
 ; func "U0" :::"|"::: "A" ->   ($#v3_msualg_1 :::"strict"::: )     ($#m1_msualg_2 :::"MSSubAlgebra"::: )   "of" "U0" equals :: MSUALG_2:def 15 (Set   ($#g3_msualg_1 :::"MSAlgebra"::: )  "(#"  "A" "," (Set  "("  ($#k4_msualg_2 :::"Opers"::: )   "(" "U0" "," "A" ")"  ")" ) "#)" ); end; 








:: deftheorem    defines :::"|"::: MSUALG_2:def 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 "U0")) "being"    ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Var "S"))  (Bool  "for" (Set (Var "A")) "being"   ($#m3_pboole :::"MSSubset":::) "of" (Set (Var "U0"))  "st" (Bool (Bool (Set (Var "A")) "is"   ($#v3_msualg_2 :::"opers_closed"::: )  )) "holds"  (Bool (Set (Set (Var "U0"))  ($#k10_msualg_2 :::"|"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set   ($#g3_msualg_1 :::"MSAlgebra"::: )  "(#"  (Set (Var "A")) "," (Set  "("  ($#k4_msualg_2 :::"Opers"::: )   "(" (Set (Var "U0")) "," (Set (Var "A")) ")"  ")" ) "#)" ))))); 
 definitionlet "S" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )    ($#l1_msualg_1 :::"ManySortedSign"::: )  ; let "U0" be    ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Const "S")); let "U1", "U2" be    ($#m1_msualg_2 :::"MSSubAlgebra"::: )   "of" (Set (Const "U0")); func "U1" :::"/\"::: "U2" ->   ($#v3_msualg_1 :::"strict"::: )     ($#m1_msualg_2 :::"MSSubAlgebra"::: )   "of" "U0" means :: MSUALG_2:def 16 (Bool  "("  (Bool (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" it)  ($#r8_pboole :::"="::: )  (Set (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" "U1")  ($#k3_pboole :::"/\"::: )  (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" "U2"))) & (Bool  "("   "for" (Set (Var "B")) "being"   ($#m3_pboole :::"MSSubset":::) "of" "U0"  "st" (Bool (Bool (Set (Var "B"))  ($#r8_pboole :::"="::: )  (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" it))) "holds"  (Bool  "("  (Bool (Set (Var "B")) "is"   ($#v3_msualg_2 :::"opers_closed"::: )  ) & (Bool (Set  "the"  ($#u4_msualg_1 :::"Charact"::: )  "of" it)  ($#r8_pboole :::"="::: )  (Set   ($#k4_msualg_2 :::"Opers"::: )   "(" "U0" "," (Set (Var "B")) ")" ))  ")" )  ")" )  ")" ); end; 








:: deftheorem    defines :::"/\"::: MSUALG_2:def 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 "U0")) "being"    ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Var "S"))  (Bool  "for" (Set (Var "U1")) "," (Set (Var "U2")) "being"    ($#m1_msualg_2 :::"MSSubAlgebra"::: )   "of" (Set (Var "U0"))  (Bool  "for" (Set (Var "b5")) "being"   ($#v3_msualg_1 :::"strict"::: )     ($#m1_msualg_2 :::"MSSubAlgebra"::: )   "of" (Set (Var "U0")) "holds"   (Bool  "("  (Bool (Set (Var "b5"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "U1"))  ($#k11_msualg_2 :::"/\"::: )  (Set (Var "U2")))) "iff" (Bool  "("  (Bool (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" (Set (Var "b5")))  ($#r8_pboole :::"="::: )  (Set (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" (Set (Var "U1")))  ($#k3_pboole :::"/\"::: )  (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" (Set (Var "U2"))))) & (Bool  "("   "for" (Set (Var "B")) "being"   ($#m3_pboole :::"MSSubset":::) "of" (Set (Var "U0"))  "st" (Bool (Bool (Set (Var "B"))  ($#r8_pboole :::"="::: )  (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" (Set (Var "b5"))))) "holds"  (Bool  "("  (Bool (Set (Var "B")) "is"   ($#v3_msualg_2 :::"opers_closed"::: )  ) & (Bool (Set  "the"  ($#u4_msualg_1 :::"Charact"::: )  "of" (Set (Var "b5")))  ($#r8_pboole :::"="::: )  (Set   ($#k4_msualg_2 :::"Opers"::: )   "(" (Set (Var "U0")) "," (Set (Var "B")) ")" ))  ")" )  ")" )  ")" )  ")" ))))); 
 definitionlet "S" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )    ($#l1_msualg_1 :::"ManySortedSign"::: )  ; let "U0" be    ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Const "S")); let "A" be   ($#m3_pboole :::"MSSubset":::) "of" (Set (Const "U0")); func  :::"GenMSAlg"::: "A" ->   ($#v3_msualg_1 :::"strict"::: )     ($#m1_msualg_2 :::"MSSubAlgebra"::: )   "of" "U0" means :: MSUALG_2:def 17 (Bool  "("  (Bool "A" "is"   ($#m3_pboole :::"MSSubset":::) "of" it) & (Bool  "("   "for" (Set (Var "U1")) "being"    ($#m1_msualg_2 :::"MSSubAlgebra"::: )   "of" "U0"  "st" (Bool (Bool "A" "is"   ($#m3_pboole :::"MSSubset":::) "of" (Set (Var "U1")))) "holds"  (Bool it "is"    ($#m1_msualg_2 :::"MSSubAlgebra"::: )   "of" (Set (Var "U1")))  ")" )  ")" ); end; 







:: deftheorem    defines :::"GenMSAlg"::: MSUALG_2:def 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 "U0")) "being"    ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Var "S"))  (Bool  "for" (Set (Var "A")) "being"   ($#m3_pboole :::"MSSubset":::) "of" (Set (Var "U0"))  (Bool  "for" (Set (Var "b4")) "being"   ($#v3_msualg_1 :::"strict"::: )     ($#m1_msualg_2 :::"MSSubAlgebra"::: )   "of" (Set (Var "U0")) "holds"   (Bool  "("  (Bool (Set (Var "b4"))  ($#r1_hidden :::"="::: )  (Set   ($#k12_msualg_2 :::"GenMSAlg"::: )  (Set (Var "A")))) "iff" (Bool  "("  (Bool (Set (Var "A")) "is"   ($#m3_pboole :::"MSSubset":::) "of" (Set (Var "b4"))) & (Bool  "("   "for" (Set (Var "U1")) "being"    ($#m1_msualg_2 :::"MSSubAlgebra"::: )   "of" (Set (Var "U0"))  "st" (Bool (Bool (Set (Var "A")) "is"   ($#m3_pboole :::"MSSubset":::) "of" (Set (Var "U1")))) "holds"  (Bool (Set (Var "b4")) "is"    ($#m1_msualg_2 :::"MSSubAlgebra"::: )   "of" (Set (Var "U1")))  ")" )  ")" )  ")" ))))); 
 registrationlet "S" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )    ($#l1_msualg_1 :::"ManySortedSign"::: )  ; let "U0" be   ($#v4_msualg_1 :::"non-empty"::: )     ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Const "S")); let "A" be bbbadV2_RELAT_1()  ($#m3_pboole :::"MSSubset":::) "of" (Set (Const "U0")); 
cluster (Set   ($#k12_msualg_2 :::"GenMSAlg"::: )  "A") ->   ($#v3_msualg_1 :::"strict"::: )     ($#v4_msualg_1 :::"non-empty"::: )   ; 
end; 
theorem :: MSUALG_2: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"    ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Var "S"))  (Bool  "for" (Set (Var "B")) "being"   ($#m3_pboole :::"MSSubset":::) "of" (Set (Var "U0"))  "st" (Bool (Bool (Set (Var "B"))  ($#r8_pboole :::"="::: )  (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" (Set (Var "U0"))))) "holds"  (Bool (Set   ($#k12_msualg_2 :::"GenMSAlg"::: )  (Set (Var "B")))  ($#r1_hidden :::"="::: )  (Set   ($#g3_msualg_1 :::"MSAlgebra"::: )  "(#"  (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" (Set (Var "U0"))) "," (Set  "the"  ($#u4_msualg_1 :::"Charact"::: )  "of" (Set (Var "U0"))) "#)" ))))) ; 
 
theorem :: MSUALG_2: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"    ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Var "S"))  (Bool  "for" (Set (Var "U1")) "being"    ($#m1_msualg_2 :::"MSSubAlgebra"::: )   "of" (Set (Var "U0"))  (Bool  "for" (Set (Var "B")) "being"   ($#m3_pboole :::"MSSubset":::) "of" (Set (Var "U0"))  "st" (Bool (Bool (Set (Var "B"))  ($#r8_pboole :::"="::: )  (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" (Set (Var "U1"))))) "holds"  (Bool (Set   ($#k12_msualg_2 :::"GenMSAlg"::: )  (Set (Var "B")))  ($#r1_hidden :::"="::: )  (Set   ($#g3_msualg_1 :::"MSAlgebra"::: )  "(#"  (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" (Set (Var "U1"))) "," (Set  "the"  ($#u4_msualg_1 :::"Charact"::: )  "of" (Set (Var "U1"))) "#)" )))))) ; 
 
theorem :: MSUALG_2: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 "U1")) "being"    ($#m1_msualg_2 :::"MSSubAlgebra"::: )   "of" (Set (Var "U0")) "holds"  (Bool (Set (Set  "("  ($#k12_msualg_2 :::"GenMSAlg"::: )  (Set  "("  ($#k2_msualg_2 :::"Constants"::: )  (Set (Var "U0")) ")" ) ")" )  ($#k11_msualg_2 :::"/\"::: )  (Set (Var "U1")))  ($#r1_hidden :::"="::: )  (Set   ($#k12_msualg_2 :::"GenMSAlg"::: )  (Set  "("  ($#k2_msualg_2 :::"Constants"::: )  (Set (Var "U0")) ")" )))))) ; 
 definitionlet "S" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )    ($#l1_msualg_1 :::"ManySortedSign"::: )  ; let "U0" be   ($#v4_msualg_1 :::"non-empty"::: )     ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Const "S")); let "U1", "U2" be    ($#m1_msualg_2 :::"MSSubAlgebra"::: )   "of" (Set (Const "U0")); func "U1" :::""\/""::: "U2" ->   ($#v3_msualg_1 :::"strict"::: )     ($#m1_msualg_2 :::"MSSubAlgebra"::: )   "of" "U0" means :: MSUALG_2:def 18 (Bool  "for" (Set (Var "A")) "being"   ($#m3_pboole :::"MSSubset":::) "of" "U0"  "st" (Bool (Bool (Set (Var "A"))  ($#r8_pboole :::"="::: )  (Set (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" "U1")  ($#k2_pboole :::"\/"::: )  (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" "U2")))) "holds"  (Bool it  ($#r1_hidden :::"="::: )  (Set   ($#k12_msualg_2 :::"GenMSAlg"::: )  (Set (Var "A"))))); end; 








:: deftheorem    defines :::""\/""::: MSUALG_2:def 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"   ($#v4_msualg_1 :::"non-empty"::: )     ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Var "S"))  (Bool  "for" (Set (Var "U1")) "," (Set (Var "U2")) "being"    ($#m1_msualg_2 :::"MSSubAlgebra"::: )   "of" (Set (Var "U0"))  (Bool  "for" (Set (Var "b5")) "being"   ($#v3_msualg_1 :::"strict"::: )     ($#m1_msualg_2 :::"MSSubAlgebra"::: )   "of" (Set (Var "U0")) "holds"   (Bool  "("  (Bool (Set (Var "b5"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "U1"))  ($#k13_msualg_2 :::""\/""::: )  (Set (Var "U2")))) "iff" (Bool  "for" (Set (Var "A")) "being"   ($#m3_pboole :::"MSSubset":::) "of" (Set (Var "U0"))  "st" (Bool (Bool (Set (Var "A"))  ($#r8_pboole :::"="::: )  (Set (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" (Set (Var "U1")))  ($#k2_pboole :::"\/"::: )  (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" (Set (Var "U2")))))) "holds"  (Bool (Set (Var "b5"))  ($#r1_hidden :::"="::: )  (Set   ($#k12_msualg_2 :::"GenMSAlg"::: )  (Set (Var "A")))))  ")" ))))); 
 
theorem :: MSUALG_2: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")) "being"   ($#v4_msualg_1 :::"non-empty"::: )     ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Var "S"))  (Bool  "for" (Set (Var "U1")) "being"    ($#m1_msualg_2 :::"MSSubAlgebra"::: )   "of" (Set (Var "U0"))  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m3_pboole :::"MSSubset":::) "of" (Set (Var "U0"))  "st" (Bool (Bool (Set (Var "B"))  ($#r8_pboole :::"="::: )  (Set (Set (Var "A"))  ($#k2_pboole :::"\/"::: )  (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" (Set (Var "U1")))))) "holds"  (Bool (Set (Set  "("  ($#k12_msualg_2 :::"GenMSAlg"::: )  (Set (Var "A")) ")" )  ($#k13_msualg_2 :::""\/""::: )  (Set (Var "U1")))  ($#r1_hidden :::"="::: )  (Set   ($#k12_msualg_2 :::"GenMSAlg"::: )  (Set (Var "B")))))))) ; 
 
theorem :: MSUALG_2: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 "U0")) "being"   ($#v4_msualg_1 :::"non-empty"::: )     ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Var "S"))  (Bool  "for" (Set (Var "U1")) "being"    ($#m1_msualg_2 :::"MSSubAlgebra"::: )   "of" (Set (Var "U0"))  (Bool  "for" (Set (Var "B")) "being"   ($#m3_pboole :::"MSSubset":::) "of" (Set (Var "U0"))  "st" (Bool (Bool (Set (Var "B"))  ($#r8_pboole :::"="::: )  (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" (Set (Var "U0"))))) "holds"  (Bool (Set (Set  "("  ($#k12_msualg_2 :::"GenMSAlg"::: )  (Set (Var "B")) ")" )  ($#k13_msualg_2 :::""\/""::: )  (Set (Var "U1")))  ($#r1_hidden :::"="::: )  (Set   ($#k12_msualg_2 :::"GenMSAlg"::: )  (Set (Var "B")))))))) ; 
 
theorem :: MSUALG_2: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 "U1")) "," (Set (Var "U2")) "being"    ($#m1_msualg_2 :::"MSSubAlgebra"::: )   "of" (Set (Var "U0")) "holds"  (Bool (Set (Set (Var "U1"))  ($#k13_msualg_2 :::""\/""::: )  (Set (Var "U2")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "U2"))  ($#k13_msualg_2 :::""\/""::: )  (Set (Var "U1"))))))) ; 
 
theorem :: MSUALG_2:27 (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 "U1")) "," (Set (Var "U2")) "being"    ($#m1_msualg_2 :::"MSSubAlgebra"::: )   "of" (Set (Var "U0")) "holds"  (Bool (Set (Set (Var "U1"))  ($#k11_msualg_2 :::"/\"::: )  (Set  "(" (Set (Var "U1"))  ($#k13_msualg_2 :::""\/""::: )  (Set (Var "U2")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#g3_msualg_1 :::"MSAlgebra"::: )  "(#"  (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" (Set (Var "U1"))) "," (Set  "the"  ($#u4_msualg_1 :::"Charact"::: )  "of" (Set (Var "U1"))) "#)" ))))) ; 
 
theorem :: MSUALG_2: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"   ($#v4_msualg_1 :::"non-empty"::: )     ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Var "S"))  (Bool  "for" (Set (Var "U1")) "," (Set (Var "U2")) "being"    ($#m1_msualg_2 :::"MSSubAlgebra"::: )   "of" (Set (Var "U0")) "holds"  (Bool (Set (Set  "(" (Set (Var "U1"))  ($#k11_msualg_2 :::"/\"::: )  (Set (Var "U2")) ")" )  ($#k13_msualg_2 :::""\/""::: )  (Set (Var "U2")))  ($#r1_hidden :::"="::: )  (Set   ($#g3_msualg_1 :::"MSAlgebra"::: )  "(#"  (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" (Set (Var "U2"))) "," (Set  "the"  ($#u4_msualg_1 :::"Charact"::: )  "of" (Set (Var "U2"))) "#)" ))))) ; 
 begin  definitionlet "S" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )    ($#l1_msualg_1 :::"ManySortedSign"::: )  ; let "U0" be    ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Const "S")); func  :::"MSSub"::: "U0" ->    ($#m1_hidden :::"set"::: )   means :: MSUALG_2:def 19 (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  it) "iff" (Bool (Set (Var "x")) "is"   ($#v3_msualg_1 :::"strict"::: )     ($#m1_msualg_2 :::"MSSubAlgebra"::: )   "of" "U0")  ")" )); end; 






:: deftheorem    defines :::"MSSub"::: MSUALG_2:def 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 "b3")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k14_msualg_2 :::"MSSub"::: )  (Set (Var "U0")))) "iff" (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "b3"))) "iff" (Bool (Set (Var "x")) "is"   ($#v3_msualg_1 :::"strict"::: )     ($#m1_msualg_2 :::"MSSubAlgebra"::: )   "of" (Set (Var "U0")))  ")" ))  ")" )))); 
 registrationlet "S" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )    ($#l1_msualg_1 :::"ManySortedSign"::: )  ; let "U0" be    ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Const "S")); 
cluster (Set   ($#k14_msualg_2 :::"MSSub"::: )  "U0") ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )  ; 
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 "U0" be   ($#v4_msualg_1 :::"non-empty"::: )     ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Const "S")); func  :::"MSAlg_join"::: "U0" ->   ($#m1_subset_1 :::"BinOp":::) "of" (Set  "("  ($#k14_msualg_2 :::"MSSub"::: )  "U0" ")" ) means :: MSUALG_2:def 20 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k14_msualg_2 :::"MSSub"::: )  "U0")  (Bool  "for" (Set (Var "U1")) "," (Set (Var "U2")) "being"   ($#v3_msualg_1 :::"strict"::: )     ($#m1_msualg_2 :::"MSSubAlgebra"::: )   "of" "U0"  "st" (Bool (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Var "U1"))) & (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set (Var "U2")))) "holds"  (Bool (Set it  ($#k5_binop_1 :::"."::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "U1"))  ($#k13_msualg_2 :::""\/""::: )  (Set (Var "U2")))))); end; 






:: deftheorem    defines :::"MSAlg_join"::: MSUALG_2:def 20 :  (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 "b3")) "being"   ($#m1_subset_1 :::"BinOp":::) "of" (Set  "("  ($#k14_msualg_2 :::"MSSub"::: )  (Set (Var "U0")) ")" ) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k15_msualg_2 :::"MSAlg_join"::: )  (Set (Var "U0")))) "iff" (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k14_msualg_2 :::"MSSub"::: )  (Set (Var "U0")))  (Bool  "for" (Set (Var "U1")) "," (Set (Var "U2")) "being"   ($#v3_msualg_1 :::"strict"::: )     ($#m1_msualg_2 :::"MSSubAlgebra"::: )   "of" (Set (Var "U0"))  "st" (Bool (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Var "U1"))) & (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set (Var "U2")))) "holds"  (Bool (Set (Set (Var "b3"))  ($#k5_binop_1 :::"."::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "U1"))  ($#k13_msualg_2 :::""\/""::: )  (Set (Var "U2"))))))  ")" )))); 
 definitionlet "S" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )    ($#l1_msualg_1 :::"ManySortedSign"::: )  ; let "U0" be   ($#v4_msualg_1 :::"non-empty"::: )     ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Const "S")); func  :::"MSAlg_meet"::: "U0" ->   ($#m1_subset_1 :::"BinOp":::) "of" (Set  "("  ($#k14_msualg_2 :::"MSSub"::: )  "U0" ")" ) means :: MSUALG_2:def 21 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k14_msualg_2 :::"MSSub"::: )  "U0")  (Bool  "for" (Set (Var "U1")) "," (Set (Var "U2")) "being"   ($#v3_msualg_1 :::"strict"::: )     ($#m1_msualg_2 :::"MSSubAlgebra"::: )   "of" "U0"  "st" (Bool (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Var "U1"))) & (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set (Var "U2")))) "holds"  (Bool (Set it  ($#k5_binop_1 :::"."::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "U1"))  ($#k11_msualg_2 :::"/\"::: )  (Set (Var "U2")))))); end; 






:: deftheorem    defines :::"MSAlg_meet"::: MSUALG_2:def 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 "b3")) "being"   ($#m1_subset_1 :::"BinOp":::) "of" (Set  "("  ($#k14_msualg_2 :::"MSSub"::: )  (Set (Var "U0")) ")" ) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k16_msualg_2 :::"MSAlg_meet"::: )  (Set (Var "U0")))) "iff" (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k14_msualg_2 :::"MSSub"::: )  (Set (Var "U0")))  (Bool  "for" (Set (Var "U1")) "," (Set (Var "U2")) "being"   ($#v3_msualg_1 :::"strict"::: )     ($#m1_msualg_2 :::"MSSubAlgebra"::: )   "of" (Set (Var "U0"))  "st" (Bool (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Var "U1"))) & (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set (Var "U2")))) "holds"  (Bool (Set (Set (Var "b3"))  ($#k5_binop_1 :::"."::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "U1"))  ($#k11_msualg_2 :::"/\"::: )  (Set (Var "U2"))))))  ")" )))); 
 



theorem :: MSUALG_2: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 "U0")) "being"   ($#v4_msualg_1 :::"non-empty"::: )     ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Var "S")) "holds"  (Bool (Set   ($#k15_msualg_2 :::"MSAlg_join"::: )  (Set (Var "U0"))) "is"   ($#v1_binop_1 :::"commutative"::: )  ))) ; 
 
theorem :: MSUALG_2: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 "U0")) "being"   ($#v4_msualg_1 :::"non-empty"::: )     ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Var "S")) "holds"  (Bool (Set   ($#k15_msualg_2 :::"MSAlg_join"::: )  (Set (Var "U0"))) "is"   ($#v2_binop_1 :::"associative"::: )  ))) ; 
 
theorem :: MSUALG_2: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")) "holds"  (Bool (Set   ($#k16_msualg_2 :::"MSAlg_meet"::: )  (Set (Var "U0"))) "is"   ($#v1_binop_1 :::"commutative"::: )  ))) ; 
 
theorem :: MSUALG_2: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")) "holds"  (Bool (Set   ($#k16_msualg_2 :::"MSAlg_meet"::: )  (Set (Var "U0"))) "is"   ($#v2_binop_1 :::"associative"::: )  ))) ; 
 definitionlet "S" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )    ($#l1_msualg_1 :::"ManySortedSign"::: )  ; let "U0" be   ($#v4_msualg_1 :::"non-empty"::: )     ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Const "S")); func  :::"MSSubAlLattice"::: "U0" ->   ($#v3_lattices :::"strict"::: )    ($#l3_lattices :::"Lattice":::) equals :: MSUALG_2:def 22 (Set   ($#g3_lattices :::"LattStr"::: )  "(#"  (Set  "("  ($#k14_msualg_2 :::"MSSub"::: )  "U0" ")" ) "," (Set  "("  ($#k15_msualg_2 :::"MSAlg_join"::: )  "U0" ")" ) "," (Set  "("  ($#k16_msualg_2 :::"MSAlg_meet"::: )  "U0" ")" ) "#)" ); end; 






:: deftheorem    defines :::"MSSubAlLattice"::: MSUALG_2:def 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")) "holds"  (Bool (Set   ($#k17_msualg_2 :::"MSSubAlLattice"::: )  (Set (Var "U0")))  ($#r1_hidden :::"="::: )  (Set   ($#g3_lattices :::"LattStr"::: )  "(#"  (Set  "("  ($#k14_msualg_2 :::"MSSub"::: )  (Set (Var "U0")) ")" ) "," (Set  "("  ($#k15_msualg_2 :::"MSAlg_join"::: )  (Set (Var "U0")) ")" ) "," (Set  "("  ($#k16_msualg_2 :::"MSAlg_meet"::: )  (Set (Var "U0")) ")" ) "#)" )))); 
 
theorem :: MSUALG_2: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")) "being"   ($#v4_msualg_1 :::"non-empty"::: )     ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Var "S")) "holds"  (Bool (Set   ($#k17_msualg_2 :::"MSSubAlLattice"::: )  (Set (Var "U0"))) "is"   ($#v15_lattices :::"bounded"::: )  ))) ; 
 registrationlet "S" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )    ($#l1_msualg_1 :::"ManySortedSign"::: )  ; let "U0" be   ($#v4_msualg_1 :::"non-empty"::: )     ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Const "S")); 
cluster (Set   ($#k17_msualg_2 :::"MSSubAlLattice"::: )  "U0") ->   ($#v3_lattices :::"strict"::: )     ($#v15_lattices :::"bounded"::: )   ; 
end; 
theorem :: MSUALG_2: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")) "being"   ($#v4_msualg_1 :::"non-empty"::: )     ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Var "S")) "holds"  (Bool (Set   ($#k5_lattices :::"Bottom"::: )  (Set  "("  ($#k17_msualg_2 :::"MSSubAlLattice"::: )  (Set (Var "U0")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k12_msualg_2 :::"GenMSAlg"::: )  (Set  "("  ($#k2_msualg_2 :::"Constants"::: )  (Set (Var "U0")) ")" ))))) ; 
 
theorem :: MSUALG_2: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 "B")) "being"   ($#m3_pboole :::"MSSubset":::) "of" (Set (Var "U0"))  "st" (Bool (Bool (Set (Var "B"))  ($#r8_pboole :::"="::: )  (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" (Set (Var "U0"))))) "holds"  (Bool (Set   ($#k6_lattices :::"Top"::: )  (Set  "("  ($#k17_msualg_2 :::"MSSubAlLattice"::: )  (Set (Var "U0")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k12_msualg_2 :::"GenMSAlg"::: )  (Set (Var "B"))))))) ; 
 
theorem :: MSUALG_2: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")) "holds"  (Bool (Set   ($#k6_lattices :::"Top"::: )  (Set  "("  ($#k17_msualg_2 :::"MSSubAlLattice"::: )  (Set (Var "U0")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#g3_msualg_1 :::"MSAlgebra"::: )  "(#"  (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" (Set (Var "U0"))) "," (Set  "the"  ($#u4_msualg_1 :::"Charact"::: )  "of" (Set (Var "U0"))) "#)" )))) ; 
 
theorem :: MSUALG_2:37 (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")) "holds"  (Bool (Set   ($#g3_msualg_1 :::"MSAlgebra"::: )  "(#"  (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" (Set (Var "U0"))) "," (Set  "the"  ($#u4_msualg_1 :::"Charact"::: )  "of" (Set (Var "U0"))) "#)" ) "is"    ($#m1_msualg_2 :::"MSSubAlgebra"::: )   "of" (Set (Var "U0"))))) ; 
 
theorem :: MSUALG_2:38 (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"   ($#m3_pboole :::"MSSubset":::) "of" (Set (Var "U0")) "holds"  (Bool (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" (Set (Var "U0")))  ($#r2_hidden :::"in"::: )  (Set   ($#k5_msualg_2 :::"SubSort"::: )  (Set (Var "A"))))))) ; 
 
theorem :: MSUALG_2:39 (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"   ($#m3_pboole :::"MSSubset":::) "of" (Set (Var "U0")) "holds"  (Bool (Set   ($#k5_msualg_2 :::"SubSort"::: )  (Set (Var "A")))  ($#r1_tarski :::"c="::: )  (Set   ($#k6_msualg_2 :::"SubSort"::: )  (Set (Var "U0"))))))) ;