:: UNIALG_1  semantic presentation begin  


definitionattr "c1" is  :::"strict"::: ; struct  :::"UAStr":::  ->    ($#l1_struct_0 :::"1-sorted"::: )  ; aggr :::"UAStr":::(# :::"carrier":::, :::"charact"::: #) ->    ($#l1_unialg_1 :::"UAStr"::: )  ; sel  :::"charact"::: "c1" ->   ($#m2_finseq_1 :::"PFuncFinSequence":::) "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "c1"); end; registration
cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_unialg_1 :::"strict"::: )    for    ($#l1_unialg_1 :::"UAStr"::: )  ; 
end; registrationlet "D" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; let "c" be   ($#m2_finseq_1 :::"PFuncFinSequence":::) "of" (Set (Const "D")); 
cluster (Set   ($#g1_unialg_1 :::"UAStr"::: )  "(#"  "D" "," "c" "#)" ) ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )  ; 
end; definitionlet "IT" be    ($#l1_unialg_1 :::"UAStr"::: )  ; attr "IT" is  :::"partial":::  means :: UNIALG_1:def 1 (Bool (Set  "the"  ($#u1_unialg_1 :::"charact"::: )  "of" "IT") "is"   ($#v4_margrel1 :::"homogeneous"::: )  ); attr "IT" is  :::"quasi_total":::  means :: UNIALG_1:def 2 (Bool (Set  "the"  ($#u1_unialg_1 :::"charact"::: )  "of" "IT") "is"   ($#v5_margrel1 :::"quasi_total"::: )  ); attr "IT" is  :::"non-empty":::  means :: UNIALG_1:def 3 (Bool  "("  (Bool (Set  "the"  ($#u1_unialg_1 :::"charact"::: )  "of" "IT")  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) & (Bool (Set  "the"  ($#u1_unialg_1 :::"charact"::: )  "of" "IT") "is"   ($#v2_relat_1 :::"non-empty"::: )  )  ")" ); end; 












:: deftheorem    defines :::"partial"::: UNIALG_1:def 1 :  (Bool  "for" (Set (Var "IT")) "being"    ($#l1_unialg_1 :::"UAStr"::: )   "holds"   (Bool  "("  (Bool (Set (Var "IT")) "is"   ($#v2_unialg_1 :::"partial"::: )  ) "iff" (Bool (Set  "the"  ($#u1_unialg_1 :::"charact"::: )  "of" (Set (Var "IT"))) "is"   ($#v4_margrel1 :::"homogeneous"::: )  )  ")" )); 
 
:: deftheorem    defines :::"quasi_total"::: UNIALG_1:def 2 :  (Bool  "for" (Set (Var "IT")) "being"    ($#l1_unialg_1 :::"UAStr"::: )   "holds"   (Bool  "("  (Bool (Set (Var "IT")) "is"   ($#v3_unialg_1 :::"quasi_total"::: )  ) "iff" (Bool (Set  "the"  ($#u1_unialg_1 :::"charact"::: )  "of" (Set (Var "IT"))) "is"   ($#v5_margrel1 :::"quasi_total"::: )  )  ")" )); 
 
:: deftheorem    defines :::"non-empty"::: UNIALG_1:def 3 :  (Bool  "for" (Set (Var "IT")) "being"    ($#l1_unialg_1 :::"UAStr"::: )   "holds"   (Bool  "("  (Bool (Set (Var "IT")) "is"   ($#v4_unialg_1 :::"non-empty"::: )  ) "iff" (Bool  "("  (Bool (Set  "the"  ($#u1_unialg_1 :::"charact"::: )  "of" (Set (Var "IT")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) & (Bool (Set  "the"  ($#u1_unialg_1 :::"charact"::: )  "of" (Set (Var "IT"))) "is"   ($#v2_relat_1 :::"non-empty"::: )  )  ")" )  ")" )); 
 registration
cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_unialg_1 :::"strict"::: )     ($#v2_unialg_1 :::"partial"::: )     ($#v3_unialg_1 :::"quasi_total"::: )     ($#v4_unialg_1 :::"non-empty"::: )    for    ($#l1_unialg_1 :::"UAStr"::: )  ; 
end; registrationlet "U1" be   ($#v2_unialg_1 :::"partial"::: )     ($#l1_unialg_1 :::"UAStr"::: )  ; 
cluster (Set  "the"  ($#u1_unialg_1 :::"charact"::: )  "of" "U1") ->   ($#v4_margrel1 :::"homogeneous"::: )   ; 
end; registrationlet "U1" be   ($#v3_unialg_1 :::"quasi_total"::: )     ($#l1_unialg_1 :::"UAStr"::: )  ; 
cluster (Set  "the"  ($#u1_unialg_1 :::"charact"::: )  "of" "U1") ->   ($#v5_margrel1 :::"quasi_total"::: )   ; 
end; registrationlet "U1" be   ($#v4_unialg_1 :::"non-empty"::: )     ($#l1_unialg_1 :::"UAStr"::: )  ; 
cluster (Set  "the"  ($#u1_unialg_1 :::"charact"::: )  "of" "U1") ->   ($#v2_relat_1 :::"non-empty"::: )    ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )  ; 
end; definitionmode Universal_Algebra is  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v2_unialg_1 :::"partial"::: )     ($#v3_unialg_1 :::"quasi_total"::: )     ($#v4_unialg_1 :::"non-empty"::: )     ($#l1_unialg_1 :::"UAStr"::: )  ; end; 



theorem :: UNIALG_1:1 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "U1")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v2_unialg_1 :::"partial"::: )     ($#v4_unialg_1 :::"non-empty"::: )     ($#l1_unialg_1 :::"UAStr"::: )    "st" (Bool (Bool (Set (Var "n"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set  "the"  ($#u1_unialg_1 :::"charact"::: )  "of" (Set (Var "U1")))))) "holds"  (Bool (Set (Set  "the"  ($#u1_unialg_1 :::"charact"::: )  "of" (Set (Var "U1")))  ($#k1_funct_1 :::"."::: )  (Set (Var "n"))) "is"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  "(" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "U1")))  ($#k3_finseq_2 :::"*"::: )  ")" ) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "U1")))))) ; 
 definitionlet "U1" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v2_unialg_1 :::"partial"::: )     ($#v4_unialg_1 :::"non-empty"::: )     ($#l1_unialg_1 :::"UAStr"::: )  ; func  :::"signature"::: "U1" ->    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) means :: UNIALG_1:def 4 (Bool  "("  (Bool (Set   ($#k3_finseq_1 :::"len"::: )  it)  ($#r1_hidden :::"="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set  "the"  ($#u1_unialg_1 :::"charact"::: )  "of" "U1"))) & (Bool  "("   "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "n"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  it))) "holds"  (Bool  "for" (Set (Var "h")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_margrel1 :::"homogeneous"::: )    ($#m1_subset_1 :::"PartFunc":::) "of" (Set  "(" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "U1")  ($#k3_finseq_2 :::"*"::: )  ")" ) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "U1")  "st" (Bool (Bool (Set (Var "h"))  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u1_unialg_1 :::"charact"::: )  "of" "U1")  ($#k1_funct_1 :::"."::: )  (Set (Var "n"))))) "holds"  (Bool (Set it  ($#k1_funct_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set   ($#k19_margrel1 :::"arity"::: )  (Set (Var "h")))))  ")" )  ")" ); end; 





:: deftheorem    defines :::"signature"::: UNIALG_1:def 4 :  (Bool  "for" (Set (Var "U1")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v2_unialg_1 :::"partial"::: )     ($#v4_unialg_1 :::"non-empty"::: )     ($#l1_unialg_1 :::"UAStr"::: )    (Bool  "for" (Set (Var "b2")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_unialg_1 :::"signature"::: )  (Set (Var "U1")))) "iff" (Bool  "("  (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "b2")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set  "the"  ($#u1_unialg_1 :::"charact"::: )  "of" (Set (Var "U1"))))) & (Bool  "("   "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "n"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "b2"))))) "holds"  (Bool  "for" (Set (Var "h")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_margrel1 :::"homogeneous"::: )    ($#m1_subset_1 :::"PartFunc":::) "of" (Set  "(" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "U1")))  ($#k3_finseq_2 :::"*"::: )  ")" ) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "U1")))  "st" (Bool (Bool (Set (Var "h"))  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u1_unialg_1 :::"charact"::: )  "of" (Set (Var "U1")))  ($#k1_funct_1 :::"."::: )  (Set (Var "n"))))) "holds"  (Bool (Set (Set (Var "b2"))  ($#k1_funct_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set   ($#k19_margrel1 :::"arity"::: )  (Set (Var "h")))))  ")" )  ")" )  ")" ))); 
 begin  registrationlet "U0" be   ($#l1_unialg_1 :::"Universal_Algebra":::); 
cluster (Set  "the"  ($#u1_unialg_1 :::"charact"::: )  "of" "U0") ->   ($#v1_funcop_1 :::"Function-yielding"::: )   ; 
end;