begin
begin
:: deftheorem MSUALG_1:def 1 :
canceled;
:: deftheorem MSUALG_1:def 2 :
canceled;
:: deftheorem MSUALG_1:def 3 :
canceled;
:: deftheorem MSUALG_1:def 4 :
canceled;
:: deftheorem MSUALG_1:def 5 :
canceled;
:: deftheorem defines the_arity_of MSUALG_1:def 6 :
for S being non empty non void ManySortedSign
for o being OperSymbol of S holds the_arity_of o = the Arity of S . o;
:: deftheorem defines the_result_sort_of MSUALG_1:def 7 :
for S being non empty non void ManySortedSign
for o being OperSymbol of S holds the_result_sort_of o = the ResultSort of S . o;
begin
:: deftheorem Def8 defines non-empty MSUALG_1:def 8 :
for S being 1-sorted
for A being many-sorted of S holds
( A is non-empty iff the Sorts of A is non-empty );
:: deftheorem defines Args MSUALG_1:def 9 :
for S being non empty non void ManySortedSign
for o being OperSymbol of S
for A being MSAlgebra of S holds Args (o,A) = (( the Sorts of A #) * the Arity of S) . o;
:: deftheorem defines Result MSUALG_1:def 10 :
for S being non empty non void ManySortedSign
for o being OperSymbol of S
for A being MSAlgebra of S holds Result (o,A) = ( the Sorts of A * the ResultSort of S) . o;
:: deftheorem defines Den MSUALG_1:def 11 :
for S being non empty non void ManySortedSign
for o being OperSymbol of S
for A being MSAlgebra of S holds Den (o,A) = the Charact of A . o;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
begin
Lm1:
for D being non empty set
for h being non empty homogeneous quasi_total PartFunc of (D *),D holds dom h = (arity h) -tuples_on D
theorem Th7:
theorem Th8:
theorem Th9:
begin
:: deftheorem Def12 defines segmental MSUALG_1:def 12 :
for IT being ManySortedSign holds
( IT is segmental iff ex n being Nat st the carrier' of IT = Seg n );
theorem Th10:
reconsider z = 0 as Element of {0} by TARSKI:def 1;
Lm2:
for A being Universal_Algebra
for f being Function of (dom (signature A)),({0} *) holds
( not ManySortedSign(# {0},(dom (signature A)),f,((dom (signature A)) --> z) #) is empty & ManySortedSign(# {0},(dom (signature A)),f,((dom (signature A)) --> z) #) is segmental & ManySortedSign(# {0},(dom (signature A)),f,((dom (signature A)) --> z) #) is trivial & not ManySortedSign(# {0},(dom (signature A)),f,((dom (signature A)) --> z) #) is void & ManySortedSign(# {0},(dom (signature A)),f,((dom (signature A)) --> z) #) is strict )
:: deftheorem Def13 defines MSSign MSUALG_1:def 13 :
for A being Universal_Algebra
for b2 being trivial non void strict segmental ManySortedSign holds
( b2 = MSSign A iff ( the carrier of b2 = {0} & the carrier' of b2 = dom (signature A) & the Arity of b2 = (*--> 0) * (signature A) & the ResultSort of b2 = (dom (signature A)) --> 0 ) );
:: deftheorem defines MSSorts MSUALG_1:def 14 :
for A being Universal_Algebra holds MSSorts A = 0 .--> the carrier of A;
:: deftheorem defines MSCharact MSUALG_1:def 15 :
for A being Universal_Algebra holds MSCharact A = the charact of A;
:: deftheorem defines MSAlg MSUALG_1:def 16 :
for A being Universal_Algebra holds MSAlg A = MSAlgebra(# (MSSorts A),(MSCharact A) #);
:: deftheorem Def17 defines the_sort_of MSUALG_1:def 17 :
for MS being non empty trivial ManySortedSign
for A being MSAlgebra of MS
for b3 being set holds
( b3 = the_sort_of A iff b3 is Component of the Sorts of A );
theorem Th11:
theorem
canceled;
theorem Th13:
theorem Th14:
:: deftheorem defines the_charact_of MSUALG_1:def 18 :
for MS being non empty trivial non void segmental ManySortedSign
for A being non-empty MSAlgebra of MS holds the_charact_of A = the Charact of A;
:: deftheorem defines 1-Alg MSUALG_1:def 19 :
for MS being non empty trivial non void segmental ManySortedSign
for A being non-empty MSAlgebra of MS holds 1-Alg A = UAStr(# (the_sort_of A),(the_charact_of A) #);
theorem
theorem