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

registration
let I be non empty set ;
let S be non empty non void ManySortedSign ;
let AF be MSAlgebra-Family of I,S;
let i be Element of I;
let o be OperSymbol of S;
cluster ((OPER AF) . i) . o -> Relation-like Function-like ;
coherence
( ((OPER AF) . i) . o is Function-like & ((OPER AF) . i) . o is Relation-like )
proof end;
end;

registration
let I be non empty set ;
let S be non empty non void ManySortedSign ;
let AF be MSAlgebra-Family of I,S;
let s be SortSymbol of S;
cluster (SORTS AF) . s -> functional ;
coherence
(SORTS AF) . s is functional
proof end;
end;

definition
let P be non empty Poset;
let S be non empty non void ManySortedSign ;
mode OrderedAlgFam of P,S -> MSAlgebra-Family of the carrier of P,S means :Def1: :: MSALIMIT:def 1
 ex F being ManySortedFunction of the InternalRel of P st
for i, j, k being Element of P st i >= j & j >= k holds
ex f1 being ManySortedFunction of (it . i),(it . j) ex f2 being ManySortedFunction of (it . j),(it . k) st
( f1 = F . j,i & f2 = F . k,j & F . k,i = f2 ** f1 & f1 is_homomorphism it . i,it . j );
existence
ex b1 being MSAlgebra-Family of the carrier of P,S ex F being ManySortedFunction of the InternalRel of P st
for i, j, k being Element of P st i >= j & j >= k holds
ex f1 being ManySortedFunction of (b1 . i),(b1 . j) ex f2 being ManySortedFunction of (b1 . j),(b1 . k) st
( f1 = F . j,i & f2 = F . k,j & F . k,i = f2 ** f1 & f1 is_homomorphism b1 . i,b1 . j )
proof end;
end;

:: deftheorem Def1 defines OrderedAlgFam MSALIMIT:def 1 :
for P being non empty Poset
for S being non empty non void ManySortedSign
for b3 being MSAlgebra-Family of the carrier of P,S holds
( b3 is OrderedAlgFam of P,S iff ex F being ManySortedFunction of the InternalRel of P st
for i, j, k being Element of P st i >= j & j >= k holds
ex f1 being ManySortedFunction of (b3 . i),(b3 . j) ex f2 being ManySortedFunction of (b3 . j),(b3 . k) st
( f1 = F . j,i & f2 = F . k,j & F . k,i = f2 ** f1 & f1 is_homomorphism b3 . i,b3 . j ) );

definition
let P be non empty Poset;
let S be non empty non void ManySortedSign ;
let OAF be OrderedAlgFam of P,S;
mode Binding of OAF -> ManySortedFunction of the InternalRel of P means :Def2: :: MSALIMIT:def 2
for i, j, k being Element of P st i >= j & j >= k holds
ex f1 being ManySortedFunction of (OAF . i),(OAF . j) ex f2 being ManySortedFunction of (OAF . j),(OAF . k) st
( f1 = it . j,i & f2 = it . k,j & it . k,i = f2 ** f1 & f1 is_homomorphism OAF . i,OAF . j );
existence
ex b1 being ManySortedFunction of the InternalRel of P st
for i, j, k being Element of P st i >= j & j >= k holds
ex f1 being ManySortedFunction of (OAF . i),(OAF . j) ex f2 being ManySortedFunction of (OAF . j),(OAF . k) st
( f1 = b1 . j,i & f2 = b1 . k,j & b1 . k,i = f2 ** f1 & f1 is_homomorphism OAF . i,OAF . j ) by Def1;
end;

:: deftheorem Def2 defines Binding MSALIMIT:def 2 :
for P being non empty Poset
for S being non empty non void ManySortedSign
for OAF being OrderedAlgFam of P,S
for b4 being ManySortedFunction of the InternalRel of P holds
( b4 is Binding of OAF iff for i, j, k being Element of P st i >= j & j >= k holds
ex f1 being ManySortedFunction of (OAF . i),(OAF . j) ex f2 being ManySortedFunction of (OAF . j),(OAF . k) st
( f1 = b4 . j,i & f2 = b4 . k,j & b4 . k,i = f2 ** f1 & f1 is_homomorphism OAF . i,OAF . j ) );

definition
let P be non empty Poset;
let S be non empty non void ManySortedSign ;
let OAF be OrderedAlgFam of P,S;
let B be Binding of OAF;
let i, j be Element of P;
assume A1: i >= j ;
func bind B,i,j -> ManySortedFunction of (OAF . i),(OAF . j) equals :Def3: :: MSALIMIT:def 3
B . j,i;
coherence
B . j,i is ManySortedFunction of (OAF . i),(OAF . j)
proof end;
end;

:: deftheorem Def3 defines bind MSALIMIT:def 3 :
for P being non empty Poset
for S being non empty non void ManySortedSign
for OAF being OrderedAlgFam of P,S
for B being Binding of OAF
for i, j being Element of P st i >= j holds
bind B,i,j = B . j,i;

theorem Th1: :: MSALIMIT:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P being non empty Poset
for i, j, k being Element of P
for S being non empty non void ManySortedSign
for OAF being OrderedAlgFam of P,S
for B being Binding of OAF st i >= j & j >= k holds
(bind B,j,k) ** (bind B,i,j) = bind B,i,k
proof end;

definition
let P be non empty Poset;
let S be non empty non void ManySortedSign ;
let OAF be OrderedAlgFam of P,S;
let IT be Binding of OAF;
attr IT is normalized means :Def4: :: MSALIMIT:def 4
for i being Element of P holds IT . i,i = id the Sorts of (OAF . i);
end;

:: deftheorem Def4 defines normalized MSALIMIT:def 4 :
for P being non empty Poset
for S being non empty non void ManySortedSign
for OAF being OrderedAlgFam of P,S
for IT being Binding of OAF holds
( IT is normalized iff for i being Element of P holds IT . i,i = id the Sorts of (OAF . i) );

theorem Th2: :: MSALIMIT:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P being non empty Poset
for S being non empty non void ManySortedSign
for OAF being OrderedAlgFam of P,S
for B being Binding of OAF
for i, j being Element of P st i >= j holds
for f being ManySortedFunction of (OAF . i),(OAF . j) st f = bind B,i,j holds
f is_homomorphism OAF . i,OAF . j
proof end;

definition
let P be non empty Poset;
let S be non empty non void ManySortedSign ;
let OAF be OrderedAlgFam of P,S;
let B be Binding of OAF;
func Normalized B -> Binding of OAF means :Def5: :: MSALIMIT:def 5
for i, j being Element of P st i >= j holds
it . j,i = IFEQ j,i,(id the Sorts of (OAF . i)),((bind B,i,j) ** (id the Sorts of (OAF . i)));
existence
ex b1 being Binding of OAF st
for i, j being Element of P st i >= j holds
b1 . j,i = IFEQ j,i,(id the Sorts of (OAF . i)),((bind B,i,j) ** (id the Sorts of (OAF . i)))
proof end;
uniqueness
for b1, b2 being Binding of OAF st ( for i, j being Element of P st i >= j holds
b1 . j,i = IFEQ j,i,(id the Sorts of (OAF . i)),((bind B,i,j) ** (id the Sorts of (OAF . i))) ) & ( for i, j being Element of P st i >= j holds
b2 . j,i = IFEQ j,i,(id the Sorts of (OAF . i)),((bind B,i,j) ** (id the Sorts of (OAF . i))) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def5 defines Normalized MSALIMIT:def 5 :
for P being non empty Poset
for S being non empty non void ManySortedSign
for OAF being OrderedAlgFam of P,S
for B, b5 being Binding of OAF holds
( b5 = Normalized B iff for i, j being Element of P st i >= j holds
b5 . j,i = IFEQ j,i,(id the Sorts of (OAF . i)),((bind B,i,j) ** (id the Sorts of (OAF . i))) );

theorem Th3: :: MSALIMIT:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P being non empty Poset
for S being non empty non void ManySortedSign
for OAF being OrderedAlgFam of P,S
for B being Binding of OAF
for i, j being Element of P st i >= j & i <> j holds
B . j,i = (Normalized B) . j,i
proof end;

registration
let P be non empty Poset;
let S be non empty non void ManySortedSign ;
let OAF be OrderedAlgFam of P,S;
let B be Binding of OAF;
cluster Normalized B -> normalized ;
coherence
Normalized B is normalized
proof end;
end;

registration
let P be non empty Poset;
let S be non empty non void ManySortedSign ;
let OAF be OrderedAlgFam of P,S;
cluster normalized Binding of OAF;
existence
ex b1 being Binding of OAF st b1 is normalized
proof end;
end;

theorem :: MSALIMIT:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P being non empty Poset
for S being non empty non void ManySortedSign
for OAF being OrderedAlgFam of P,S
for NB being normalized Binding of OAF
for i, j being Element of P st i >= j holds
(Normalized NB) . j,i = NB . j,i
proof end;

definition
let P be non empty Poset;
let S be non empty non void ManySortedSign ;
let OAF be OrderedAlgFam of P,S;
let B be Binding of OAF;
func InvLim B -> strict MSSubAlgebra of product OAF means :Def6: :: MSALIMIT:def 6
for s being SortSymbol of S
for f being Element of (SORTS OAF) . s holds
( f in the Sorts of it . s iff for i, j being Element of P st i >= j holds
((bind B,i,j) . s) . (f . i) = f . j );
existence
ex b1 being strict MSSubAlgebra of product OAF st
for s being SortSymbol of S
for f being Element of (SORTS OAF) . s holds
( f in the Sorts of b1 . s iff for i, j being Element of P st i >= j holds
((bind B,i,j) . s) . (f . i) = f . j )
proof end;
uniqueness
for b1, b2 being strict MSSubAlgebra of product OAF st ( for s being SortSymbol of S
for f being Element of (SORTS OAF) . s holds
( f in the Sorts of b1 . s iff for i, j being Element of P st i >= j holds
((bind B,i,j) . s) . (f . i) = f . j ) ) & ( for s being SortSymbol of S
for f being Element of (SORTS OAF) . s holds
( f in the Sorts of b2 . s iff for i, j being Element of P st i >= j holds
((bind B,i,j) . s) . (f . i) = f . j ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def6 defines InvLim MSALIMIT:def 6 :
for P being non empty Poset
for S being non empty non void ManySortedSign
for OAF being OrderedAlgFam of P,S
for B being Binding of OAF
for b5 being strict MSSubAlgebra of product OAF holds
( b5 = InvLim B iff for s being SortSymbol of S
for f being Element of (SORTS OAF) . s holds
( f in the Sorts of b5 . s iff for i, j being Element of P st i >= j holds
((bind B,i,j) . s) . (f . i) = f . j ) );

theorem :: MSALIMIT:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for DP being non empty discrete Poset
for S being non empty non void ManySortedSign
for OAF being OrderedAlgFam of DP,S
for B being normalized Binding of OAF holds InvLim B = product OAF
proof end;

definition
let X be set ;
attr X is MSS-membered means :Def7: :: MSALIMIT:def 7
for x being set st x in X holds
x is non empty strict non void ManySortedSign ;
end;

:: deftheorem Def7 defines MSS-membered MSALIMIT:def 7 :
for X being set holds
( X is MSS-membered iff for x being set st x in X holds
x is non empty strict non void ManySortedSign );

registration
cluster non empty MSS-membered set ;
existence
ex b1 being set st
( not b1 is empty & b1 is MSS-membered )
proof end;
end;

definition
func TrivialMSSign -> strict ManySortedSign means :Def8: :: MSALIMIT:def 8
( it is empty & it is void );
existence
ex b1 being strict ManySortedSign st
( b1 is empty & b1 is void )
proof end;
uniqueness
for b1, b2 being strict ManySortedSign st b1 is empty & b1 is void & b2 is empty & b2 is void holds
b1 = b2
proof end;
end;

:: deftheorem Def8 defines TrivialMSSign MSALIMIT:def 8 :
for b1 being strict ManySortedSign holds
( b1 = TrivialMSSign iff ( b1 is empty & b1 is void ) );

registration
cluster TrivialMSSign -> empty strict void ;
coherence
( TrivialMSSign is empty & TrivialMSSign is void ) by Def8;
end;

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

Lm1: for S being empty void ManySortedSign holds id the carrier of S, id the OperSymbols of S form_morphism_between S,S
proof end;

Lm2: for S being non empty void ManySortedSign holds id the carrier of S, id the OperSymbols of S form_morphism_between S,S
proof end;

theorem :: MSALIMIT:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being void ManySortedSign holds id the carrier of S, id the OperSymbols of S form_morphism_between S,S
proof end;

definition
let A be non empty set ;
func MSS_set A -> set means :Def9: :: MSALIMIT:def 9
for x being set holds
( x in it iff ex S being non empty strict non void ManySortedSign st
( x = S & the carrier of S c= A & the OperSymbols of S c= A ) );
existence
ex b1 being set st
for x being set holds
( x in b1 iff ex S being non empty strict non void ManySortedSign st
( x = S & the carrier of S c= A & the OperSymbols of S c= A ) )
proof end;
uniqueness
for b1, b2 being set st ( for x being set holds
( x in b1 iff ex S being non empty strict non void ManySortedSign st
( x = S & the carrier of S c= A & the OperSymbols of S c= A ) ) ) & ( for x being set holds
( x in b2 iff ex S being non empty strict non void ManySortedSign st
( x = S & the carrier of S c= A & the OperSymbols of S c= A ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def9 defines MSS_set MSALIMIT:def 9 :
for A being non empty set
for b2 being set holds
( b2 = MSS_set A iff for x being set holds
( x in b2 iff ex S being non empty strict non void ManySortedSign st
( x = S & the carrier of S c= A & the OperSymbols of S c= A ) ) );

registration
let A be non empty set ;
cluster MSS_set A -> non empty MSS-membered ;
coherence
( not MSS_set A is empty & MSS_set A is MSS-membered )
proof end;
end;

definition
let A be non empty MSS-membered set ;
:: original: Element
redefine mode Element of A -> non empty strict non void ManySortedSign ;
coherence
for b1 being Element of A holds b1 is non empty strict non void ManySortedSign by Def7;
end;

definition
let S1, S2 be ManySortedSign ;
func MSS_morph S1,S2 -> set means :: MSALIMIT:def 10
for x being set holds
( x in it iff ex f, g being Function st
( x = [f,g] & f,g form_morphism_between S1,S2 ) );
existence
ex b1 being set st
for x being set holds
( x in b1 iff ex f, g being Function st
( x = [f,g] & f,g form_morphism_between S1,S2 ) )
proof end;
uniqueness
for b1, b2 being set st ( for x being set holds
( x in b1 iff ex f, g being Function st
( x = [f,g] & f,g form_morphism_between S1,S2 ) ) ) & ( for x being set holds
( x in b2 iff ex f, g being Function st
( x = [f,g] & f,g form_morphism_between S1,S2 ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem defines MSS_morph MSALIMIT:def 10 :
for S1, S2 being ManySortedSign
for b3 being set holds
( b3 = MSS_morph S1,S2 iff for x being set holds
( x in b3 iff ex f, g being Function st
( x = [f,g] & f,g form_morphism_between S1,S2 ) ) );