begin
theorem Th9:
for
S being non
empty non
void ManySortedSign for
o being
OperSymbol of
S for
i being
Element of
NAT st
i in dom (the_arity_of o) holds
for
A1,
A2 being
MSAlgebra over
S for
h being
ManySortedFunction of
A1,
A2 for
a,
b being
Element of
Args (
o,
A1) st
a in Args (
o,
A1) &
h # a in Args (
o,
A2) holds
for
f,
g1,
g2 being
Function st
f = a &
g1 = h # a &
g2 = h # b holds
for
x being
Element of
A1,
((the_arity_of o) /. i) st
b = f +* (
i,
x) holds
(
g2 . i = (h . ((the_arity_of o) /. i)) . x &
h # b = g1 +* (
i,
(g2 . i)) )
theorem Th18:
for
S being non
empty non
void ManySortedSign for
A being
non-empty MSAlgebra over
S for
s1,
s2,
s3 being
SortSymbol of
S st
TranslationRel S reduces s1,
s2 &
TranslationRel S reduces s2,
s3 holds
for
t1 being
Translation of
A,
s1,
s2 for
t2 being
Translation of
A,
s2,
s3 holds
t2 * t1 is
Translation of
A,
s1,
s3
scheme
TranslationInd{
F1()
-> non
empty non
void ManySortedSign ,
F2()
-> non-empty MSAlgebra over
F1(),
P1[
set ,
set ,
set ] } :
provided
A1:
for
s being
SortSymbol of
F1() holds
P1[
id ( the Sorts of F2() . s),
s,
s]
and A2:
for
s1,
s2,
s3 being
SortSymbol of
F1() st
TranslationRel F1()
reduces s1,
s2 holds
for
t being
Translation of
F2(),
s1,
s2 st
P1[
t,
s1,
s2] holds
for
f being
Function st
f is_e.translation_of F2(),
s2,
s3 holds
P1[
f * t,
s1,
s3]
theorem Th21:
for
S being non
empty non
void ManySortedSign for
A1,
A2 being
non-empty MSAlgebra over
S for
h being
ManySortedFunction of
A1,
A2 st
h is_homomorphism A1,
A2 holds
for
o being
OperSymbol of
S for
i being
Element of
NAT st
i in dom (the_arity_of o) holds
for
a being
Element of
Args (
o,
A1) holds
(h . (the_result_sort_of o)) * (transl (o,i,a,A1)) = (transl (o,i,(h # a),A2)) * (h . ((the_arity_of o) /. i))
begin
begin
scheme
MSRelCl{
F1()
-> non
empty non
void ManySortedSign ,
F2()
-> non-empty MSAlgebra over
F1(),
P1[
set ,
set ,
set ],
P2[
set ],
F3()
-> ManySortedRelation of
F2(),
F4()
-> ManySortedRelation of
F2() } :
provided
A1:
for
R being
ManySortedRelation of
F2() holds
(
P2[
R] iff for
s1,
s2 being
SortSymbol of
F1()
for
f being
Function of
( the Sorts of F2() . s1),
( the Sorts of F2() . s2) st
P1[
f,
s1,
s2] holds
for
a,
b being
set st
[a,b] in R . s1 holds
[(f . a),(f . b)] in R . s2 )
and A2:
for
s1,
s2,
s3 being
SortSymbol of
F1()
for
f1 being
Function of
( the Sorts of F2() . s1),
( the Sorts of F2() . s2) for
f2 being
Function of
( the Sorts of F2() . s2),
( the Sorts of F2() . s3) st
P1[
f1,
s1,
s2] &
P1[
f2,
s2,
s3] holds
P1[
f2 * f1,
s1,
s3]
and A3:
for
s being
SortSymbol of
F1() holds
P1[
id ( the Sorts of F2() . s),
s,
s]
and A4:
for
s being
SortSymbol of
F1()
for
a,
b being
Element of
F2(),
s holds
(
[a,b] in F4()
. s iff ex
s9 being
SortSymbol of
F1() ex
f being
Function of
( the Sorts of F2() . s9),
( the Sorts of F2() . s) ex
x,
y being
Element of
F2(),
s9 st
(
P1[
f,
s9,
s] &
[x,y] in F3()
. s9 &
a = f . x &
b = f . y ) )
Lm1:
now for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for R, Q being ManySortedRelation of A st ( for s being SortSymbol of S
for a, b being Element of A,s holds
( [a,b] in Q . s iff ex s9 being SortSymbol of S ex f being Function of ( the Sorts of A . s9),( the Sorts of A . s) ex x, y being Element of A,s9 st
( S2[f,s9,s] & [x,y] in R . s9 & a = f . x & b = f . y ) ) ) holds
( S1[Q] & R c= Q & ( for P being ManySortedRelation of A st S1[P] & R c= P holds
Q c= P ) )
let S be non
empty non
void ManySortedSign ;
for A being non-empty MSAlgebra over S
for R, Q being ManySortedRelation of A st ( for s being SortSymbol of S
for a, b being Element of A,s holds
( [a,b] in Q . s iff ex s9 being SortSymbol of S ex f being Function of ( the Sorts of A . s9),( the Sorts of A . s) ex x, y being Element of A,s9 st
( S2[f,s9,s] & [x,y] in R . s9 & a = f . x & b = f . y ) ) ) holds
( S1[Q] & R c= Q & ( for P being ManySortedRelation of A st S1[P] & R c= P holds
Q c= P ) )let A be
non-empty MSAlgebra over
S;
for R, Q being ManySortedRelation of A st ( for s being SortSymbol of S
for a, b being Element of A,s holds
( [a,b] in Q . s iff ex s9 being SortSymbol of S ex f being Function of ( the Sorts of A . s9),( the Sorts of A . s) ex x, y being Element of A,s9 st
( S2[f,s9,s] & [x,y] in R . s9 & a = f . x & b = f . y ) ) ) holds
( S1[Q] & R c= Q & ( for P being ManySortedRelation of A st S1[P] & R c= P holds
Q c= P ) )let R,
Q be
ManySortedRelation of
A;
( ( for s being SortSymbol of S
for a, b being Element of A,s holds
( [a,b] in Q . s iff ex s9 being SortSymbol of S ex f being Function of ( the Sorts of A . s9),( the Sorts of A . s) ex x, y being Element of A,s9 st
( S2[f,s9,s] & [x,y] in R . s9 & a = f . x & b = f . y ) ) ) implies ( S1[Q] & R c= Q & ( for P being ManySortedRelation of A st S1[P] & R c= P holds
Q c= P ) ) )defpred S1[
ManySortedRelation of
A]
means $1 is
invariant ;
defpred S2[
Function,
SortSymbol of
S,
SortSymbol of
S]
means (
TranslationRel S reduces $2,$3 & $1 is
Translation of
A,$2,$3 );
assume A1:
for
s being
SortSymbol of
S for
a,
b being
Element of
A,
s holds
(
[a,b] in Q . s iff ex
s9 being
SortSymbol of
S ex
f being
Function of
( the Sorts of A . s9),
( the Sorts of A . s) ex
x,
y being
Element of
A,
s9 st
(
S2[
f,
s9,
s] &
[x,y] in R . s9 &
a = f . x &
b = f . y ) )
;
( S1[Q] & R c= Q & ( for P being ManySortedRelation of A st S1[P] & R c= P holds
Q c= P ) )A2:
for
s being
SortSymbol of
S holds
S2[
id ( the Sorts of A . s),
s,
s]
by Th16, REWRITE1:12;
A3:
now for R being ManySortedRelation of A holds
( ( S1[R] implies for s1, s2 being SortSymbol of S
for f being Function of ( the Sorts of A . s1),( the Sorts of A . s2) st S2[f,s1,s2] holds
for a, b being set st [a,b] in R . s1 holds
[(f . a),(f . b)] in R . s2 ) & ( ( for s1, s2 being SortSymbol of S
for f being Function of ( the Sorts of A . s1),( the Sorts of A . s2) st S2[f,s1,s2] holds
for a, b being set st [a,b] in R . s1 holds
[(f . a),(f . b)] in R . s2 ) implies S1[R] ) )
let R be
ManySortedRelation of
A;
( ( S1[R] implies for s1, s2 being SortSymbol of S
for f being Function of ( the Sorts of A . s1),( the Sorts of A . s2) st S2[f,s1,s2] holds
for a, b being set st [a,b] in R . s1 holds
[(f . a),(f . b)] in R . s2 ) & ( ( for s1, s2 being SortSymbol of S
for f being Function of ( the Sorts of A . s1),( the Sorts of A . s2) st S2[f,s1,s2] holds
for a, b being set st [a,b] in R . s1 holds
[(f . a),(f . b)] in R . s2 ) implies S1[R] ) )thus
(
S1[
R] implies for
s1,
s2 being
SortSymbol of
S for
f being
Function of
( the Sorts of A . s1),
( the Sorts of A . s2) st
S2[
f,
s1,
s2] holds
for
a,
b being
set st
[a,b] in R . s1 holds
[(f . a),(f . b)] in R . s2 )
by Th28;
( ( for s1, s2 being SortSymbol of S
for f being Function of ( the Sorts of A . s1),( the Sorts of A . s2) st S2[f,s1,s2] holds
for a, b being set st [a,b] in R . s1 holds
[(f . a),(f . b)] in R . s2 ) implies S1[R] )assume
for
s1,
s2 being
SortSymbol of
S for
f being
Function of
( the Sorts of A . s1),
( the Sorts of A . s2) st
S2[
f,
s1,
s2] holds
for
a,
b being
set st
[a,b] in R . s1 holds
[(f . a),(f . b)] in R . s2
;
S1[R]then
for
s1,
s2 being
SortSymbol of
S st
TranslationRel S reduces s1,
s2 holds
for
f being
Translation of
A,
s1,
s2 for
a,
b being
set st
[a,b] in R . s1 holds
[(f . a),(f . b)] in R . s2
;
hence
S1[
R]
by Th28;
verum
end;
A4:
for
s1,
s2,
s3 being
SortSymbol of
S for
f1 being
Function of
( the Sorts of A . s1),
( the Sorts of A . s2) for
f2 being
Function of
( the Sorts of A . s2),
( the Sorts of A . s3) st
S2[
f1,
s1,
s2] &
S2[
f2,
s2,
s3] holds
S2[
f2 * f1,
s1,
s3]
by Th18, REWRITE1:16;
thus
(
S1[
Q] &
R c= Q & ( for
P being
ManySortedRelation of
A st
S1[
P] &
R c= P holds
Q c= P ) )
from MSUALG_6:sch 4(A3, A4, A2, A1); verum
end;
Lm2:
now for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for R, Q being ManySortedRelation of A st ( for s being SortSymbol of S
for a, b being Element of A,s holds
( [a,b] in Q . s iff ex s9 being SortSymbol of S ex f being Function of ( the Sorts of A . s9),( the Sorts of A . s) ex x, y being Element of A,s9 st
( S2[f,s9,s] & [x,y] in R . s9 & a = f . x & b = f . y ) ) ) holds
( S1[Q] & R c= Q & ( for P being ManySortedRelation of A st S1[P] & R c= P holds
Q c= P ) )
let S be non
empty non
void ManySortedSign ;
for A being non-empty MSAlgebra over S
for R, Q being ManySortedRelation of A st ( for s being SortSymbol of S
for a, b being Element of A,s holds
( [a,b] in Q . s iff ex s9 being SortSymbol of S ex f being Function of ( the Sorts of A . s9),( the Sorts of A . s) ex x, y being Element of A,s9 st
( S2[f,s9,s] & [x,y] in R . s9 & a = f . x & b = f . y ) ) ) holds
( S1[Q] & R c= Q & ( for P being ManySortedRelation of A st S1[P] & R c= P holds
Q c= P ) )let A be
non-empty MSAlgebra over
S;
for R, Q being ManySortedRelation of A st ( for s being SortSymbol of S
for a, b being Element of A,s holds
( [a,b] in Q . s iff ex s9 being SortSymbol of S ex f being Function of ( the Sorts of A . s9),( the Sorts of A . s) ex x, y being Element of A,s9 st
( S2[f,s9,s] & [x,y] in R . s9 & a = f . x & b = f . y ) ) ) holds
( S1[Q] & R c= Q & ( for P being ManySortedRelation of A st S1[P] & R c= P holds
Q c= P ) )let R,
Q be
ManySortedRelation of
A;
( ( for s being SortSymbol of S
for a, b being Element of A,s holds
( [a,b] in Q . s iff ex s9 being SortSymbol of S ex f being Function of ( the Sorts of A . s9),( the Sorts of A . s) ex x, y being Element of A,s9 st
( S2[f,s9,s] & [x,y] in R . s9 & a = f . x & b = f . y ) ) ) implies ( S1[Q] & R c= Q & ( for P being ManySortedRelation of A st S1[P] & R c= P holds
Q c= P ) ) )defpred S1[
ManySortedRelation of
A]
means $1 is
stable ;
defpred S2[
Function,
SortSymbol of
S,
SortSymbol of
S]
means ( $2
= $3 & ex
h being
Endomorphism of
A st $1
= h . $2 );
A1:
for
s1,
s2,
s3 being
SortSymbol of
S for
f1 being
Function of
( the Sorts of A . s1),
( the Sorts of A . s2) for
f2 being
Function of
( the Sorts of A . s2),
( the Sorts of A . s3) st
S2[
f1,
s1,
s2] &
S2[
f2,
s2,
s3] holds
S2[
f2 * f1,
s1,
s3]
proof
let s1,
s2,
s3 be
SortSymbol of
S;
for f1 being Function of ( the Sorts of A . s1),( the Sorts of A . s2)
for f2 being Function of ( the Sorts of A . s2),( the Sorts of A . s3) st S2[f1,s1,s2] & S2[f2,s2,s3] holds
S2[f2 * f1,s1,s3]let f1 be
Function of
( the Sorts of A . s1),
( the Sorts of A . s2);
for f2 being Function of ( the Sorts of A . s2),( the Sorts of A . s3) st S2[f1,s1,s2] & S2[f2,s2,s3] holds
S2[f2 * f1,s1,s3]let f2 be
Function of
( the Sorts of A . s2),
( the Sorts of A . s3);
( S2[f1,s1,s2] & S2[f2,s2,s3] implies S2[f2 * f1,s1,s3] )
assume A2:
s1 = s2
;
( for h being Endomorphism of A holds not f1 = h . s1 or not S2[f2,s2,s3] or S2[f2 * f1,s1,s3] )
given h1 being
Endomorphism of
A such that A3:
f1 = h1 . s1
;
( not S2[f2,s2,s3] or S2[f2 * f1,s1,s3] )
assume A4:
s2 = s3
;
( for h being Endomorphism of A holds not f2 = h . s2 or S2[f2 * f1,s1,s3] )
given h2 being
Endomorphism of
A such that A5:
f2 = h2 . s2
;
S2[f2 * f1,s1,s3]
thus
s1 = s3
by A2, A4;
ex h being Endomorphism of A st f2 * f1 = h . s1
reconsider h =
h2 ** h1 as
Endomorphism of
A ;
take
h
;
f2 * f1 = h . s1
thus
f2 * f1 = h . s1
by A2, A3, A5, MSUALG_3:2;
verum
end;
A6:
for
R being
ManySortedRelation of
A holds
(
S1[
R] iff for
s1,
s2 being
SortSymbol of
S for
f being
Function of
( the Sorts of A . s1),
( the Sorts of A . s2) st
S2[
f,
s1,
s2] holds
for
a,
b being
set st
[a,b] in R . s1 holds
[(f . a),(f . b)] in R . s2 )
proof
let R be
ManySortedRelation of
A;
( S1[R] iff for s1, s2 being SortSymbol of S
for f being Function of ( the Sorts of A . s1),( the Sorts of A . s2) st S2[f,s1,s2] holds
for a, b being set st [a,b] in R . s1 holds
[(f . a),(f . b)] in R . s2 )
thus
(
R is
stable implies for
s1,
s2 being
SortSymbol of
S for
f being
Function of
( the Sorts of A . s1),
( the Sorts of A . s2) st
s1 = s2 & ex
h being
Endomorphism of
A st
f = h . s1 holds
for
a,
b being
set st
[a,b] in R . s1 holds
[(f . a),(f . b)] in R . s2 )
by Def9;
( ( for s1, s2 being SortSymbol of S
for f being Function of ( the Sorts of A . s1),( the Sorts of A . s2) st S2[f,s1,s2] holds
for a, b being set st [a,b] in R . s1 holds
[(f . a),(f . b)] in R . s2 ) implies S1[R] )
assume A7:
for
s1,
s2 being
SortSymbol of
S for
f being
Function of
( the Sorts of A . s1),
( the Sorts of A . s2) st
S2[
f,
s1,
s2] holds
for
a,
b being
set st
[a,b] in R . s1 holds
[(f . a),(f . b)] in R . s2
;
S1[R]
thus
R is
stable
verum
end;
A8:
for
s being
SortSymbol of
S holds
S2[
id ( the Sorts of A . s),
s,
s]
assume A9:
for
s being
SortSymbol of
S for
a,
b being
Element of
A,
s holds
(
[a,b] in Q . s iff ex
s9 being
SortSymbol of
S ex
f being
Function of
( the Sorts of A . s9),
( the Sorts of A . s) ex
x,
y being
Element of
A,
s9 st
(
S2[
f,
s9,
s] &
[x,y] in R . s9 &
a = f . x &
b = f . y ) )
;
( S1[Q] & R c= Q & ( for P being ManySortedRelation of A st S1[P] & R c= P holds
Q c= P ) )thus
(
S1[
Q] &
R c= Q & ( for
P being
ManySortedRelation of
A st
S1[
P] &
R c= P holds
Q c= P ) )
from MSUALG_6:sch 4(A6, A1, A8, A9); verum
end;
begin