begin
:: deftheorem Def1 defines Relation-yielding MSUALG_4:def 1 :
for IT being Function holds
( IT is Relation-yielding iff for x being set st x in dom IT holds
IT . x is Relation );
:: deftheorem Def2 defines ManySortedRelation MSUALG_4:def 2 :
for I being set
for A, B, b4 being ManySortedSet of I holds
( b4 is ManySortedRelation of A,B iff for i being set st i in I holds
b4 . i is Relation of (A . i),(B . i) );
:: deftheorem Def3 defines MSEquivalence_Relation-like MSUALG_4:def 3 :
for I being set
for A being ManySortedSet of I
for IT being ManySortedRelation of A holds
( IT is MSEquivalence_Relation-like iff for i being set
for R being Relation of (A . i) st i in I & IT . i = R holds
R is Equivalence_Relation of (A . i) );
:: deftheorem MSUALG_4:def 4 :
canceled;
:: deftheorem Def5 defines MSEquivalence-like MSUALG_4:def 5 :
for S being non empty ManySortedSign
for U1 being MSAlgebra of S
for IT being ManySortedRelation of U1 holds
( IT is MSEquivalence-like iff IT is MSEquivalence_Relation-like );
theorem Th1:
:: deftheorem Def6 defines MSCongruence-like MSUALG_4:def 6 :
for S being non empty non void ManySortedSign
for U1 being non-empty MSAlgebra of S
for R being MSEquivalence-like ManySortedRelation of U1 holds
( R is MSCongruence-like iff for o being OperSymbol of S
for x, y being Element of Args (o,U1) st ( for n being Nat st n in dom x holds
[(x . n),(y . n)] in R . ((the_arity_of o) /. n) ) holds
[((Den (o,U1)) . x),((Den (o,U1)) . y)] in R . (the_result_sort_of o) );
:: deftheorem defines Class MSUALG_4:def 7 :
for S being non empty non void ManySortedSign
for U1 being MSAlgebra of S
for R being MSEquivalence-like ManySortedRelation of U1
for i being Element of S
for x being Element of the Sorts of U1 . i holds Class (R,x) = Class ((R . i),x);
:: deftheorem Def8 defines Class MSUALG_4:def 8 :
for S being non empty non void ManySortedSign
for U1 being non-empty MSAlgebra of S
for R being MSCongruence of U1
for b4 being V8() ManySortedSet of the carrier of S holds
( b4 = Class R iff for s being Element of S holds b4 . s = Class (R . s) );
begin
:: deftheorem Def9 defines # MSUALG_4:def 9 :
for S being non empty non void ManySortedSign
for o being OperSymbol of S
for A being non-empty MSAlgebra of S
for R being MSCongruence of A
for x being Element of Args (o,A)
for b6 being Element of product ((Class R) * (the_arity_of o)) holds
( b6 = R # x iff for n being Nat st n in dom (the_arity_of o) holds
b6 . n = Class ((R . ((the_arity_of o) /. n)),(x . n)) );
definition
let S be non
empty non
void ManySortedSign ;
let o be
OperSymbol of
S;
let A be
non-empty MSAlgebra of
S;
let R be
MSCongruence of
A;
func QuotRes (
R,
o)
-> Function of
(( the Sorts of A * the ResultSort of S) . o),
(((Class R) * the ResultSort of S) . o) means :
Def10:
for
x being
Element of the
Sorts of
A . (the_result_sort_of o) holds
it . x = Class (
R,
x);
existence
ex b1 being Function of (( the Sorts of A * the ResultSort of S) . o),(((Class R) * the ResultSort of S) . o) st
for x being Element of the Sorts of A . (the_result_sort_of o) holds b1 . x = Class (R,x)
uniqueness
for b1, b2 being Function of (( the Sorts of A * the ResultSort of S) . o),(((Class R) * the ResultSort of S) . o) st ( for x being Element of the Sorts of A . (the_result_sort_of o) holds b1 . x = Class (R,x) ) & ( for x being Element of the Sorts of A . (the_result_sort_of o) holds b2 . x = Class (R,x) ) holds
b1 = b2
func QuotArgs (
R,
o)
-> Function of
((( the Sorts of A #) * the Arity of S) . o),
((((Class R) #) * the Arity of S) . o) means
for
x being
Element of
Args (
o,
A) holds
it . x = R # x;
existence
ex b1 being Function of ((( the Sorts of A #) * the Arity of S) . o),((((Class R) #) * the Arity of S) . o) st
for x being Element of Args (o,A) holds b1 . x = R # x
uniqueness
for b1, b2 being Function of ((( the Sorts of A #) * the Arity of S) . o),((((Class R) #) * the Arity of S) . o) st ( for x being Element of Args (o,A) holds b1 . x = R # x ) & ( for x being Element of Args (o,A) holds b2 . x = R # x ) holds
b1 = b2
end;
:: deftheorem Def10 defines QuotRes MSUALG_4:def 10 :
for S being non empty non void ManySortedSign
for o being OperSymbol of S
for A being non-empty MSAlgebra of S
for R being MSCongruence of A
for b5 being Function of (( the Sorts of A * the ResultSort of S) . o),(((Class R) * the ResultSort of S) . o) holds
( b5 = QuotRes (R,o) iff for x being Element of the Sorts of A . (the_result_sort_of o) holds b5 . x = Class (R,x) );
:: deftheorem defines QuotArgs MSUALG_4:def 11 :
for S being non empty non void ManySortedSign
for o being OperSymbol of S
for A being non-empty MSAlgebra of S
for R being MSCongruence of A
for b5 being Function of ((( the Sorts of A #) * the Arity of S) . o),((((Class R) #) * the Arity of S) . o) holds
( b5 = QuotArgs (R,o) iff for x being Element of Args (o,A) holds b5 . x = R # x );
definition
let S be non
empty non
void ManySortedSign ;
let A be
non-empty MSAlgebra of
S;
let R be
MSCongruence of
A;
func QuotRes R -> ManySortedFunction of the
Sorts of
A * the
ResultSort of
S,
(Class R) * the
ResultSort of
S means
for
o being
OperSymbol of
S holds
it . o = QuotRes (
R,
o);
existence
ex b1 being ManySortedFunction of the Sorts of A * the ResultSort of S,(Class R) * the ResultSort of S st
for o being OperSymbol of S holds b1 . o = QuotRes (R,o)
uniqueness
for b1, b2 being ManySortedFunction of the Sorts of A * the ResultSort of S,(Class R) * the ResultSort of S st ( for o being OperSymbol of S holds b1 . o = QuotRes (R,o) ) & ( for o being OperSymbol of S holds b2 . o = QuotRes (R,o) ) holds
b1 = b2
func QuotArgs R -> ManySortedFunction of
( the Sorts of A #) * the
Arity of
S,
((Class R) #) * the
Arity of
S means
for
o being
OperSymbol of
S holds
it . o = QuotArgs (
R,
o);
existence
ex b1 being ManySortedFunction of ( the Sorts of A #) * the Arity of S,((Class R) #) * the Arity of S st
for o being OperSymbol of S holds b1 . o = QuotArgs (R,o)
uniqueness
for b1, b2 being ManySortedFunction of ( the Sorts of A #) * the Arity of S,((Class R) #) * the Arity of S st ( for o being OperSymbol of S holds b1 . o = QuotArgs (R,o) ) & ( for o being OperSymbol of S holds b2 . o = QuotArgs (R,o) ) holds
b1 = b2
end;
:: deftheorem defines QuotRes MSUALG_4:def 12 :
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra of S
for R being MSCongruence of A
for b4 being ManySortedFunction of the Sorts of A * the ResultSort of S,(Class R) * the ResultSort of S holds
( b4 = QuotRes R iff for o being OperSymbol of S holds b4 . o = QuotRes (R,o) );
:: deftheorem defines QuotArgs MSUALG_4:def 13 :
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra of S
for R being MSCongruence of A
for b4 being ManySortedFunction of ( the Sorts of A #) * the Arity of S,((Class R) #) * the Arity of S holds
( b4 = QuotArgs R iff for o being OperSymbol of S holds b4 . o = QuotArgs (R,o) );
theorem Th2:
definition
let S be non
empty non
void ManySortedSign ;
let o be
OperSymbol of
S;
let A be
non-empty MSAlgebra of
S;
let R be
MSCongruence of
A;
func QuotCharact (
R,
o)
-> Function of
((((Class R) #) * the Arity of S) . o),
(((Class R) * the ResultSort of S) . o) means :
Def14:
for
a being
Element of
Args (
o,
A) st
R # a in (((Class R) #) * the Arity of S) . o holds
it . (R # a) = ((QuotRes (R,o)) * (Den (o,A))) . a;
existence
ex b1 being Function of ((((Class R) #) * the Arity of S) . o),(((Class R) * the ResultSort of S) . o) st
for a being Element of Args (o,A) st R # a in (((Class R) #) * the Arity of S) . o holds
b1 . (R # a) = ((QuotRes (R,o)) * (Den (o,A))) . a
uniqueness
for b1, b2 being Function of ((((Class R) #) * the Arity of S) . o),(((Class R) * the ResultSort of S) . o) st ( for a being Element of Args (o,A) st R # a in (((Class R) #) * the Arity of S) . o holds
b1 . (R # a) = ((QuotRes (R,o)) * (Den (o,A))) . a ) & ( for a being Element of Args (o,A) st R # a in (((Class R) #) * the Arity of S) . o holds
b2 . (R # a) = ((QuotRes (R,o)) * (Den (o,A))) . a ) holds
b1 = b2
end;
:: deftheorem Def14 defines QuotCharact MSUALG_4:def 14 :
for S being non empty non void ManySortedSign
for o being OperSymbol of S
for A being non-empty MSAlgebra of S
for R being MSCongruence of A
for b5 being Function of ((((Class R) #) * the Arity of S) . o),(((Class R) * the ResultSort of S) . o) holds
( b5 = QuotCharact (R,o) iff for a being Element of Args (o,A) st R # a in (((Class R) #) * the Arity of S) . o holds
b5 . (R # a) = ((QuotRes (R,o)) * (Den (o,A))) . a );
:: deftheorem Def15 defines QuotCharact MSUALG_4:def 15 :
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra of S
for R being MSCongruence of A
for b4 being ManySortedFunction of ((Class R) #) * the Arity of S,(Class R) * the ResultSort of S holds
( b4 = QuotCharact R iff for o being OperSymbol of S holds b4 . o = QuotCharact (R,o) );
:: deftheorem defines QuotMSAlg MSUALG_4:def 16 :
for S being non empty non void ManySortedSign
for U1 being non-empty MSAlgebra of S
for R being MSCongruence of U1 holds QuotMSAlg (U1,R) = MSAlgebra(# (Class R),(QuotCharact R) #);
definition
let S be non
empty non
void ManySortedSign ;
let U1 be
non-empty MSAlgebra of
S;
let R be
MSCongruence of
U1;
let s be
SortSymbol of
S;
func MSNat_Hom (
U1,
R,
s)
-> Function of
( the Sorts of U1 . s),
((Class R) . s) means :
Def17:
for
x being
set st
x in the
Sorts of
U1 . s holds
it . x = Class (
(R . s),
x);
existence
ex b1 being Function of ( the Sorts of U1 . s),((Class R) . s) st
for x being set st x in the Sorts of U1 . s holds
b1 . x = Class ((R . s),x)
uniqueness
for b1, b2 being Function of ( the Sorts of U1 . s),((Class R) . s) st ( for x being set st x in the Sorts of U1 . s holds
b1 . x = Class ((R . s),x) ) & ( for x being set st x in the Sorts of U1 . s holds
b2 . x = Class ((R . s),x) ) holds
b1 = b2
end;
:: deftheorem Def17 defines MSNat_Hom MSUALG_4:def 17 :
for S being non empty non void ManySortedSign
for U1 being non-empty MSAlgebra of S
for R being MSCongruence of U1
for s being SortSymbol of S
for b5 being Function of ( the Sorts of U1 . s),((Class R) . s) holds
( b5 = MSNat_Hom (U1,R,s) iff for x being set st x in the Sorts of U1 . s holds
b5 . x = Class ((R . s),x) );
definition
let S be non
empty non
void ManySortedSign ;
let U1 be
non-empty MSAlgebra of
S;
let R be
MSCongruence of
U1;
func MSNat_Hom (
U1,
R)
-> ManySortedFunction of
U1,
(QuotMSAlg (U1,R)) means :
Def18:
for
s being
SortSymbol of
S holds
it . s = MSNat_Hom (
U1,
R,
s);
existence
ex b1 being ManySortedFunction of U1,(QuotMSAlg (U1,R)) st
for s being SortSymbol of S holds b1 . s = MSNat_Hom (U1,R,s)
uniqueness
for b1, b2 being ManySortedFunction of U1,(QuotMSAlg (U1,R)) st ( for s being SortSymbol of S holds b1 . s = MSNat_Hom (U1,R,s) ) & ( for s being SortSymbol of S holds b2 . s = MSNat_Hom (U1,R,s) ) holds
b1 = b2
end;
:: deftheorem Def18 defines MSNat_Hom MSUALG_4:def 18 :
for S being non empty non void ManySortedSign
for U1 being non-empty MSAlgebra of S
for R being MSCongruence of U1
for b4 being ManySortedFunction of U1,(QuotMSAlg (U1,R)) holds
( b4 = MSNat_Hom (U1,R) iff for s being SortSymbol of S holds b4 . s = MSNat_Hom (U1,R,s) );
theorem
definition
let S be non
empty non
void ManySortedSign ;
let U1,
U2 be
non-empty MSAlgebra of
S;
let F be
ManySortedFunction of
U1,
U2;
let s be
SortSymbol of
S;
func MSCng (
F,
s)
-> Equivalence_Relation of
( the Sorts of U1 . s) means :
Def19:
for
x,
y being
Element of the
Sorts of
U1 . s holds
(
[x,y] in it iff
(F . s) . x = (F . s) . y );
existence
ex b1 being Equivalence_Relation of ( the Sorts of U1 . s) st
for x, y being Element of the Sorts of U1 . s holds
( [x,y] in b1 iff (F . s) . x = (F . s) . y )
uniqueness
for b1, b2 being Equivalence_Relation of ( the Sorts of U1 . s) st ( for x, y being Element of the Sorts of U1 . s holds
( [x,y] in b1 iff (F . s) . x = (F . s) . y ) ) & ( for x, y being Element of the Sorts of U1 . s holds
( [x,y] in b2 iff (F . s) . x = (F . s) . y ) ) holds
b1 = b2
end;
:: deftheorem Def19 defines MSCng MSUALG_4:def 19 :
for S being non empty non void ManySortedSign
for U1, U2 being non-empty MSAlgebra of S
for F being ManySortedFunction of U1,U2
for s being SortSymbol of S
for b6 being Equivalence_Relation of ( the Sorts of U1 . s) holds
( b6 = MSCng (F,s) iff for x, y being Element of the Sorts of U1 . s holds
( [x,y] in b6 iff (F . s) . x = (F . s) . y ) );
:: deftheorem Def20 defines MSCng MSUALG_4:def 20 :
for S being non empty non void ManySortedSign
for U1, U2 being non-empty MSAlgebra of S
for F being ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 holds
for b5 being MSCongruence of U1 holds
( b5 = MSCng F iff for s being SortSymbol of S holds b5 . s = MSCng (F,s) );
definition
let S be non
empty non
void ManySortedSign ;
let U1,
U2 be
non-empty MSAlgebra of
S;
let F be
ManySortedFunction of
U1,
U2;
let s be
SortSymbol of
S;
assume A1:
F is_homomorphism U1,
U2
;
func MSHomQuot (
F,
s)
-> Function of
( the Sorts of (QuotMSAlg (U1,(MSCng F))) . s),
( the Sorts of U2 . s) means :
Def21:
for
x being
Element of the
Sorts of
U1 . s holds
it . (Class ((MSCng (F,s)),x)) = (F . s) . x;
existence
ex b1 being Function of ( the Sorts of (QuotMSAlg (U1,(MSCng F))) . s),( the Sorts of U2 . s) st
for x being Element of the Sorts of U1 . s holds b1 . (Class ((MSCng (F,s)),x)) = (F . s) . x
uniqueness
for b1, b2 being Function of ( the Sorts of (QuotMSAlg (U1,(MSCng F))) . s),( the Sorts of U2 . s) st ( for x being Element of the Sorts of U1 . s holds b1 . (Class ((MSCng (F,s)),x)) = (F . s) . x ) & ( for x being Element of the Sorts of U1 . s holds b2 . (Class ((MSCng (F,s)),x)) = (F . s) . x ) holds
b1 = b2
end;
:: deftheorem Def21 defines MSHomQuot MSUALG_4:def 21 :
for S being non empty non void ManySortedSign
for U1, U2 being non-empty MSAlgebra of S
for F being ManySortedFunction of U1,U2
for s being SortSymbol of S st F is_homomorphism U1,U2 holds
for b6 being Function of ( the Sorts of (QuotMSAlg (U1,(MSCng F))) . s),( the Sorts of U2 . s) holds
( b6 = MSHomQuot (F,s) iff for x being Element of the Sorts of U1 . s holds b6 . (Class ((MSCng (F,s)),x)) = (F . s) . x );
definition
let S be non
empty non
void ManySortedSign ;
let U1,
U2 be
non-empty MSAlgebra of
S;
let F be
ManySortedFunction of
U1,
U2;
func MSHomQuot F -> ManySortedFunction of
(QuotMSAlg (U1,(MSCng F))),
U2 means :
Def22:
for
s being
SortSymbol of
S holds
it . s = MSHomQuot (
F,
s);
existence
ex b1 being ManySortedFunction of (QuotMSAlg (U1,(MSCng F))),U2 st
for s being SortSymbol of S holds b1 . s = MSHomQuot (F,s)
uniqueness
for b1, b2 being ManySortedFunction of (QuotMSAlg (U1,(MSCng F))),U2 st ( for s being SortSymbol of S holds b1 . s = MSHomQuot (F,s) ) & ( for s being SortSymbol of S holds b2 . s = MSHomQuot (F,s) ) holds
b1 = b2
end;
:: deftheorem Def22 defines MSHomQuot MSUALG_4:def 22 :
for S being non empty non void ManySortedSign
for U1, U2 being non-empty MSAlgebra of S
for F being ManySortedFunction of U1,U2
for b5 being ManySortedFunction of (QuotMSAlg (U1,(MSCng F))),U2 holds
( b5 = MSHomQuot F iff for s being SortSymbol of S holds b5 . s = MSHomQuot (F,s) );
theorem Th4:
theorem Th5:
theorem