:: MSUALG_1  semantic presentation begin  


begin  definitionattr "c1" is  :::"strict"::: ; struct  :::"ManySortedSign":::  ->    ($#l5_struct_0 :::"2-sorted"::: )  ; aggr :::"ManySortedSign":::(# :::"carrier":::, :::"carrier'":::, :::"Arity":::, :::"ResultSort"::: #) ->    ($#l1_msualg_1 :::"ManySortedSign"::: )  ; sel  :::"Arity"::: "c1" ->   ($#m1_subset_1 :::"Function":::) "of" (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" "c1") "," (Set  "(" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "c1")  ($#k3_finseq_2 :::"*"::: )  ")" ); sel  :::"ResultSort"::: "c1" ->   ($#m1_subset_1 :::"Function":::) "of" (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" "c1") "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "c1"); end; registration
cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v11_struct_0 :::"void"::: )     ($#v1_msualg_1 :::"strict"::: )    for    ($#l1_msualg_1 :::"ManySortedSign"::: )  ; 

cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )    ($#v1_msualg_1 :::"strict"::: )    for    ($#l1_msualg_1 :::"ManySortedSign"::: )  ; 
end; 


definitionlet "S" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_msualg_1 :::"ManySortedSign"::: )  ; mode SortSymbol of "S" is   ($#m1_subset_1 :::"Element":::) "of" "S"; mode OperSymbol of "S" is    ($#m1_subset_1 :::"Element"::: )   "of" (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" "S"); end; definitionlet "S" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )    ($#l1_msualg_1 :::"ManySortedSign"::: )  ; let "o" be   ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Const "S")); func  :::"the_arity_of"::: "o" ->    ($#m2_finseq_2 :::"Element"::: )   "of" (Set (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "S")  ($#k3_finseq_2 :::"*"::: )  ) equals :: MSUALG_1:def 1 (Set (Set  "the"  ($#u1_msualg_1 :::"Arity"::: )  "of" "S")  ($#k3_funct_2 :::"."::: )  "o"); func  :::"the_result_sort_of"::: "o" ->   ($#m1_subset_1 :::"Element":::) "of" "S" equals :: MSUALG_1:def 2 (Set (Set  "the"  ($#u2_msualg_1 :::"ResultSort"::: )  "of" "S")  ($#k3_funct_2 :::"."::: )  "o"); end; 












:: deftheorem    defines :::"the_arity_of"::: MSUALG_1:def 1 :  (Bool  "for" (Set (Var "S")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )    ($#l1_msualg_1 :::"ManySortedSign"::: )    (Bool  "for" (Set (Var "o")) "being"   ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S")) "holds"  (Bool (Set   ($#k1_msualg_1 :::"the_arity_of"::: )  (Set (Var "o")))  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u1_msualg_1 :::"Arity"::: )  "of" (Set (Var "S")))  ($#k3_funct_2 :::"."::: )  (Set (Var "o")))))); 
 
:: deftheorem    defines :::"the_result_sort_of"::: MSUALG_1:def 2 :  (Bool  "for" (Set (Var "S")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )    ($#l1_msualg_1 :::"ManySortedSign"::: )    (Bool  "for" (Set (Var "o")) "being"   ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S")) "holds"  (Bool (Set   ($#k2_msualg_1 :::"the_result_sort_of"::: )  (Set (Var "o")))  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u2_msualg_1 :::"ResultSort"::: )  "of" (Set (Var "S")))  ($#k3_funct_2 :::"."::: )  (Set (Var "o")))))); 
 begin  definitionlet "S" be    ($#l1_struct_0 :::"1-sorted"::: )  ; attr "c2" is  :::"strict"::: ; struct  :::"many-sorted":::  "over" "S" -> ; aggr :::"many-sorted":::(# :::"Sorts"::: #) ->    ($#l2_msualg_1 :::"many-sorted"::: )   "over" "S"; sel  :::"Sorts"::: "c2" ->   ($#m1_hidden :::"ManySortedSet":::) "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "S"); end; definitionlet "S" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_msualg_1 :::"ManySortedSign"::: )  ; attr "c2" is  :::"strict"::: ; struct  :::"MSAlgebra":::  "over" "S" ->    ($#l2_msualg_1 :::"many-sorted"::: )   "over" "S"; aggr :::"MSAlgebra":::(# :::"Sorts":::, :::"Charact"::: #) ->    ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" "S"; sel  :::"Charact"::: "c2" ->    ($#m2_pboole :::"ManySortedFunction"::: )   "of" (Set (Set  "(" (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" "c2")  ($#k6_finseq_2 :::"#"::: )  ")" )  ($#k3_relat_1 :::"*"::: )  (Set  "the"  ($#u1_msualg_1 :::"Arity"::: )  "of" "S")) "," (Set (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" "c2")  ($#k3_relat_1 :::"*"::: )  (Set  "the"  ($#u2_msualg_1 :::"ResultSort"::: )  "of" "S")); end; definitionlet "S" be    ($#l1_struct_0 :::"1-sorted"::: )  ; let "A" be    ($#l2_msualg_1 :::"many-sorted"::: )   "over" (Set (Const "S")); attr "A" is  :::"non-empty":::  means :: MSUALG_1:def 3 (Bool (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" "A") "is" bbbadV2_RELAT_1()); end; 





:: deftheorem    defines :::"non-empty"::: MSUALG_1:def 3 :  (Bool  "for" (Set (Var "S")) "being"    ($#l1_struct_0 :::"1-sorted"::: )    (Bool  "for" (Set (Var "A")) "being"    ($#l2_msualg_1 :::"many-sorted"::: )   "over" (Set (Var "S")) "holds"   (Bool  "("  (Bool (Set (Var "A")) "is"   ($#v4_msualg_1 :::"non-empty"::: )  ) "iff" (Bool (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" (Set (Var "A"))) "is" bbbadV2_RELAT_1())  ")" ))); 
 registrationlet "S" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_msualg_1 :::"ManySortedSign"::: )  ; 
cluster   ($#v3_msualg_1 :::"strict"::: )     ($#v4_msualg_1 :::"non-empty"::: )    for    ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" "S"; 
end; registrationlet "S" be    ($#l1_struct_0 :::"1-sorted"::: )  ; 
cluster   ($#v2_msualg_1 :::"strict"::: )     ($#v4_msualg_1 :::"non-empty"::: )    for    ($#l2_msualg_1 :::"many-sorted"::: )   "over" "S"; 
end; registrationlet "S" be    ($#l1_struct_0 :::"1-sorted"::: )  ; let "A" be   ($#v4_msualg_1 :::"non-empty"::: )     ($#l2_msualg_1 :::"many-sorted"::: )   "over" (Set (Const "S")); 
cluster (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" "A") -> bbbadV2_RELAT_1() ; 
end; registrationlet "S" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_msualg_1 :::"ManySortedSign"::: )  ; let "A" be   ($#v4_msualg_1 :::"non-empty"::: )     ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Const "S")); 
cluster   ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" "A")); 

cluster   ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set  "(" (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" "A")  ($#k6_finseq_2 :::"#"::: )  ")" )); 
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 "o" be   ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Const "S")); let "A" be    ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Const "S")); func  :::"Args":::  "(" "o" "," "A" ")"  ->   ($#m1_subset_1 :::"Component":::) "of" (Set  "(" (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" "A")  ($#k6_finseq_2 :::"#"::: )  ")" ) equals :: MSUALG_1:def 4 (Set (Set  "(" (Set  "(" (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" "A")  ($#k6_finseq_2 :::"#"::: )  ")" )  ($#k3_relat_1 :::"*"::: )  (Set  "the"  ($#u1_msualg_1 :::"Arity"::: )  "of" "S") ")" )  ($#k1_funct_1 :::"."::: )  "o"); func  :::"Result":::  "(" "o" "," "A" ")"  ->   ($#m1_subset_1 :::"Component":::) "of" (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" "A") equals :: MSUALG_1:def 5 (Set (Set  "(" (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" "A")  ($#k3_relat_1 :::"*"::: )  (Set  "the"  ($#u2_msualg_1 :::"ResultSort"::: )  "of" "S") ")" )  ($#k1_funct_1 :::"."::: )  "o"); end; 














:: deftheorem    defines :::"Args"::: MSUALG_1: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 "o")) "being"   ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S"))  (Bool  "for" (Set (Var "A")) "being"    ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Var "S")) "holds"  (Bool (Set   ($#k3_msualg_1 :::"Args"::: )   "(" (Set (Var "o")) "," (Set (Var "A")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" (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"))))))); 
 
:: deftheorem    defines :::"Result"::: MSUALG_1: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 "o")) "being"   ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S"))  (Bool  "for" (Set (Var "A")) "being"    ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Var "S")) "holds"  (Bool (Set   ($#k4_msualg_1 :::"Result"::: )   "(" (Set (Var "o")) "," (Set (Var "A")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" (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 "o" be   ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Const "S")); let "A" be    ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Const "S")); func  :::"Den":::  "(" "o" "," "A" ")"  ->   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k3_msualg_1 :::"Args"::: )   "(" "o" "," "A" ")"  ")" ) "," (Set  "("  ($#k4_msualg_1 :::"Result"::: )   "(" "o" "," "A" ")"  ")" ) equals :: MSUALG_1:def 6 (Set (Set  "the"  ($#u4_msualg_1 :::"Charact"::: )  "of" "A")  ($#k1_funct_1 :::"."::: )  "o"); end; 







:: deftheorem    defines :::"Den"::: MSUALG_1: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 "o")) "being"   ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S"))  (Bool  "for" (Set (Var "A")) "being"    ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Var "S")) "holds"  (Bool (Set   ($#k5_msualg_1 :::"Den"::: )   "(" (Set (Var "o")) "," (Set (Var "A")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u4_msualg_1 :::"Charact"::: )  "of" (Set (Var "A")))  ($#k1_funct_1 :::"."::: )  (Set (Var "o"))))))); 
 
theorem :: MSUALG_1:1 (Bool  "for" (Set (Var "S")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )    ($#l1_msualg_1 :::"ManySortedSign"::: )    (Bool  "for" (Set (Var "o")) "being"   ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S"))  (Bool  "for" (Set (Var "A")) "being"   ($#v4_msualg_1 :::"non-empty"::: )     ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Var "S"))  "holds" (Bool (Bool  "not" (Set   ($#k5_msualg_1 :::"Den"::: )   "(" (Set (Var "o")) "," (Set (Var "A")) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))))) ; 
 begin  






theorem :: MSUALG_1:2 (Bool  "for" (Set (Var "C")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "F")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set (Var "A"))  (Bool  "for" (Set (Var "G")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set (Var "B")) "holds"  (Bool (Set (Set (Var "G"))  ($#k1_partfun1 :::"*"::: )  (Set (Var "F"))) "is"   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "F")) ")" ) "," (Set (Var "B"))))))) ; 
 
theorem :: MSUALG_1:3 (Bool  "for" (Set (Var "D")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "h")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_margrel1 :::"homogeneous"::: )     ($#v3_margrel1 :::"quasi_total"::: )    ($#m1_subset_1 :::"PartFunc":::) "of" (Set  "(" (Set (Var "D"))  ($#k3_finseq_2 :::"*"::: )  ")" ) "," (Set (Var "D")) "holds"  (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "h")))  ($#r1_hidden :::"="::: )  (Set   ($#k9_funct_2 :::"Funcs"::: )   "(" (Set  "("  ($#k2_finseq_1 :::"Seg"::: )  (Set  "("  ($#k19_margrel1 :::"arity"::: )  (Set (Var "h")) ")" ) ")" ) "," (Set (Var "D")) ")" )))) ; 
 
theorem :: MSUALG_1:4 (Bool  "for" (Set (Var "A")) "being"   ($#l1_unialg_1 :::"Universal_Algebra":::)  "holds" (Bool (Bool  "not" (Set   ($#k1_unialg_1 :::"signature"::: )  (Set (Var "A"))) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) ; 
 begin  definitionlet "IT" be    ($#l1_msualg_1 :::"ManySortedSign"::: )  ; attr "IT" is  :::"segmental":::  means :: MSUALG_1:def 7 (Bool  "ex" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "st" (Bool (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" "IT")  ($#r1_hidden :::"="::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set (Var "n"))))); end; 




:: deftheorem    defines :::"segmental"::: MSUALG_1:def 7 :  (Bool  "for" (Set (Var "IT")) "being"    ($#l1_msualg_1 :::"ManySortedSign"::: )   "holds"   (Bool  "("  (Bool (Set (Var "IT")) "is"   ($#v5_msualg_1 :::"segmental"::: )  ) "iff" (Bool  "ex" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "st" (Bool (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set (Var "IT")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set (Var "n")))))  ")" )); 
 
theorem :: MSUALG_1:5 (Bool  "for" (Set (Var "S")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_msualg_1 :::"ManySortedSign"::: )    "st" (Bool (Bool (Set (Var "S")) "is"   ($#v7_struct_0 :::"trivial"::: )  )) "holds"  (Bool  "for" (Set (Var "A")) "being"    ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Var "S"))  (Bool  "for" (Set (Var "c1")) "," (Set (Var "c2")) "being"   ($#m1_subset_1 :::"Component":::) "of" (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" (Set (Var "A"))) "holds"  (Bool (Set (Var "c1"))  ($#r1_hidden :::"="::: )  (Set (Var "c2")))))) ; 
 registration
cluster  ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )  (Num 1)  ($#v13_struct_0 :::"-element"::: )     ($#v1_msualg_1 :::"strict"::: )     ($#v5_msualg_1 :::"segmental"::: )    for    ($#l1_msualg_1 :::"ManySortedSign"::: )  ; 
end; definitionlet "A" be   ($#l1_unialg_1 :::"Universal_Algebra":::); func  :::"MSSign"::: "A" ->   ($#v7_struct_0 :::"trivial"::: )    ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )    ($#v1_msualg_1 :::"strict"::: )     ($#v5_msualg_1 :::"segmental"::: )     ($#l1_msualg_1 :::"ManySortedSign"::: )   means :: MSUALG_1:def 8 (Bool  "("  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" it)  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set  ($#k6_numbers :::"0"::: ) ) ($#k1_tarski :::"}"::: ) )) & (Bool (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" it)  ($#r1_hidden :::"="::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set  "("  ($#k1_unialg_1 :::"signature"::: )  "A" ")" ))) & (Bool (Set  "the"  ($#u1_msualg_1 :::"Arity"::: )  "of" it)  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k7_finseq_2 :::"*-->"::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" )  ($#k1_partfun1 :::"*"::: )  (Set  "("  ($#k1_unialg_1 :::"signature"::: )  "A" ")" ))) & (Bool (Set  "the"  ($#u2_msualg_1 :::"ResultSort"::: )  "of" it)  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k4_finseq_1 :::"dom"::: )  (Set  "("  ($#k1_unialg_1 :::"signature"::: )  "A" ")" ) ")" )  ($#k1_margrel1 :::"-->"::: )  (Set  ($#k6_numbers :::"0"::: ) )))  ")" ); end; 





:: deftheorem    defines :::"MSSign"::: MSUALG_1:def 8 :  (Bool  "for" (Set (Var "A")) "being"   ($#l1_unialg_1 :::"Universal_Algebra":::)  (Bool  "for" (Set (Var "b2")) "being"   ($#v7_struct_0 :::"trivial"::: )    ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )    ($#v1_msualg_1 :::"strict"::: )     ($#v5_msualg_1 :::"segmental"::: )     ($#l1_msualg_1 :::"ManySortedSign"::: )   "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_msualg_1 :::"MSSign"::: )  (Set (Var "A")))) "iff" (Bool  "("  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "b2")))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set  ($#k6_numbers :::"0"::: ) ) ($#k1_tarski :::"}"::: ) )) & (Bool (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set (Var "b2")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set  "("  ($#k1_unialg_1 :::"signature"::: )  (Set (Var "A")) ")" ))) & (Bool (Set  "the"  ($#u1_msualg_1 :::"Arity"::: )  "of" (Set (Var "b2")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k7_finseq_2 :::"*-->"::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" )  ($#k1_partfun1 :::"*"::: )  (Set  "("  ($#k1_unialg_1 :::"signature"::: )  (Set (Var "A")) ")" ))) & (Bool (Set  "the"  ($#u2_msualg_1 :::"ResultSort"::: )  "of" (Set (Var "b2")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k4_finseq_1 :::"dom"::: )  (Set  "("  ($#k1_unialg_1 :::"signature"::: )  (Set (Var "A")) ")" ) ")" )  ($#k1_margrel1 :::"-->"::: )  (Set  ($#k6_numbers :::"0"::: ) )))  ")" )  ")" ))); 
 registrationlet "A" be   ($#l1_unialg_1 :::"Universal_Algebra":::); 
cluster (Set   ($#k6_msualg_1 :::"MSSign"::: )  "A") ->   ($#v7_struct_0 :::"trivial"::: )    ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )  (Num 1)  ($#v13_struct_0 :::"-element"::: )     ($#v1_msualg_1 :::"strict"::: )     ($#v5_msualg_1 :::"segmental"::: )   ; 
end; definitionlet "A" be   ($#l1_unialg_1 :::"Universal_Algebra":::); func  :::"MSSorts"::: "A" -> bbbadV2_RELAT_1()  ($#m1_hidden :::"ManySortedSet":::) "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "("  ($#k6_msualg_1 :::"MSSign"::: )  "A" ")" )) equals :: MSUALG_1:def 9 (Set (Set  ($#k6_numbers :::"0"::: ) )  ($#k16_funcop_1 :::".-->"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "A")); end; 





:: deftheorem    defines :::"MSSorts"::: MSUALG_1:def 9 :  (Bool  "for" (Set (Var "A")) "being"   ($#l1_unialg_1 :::"Universal_Algebra":::) "holds"  (Bool (Set   ($#k7_msualg_1 :::"MSSorts"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set (Set  ($#k6_numbers :::"0"::: ) )  ($#k16_funcop_1 :::".-->"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "A")))))); 
 definitionlet "A" be   ($#l1_unialg_1 :::"Universal_Algebra":::); func  :::"MSCharact"::: "A" ->    ($#m2_pboole :::"ManySortedFunction"::: )   "of" (Set (Set  "(" (Set  "("  ($#k7_msualg_1 :::"MSSorts"::: )  "A" ")" )  ($#k6_finseq_2 :::"#"::: )  ")" )  ($#k3_relat_1 :::"*"::: )  (Set  "the"  ($#u1_msualg_1 :::"Arity"::: )  "of" (Set  "("  ($#k6_msualg_1 :::"MSSign"::: )  "A" ")" ))) "," (Set (Set  "("  ($#k7_msualg_1 :::"MSSorts"::: )  "A" ")" )  ($#k3_relat_1 :::"*"::: )  (Set  "the"  ($#u2_msualg_1 :::"ResultSort"::: )  "of" (Set  "("  ($#k6_msualg_1 :::"MSSign"::: )  "A" ")" ))) equals :: MSUALG_1:def 10 (Set  "the"  ($#u1_unialg_1 :::"charact"::: )  "of" "A"); end; 





:: deftheorem    defines :::"MSCharact"::: MSUALG_1:def 10 :  (Bool  "for" (Set (Var "A")) "being"   ($#l1_unialg_1 :::"Universal_Algebra":::) "holds"  (Bool (Set   ($#k8_msualg_1 :::"MSCharact"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set  "the"  ($#u1_unialg_1 :::"charact"::: )  "of" (Set (Var "A"))))); 
 definitionlet "A" be   ($#l1_unialg_1 :::"Universal_Algebra":::); func  :::"MSAlg"::: "A" ->   ($#v3_msualg_1 :::"strict"::: )     ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set   ($#k6_msualg_1 :::"MSSign"::: )  "A") equals :: MSUALG_1:def 11 (Set   ($#g3_msualg_1 :::"MSAlgebra"::: )  "(#"  (Set  "("  ($#k7_msualg_1 :::"MSSorts"::: )  "A" ")" ) "," (Set  "("  ($#k8_msualg_1 :::"MSCharact"::: )  "A" ")" ) "#)" ); end; 





:: deftheorem    defines :::"MSAlg"::: MSUALG_1:def 11 :  (Bool  "for" (Set (Var "A")) "being"   ($#l1_unialg_1 :::"Universal_Algebra":::) "holds"  (Bool (Set   ($#k9_msualg_1 :::"MSAlg"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set   ($#g3_msualg_1 :::"MSAlgebra"::: )  "(#"  (Set  "("  ($#k7_msualg_1 :::"MSSorts"::: )  (Set (Var "A")) ")" ) "," (Set  "("  ($#k8_msualg_1 :::"MSCharact"::: )  (Set (Var "A")) ")" ) "#)" ))); 
 registrationlet "A" be   ($#l1_unialg_1 :::"Universal_Algebra":::); 
cluster (Set   ($#k9_msualg_1 :::"MSAlg"::: )  "A") ->   ($#v3_msualg_1 :::"strict"::: )     ($#v4_msualg_1 :::"non-empty"::: )   ; 
end; definitionlet "MS" be (Num 1)  ($#v13_struct_0 :::"-element"::: )     ($#l1_msualg_1 :::"ManySortedSign"::: )  ; let "A" be    ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Const "MS")); func  :::"the_sort_of"::: "A" ->    ($#m1_hidden :::"set"::: )   means :: MSUALG_1:def 12 (Bool it "is"   ($#m1_subset_1 :::"Component":::) "of" (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" "A")); end; 






:: deftheorem    defines :::"the_sort_of"::: MSUALG_1:def 12 :  (Bool  "for" (Set (Var "MS")) "being" (Num 1)  ($#v13_struct_0 :::"-element"::: )     ($#l1_msualg_1 :::"ManySortedSign"::: )    (Bool  "for" (Set (Var "A")) "being"    ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Var "MS"))  (Bool  "for" (Set (Var "b3")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k10_msualg_1 :::"the_sort_of"::: )  (Set (Var "A")))) "iff" (Bool (Set (Var "b3")) "is"   ($#m1_subset_1 :::"Component":::) "of" (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" (Set (Var "A"))))  ")" )))); 
 registrationlet "MS" be (Num 1)  ($#v13_struct_0 :::"-element"::: )     ($#l1_msualg_1 :::"ManySortedSign"::: )  ; let "A" be   ($#v4_msualg_1 :::"non-empty"::: )     ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Const "MS")); 
cluster (Set   ($#k10_msualg_1 :::"the_sort_of"::: )  "A") ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )  ; 
end; 
theorem :: MSUALG_1:6 (Bool  "for" (Set (Var "MS")) "being"  ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )  (Num 1)  ($#v13_struct_0 :::"-element"::: )     ($#v5_msualg_1 :::"segmental"::: )     ($#l1_msualg_1 :::"ManySortedSign"::: )    (Bool  "for" (Set (Var "i")) "being"   ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "MS"))  (Bool  "for" (Set (Var "A")) "being"   ($#v4_msualg_1 :::"non-empty"::: )     ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Var "MS")) "holds"  (Bool (Set   ($#k3_msualg_1 :::"Args"::: )   "(" (Set (Var "i")) "," (Set (Var "A")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set  "("  ($#k1_msualg_1 :::"the_arity_of"::: )  (Set (Var "i")) ")" ) ")" )  ($#k4_finseq_2 :::"-tuples_on"::: )  (Set  "("  ($#k10_msualg_1 :::"the_sort_of"::: )  (Set (Var "A")) ")" )))))) ; 
 
theorem :: MSUALG_1:7 (Bool  "for" (Set (Var "MS")) "being"  ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )  (Num 1)  ($#v13_struct_0 :::"-element"::: )     ($#v5_msualg_1 :::"segmental"::: )     ($#l1_msualg_1 :::"ManySortedSign"::: )    (Bool  "for" (Set (Var "i")) "being"   ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "MS"))  (Bool  "for" (Set (Var "A")) "being"   ($#v4_msualg_1 :::"non-empty"::: )     ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Var "MS")) "holds"  (Bool (Set   ($#k3_msualg_1 :::"Args"::: )   "(" (Set (Var "i")) "," (Set (Var "A")) ")" )  ($#r1_tarski :::"c="::: )  (Set (Set  "("  ($#k10_msualg_1 :::"the_sort_of"::: )  (Set (Var "A")) ")" )  ($#k3_finseq_2 :::"*"::: )  ))))) ; 
 
theorem :: MSUALG_1:8 (Bool  "for" (Set (Var "MS")) "being"  ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )  (Num 1)  ($#v13_struct_0 :::"-element"::: )     ($#v5_msualg_1 :::"segmental"::: )     ($#l1_msualg_1 :::"ManySortedSign"::: )    (Bool  "for" (Set (Var "A")) "being"   ($#v4_msualg_1 :::"non-empty"::: )     ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Var "MS")) "holds"  (Bool (Set  "the"  ($#u4_msualg_1 :::"Charact"::: )  "of" (Set (Var "A"))) "is"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k4_partfun1 :::"PFuncs"::: )   "(" (Set  "(" (Set  "("  ($#k10_msualg_1 :::"the_sort_of"::: )  (Set (Var "A")) ")" )  ($#k3_finseq_2 :::"*"::: )  ")" ) "," (Set  "("  ($#k10_msualg_1 :::"the_sort_of"::: )  (Set (Var "A")) ")" ) ")" )))) ; 
 definitionlet "MS" be  ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )  (Num 1)  ($#v13_struct_0 :::"-element"::: )     ($#v5_msualg_1 :::"segmental"::: )     ($#l1_msualg_1 :::"ManySortedSign"::: )  ; let "A" be   ($#v4_msualg_1 :::"non-empty"::: )     ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Const "MS")); func  :::"the_charact_of"::: "A" ->   ($#m2_finseq_1 :::"PFuncFinSequence":::) "of" (Set  "("  ($#k10_msualg_1 :::"the_sort_of"::: )  "A" ")" ) equals :: MSUALG_1:def 13 (Set  "the"  ($#u4_msualg_1 :::"Charact"::: )  "of" "A"); end; 






:: deftheorem    defines :::"the_charact_of"::: MSUALG_1:def 13 :  (Bool  "for" (Set (Var "MS")) "being"  ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )  (Num 1)  ($#v13_struct_0 :::"-element"::: )     ($#v5_msualg_1 :::"segmental"::: )     ($#l1_msualg_1 :::"ManySortedSign"::: )    (Bool  "for" (Set (Var "A")) "being"   ($#v4_msualg_1 :::"non-empty"::: )     ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Var "MS")) "holds"  (Bool (Set   ($#k11_msualg_1 :::"the_charact_of"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set  "the"  ($#u4_msualg_1 :::"Charact"::: )  "of" (Set (Var "A")))))); 
 












definitionlet "MS" be  ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )  (Num 1)  ($#v13_struct_0 :::"-element"::: )     ($#v5_msualg_1 :::"segmental"::: )     ($#l1_msualg_1 :::"ManySortedSign"::: )  ; let "A" be   ($#v4_msualg_1 :::"non-empty"::: )     ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Const "MS")); func  :::"1-Alg"::: "A" ->   ($#v1_unialg_1 :::"strict"::: )    ($#l1_unialg_1 :::"Universal_Algebra":::) equals :: MSUALG_1:def 14 (Set   ($#g1_unialg_1 :::"UAStr"::: )  "(#"  (Set  "("  ($#k10_msualg_1 :::"the_sort_of"::: )  "A" ")" ) "," (Set  "("  ($#k11_msualg_1 :::"the_charact_of"::: )  "A" ")" ) "#)" ); end; 






:: deftheorem    defines :::"1-Alg"::: MSUALG_1:def 14 :  (Bool  "for" (Set (Var "MS")) "being"  ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )  (Num 1)  ($#v13_struct_0 :::"-element"::: )     ($#v5_msualg_1 :::"segmental"::: )     ($#l1_msualg_1 :::"ManySortedSign"::: )    (Bool  "for" (Set (Var "A")) "being"   ($#v4_msualg_1 :::"non-empty"::: )     ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Var "MS")) "holds"  (Bool (Set   ($#k12_msualg_1 :::"1-Alg"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set   ($#g1_unialg_1 :::"UAStr"::: )  "(#"  (Set  "("  ($#k10_msualg_1 :::"the_sort_of"::: )  (Set (Var "A")) ")" ) "," (Set  "("  ($#k11_msualg_1 :::"the_charact_of"::: )  (Set (Var "A")) ")" ) "#)" )))); 
 
theorem :: MSUALG_1:9 (Bool  "for" (Set (Var "A")) "being"   ($#v1_unialg_1 :::"strict"::: )    ($#l1_unialg_1 :::"Universal_Algebra":::) "holds"  (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set   ($#k12_msualg_1 :::"1-Alg"::: )  (Set  "("  ($#k9_msualg_1 :::"MSAlg"::: )  (Set (Var "A")) ")" )))) ; 
 
theorem :: MSUALG_1:10 (Bool  "for" (Set (Var "A")) "being"   ($#l1_unialg_1 :::"Universal_Algebra":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k4_finseq_1 :::"dom"::: )  (Set  "("  ($#k1_unialg_1 :::"signature"::: )  (Set (Var "A")) ")" ) ")" ) "," (Set  "(" (Set  ($#k1_tarski :::"{"::: ) (Set  ($#k6_numbers :::"0"::: ) ) ($#k1_tarski :::"}"::: ) )  ($#k3_finseq_2 :::"*"::: )  ")" )  (Bool  "for" (Set (Var "z")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set  ($#k1_tarski :::"{"::: ) (Set  ($#k6_numbers :::"0"::: ) ) ($#k1_tarski :::"}"::: ) )  "st" (Bool (Bool (Set (Var "f"))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k7_finseq_2 :::"*-->"::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" )  ($#k1_partfun1 :::"*"::: )  (Set  "("  ($#k1_unialg_1 :::"signature"::: )  (Set (Var "A")) ")" )))) "holds"  (Bool (Set   ($#k6_msualg_1 :::"MSSign"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set   ($#g1_msualg_1 :::"ManySortedSign"::: )  "(#"  (Set  ($#k1_tarski :::"{"::: ) (Set  ($#k6_numbers :::"0"::: ) ) ($#k1_tarski :::"}"::: ) ) "," (Set  "("  ($#k4_finseq_1 :::"dom"::: )  (Set  "("  ($#k1_unialg_1 :::"signature"::: )  (Set (Var "A")) ")" ) ")" ) "," (Set (Var "f")) "," (Set  "(" (Set  "("  ($#k4_finseq_1 :::"dom"::: )  (Set  "("  ($#k1_unialg_1 :::"signature"::: )  (Set (Var "A")) ")" ) ")" )  ($#k1_margrel1 :::"-->"::: )  (Set (Var "z")) ")" ) "#)" ))))) ;