begin
theorem Th1:
theorem Th2:
:: deftheorem Def1 defines feasible MSUALG_6:def 1 :
for S being non empty non void ManySortedSign
for A being MSAlgebra of S holds
( A is feasible iff for o being OperSymbol of S st Args (o,A) <> {} holds
Result (o,A) <> {} );
theorem Th3:
:: deftheorem Def2 defines Endomorphism MSUALG_6:def 2 :
for S being non empty non void ManySortedSign
for A being MSAlgebra of S
for b3 being ManySortedFunction of A,A holds
( b3 is Endomorphism of A iff b3 is_homomorphism A,A );
theorem Th4:
theorem Th5:
theorem Th6:
:: deftheorem Def3 defines TranslationRel MSUALG_6:def 3 :
for S being non empty non void ManySortedSign
for b2 being Relation of the carrier of S holds
( b2 = TranslationRel S iff for s1, s2 being SortSymbol of S holds
( [s1,s2] in b2 iff ex o being OperSymbol of S st
( the_result_sort_of o = s2 & ex i being Element of NAT st
( i in dom (the_arity_of o) & (the_arity_of o) /. i = s1 ) ) ) );
theorem Th7:
theorem Th8:
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 of
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)) )
definition
let S be non
empty non
void ManySortedSign ;
let o be
OperSymbol of
S;
let i be
Element of
NAT ;
let A be
MSAlgebra of
S;
let a be
Function;
func transl (
o,
i,
a,
A)
-> Function means :
Def4:
(
dom it = the
Sorts of
A . ((the_arity_of o) /. i) & ( for
x being
set st
x in the
Sorts of
A . ((the_arity_of o) /. i) holds
it . x = (Den (o,A)) . (a +* (i,x)) ) );
existence
ex b1 being Function st
( dom b1 = the Sorts of A . ((the_arity_of o) /. i) & ( for x being set st x in the Sorts of A . ((the_arity_of o) /. i) holds
b1 . x = (Den (o,A)) . (a +* (i,x)) ) )
uniqueness
for b1, b2 being Function st dom b1 = the Sorts of A . ((the_arity_of o) /. i) & ( for x being set st x in the Sorts of A . ((the_arity_of o) /. i) holds
b1 . x = (Den (o,A)) . (a +* (i,x)) ) & dom b2 = the Sorts of A . ((the_arity_of o) /. i) & ( for x being set st x in the Sorts of A . ((the_arity_of o) /. i) holds
b2 . x = (Den (o,A)) . (a +* (i,x)) ) holds
b1 = b2
end;
:: deftheorem Def4 defines transl MSUALG_6:def 4 :
for S being non empty non void ManySortedSign
for o being OperSymbol of S
for i being Element of NAT
for A being MSAlgebra of S
for a, b6 being Function holds
( b6 = transl (o,i,a,A) iff ( dom b6 = the Sorts of A . ((the_arity_of o) /. i) & ( for x being set st x in the Sorts of A . ((the_arity_of o) /. i) holds
b6 . x = (Den (o,A)) . (a +* (i,x)) ) ) );
theorem Th10:
:: deftheorem Def5 defines is_e.translation_of MSUALG_6:def 5 :
for S being non empty non void ManySortedSign
for s1, s2 being SortSymbol of S
for A being MSAlgebra of S
for f being Function holds
( f is_e.translation_of A,s1,s2 iff ex o being OperSymbol of S st
( the_result_sort_of o = s2 & ex i being Element of NAT st
( i in dom (the_arity_of o) & (the_arity_of o) /. i = s1 & ex a being Function st
( a in Args (o,A) & f = transl (o,i,a,A) ) ) ) );
theorem Th11:
theorem Th12:
theorem
theorem Th14:
definition
let S be non
empty non
void ManySortedSign ;
let A be
non-empty MSAlgebra of
S;
let s1,
s2 be
SortSymbol of
S;
assume A1:
TranslationRel S reduces s1,
s2
;
mode Translation of
A,
s1,
s2 -> Function of
( the Sorts of A . s1),
( the Sorts of A . s2) means :
Def6:
ex
q being
RedSequence of
TranslationRel S ex
p being
Function-yielding FinSequence st
(
it = compose (
p,
( the Sorts of A . s1)) &
len q = (len p) + 1 &
s1 = q . 1 &
s2 = q . (len q) & ( for
i being
Element of
NAT for
f being
Function for
s1,
s2 being
SortSymbol of
S st
i in dom p &
f = p . i &
s1 = q . i &
s2 = q . (i + 1) holds
f is_e.translation_of A,
s1,
s2 ) );
existence
ex b1 being Function of ( the Sorts of A . s1),( the Sorts of A . s2) ex q being RedSequence of TranslationRel S ex p being Function-yielding FinSequence st
( b1 = compose (p,( the Sorts of A . s1)) & len q = (len p) + 1 & s1 = q . 1 & s2 = q . (len q) & ( for i being Element of NAT
for f being Function
for s1, s2 being SortSymbol of S st i in dom p & f = p . i & s1 = q . i & s2 = q . (i + 1) holds
f is_e.translation_of A,s1,s2 ) )
end;
:: deftheorem Def6 defines Translation MSUALG_6:def 6 :
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra of S
for s1, s2 being SortSymbol of S st TranslationRel S reduces s1,s2 holds
for b5 being Function of ( the Sorts of A . s1),( the Sorts of A . s2) holds
( b5 is Translation of A,s1,s2 iff ex q being RedSequence of TranslationRel S ex p being Function-yielding FinSequence st
( b5 = compose (p,( the Sorts of A . s1)) & len q = (len p) + 1 & s1 = q . 1 & s2 = q . (len q) & ( for i being Element of NAT
for f being Function
for s1, s2 being SortSymbol of S st i in dom p & f = p . i & s1 = q . i & s2 = q . (i + 1) holds
f is_e.translation_of A,s1,s2 ) ) );
theorem
theorem Th16:
theorem Th17:
theorem Th18:
for
S being non
empty non
void ManySortedSign for
A being
non-empty MSAlgebra of
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
theorem Th19:
theorem
scheme
TranslationInd{
F1()
-> non
empty non
void ManySortedSign ,
F2()
-> non-empty MSAlgebra of
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 of
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))
theorem
theorem Th23:
theorem
theorem Th25:
theorem Th26:
begin
definition
let S be non
empty non
void ManySortedSign ;
let A be
MSAlgebra of
S;
let R be
ManySortedRelation of
A;
attr R is
compatible means :
Def7:
for
o being
OperSymbol of
S for
a,
b being
Function st
a in Args (
o,
A) &
b in Args (
o,
A) & ( for
n being
Element of
NAT st
n in dom (the_arity_of o) holds
[(a . n),(b . n)] in R . ((the_arity_of o) /. n) ) holds
[((Den (o,A)) . a),((Den (o,A)) . b)] in R . (the_result_sort_of o);
attr R is
invariant means :
Def8:
for
s1,
s2 being
SortSymbol of
S for
t being
Function st
t is_e.translation_of A,
s1,
s2 holds
for
a,
b being
set st
[a,b] in R . s1 holds
[(t . a),(t . b)] in R . s2;
attr R is
stable means :
Def9:
for
h being
Endomorphism of
A for
s being
SortSymbol of
S for
a,
b being
set st
[a,b] in R . s holds
[((h . s) . a),((h . s) . b)] in R . s;
end;
:: deftheorem Def7 defines compatible MSUALG_6:def 7 :
for S being non empty non void ManySortedSign
for A being MSAlgebra of S
for R being ManySortedRelation of A holds
( R is compatible iff for o being OperSymbol of S
for a, b being Function st a in Args (o,A) & b in Args (o,A) & ( for n being Element of NAT st n in dom (the_arity_of o) holds
[(a . n),(b . n)] in R . ((the_arity_of o) /. n) ) holds
[((Den (o,A)) . a),((Den (o,A)) . b)] in R . (the_result_sort_of o) );
:: deftheorem Def8 defines invariant MSUALG_6:def 8 :
for S being non empty non void ManySortedSign
for A being MSAlgebra of S
for R being ManySortedRelation of A holds
( R is invariant iff for s1, s2 being SortSymbol of S
for t being Function st t is_e.translation_of A,s1,s2 holds
for a, b being set st [a,b] in R . s1 holds
[(t . a),(t . b)] in R . s2 );
:: deftheorem Def9 defines stable MSUALG_6:def 9 :
for S being non empty non void ManySortedSign
for A being MSAlgebra of S
for R being ManySortedRelation of A holds
( R is stable iff for h being Endomorphism of A
for s being SortSymbol of S
for a, b being set st [a,b] in R . s holds
[((h . s) . a),((h . s) . b)] in R . s );
theorem
theorem Th28:
:: deftheorem Def10 defines id MSUALG_6:def 10 :
for I being set
for A being ManySortedSet of I
for b3 being ManySortedRelation of A holds
( b3 = id (I,A) iff for i being set st i in I holds
b3 . i = id (A . i) );
begin
scheme
MSRelCl{
F1()
-> non
empty non
void ManySortedSign ,
F2()
-> non-empty MSAlgebra of
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
let S be non
empty non
void ManySortedSign ;
for A being non-empty MSAlgebra of 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 of
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:13;
A3:
now
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:17;
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;
:: deftheorem Def11 defines InvCl MSUALG_6:def 11 :
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra of S
for R being ManySortedRelation of the Sorts of A
for b4 being invariant ManySortedRelation of A holds
( b4 = InvCl R iff ( R c= b4 & ( for Q being invariant ManySortedRelation of A st R c= Q holds
b4 c= Q ) ) );
theorem Th29:
theorem Th30:
Lm2:
now
let S be non
empty non
void ManySortedSign ;
for A being non-empty MSAlgebra of 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 of
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;
:: deftheorem Def12 defines StabCl MSUALG_6:def 12 :
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra of S
for R being ManySortedRelation of the Sorts of A
for b4 being stable ManySortedRelation of A holds
( b4 = StabCl R iff ( R c= b4 & ( for Q being stable ManySortedRelation of A st R c= Q holds
b4 c= Q ) ) );
theorem Th31:
theorem
:: deftheorem Def13 defines TRS MSUALG_6:def 13 :
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra of S
for R being ManySortedRelation of the Sorts of A
for b4 being invariant stable ManySortedRelation of A holds
( b4 = TRS R iff ( R c= b4 & ( for Q being invariant stable ManySortedRelation of A st R c= Q holds
b4 c= Q ) ) );
theorem
theorem
theorem
theorem
theorem Th37:
theorem
begin
theorem Th39:
theorem Th40:
theorem Th41:
theorem Th42:
:: deftheorem defines EqCl MSUALG_6:def 14 :
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra of S
for R being ManySortedRelation of A holds EqCl (R,A) = EqCl R;
theorem Th43:
theorem Th44:
theorem Th45:
theorem Th46:
theorem Th47:
theorem Th48:
theorem Th49:
theorem Th50:
theorem Th51:
:: deftheorem Def15 defines EqTh MSUALG_6:def 15 :
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra of S
for R being ManySortedRelation of the Sorts of A
for b4 being EquationalTheory of A holds
( b4 = EqTh R iff ( R c= b4 & ( for Q being EquationalTheory of A st R c= Q holds
b4 c= Q ) ) );
theorem
theorem
theorem