:: MSALIMIT semantic presentation

registration

let c₁ be non empty set ;
let c₂ be non empty non void ManySortedSign ;
let c₃ be MSAlgebra-Family of c₁,c₂;
let c₄ be Element of c₁;
let c₅ be OperSymbol of c₂;
cluster ((OPER a₃) . a₄) . a₅ -> Relation-like Function-like ;
coherence

proof end;

end;

registration

let c₁ be non empty set ;
let c₂ be non empty non void ManySortedSign ;
let c₃ be MSAlgebra-Family of c₁,c₂;
let c₄ be SortSymbol of c₂;
cluster (SORTS a₃) . a₄ -> functional ;
coherence

proof end;

end;

definition

let c₁ be non empty Poset;
let c₂ be non empty non void ManySortedSign ;
mode OrderedAlgFam of c₁,c₂ -> MSAlgebra-Family of the carrier of a₁,a₂ means :Def1: :: MSALIMIT:def 1
ex b₁ being ManySortedFunction of the InternalRel of a₁ st
for b₂, b₃, b₄ being Element of a₁ st b₂ >= b₃ & b₃ >= b₄ holds
ex b₅ being ManySortedFunction of (a₃ . b₂),(a₃ . b₃)ex b₆ being ManySortedFunction of (a₃ . b₃),(a₃ . b₄) st
( b₅ = b₁ . b₃,b₂ & b₆ = b₁ . b₄,b₃ & b₁ . b₄,b₂ = b₆ ** b₅ & b₅ is_homomorphism a₃ . b₂,a₃ . b₃ );
existence

proof end;

end;

:: deftheorem Def1 defines OrderedAlgFam MSALIMIT:def 1 :

definition

let c₁ be non empty Poset;
let c₂ be non empty non void ManySortedSign ;
let c₃ be OrderedAlgFam of c₁,c₂;
mode Binding of c₃ -> ManySortedFunction of the InternalRel of a₁ means :Def2: :: MSALIMIT:def 2
for b₁, b₂, b₃ being Element of a₁ st b₁ >= b₂ & b₂ >= b₃ holds
ex b₄ being ManySortedFunction of (a₃ . b₁),(a₃ . b₂)ex b₅ being ManySortedFunction of (a₃ . b₂),(a₃ . b₃) st
( b₄ = a₄ . b₂,b₁ & b₅ = a₄ . b₃,b₂ & a₄ . b₃,b₁ = b₅ ** b₄ & b₄ is_homomorphism a₃ . b₁,a₃ . b₂ );
existence by Def1;

end;

:: deftheorem Def2 defines Binding MSALIMIT:def 2 :

definition

let c₁ be non empty Poset;
let c₂ be non empty non void ManySortedSign ;
let c₃ be OrderedAlgFam of c₁,c₂;
let c₄ be Binding of c₃;
let c₅, c₆ be Element of c₁;
assume E3: c₅ >= c₆ ;
func bind c₄,c₅,c₆ -> ManySortedFunction of (a₃ . a₅),(a₃ . a₆) equals :Def3: :: MSALIMIT:def 3
a₄ . a₆,a₅;
coherence

proof end;

end;

:: deftheorem Def3 defines bind MSALIMIT:def 3 :

theorem Th1: :: MSALIMIT:1

for b₁ being non empty Poset
for b₂, b₃, b₄ being Element of b₁
for b₅ being non empty non void ManySortedSign
for b₆ being OrderedAlgFam of b₁,b₅
for b₇ being Binding of b₆ st b₂ >= b₃ & b₃ >= b₄ holds
(bind b₇,b₃,b₄) ** (bind b₇,b₂,b₃) = bind b₇,b₂,b₄

proof end;

definition

let c₁ be non empty Poset;
let c₂ be non empty non void ManySortedSign ;
let c₃ be OrderedAlgFam of c₁,c₂;
let c₄ be Binding of c₃;
attr a₄ is normalized means :Def4: :: MSALIMIT:def 4
for b₁ being Element of a₁ holds a₄ . b₁,b₁ = id the Sorts of (a₃ . b₁);

end;

:: deftheorem Def4 defines normalized MSALIMIT:def 4 :

theorem Th2: :: MSALIMIT:2

for b₁ being non empty Poset
for b₂ being non empty non void ManySortedSign
for b₃ being OrderedAlgFam of b₁,b₂
for b₄ being Binding of b₃
for b₅, b₆ being Element of b₁ st b₅ >= b₆ holds
for b₇ being ManySortedFunction of (b₃ . b₅),(b₃ . b₆) st b₇ = bind b₄,b₅,b₆ holds
b₇ is_homomorphism b₃ . b₅,b₃ . b₆

proof end;

definition

let c₁ be non empty Poset;
let c₂ be non empty non void ManySortedSign ;
let c₃ be OrderedAlgFam of c₁,c₂;
let c₄ be Binding of c₃;
func Normalized c₄ -> Binding of a₃ means :Def5: :: MSALIMIT:def 5
for b₁, b₂ being Element of a₁ st b₁ >= b₂ holds
a₅ . b₂,b₁ = IFEQ b₂,b₁,(id the Sorts of (a₃ . b₁)),((bind a₄,b₁,b₂) ** (id the Sorts of (a₃ . b₁)));
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines Normalized MSALIMIT:def 5 :

theorem Th3: :: MSALIMIT:3

for b₁ being non empty Poset
for b₂ being non empty non void ManySortedSign
for b₃ being OrderedAlgFam of b₁,b₂
for b₄ being Binding of b₃
for b₅, b₆ being Element of b₁ st b₅ >= b₆ & b₅ <> b₆ holds
b₄ . b₆,b₅ = (Normalized b₄) . b₆,b₅

proof end;

registration

let c₁ be non empty Poset;
let c₂ be non empty non void ManySortedSign ;
let c₃ be OrderedAlgFam of c₁,c₂;
let c₄ be Binding of c₃;
cluster Normalized a₄ -> normalized ;
coherence

proof end;

end;

registration

let c₁ be non empty Poset;
let c₂ be non empty non void ManySortedSign ;
let c₃ be OrderedAlgFam of c₁,c₂;
cluster normalized Binding of a₃;
existence

proof end;

end;

theorem Th4: :: MSALIMIT:4

for b₁ being non empty Poset
for b₂ being non empty non void ManySortedSign
for b₃ being OrderedAlgFam of b₁,b₂
for b₄ being normalized Binding of b₃
for b₅, b₆ being Element of b₁ st b₅ >= b₆ holds
(Normalized b₄) . b₆,b₅ = b₄ . b₆,b₅

proof end;

definition

let c₁ be non empty Poset;
let c₂ be non empty non void ManySortedSign ;
let c₃ be OrderedAlgFam of c₁,c₂;
let c₄ be Binding of c₃;
func InvLim c₄ -> strict MSSubAlgebra of product a₃ means :Def6: :: MSALIMIT:def 6
for b₁ being SortSymbol of a₂
for b₂ being Element of (SORTS a₃) . b₁ holds
( b₂ in the Sorts of a₅ . b₁ iff for b₃, b₄ being Element of a₁ st b₃ >= b₄ holds
((bind a₄,b₃,b₄) . b₁) . (b₂ . b₃) = b₂ . b₄ );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def6 defines InvLim MSALIMIT:def 6 :

theorem Th5: :: MSALIMIT:5

for b₁ being non empty discrete Poset
for b₂ being non empty non void ManySortedSign
for b₃ being OrderedAlgFam of b₁,b₂
for b₄ being normalized Binding of b₃ holds InvLim b₄ = product b₃

proof end;

definition

let c₁ be set ;
attr a₁ is MSS-membered means :Def7: :: MSALIMIT:def 7
for b₁ being set st b₁ in a₁ holds
b₁ is non empty strict non void ManySortedSign ;

end;

:: deftheorem Def7 defines MSS-membered MSALIMIT:def 7 :

registration

cluster non empty MSS-membered set ;
existence

proof end;

end;

definition

func TrivialMSSign -> strict ManySortedSign means :Def8: :: MSALIMIT:def 8
( a₁ is empty & a₁ is void );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def8 defines TrivialMSSign MSALIMIT:def 8 :

registration

cluster TrivialMSSign -> empty strict void ;
coherence by Def8;

end;

registration

cluster empty strict void ManySortedSign ;
existence

proof end;

end;

Lemma12: for b₁ being empty void ManySortedSign holds id the carrier of b₁, id the OperSymbols of b₁ form_morphism_between b₁,b₁

proof end;

Lemma13: for b₁ being non empty void ManySortedSign holds id the carrier of b₁, id the OperSymbols of b₁ form_morphism_between b₁,b₁

proof end;

theorem Th6: :: MSALIMIT:6

for b₁ being void ManySortedSign holds id the carrier of b₁, id the OperSymbols of b₁ form_morphism_between b₁,b₁

proof end;

definition

let c₁ be non empty set ;
func MSS_set c₁ -> set means :Def9: :: MSALIMIT:def 9
for b₁ being set holds
( b₁ in a₂ iff ex b₂ being non empty strict non void ManySortedSign st
( b₁ = b₂ & the carrier of b₂ c= a₁ & the OperSymbols of b₂ c= a₁ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def9 defines MSS_set MSALIMIT:def 9 :

registration

let c₁ be non empty set ;
cluster MSS_set a₁ -> non empty MSS-membered ;
coherence

proof end;

end;

definition

let c₁ be non empty MSS-membered set ;
redefine mode Element as Element of c₁ -> non empty strict non void ManySortedSign ;
coherence by Def7;

end;

definition

let c₁, c₂ be ManySortedSign ;
func MSS_morph c₁,c₂ -> set means :: MSALIMIT:def 10
for b₁ being set holds
( b₁ in a₃ iff ex b₂, b₃ being Function st
( b₁ = [b₂,b₃] & b₂,b₃ form_morphism_between a₁,a₂ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def10 defines MSS_morph MSALIMIT:def 10 :