:: MSUALG_1 semantic presentation

definition
attr a1 is strict;
struct ManySortedSign -> 1-sorted ;
aggr ManySortedSign(# carrier, OperSymbols, Arity, ResultSort #) -> ManySortedSign ;
sel OperSymbols c1 -> set ;
sel Arity c1 -> Function of the OperSymbols of a1,the carrier of a1 * ;
sel ResultSort c1 -> Function of the OperSymbols of a1,the carrier of a1;
end;

definition
let c1 be ManySortedSign ;
canceled;
canceled;
canceled;
canceled;
attr a1 is void means :Def5: :: MSUALG_1:def 5
the OperSymbols of a1 = {} ;
end;

:: deftheorem Def1 MSUALG_1:def 1 :
canceled;

:: deftheorem Def2 MSUALG_1:def 2 :
canceled;

:: deftheorem Def3 MSUALG_1:def 3 :
canceled;

:: deftheorem Def4 MSUALG_1:def 4 :
canceled;

:: deftheorem Def5 defines void MSUALG_1:def 5 :
for b1 being ManySortedSign holds
( b1 is void iff the OperSymbols of b1 = {} );

registration
cluster non empty strict void ManySortedSign ;
existence
ex b1 being ManySortedSign st
( b1 is void & b1 is strict & not b1 is empty )
proof end;
cluster non empty strict non void ManySortedSign ;
existence
ex b1 being ManySortedSign st
( not b1 is void & b1 is strict & not b1 is empty )
proof end;
end;

definition
let c1 be non empty ManySortedSign ;
mode SortSymbol of a1 is Element of a1;
mode OperSymbol of a1 is Element of the OperSymbols of a1;
end;

definition
let c1 be non empty non void ManySortedSign ;
let c2 be OperSymbol of c1;
func the_arity_of c2 -> Element of the carrier of a1 * equals :: MSUALG_1:def 6
the Arity of a1 . a2;
coherence
the Arity of c1 . c2 is Element of the carrier of c1 *
proof end;
correctness
;
func the_result_sort_of c2 -> Element of a1 equals :: MSUALG_1:def 7
the ResultSort of a1 . a2;
coherence
the ResultSort of c1 . c2 is Element of c1
proof end;
end;

:: deftheorem Def6 defines the_arity_of MSUALG_1:def 6 :
for b1 being non empty non void ManySortedSign
for b2 being OperSymbol of b1 holds the_arity_of b2 = the Arity of b1 . b2;

:: deftheorem Def7 defines the_result_sort_of MSUALG_1:def 7 :
for b1 being non empty non void ManySortedSign
for b2 being OperSymbol of b1 holds the_result_sort_of b2 = the ResultSort of b1 . b2;

definition
let c1 be 1-sorted ;
attr a2 is strict;
struct many-sorted of c1 -> ;
aggr many-sorted(# Sorts #) -> many-sorted of a1;
sel Sorts c2 -> ManySortedSet of the carrier of a1;
end;

definition
let c1 be non empty ManySortedSign ;
attr a2 is strict;
struct MSAlgebra of c1 -> many-sorted of a1;
aggr MSAlgebra(# Sorts, Charact #) -> MSAlgebra of a1;
sel Charact c2 -> ManySortedFunction of (the Sorts of a2 # ) * the Arity of a1,the Sorts of a2 * the ResultSort of a1;
end;

definition
let c1 be 1-sorted ;
let c2 be many-sorted of c1;
attr a2 is non-empty means :Def8: :: MSUALG_1:def 8
the Sorts of a2 is non-empty;
end;

:: deftheorem Def8 defines non-empty MSUALG_1:def 8 :
for b1 being 1-sorted
for b2 being many-sorted of b1 holds
( b2 is non-empty iff the Sorts of b2 is non-empty );

registration
let c1 be non empty ManySortedSign ;
cluster strict non-empty MSAlgebra of a1;
existence
ex b1 being MSAlgebra of c1 st
( b1 is strict & b1 is non-empty )
proof end;
end;

registration
let c1 be 1-sorted ;
cluster strict non-empty many-sorted of a1;
existence
ex b1 being many-sorted of c1 st
( b1 is strict & b1 is non-empty )
proof end;
end;

registration
let c1 be 1-sorted ;
let c2 be non-empty many-sorted of c1;
cluster the Sorts of a2 -> V2 ;
coherence
the Sorts of c2 is non-empty by Def8;
end;

registration
let c1 be non empty ManySortedSign ;
let c2 be non-empty MSAlgebra of c1;
cluster -> non empty Element of rng the Sorts of a2;
coherence
for b1 being Component of the Sorts of c2 holds not b1 is empty
proof end;
cluster -> non empty Element of rng (the Sorts of a2 # );
coherence
for b1 being Component of (the Sorts of c2 # ) holds not b1 is empty
proof end;
end;

definition
let c1 be non empty non void ManySortedSign ;
let c2 be OperSymbol of c1;
let c3 be MSAlgebra of c1;
func Args c2,c3 -> Component of (the Sorts of a3 # ) equals :: MSUALG_1:def 9
((the Sorts of a3 # ) * the Arity of a1) . a2;
coherence
((the Sorts of c3 # ) * the Arity of c1) . c2 is Component of (the Sorts of c3 # )
proof end;
correctness
;
func Result c2,c3 -> Component of the Sorts of a3 equals :: MSUALG_1:def 10
(the Sorts of a3 * the ResultSort of a1) . a2;
coherence
(the Sorts of c3 * the ResultSort of c1) . c2 is Component of the Sorts of c3
proof end;
correctness
;
end;

:: deftheorem Def9 defines Args MSUALG_1:def 9 :
for b1 being non empty non void ManySortedSign
for b2 being OperSymbol of b1
for b3 being MSAlgebra of b1 holds Args b2,b3 = ((the Sorts of b3 # ) * the Arity of b1) . b2;

:: deftheorem Def10 defines Result MSUALG_1:def 10 :
for b1 being non empty non void ManySortedSign
for b2 being OperSymbol of b1
for b3 being MSAlgebra of b1 holds Result b2,b3 = (the Sorts of b3 * the ResultSort of b1) . b2;

definition
let c1 be non empty non void ManySortedSign ;
let c2 be OperSymbol of c1;
let c3 be MSAlgebra of c1;
func Den c2,c3 -> Function of Args a2,a3, Result a2,a3 equals :: MSUALG_1:def 11
the Charact of a3 . a2;
coherence
the Charact of c3 . c2 is Function of Args c2,c3, Result c2,c3
proof end;
end;

:: deftheorem Def11 defines Den MSUALG_1:def 11 :
for b1 being non empty non void ManySortedSign
for b2 being OperSymbol of b1
for b3 being MSAlgebra of b1 holds Den b2,b3 = the Charact of b3 . b2;

theorem Th1: :: MSUALG_1:1
canceled;

theorem Th2: :: MSUALG_1:2
canceled;

theorem Th3: :: MSUALG_1:3
canceled;

theorem Th4: :: MSUALG_1:4
canceled;

theorem Th5: :: MSUALG_1:5
canceled;

theorem Th6: :: MSUALG_1:6
for b1 being non empty non void ManySortedSign
for b2 being OperSymbol of b1
for b3 being non-empty MSAlgebra of b1 holds not Den b2,b3 is empty by FUNCT_2:def 1, RELAT_1:60;

Lemma3: for b1 being non empty set
for b2 being non empty homogeneous quasi_total PartFunc of b1 * ,b1 holds dom b2 = (arity b2) -tuples_on b1
proof end;

theorem Th7: :: MSUALG_1:7
for b1 being set
for b2, b3 being non empty set
for b4 being PartFunc of b1,b2
for b5 being Function of b2,b3 holds b5 * b4 is Function of dom b4,b3
proof end;

theorem Th8: :: MSUALG_1:8
for b1 being non empty set
for b2 being non empty homogeneous quasi_total PartFunc of b1 * ,b1 holds dom b2 = Funcs (Seg (arity b2)),b1
proof end;

theorem Th9: :: MSUALG_1:9
for b1 being Universal_Algebra holds not signature b1 is empty
proof end;

definition
let c1 be Universal_Algebra;
redefine func signature as signature c1 -> FinSequence of NAT ;
coherence
signature c1 is FinSequence of NAT ;
end;

definition
let c1 be ManySortedSign ;
attr a1 is segmental means :Def12: :: MSUALG_1:def 12
ex b1 being Nat st the OperSymbols of a1 = Seg b1;
end;

:: deftheorem Def12 defines segmental MSUALG_1:def 12 :
for b1 being ManySortedSign holds
( b1 is segmental iff ex b2 being Nat st the OperSymbols of b1 = Seg b2 );

theorem Th10: :: MSUALG_1:10
for b1 being non empty ManySortedSign st b1 is trivial holds
for b2 being MSAlgebra of b1
for b3, b4 being Component of the Sorts of b2 holds b3 = b4
proof end;

Lemma9: for b1 being Universal_Algebra
for b2 being Function of dom (signature b1),{0} * st b2 = (*--> 0) * (signature b1) holds
( not ManySortedSign(# {0},(dom (signature b1)),b2,((dom (signature b1)) --> 0) #) is empty & ManySortedSign(# {0},(dom (signature b1)),b2,((dom (signature b1)) --> 0) #) is segmental & ManySortedSign(# {0},(dom (signature b1)),b2,((dom (signature b1)) --> 0) #) is trivial & not ManySortedSign(# {0},(dom (signature b1)),b2,((dom (signature b1)) --> 0) #) is void & ManySortedSign(# {0},(dom (signature b1)),b2,((dom (signature b1)) --> 0) #) is strict )
proof end;

registration
cluster non empty trivial strict non void segmental ManySortedSign ;
existence
ex b1 being ManySortedSign st
( b1 is segmental & b1 is trivial & not b1 is void & b1 is strict & not b1 is empty )
proof end;
end;

definition
let c1 be Universal_Algebra;
func MSSign c1 -> trivial strict non void segmental ManySortedSign means :Def13: :: MSUALG_1:def 13
( the carrier of a2 = {0} & the OperSymbols of a2 = dom (signature a1) & the Arity of a2 = (*--> 0) * (signature a1) & the ResultSort of a2 = (dom (signature a1)) --> 0 );
correctness
existence
ex b1 being trivial strict non void segmental ManySortedSign st
( the carrier of b1 = {0} & the OperSymbols of b1 = dom (signature c1) & the Arity of b1 = (*--> 0) * (signature c1) & the ResultSort of b1 = (dom (signature c1)) --> 0 );
uniqueness
for b1, b2 being trivial strict non void segmental ManySortedSign st the carrier of b1 = {0} & the OperSymbols of b1 = dom (signature c1) & the Arity of b1 = (*--> 0) * (signature c1) & the ResultSort of b1 = (dom (signature c1)) --> 0 & the carrier of b2 = {0} & the OperSymbols of b2 = dom (signature c1) & the Arity of b2 = (*--> 0) * (signature c1) & the ResultSort of b2 = (dom (signature c1)) --> 0 holds
b1 = b2;
proof end;
end;

:: deftheorem Def13 defines MSSign MSUALG_1:def 13 :
for b1 being Universal_Algebra
for b2 being trivial strict non void segmental ManySortedSign holds
( b2 = MSSign b1 iff ( the carrier of b2 = {0} & the OperSymbols of b2 = dom (signature b1) & the Arity of b2 = (*--> 0) * (signature b1) & the ResultSort of b2 = (dom (signature b1)) --> 0 ) );

registration
let c1 be Universal_Algebra;
cluster MSSign a1 -> non empty trivial strict non void segmental ;
coherence
not MSSign c1 is empty
proof end;
end;

definition
let c1 be Universal_Algebra;
func MSSorts c1 -> V2 ManySortedSet of the carrier of (MSSign a1) equals :: MSUALG_1:def 14
{0} --> the carrier of a1;
coherence
{0} --> the carrier of c1 is V2 ManySortedSet of the carrier of (MSSign c1)
proof end;
correctness
;
end;

:: deftheorem Def14 defines MSSorts MSUALG_1:def 14 :
for b1 being Universal_Algebra holds MSSorts b1 = {0} --> the carrier of b1;

definition
let c1 be Universal_Algebra;
func MSCharact c1 -> ManySortedFunction of ((MSSorts a1) # ) * the Arity of (MSSign a1),(MSSorts a1) * the ResultSort of (MSSign a1) equals :: MSUALG_1:def 15
the charact of a1;
coherence
the charact of c1 is ManySortedFunction of ((MSSorts c1) # ) * the Arity of (MSSign c1),(MSSorts c1) * the ResultSort of (MSSign c1)
proof end;
correctness
;
end;

:: deftheorem Def15 defines MSCharact MSUALG_1:def 15 :
for b1 being Universal_Algebra holds MSCharact b1 = the charact of b1;

definition
let c1 be Universal_Algebra;
func MSAlg c1 -> strict MSAlgebra of MSSign a1 equals :: MSUALG_1:def 16
 MSAlgebra(# (MSSorts a1),(MSCharact a1) #);
correctness
coherence
MSAlgebra(# (MSSorts c1),(MSCharact c1) #) is strict MSAlgebra of MSSign c1;
;
end;

:: deftheorem Def16 defines MSAlg MSUALG_1:def 16 :
for b1 being Universal_Algebra holds MSAlg b1 = MSAlgebra(# (MSSorts b1),(MSCharact b1) #);

registration
let c1 be Universal_Algebra;
cluster MSAlg a1 -> strict non-empty ;
coherence
MSAlg c1 is non-empty
proof end;
end;

definition
let c1 be non empty trivial ManySortedSign ;
let c2 be MSAlgebra of c1;
func the_sort_of c2 -> set means :Def17: :: MSUALG_1:def 17
a3 is Component of the Sorts of a2;
existence
ex b1 being set st b1 is Component of the Sorts of c2
proof end;
uniqueness
for b1, b2 being set st b1 is Component of the Sorts of c2 & b2 is Component of the Sorts of c2 holds
b1 = b2 by Th10;
end;

:: deftheorem Def17 defines the_sort_of MSUALG_1:def 17 :
for b1 being non empty trivial ManySortedSign
for b2 being MSAlgebra of b1
for b3 being set holds
( b3 = the_sort_of b2 iff b3 is Component of the Sorts of b2 );

registration
let c1 be non empty trivial ManySortedSign ;
let c2 be non-empty MSAlgebra of c1;
cluster the_sort_of a2 -> non empty ;
coherence
not the_sort_of c2 is empty
proof end;
end;

theorem Th11: :: MSUALG_1:11
for b1 being non empty trivial non void segmental ManySortedSign
for b2 being OperSymbol of b1
for b3 being non-empty MSAlgebra of b1 holds Args b2,b3 = (len (the_arity_of b2)) -tuples_on (the_sort_of b3)
proof end;

theorem Th12: :: MSUALG_1:12
for b1 being non empty set
for b2 being Nat holds b2 -tuples_on b1 c= b1 *
proof end;

theorem Th13: :: MSUALG_1:13
for b1 being non empty trivial non void segmental ManySortedSign
for b2 being OperSymbol of b1
for b3 being non-empty MSAlgebra of b1 holds Args b2,b3 c= (the_sort_of b3) *
proof end;

theorem Th14: :: MSUALG_1:14
for b1 being non empty trivial non void segmental ManySortedSign
for b2 being non-empty MSAlgebra of b1 holds the Charact of b2 is FinSequence of PFuncs ((the_sort_of b2) * ),(the_sort_of b2)
proof end;

definition
let c1 be non empty trivial non void segmental ManySortedSign ;
let c2 be non-empty MSAlgebra of c1;
func the_charact_of c2 -> PFuncFinSequence of (the_sort_of a2) equals :: MSUALG_1:def 18
the Charact of a2;
coherence
the Charact of c2 is PFuncFinSequence of (the_sort_of c2) by Th14;
end;

:: deftheorem Def18 defines the_charact_of MSUALG_1:def 18 :
for b1 being non empty trivial non void segmental ManySortedSign
for b2 being non-empty MSAlgebra of b1 holds the_charact_of b2 = the Charact of b2;

definition
let c1 be non empty trivial non void segmental ManySortedSign ;
let c2 be non-empty MSAlgebra of c1;
func 1-Alg c2 -> strict non-empty Universal_Algebra equals :: MSUALG_1:def 19
 UAStr(# (the_sort_of a2),(the_charact_of a2) #);
coherence
UAStr(# (the_sort_of c2),(the_charact_of c2) #) is strict non-empty Universal_Algebra
proof end;
correctness
;
end;

:: deftheorem Def19 defines 1-Alg MSUALG_1:def 19 :
for b1 being non empty trivial non void segmental ManySortedSign
for b2 being non-empty MSAlgebra of b1 holds 1-Alg b2 = UAStr(# (the_sort_of b2),(the_charact_of b2) #);

theorem Th15: :: MSUALG_1:15
for b1 being strict Universal_Algebra holds b1 = 1-Alg (MSAlg b1)
proof end;

theorem Th16: :: MSUALG_1:16
for b1 being Universal_Algebra
for b2 being Function of dom (signature b1),{0} * st b2 = (*--> 0) * (signature b1) holds
MSSign b1 = ManySortedSign(# {0},(dom (signature b1)),b2,((dom (signature b1)) --> 0) #)
proof end;