:: MSUALG_1 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

definition
attr c1 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 c1,the carrier of c1 * ;
sel ResultSort c1 -> Function of the OperSymbols of c1,the carrier of c1;
end;

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

:: 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 Def5 defines void MSUALG_1:def 5 :
for IT being ManySortedSign holds
( IT is void iff the OperSymbols of IT = {} );

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 S be non empty ManySortedSign ;
mode SortSymbol of S is Element of S;
mode OperSymbol of S is Element of the OperSymbols of S;
end;

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

:: 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;

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

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

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

:: 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 );

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

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

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

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

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

:: 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;

definition
let S be non empty non void ManySortedSign ;
let o be OperSymbol of S;
let A be MSAlgebra of S;
func Den o,A -> Function of Args o,A, Result o,A equals :: MSUALG_1:def 11
the Charact of A . o;
coherence
the Charact of A . o is Function of Args o,A, Result o,A
proof end;
end;

:: 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 :: MSUALG_1:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: MSUALG_1:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: MSUALG_1:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: MSUALG_1:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: MSUALG_1:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: MSUALG_1:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for o being OperSymbol of S
for A being non-empty MSAlgebra of S holds not Den o,A is empty by FUNCT_2:def 1, RELAT_1:60;

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
proof end;

theorem Th7: :: MSUALG_1:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being set
for A, B being non empty set
for F being PartFunc of C,A
for G being Function of A,B holds G * F is Function of dom F,B
proof end;

theorem Th8: :: MSUALG_1:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for h being non empty homogeneous quasi_total PartFunc of D * ,D holds dom h = Funcs (Seg (arity h)),D
proof end;

theorem Th9: :: MSUALG_1:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being Universal_Algebra holds not signature A is empty
proof end;

definition
let A be Universal_Algebra;
:: original: signature
redefine func signature A -> FinSequence of NAT ;
coherence
signature A is FinSequence of NAT ;
end;

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

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

theorem Th10: :: MSUALG_1:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty ManySortedSign st S is trivial holds
for A being MSAlgebra of S
for c1, c2 being Component of the Sorts of A holds c1 = c2
proof end;

Lm2: for A being Universal_Algebra
for f being Function of dom (signature A),{0} * st f = (*--> 0) * (signature A) holds
( not ManySortedSign(# {0},(dom (signature A)),f,((dom (signature A)) --> 0) #) is empty & ManySortedSign(# {0},(dom (signature A)),f,((dom (signature A)) --> 0) #) is segmental & ManySortedSign(# {0},(dom (signature A)),f,((dom (signature A)) --> 0) #) is trivial & not ManySortedSign(# {0},(dom (signature A)),f,((dom (signature A)) --> 0) #) is void & ManySortedSign(# {0},(dom (signature A)),f,((dom (signature A)) --> 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 A be Universal_Algebra;
func MSSign A -> trivial strict non void segmental ManySortedSign means :Def13: :: MSUALG_1:def 13
( the carrier of it = {0} & the OperSymbols of it = dom (signature A) & the Arity of it = (*--> 0) * (signature A) & the ResultSort of it = (dom (signature A)) --> 0 );
correctness
existence
ex b1 being trivial strict non void segmental ManySortedSign st
( the carrier of b1 = {0} & the OperSymbols of b1 = dom (signature A) & the Arity of b1 = (*--> 0) * (signature A) & the ResultSort of b1 = (dom (signature A)) --> 0 );
uniqueness
for b1, b2 being trivial strict non void segmental ManySortedSign st the carrier of b1 = {0} & the OperSymbols of b1 = dom (signature A) & the Arity of b1 = (*--> 0) * (signature A) & the ResultSort of b1 = (dom (signature A)) --> 0 & the carrier of b2 = {0} & the OperSymbols of b2 = dom (signature A) & the Arity of b2 = (*--> 0) * (signature A) & the ResultSort of b2 = (dom (signature A)) --> 0 holds
b1 = b2;
proof end;
end;

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

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

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

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

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

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

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

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

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

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

:: 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 );

registration
let MS be non empty trivial ManySortedSign ;
let A be non-empty MSAlgebra of MS;
cluster the_sort_of A -> non empty ;
coherence
not the_sort_of A is empty
proof end;
end;

theorem Th11: :: MSUALG_1:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for MS being non empty trivial non void segmental ManySortedSign
for i being OperSymbol of MS
for A being non-empty MSAlgebra of MS holds Args i,A = (len (the_arity_of i)) -tuples_on (the_sort_of A)
proof end;

theorem Th12: :: MSUALG_1:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being non empty set
for n being Nat holds n -tuples_on A c= A *
proof end;

theorem Th13: :: MSUALG_1:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for MS being non empty trivial non void segmental ManySortedSign
for i being OperSymbol of MS
for A being non-empty MSAlgebra of MS holds Args i,A c= (the_sort_of A) *
proof end;

theorem Th14: :: MSUALG_1:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for MS being non empty trivial non void segmental ManySortedSign
for A being non-empty MSAlgebra of MS holds the Charact of A is FinSequence of PFuncs ((the_sort_of A) * ),(the_sort_of A)
proof end;

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

:: 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;

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

:: 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 :: MSUALG_1:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being strict Universal_Algebra holds A = 1-Alg (MSAlg A)
proof end;

theorem :: MSUALG_1:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being Universal_Algebra
for f being Function of dom (signature A),{0} * st f = (*--> 0) * (signature A) holds
MSSign A = ManySortedSign(# {0},(dom (signature A)),f,((dom (signature A)) --> 0) #)
proof end;