:: by Grzegorz Bancerek

::

:: Received February 9, 1996

:: Copyright (c) 1996-2012 Association of Mizar Users

begin

definition

let S be non empty ManySortedSign ;

let A be MSAlgebra over S;

let s be SortSymbol of S;

mode Element of A,s is Element of the Sorts of A . s;

end;
let A be MSAlgebra over S;

let s be SortSymbol of S;

mode Element of A,s is Element of the Sorts of A . s;

definition

let I be set ;

let A be ManySortedSet of I;

let h1, h2 be ManySortedFunction of A,A;

:: original: **

redefine func h2 ** h1 -> ManySortedFunction of A,A;

coherence

h2 ** h1 is ManySortedFunction of A,A

end;
let A be ManySortedSet of I;

let h1, h2 be ManySortedFunction of A,A;

:: original: **

redefine func h2 ** h1 -> ManySortedFunction of A,A;

coherence

h2 ** h1 is ManySortedFunction of A,A

proof end;

theorem Th1: :: MSUALG_6:1

for S being non empty non void ManySortedSign

for A being MSAlgebra over S

for o being OperSymbol of S

for a being set st a in Args (o,A) holds

a is Function

for A being MSAlgebra over S

for o being OperSymbol of S

for a being set st a in Args (o,A) holds

a is Function

proof end;

theorem Th2: :: MSUALG_6:2

for S being non empty non void ManySortedSign

for A being MSAlgebra over S

for o being OperSymbol of S

for a being Function st a in Args (o,A) holds

( dom a = dom (the_arity_of o) & ( for i being set st i in dom (the_arity_of o) holds

a . i in the Sorts of A . ((the_arity_of o) /. i) ) )

for A being MSAlgebra over S

for o being OperSymbol of S

for a being Function st a in Args (o,A) holds

( dom a = dom (the_arity_of o) & ( for i being set st i in dom (the_arity_of o) holds

a . i in the Sorts of A . ((the_arity_of o) /. i) ) )

proof end;

definition

let S be non empty non void ManySortedSign ;

let A be MSAlgebra over S;

end;
let A be MSAlgebra over S;

attr A is feasible means :Def1: :: MSUALG_6:def 1

for o being OperSymbol of S st Args (o,A) <> {} holds

Result (o,A) <> {} ;

for o being OperSymbol of S st Args (o,A) <> {} holds

Result (o,A) <> {} ;

:: deftheorem Def1 defines feasible MSUALG_6:def 1 :

for S being non empty non void ManySortedSign

for A being MSAlgebra over S holds

( A is feasible iff for o being OperSymbol of S st Args (o,A) <> {} holds

Result (o,A) <> {} );

for S being non empty non void ManySortedSign

for A being MSAlgebra over S holds

( A is feasible iff for o being OperSymbol of S st Args (o,A) <> {} holds

Result (o,A) <> {} );

theorem Th3: :: MSUALG_6:3

for S being non empty non void ManySortedSign

for o being OperSymbol of S

for A being MSAlgebra over S holds

( Args (o,A) <> {} iff for i being Element of NAT st i in dom (the_arity_of o) holds

the Sorts of A . ((the_arity_of o) /. i) <> {} )

for o being OperSymbol of S

for A being MSAlgebra over S holds

( Args (o,A) <> {} iff for i being Element of NAT st i in dom (the_arity_of o) holds

the Sorts of A . ((the_arity_of o) /. i) <> {} )

proof end;

registration

let S be non empty non void ManySortedSign ;

coherence

for b_{1} being MSAlgebra over S st b_{1} is non-empty holds

b_{1} is feasible

end;
coherence

for b

b

proof end;

registration

let S be non empty non void ManySortedSign ;

existence

ex b_{1} being MSAlgebra over S st b_{1} is non-empty

end;
existence

ex b

proof end;

definition

let S be non empty non void ManySortedSign ;

let A be MSAlgebra over S;

ex b_{1} being ManySortedFunction of A,A st b_{1} is_homomorphism A,A

end;
let A be MSAlgebra over S;

mode Endomorphism of A -> ManySortedFunction of A,A means :Def2: :: MSUALG_6:def 2

it is_homomorphism A,A;

existence it is_homomorphism A,A;

ex b

proof end;

:: deftheorem Def2 defines Endomorphism MSUALG_6:def 2 :

for S being non empty non void ManySortedSign

for A being MSAlgebra over S

for b_{3} being ManySortedFunction of A,A holds

( b_{3} is Endomorphism of A iff b_{3} is_homomorphism A,A );

for S being non empty non void ManySortedSign

for A being MSAlgebra over S

for b

( b

theorem Th4: :: MSUALG_6:4

for S being non empty non void ManySortedSign

for A being MSAlgebra over S holds id the Sorts of A is Endomorphism of A

for A being MSAlgebra over S holds id the Sorts of A is Endomorphism of A

proof end;

theorem Th5: :: MSUALG_6:5

for S being non empty non void ManySortedSign

for A being MSAlgebra over S

for h1, h2 being ManySortedFunction of A,A

for o being OperSymbol of S

for a being Element of Args (o,A) st a in Args (o,A) holds

h2 # (h1 # a) = (h2 ** h1) # a

for A being MSAlgebra over S

for h1, h2 being ManySortedFunction of A,A

for o being OperSymbol of S

for a being Element of Args (o,A) st a in Args (o,A) holds

h2 # (h1 # a) = (h2 ** h1) # a

proof end;

theorem Th6: :: MSUALG_6:6

for S being non empty non void ManySortedSign

for A being MSAlgebra over S

for h1, h2 being Endomorphism of A holds h2 ** h1 is Endomorphism of A

for A being MSAlgebra over S

for h1, h2 being Endomorphism of A holds h2 ** h1 is Endomorphism of A

proof end;

definition

let S be non empty non void ManySortedSign ;

let A be MSAlgebra over S;

let h1, h2 be Endomorphism of A;

:: original: **

redefine func h2 ** h1 -> Endomorphism of A;

coherence

h2 ** h1 is Endomorphism of A by Th6;

end;
let A be MSAlgebra over S;

let h1, h2 be Endomorphism of A;

:: original: **

redefine func h2 ** h1 -> Endomorphism of A;

coherence

h2 ** h1 is Endomorphism of A by Th6;

definition

let S be non empty non void ManySortedSign ;

ex b_{1} being Relation of the carrier of S st

for s1, s2 being SortSymbol of S holds

( [s1,s2] in b_{1} 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 ) ) )

uniqueness

for b_{1}, b_{2} being Relation of the carrier of S st ( for s1, s2 being SortSymbol of S holds

( [s1,s2] in b_{1} 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 ) ) ) ) & ( for s1, s2 being SortSymbol of S holds

( [s1,s2] in b_{2} 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 ) ) ) ) holds

b_{1} = b_{2};

end;
func TranslationRel S -> Relation of the carrier of S means :Def3: :: MSUALG_6:def 3

for s1, s2 being SortSymbol of S holds

( [s1,s2] in it 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 ) ) );

existence for s1, s2 being SortSymbol of S holds

( [s1,s2] in it 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 b

for s1, s2 being SortSymbol of S holds

( [s1,s2] in b

( 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 ) ) )

proof end;

correctness uniqueness

for b

( [s1,s2] in b

( 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 ) ) ) ) & ( for s1, s2 being SortSymbol of S holds

( [s1,s2] in b

( 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 ) ) ) ) holds

b

proof end;

:: deftheorem Def3 defines TranslationRel MSUALG_6:def 3 :

for S being non empty non void ManySortedSign

for b_{2} being Relation of the carrier of S holds

( b_{2} = TranslationRel S iff for s1, s2 being SortSymbol of S holds

( [s1,s2] in b_{2} 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 ) ) ) );

for S being non empty non void ManySortedSign

for b

( b

( [s1,s2] in b

( 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: :: MSUALG_6:7

for S being non empty non void ManySortedSign

for o being OperSymbol of S

for A being MSAlgebra over S

for a being Function st a in Args (o,A) holds

for i being Element of NAT

for x being Element of A,((the_arity_of o) /. i) holds a +* (i,x) in Args (o,A)

for o being OperSymbol of S

for A being MSAlgebra over S

for a being Function st a in Args (o,A) holds

for i being Element of NAT

for x being Element of A,((the_arity_of o) /. i) holds a +* (i,x) in Args (o,A)

proof end;

theorem Th8: :: MSUALG_6:8

for S being non empty non void ManySortedSign

for A1, A2 being MSAlgebra over S

for h being ManySortedFunction of A1,A2

for o being OperSymbol of S st Args (o,A1) <> {} & Args (o,A2) <> {} holds

for i being Element of NAT st i in dom (the_arity_of o) holds

for x being Element of A1,((the_arity_of o) /. i) holds (h . ((the_arity_of o) /. i)) . x in the Sorts of A2 . ((the_arity_of o) /. i)

for A1, A2 being MSAlgebra over S

for h being ManySortedFunction of A1,A2

for o being OperSymbol of S st Args (o,A1) <> {} & Args (o,A2) <> {} holds

for i being Element of NAT st i in dom (the_arity_of o) holds

for x being Element of A1,((the_arity_of o) /. i) holds (h . ((the_arity_of o) /. i)) . x in the Sorts of A2 . ((the_arity_of o) /. i)

proof end;

theorem Th9: :: MSUALG_6:9

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)) )

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)) )

proof end;

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 over S;

let a be Function;

ex b_{1} being Function st

( dom b_{1} = 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

b_{1} . x = (Den (o,A)) . (a +* (i,x)) ) )

for b_{1}, b_{2} being Function st dom b_{1} = 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

b_{1} . x = (Den (o,A)) . (a +* (i,x)) ) & dom b_{2} = 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

b_{2} . x = (Den (o,A)) . (a +* (i,x)) ) holds

b_{1} = b_{2}

end;
let o be OperSymbol of S;

let i be Element of NAT ;

let A be MSAlgebra over S;

let a be Function;

func transl (o,i,a,A) -> Function means :Def4: :: MSUALG_6:def 4

( 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 ( 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)) ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof 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 over S

for a, b_{6} being Function holds

( b_{6} = transl (o,i,a,A) iff ( dom b_{6} = 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

b_{6} . x = (Den (o,A)) . (a +* (i,x)) ) ) );

for S being non empty non void ManySortedSign

for o being OperSymbol of S

for i being Element of NAT

for A being MSAlgebra over S

for a, b

( b

b

theorem Th10: :: MSUALG_6:10

for S being non empty non void ManySortedSign

for o being OperSymbol of S

for i being Element of NAT

for A being feasible MSAlgebra over S

for a being Function st a in Args (o,A) holds

transl (o,i,a,A) is Function of ( the Sorts of A . ((the_arity_of o) /. i)),( the Sorts of A . (the_result_sort_of o))

for o being OperSymbol of S

for i being Element of NAT

for A being feasible MSAlgebra over S

for a being Function st a in Args (o,A) holds

transl (o,i,a,A) is Function of ( the Sorts of A . ((the_arity_of o) /. i)),( the Sorts of A . (the_result_sort_of o))

proof end;

definition

let S be non empty non void ManySortedSign ;

let s1, s2 be SortSymbol of S;

let A be MSAlgebra over S;

let f be Function;

end;
let s1, s2 be SortSymbol of S;

let A be MSAlgebra over S;

let f be Function;

pred f is_e.translation_of A,s1,s2 means :Def5: :: MSUALG_6:def 5

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) ) ) );

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) ) ) );

:: 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 over 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) ) ) ) );

for S being non empty non void ManySortedSign

for s1, s2 being SortSymbol of S

for A being MSAlgebra over 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: :: MSUALG_6:11

for S being non empty non void ManySortedSign

for s1, s2 being SortSymbol of S

for A being feasible MSAlgebra over S

for f being Function st f is_e.translation_of A,s1,s2 holds

( f is Function of ( the Sorts of A . s1),( the Sorts of A . s2) & the Sorts of A . s1 <> {} & the Sorts of A . s2 <> {} )

for s1, s2 being SortSymbol of S

for A being feasible MSAlgebra over S

for f being Function st f is_e.translation_of A,s1,s2 holds

( f is Function of ( the Sorts of A . s1),( the Sorts of A . s2) & the Sorts of A . s1 <> {} & the Sorts of A . s2 <> {} )

proof end;

theorem Th12: :: MSUALG_6:12

for S being non empty non void ManySortedSign

for s1, s2 being SortSymbol of S

for A being MSAlgebra over S

for f being Function st f is_e.translation_of A,s1,s2 holds

[s1,s2] in TranslationRel S

for s1, s2 being SortSymbol of S

for A being MSAlgebra over S

for f being Function st f is_e.translation_of A,s1,s2 holds

[s1,s2] in TranslationRel S

proof end;

theorem :: MSUALG_6:13

for S being non empty non void ManySortedSign

for s1, s2 being SortSymbol of S

for A being non-empty MSAlgebra over S st [s1,s2] in TranslationRel S holds

ex f being Function st f is_e.translation_of A,s1,s2

for s1, s2 being SortSymbol of S

for A being non-empty MSAlgebra over S st [s1,s2] in TranslationRel S holds

ex f being Function st f is_e.translation_of A,s1,s2

proof end;

theorem Th14: :: MSUALG_6:14

for S being non empty non void ManySortedSign

for A being feasible MSAlgebra over S

for s1, s2 being SortSymbol of S

for q being RedSequence of TranslationRel S

for p being Function-yielding FinSequence st 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 ) holds

( compose (p,( the Sorts of A . s1)) is Function of ( the Sorts of A . s1),( the Sorts of A . s2) & ( p <> {} implies ( the Sorts of A . s1 <> {} & the Sorts of A . s2 <> {} ) ) )

for A being feasible MSAlgebra over S

for s1, s2 being SortSymbol of S

for q being RedSequence of TranslationRel S

for p being Function-yielding FinSequence st 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 ) holds

( compose (p,( the Sorts of A . s1)) is Function of ( the Sorts of A . s1),( the Sorts of A . s2) & ( p <> {} implies ( the Sorts of A . s1 <> {} & the Sorts of A . s2 <> {} ) ) )

proof end;

definition

let S be non empty non void ManySortedSign ;

let A be non-empty MSAlgebra over S;

let s1, s2 be SortSymbol of S;

assume B1: TranslationRel S reduces s1,s2 ;

ex b_{1} 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

( b_{1} = 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;
let A be non-empty MSAlgebra over S;

let s1, s2 be SortSymbol of S;

assume B1: 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: :: MSUALG_6:def 6

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 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 ) );

ex b

( b

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 ) )

proof end;

:: deftheorem Def6 defines Translation MSUALG_6:def 6 :

for S being non empty non void ManySortedSign

for A being non-empty MSAlgebra over S

for s1, s2 being SortSymbol of S st TranslationRel S reduces s1,s2 holds

for b_{5} being Function of ( the Sorts of A . s1),( the Sorts of A . s2) holds

( b_{5} is Translation of A,s1,s2 iff ex q being RedSequence of TranslationRel S ex p being Function-yielding FinSequence st

( b_{5} = 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 ) ) );

for S being non empty non void ManySortedSign

for A being non-empty MSAlgebra over S

for s1, s2 being SortSymbol of S st TranslationRel S reduces s1,s2 holds

for b

( b

( b

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 :: MSUALG_6:15

for S being non empty non void ManySortedSign

for A being non-empty MSAlgebra over S

for s1, s2 being SortSymbol of S st TranslationRel S reduces s1,s2 holds

for q being RedSequence of TranslationRel S

for p being Function-yielding FinSequence st 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 ) holds

compose (p,( the Sorts of A . s1)) is Translation of A,s1,s2

for A being non-empty MSAlgebra over S

for s1, s2 being SortSymbol of S st TranslationRel S reduces s1,s2 holds

for q being RedSequence of TranslationRel S

for p being Function-yielding FinSequence st 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 ) holds

compose (p,( the Sorts of A . s1)) is Translation of A,s1,s2

proof end;

theorem Th16: :: MSUALG_6:16

for S being non empty non void ManySortedSign

for A being non-empty MSAlgebra over S

for s being SortSymbol of S holds id ( the Sorts of A . s) is Translation of A,s,s

for A being non-empty MSAlgebra over S

for s being SortSymbol of S holds id ( the Sorts of A . s) is Translation of A,s,s

proof end;

theorem Th17: :: MSUALG_6:17

for S being non empty non void ManySortedSign

for A being non-empty MSAlgebra over S

for s1, s2 being SortSymbol of S

for f being Function st f is_e.translation_of A,s1,s2 holds

( TranslationRel S reduces s1,s2 & f is Translation of A,s1,s2 )

for A being non-empty MSAlgebra over S

for s1, s2 being SortSymbol of S

for f being Function st f is_e.translation_of A,s1,s2 holds

( TranslationRel S reduces s1,s2 & f is Translation of A,s1,s2 )

proof end;

theorem Th18: :: MSUALG_6:18

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

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

proof end;

theorem Th19: :: MSUALG_6:19

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 holds

for t being Translation of A,s1,s2

for f being Function st f is_e.translation_of A,s2,s3 holds

f * t is Translation of A,s1,s3

for A being non-empty MSAlgebra over S

for s1, s2, s3 being SortSymbol of S st TranslationRel S reduces s1,s2 holds

for t being Translation of A,s1,s2

for f being Function st f is_e.translation_of A,s2,s3 holds

f * t is Translation of A,s1,s3

proof end;

theorem :: MSUALG_6:20

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 s2,s3 holds

for f being Function st f is_e.translation_of A,s1,s2 holds

for t being Translation of A,s2,s3 holds t * f is Translation of A,s1,s3

for A being non-empty MSAlgebra over S

for s1, s2, s3 being SortSymbol of S st TranslationRel S reduces s2,s3 holds

for f being Function st f is_e.translation_of A,s1,s2 holds

for t being Translation of A,s2,s3 holds t * f is Translation of A,s1,s3

proof end;

scheme :: MSUALG_6:sch 1

TranslationInd{ F_{1}() -> non empty non void ManySortedSign , F_{2}() -> non-empty MSAlgebra over F_{1}(), P_{1}[ set , set , set ] } :

TranslationInd{ F

for s1, s2 being SortSymbol of F_{1}() st TranslationRel F_{1}() reduces s1,s2 holds

for t being Translation of F_{2}(),s1,s2 holds P_{1}[t,s1,s2]

providedfor t being Translation of F

A1:
for s being SortSymbol of F_{1}() holds P_{1}[ id ( the Sorts of F_{2}() . s),s,s]
and

A2: for s1, s2, s3 being SortSymbol of F_{1}() st TranslationRel F_{1}() reduces s1,s2 holds

for t being Translation of F_{2}(),s1,s2 st P_{1}[t,s1,s2] holds

for f being Function st f is_e.translation_of F_{2}(),s2,s3 holds

P_{1}[f * t,s1,s3]

A2: for s1, s2, s3 being SortSymbol of F

for t being Translation of F

for f being Function st f is_e.translation_of F

P

proof end;

theorem Th21: :: MSUALG_6:21

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))

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))

proof end;

theorem :: MSUALG_6:22

for S being non empty non void ManySortedSign

for A being non-empty MSAlgebra over S

for h being Endomorphism of A

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,A) holds (h . (the_result_sort_of o)) * (transl (o,i,a,A)) = (transl (o,i,(h # a),A)) * (h . ((the_arity_of o) /. i))

for A being non-empty MSAlgebra over S

for h being Endomorphism of A

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,A) holds (h . (the_result_sort_of o)) * (transl (o,i,a,A)) = (transl (o,i,(h # a),A)) * (h . ((the_arity_of o) /. i))

proof end;

theorem Th23: :: MSUALG_6:23

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 s1, s2 being SortSymbol of S

for t being Function st t is_e.translation_of A1,s1,s2 holds

ex T being Function of ( the Sorts of A2 . s1),( the Sorts of A2 . s2) st

( T is_e.translation_of A2,s1,s2 & T * (h . s1) = (h . s2) * t )

for A1, A2 being non-empty MSAlgebra over S

for h being ManySortedFunction of A1,A2 st h is_homomorphism A1,A2 holds

for s1, s2 being SortSymbol of S

for t being Function st t is_e.translation_of A1,s1,s2 holds

ex T being Function of ( the Sorts of A2 . s1),( the Sorts of A2 . s2) st

( T is_e.translation_of A2,s1,s2 & T * (h . s1) = (h . s2) * t )

proof end;

theorem :: MSUALG_6:24

for S being non empty non void ManySortedSign

for A being non-empty MSAlgebra over S

for h being Endomorphism of A

for s1, s2 being SortSymbol of S

for t being Function st t is_e.translation_of A,s1,s2 holds

ex T being Function of ( the Sorts of A . s1),( the Sorts of A . s2) st

( T is_e.translation_of A,s1,s2 & T * (h . s1) = (h . s2) * t )

for A being non-empty MSAlgebra over S

for h being Endomorphism of A

for s1, s2 being SortSymbol of S

for t being Function st t is_e.translation_of A,s1,s2 holds

ex T being Function of ( the Sorts of A . s1),( the Sorts of A . s2) st

( T is_e.translation_of A,s1,s2 & T * (h . s1) = (h . s2) * t )

proof end;

theorem Th25: :: MSUALG_6:25

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 s1, s2 being SortSymbol of S st TranslationRel S reduces s1,s2 holds

for t being Translation of A1,s1,s2 ex T being Translation of A2,s1,s2 st T * (h . s1) = (h . s2) * t

for A1, A2 being non-empty MSAlgebra over S

for h being ManySortedFunction of A1,A2 st h is_homomorphism A1,A2 holds

for s1, s2 being SortSymbol of S st TranslationRel S reduces s1,s2 holds

for t being Translation of A1,s1,s2 ex T being Translation of A2,s1,s2 st T * (h . s1) = (h . s2) * t

proof end;

theorem Th26: :: MSUALG_6:26

for S being non empty non void ManySortedSign

for A being non-empty MSAlgebra over S

for h being Endomorphism of A

for s1, s2 being SortSymbol of S st TranslationRel S reduces s1,s2 holds

for t being Translation of A,s1,s2 ex T being Translation of A,s1,s2 st T * (h . s1) = (h . s2) * t

for A being non-empty MSAlgebra over S

for h being Endomorphism of A

for s1, s2 being SortSymbol of S st TranslationRel S reduces s1,s2 holds

for t being Translation of A,s1,s2 ex T being Translation of A,s1,s2 st T * (h . s1) = (h . s2) * t

proof end;

begin

definition

let S be non empty non void ManySortedSign ;

let A be MSAlgebra over S;

let R be ManySortedRelation of A;

end;
let A be MSAlgebra over S;

let R be ManySortedRelation of A;

attr R is compatible means :Def7: :: MSUALG_6:def 7

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);

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: :: MSUALG_6:def 8

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;

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 Def7 defines compatible MSUALG_6:def 7 :

for S being non empty non void ManySortedSign

for A being MSAlgebra over 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) );

for S being non empty non void ManySortedSign

for A being MSAlgebra over 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 over 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 );

for S being non empty non void ManySortedSign

for A being MSAlgebra over 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 over 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 );

for S being non empty non void ManySortedSign

for A being MSAlgebra over 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 :: MSUALG_6:27

for S being non empty non void ManySortedSign

for A being non-empty MSAlgebra over S

for R being MSEquivalence-like ManySortedRelation of A holds

( R is compatible iff R is MSCongruence of A )

for A being non-empty MSAlgebra over S

for R being MSEquivalence-like ManySortedRelation of A holds

( R is compatible iff R is MSCongruence of A )

proof end;

theorem Th28: :: MSUALG_6:28

for S being non empty non void ManySortedSign

for A being non-empty MSAlgebra over S

for R being ManySortedRelation of A holds

( R is invariant iff 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 )

for A being non-empty MSAlgebra over S

for R being ManySortedRelation of A holds

( R is invariant iff 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 )

proof end;

registration

let S be non empty non void ManySortedSign ;

let A be non-empty MSAlgebra over S;

for b_{1} being MSEquivalence-like ManySortedRelation of A st b_{1} is invariant holds

b_{1} is compatible

for b_{1} being MSEquivalence-like ManySortedRelation of A st b_{1} is compatible holds

b_{1} is invariant

end;
let A be non-empty MSAlgebra over S;

cluster MSEquivalence-like invariant -> MSEquivalence-like compatible for ManySortedRelation of the Sorts of A, the Sorts of A;

coherence for b

b

proof end;

cluster MSEquivalence-like compatible -> MSEquivalence-like invariant for ManySortedRelation of the Sorts of A, the Sorts of A;

coherence for b

b

proof end;

registration
end;

scheme :: MSUALG_6:sch 2

MSRExistence{ F_{1}() -> non empty set , F_{2}() -> V16() ManySortedSet of F_{1}(), P_{1}[ set , set , set ] } :

MSRExistence{ F

ex R being ManySortedRelation of F_{2}() st

for i being Element of F_{1}()

for a, b being Element of F_{2}() . i holds

( [a,b] in R . i iff P_{1}[i,a,b] )

for i being Element of F

for a, b being Element of F

( [a,b] in R . i iff P

proof end;

scheme :: MSUALG_6:sch 3

MSRLambdaU{ F_{1}() -> set , F_{2}() -> ManySortedSet of F_{1}(), F_{3}( set ) -> set } :

MSRLambdaU{ F

( ex R being ManySortedRelation of F_{2}() st

for i being set st i in F_{1}() holds

R . i = F_{3}(i) & ( for R1, R2 being ManySortedRelation of F_{2}() st ( for i being set st i in F_{1}() holds

R1 . i = F_{3}(i) ) & ( for i being set st i in F_{1}() holds

R2 . i = F_{3}(i) ) holds

R1 = R2 ) )

provided
for i being set st i in F

R . i = F

R1 . i = F

R2 . i = F

R1 = R2 ) )

proof end;

definition

let I be set ;

let A be ManySortedSet of I;

existence

ex b_{1} being ManySortedRelation of A st

for i being set st i in I holds

b_{1} . i = id (A . i);

uniqueness

for b_{1}, b_{2} being ManySortedRelation of A st ( for i being set st i in I holds

b_{1} . i = id (A . i) ) & ( for i being set st i in I holds

b_{2} . i = id (A . i) ) holds

b_{1} = b_{2};

end;
let A be ManySortedSet of I;

func id (I,A) -> ManySortedRelation of A means :Def10: :: MSUALG_6:def 10

for i being set st i in I holds

it . i = id (A . i);

correctness for i being set st i in I holds

it . i = id (A . i);

existence

ex b

for i being set st i in I holds

b

uniqueness

for b

b

b

b

proof end;

:: deftheorem Def10 defines id MSUALG_6:def 10 :

for I being set

for A being ManySortedSet of I

for b_{3} being ManySortedRelation of A holds

( b_{3} = id (I,A) iff for i being set st i in I holds

b_{3} . i = id (A . i) );

for I being set

for A being ManySortedSet of I

for b

( b

b

registration

let S be non empty non void ManySortedSign ;

let A be non-empty MSAlgebra over S;

coherence

for b_{1} being ManySortedRelation of A st b_{1} is MSEquivalence-like holds

b_{1} is V16()

end;
let A be non-empty MSAlgebra over S;

coherence

for b

b

proof end;

registration

let S be non empty non void ManySortedSign ;

let A be non-empty MSAlgebra over S;

ex b_{1} being ManySortedRelation of A st

( b_{1} is invariant & b_{1} is stable & b_{1} is MSEquivalence-like )

end;
let A be non-empty MSAlgebra over S;

cluster non empty Relation-like the carrier of S -defined Function-like total Relation-yielding MSEquivalence-like invariant stable for ManySortedRelation of the Sorts of A, the Sorts of A;

existence ex b

( b

proof end;

begin

scheme :: MSUALG_6:sch 4

MSRelCl{ F_{1}() -> non empty non void ManySortedSign , F_{2}() -> non-empty MSAlgebra over F_{1}(), P_{1}[ set , set , set ], P_{2}[ set ], F_{3}() -> ManySortedRelation of F_{2}(), F_{4}() -> ManySortedRelation of F_{2}() } :

MSRelCl{ F

( P_{2}[F_{4}()] & F_{3}() c= F_{4}() & ( for P being ManySortedRelation of F_{2}() st P_{2}[P] & F_{3}() c= P holds

F_{4}() c= P ) )

providedF

A1:
for R being ManySortedRelation of F_{2}() holds

( P_{2}[R] iff for s1, s2 being SortSymbol of F_{1}()

for f being Function of ( the Sorts of F_{2}() . s1),( the Sorts of F_{2}() . s2) st P_{1}[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 F_{1}()

for f1 being Function of ( the Sorts of F_{2}() . s1),( the Sorts of F_{2}() . s2)

for f2 being Function of ( the Sorts of F_{2}() . s2),( the Sorts of F_{2}() . s3) st P_{1}[f1,s1,s2] & P_{1}[f2,s2,s3] holds

P_{1}[f2 * f1,s1,s3]
and

A3: for s being SortSymbol of F_{1}() holds P_{1}[ id ( the Sorts of F_{2}() . s),s,s]
and

A4: for s being SortSymbol of F_{1}()

for a, b being Element of F_{2}(),s holds

( [a,b] in F_{4}() . s iff ex s9 being SortSymbol of F_{1}() ex f being Function of ( the Sorts of F_{2}() . s9),( the Sorts of F_{2}() . s) ex x, y being Element of F_{2}(),s9 st

( P_{1}[f,s9,s] & [x,y] in F_{3}() . s9 & a = f . x & b = f . y ) )

( P

for f being Function of ( the Sorts of F

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 F

for f1 being Function of ( the Sorts of F

for f2 being Function of ( the Sorts of F

P

A3: for s being SortSymbol of F

A4: for s being SortSymbol of F

for a, b being Element of F

( [a,b] in F

( P

proof end;

Lm1: now :: thesis: 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

( S_{2}[f,s9,s] & [x,y] in R . s9 & a = f . x & b = f . y ) ) ) holds

( S_{1}[Q] & R c= Q & ( for P being ManySortedRelation of A st S_{1}[P] & R c= P holds

Q c= P ) )

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

( S

( S

Q c= P ) )

let S be non empty non void ManySortedSign ; :: thesis: 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

( S_{2}[f,s9,s] & [x,y] in R . s9 & a = f . x & b = f . y ) ) ) holds

( S_{1}[Q] & R c= Q & ( for P being ManySortedRelation of A st S_{1}[P] & R c= P holds

Q c= P ) )

let A be non-empty MSAlgebra over S; :: thesis: 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

( S_{2}[f,s9,s] & [x,y] in R . s9 & a = f . x & b = f . y ) ) ) holds

( S_{1}[Q] & R c= Q & ( for P being ManySortedRelation of A st S_{1}[P] & R c= P holds

Q c= P ) )

let R, Q be ManySortedRelation of A; :: thesis: ( ( 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

( S_{2}[f,s9,s] & [x,y] in R . s9 & a = f . x & b = f . y ) ) ) implies ( S_{1}[Q] & R c= Q & ( for P being ManySortedRelation of A st S_{1}[P] & R c= P holds

Q c= P ) ) )

defpred S_{1}[ ManySortedRelation of A] means $1 is invariant ;

defpred S_{2}[ 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

( S_{2}[f,s9,s] & [x,y] in R . s9 & a = f . x & b = f . y ) )
; :: thesis: ( S_{1}[Q] & R c= Q & ( for P being ManySortedRelation of A st S_{1}[P] & R c= P holds

Q c= P ) )

A2: for s being SortSymbol of S holds S_{2}[ id ( the Sorts of A . s),s,s]
by Th16, REWRITE1:12;

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 S_{2}[f1,s1,s2] & S_{2}[f2,s2,s3] holds

S_{2}[f2 * f1,s1,s3]
by Th18, REWRITE1:16;

thus ( S_{1}[Q] & R c= Q & ( for P being ManySortedRelation of A st S_{1}[P] & R c= P holds

Q c= P ) ) from MSUALG_6:sch 4(A3, A4, A2, A1); :: thesis: verum

end;
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

( S

( S

Q c= P ) )

let A be non-empty MSAlgebra over S; :: thesis: 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

( S

( S

Q c= P ) )

let R, Q be ManySortedRelation of A; :: thesis: ( ( 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

( S

Q c= P ) ) )

defpred S

defpred S

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

( S

Q c= P ) )

A2: for s being SortSymbol of S holds S

A3: now :: thesis: for R being ManySortedRelation of A holds

( ( S_{1}[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 S_{2}[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 S_{2}[f,s1,s2] holds

for a, b being set st [a,b] in R . s1 holds

[(f . a),(f . b)] in R . s2 ) implies S_{1}[R] ) )

A4:
for s1, s2, s3 being SortSymbol of S( ( S

for f being Function of ( the Sorts of A . s1),( the Sorts of A . s2) st S

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 S

for a, b being set st [a,b] in R . s1 holds

[(f . a),(f . b)] in R . s2 ) implies S

let R be ManySortedRelation of A; :: thesis: ( ( S_{1}[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 S_{2}[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 S_{2}[f,s1,s2] holds

for a, b being set st [a,b] in R . s1 holds

[(f . a),(f . b)] in R . s2 ) implies S_{1}[R] ) )

thus ( S_{1}[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 S_{2}[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; :: thesis: ( ( for s1, s2 being SortSymbol of S

for f being Function of ( the Sorts of A . s1),( the Sorts of A . s2) st S_{2}[f,s1,s2] holds

for a, b being set st [a,b] in R . s1 holds

[(f . a),(f . b)] in R . s2 ) implies S_{1}[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 S_{2}[f,s1,s2] holds

for a, b being set st [a,b] in R . s1 holds

[(f . a),(f . b)] in R . s2 ; :: thesis: S_{1}[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 S_{1}[R]
by Th28; :: thesis: verum

end;
for f being Function of ( the Sorts of A . s1),( the Sorts of A . s2) st S

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 S

for a, b being set st [a,b] in R . s1 holds

[(f . a),(f . b)] in R . s2 ) implies S

thus ( S

for f being Function of ( the Sorts of A . s1),( the Sorts of A . s2) st S

for a, b being set st [a,b] in R . s1 holds

[(f . a),(f . b)] in R . s2 ) by Th28; :: thesis: ( ( for s1, s2 being SortSymbol of S

for f being Function of ( the Sorts of A . s1),( the Sorts of A . s2) st S

for a, b being set st [a,b] in R . s1 holds

[(f . a),(f . b)] in R . s2 ) implies S

assume for s1, s2 being SortSymbol of S

for f being Function of ( the Sorts of A . s1),( the Sorts of A . s2) st S

for a, b being set st [a,b] in R . s1 holds

[(f . a),(f . b)] in R . s2 ; :: thesis: S

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 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 S

S

thus ( S

Q c= P ) ) from MSUALG_6:sch 4(A3, A4, A2, A1); :: thesis: verum

definition

let S be non empty non void ManySortedSign ;

let A be non-empty MSAlgebra over S;

let R be ManySortedRelation of the Sorts of A;

for b_{1}, b_{2} being invariant ManySortedRelation of A st R c= b_{1} & ( for Q being invariant ManySortedRelation of A st R c= Q holds

b_{1} c= Q ) & R c= b_{2} & ( for Q being invariant ManySortedRelation of A st R c= Q holds

b_{2} c= Q ) holds

b_{1} = b_{2}

ex b_{1} being invariant ManySortedRelation of A st

( R c= b_{1} & ( for Q being invariant ManySortedRelation of A st R c= Q holds

b_{1} c= Q ) )

end;
let A be non-empty MSAlgebra over S;

let R be ManySortedRelation of the Sorts of A;

func InvCl R -> invariant ManySortedRelation of A means :Def11: :: MSUALG_6:def 11

( R c= it & ( for Q being invariant ManySortedRelation of A st R c= Q holds

it c= Q ) );

uniqueness ( R c= it & ( for Q being invariant ManySortedRelation of A st R c= Q holds

it c= Q ) );

for b

b

b

b

proof end;

existence ex b

( R c= b

b

proof end;

:: deftheorem Def11 defines InvCl MSUALG_6:def 11 :

for S being non empty non void ManySortedSign

for A being non-empty MSAlgebra over S

for R being ManySortedRelation of the Sorts of A

for b_{4} being invariant ManySortedRelation of A holds

( b_{4} = InvCl R iff ( R c= b_{4} & ( for Q being invariant ManySortedRelation of A st R c= Q holds

b_{4} c= Q ) ) );

for S being non empty non void ManySortedSign

for A being non-empty MSAlgebra over S

for R being ManySortedRelation of the Sorts of A

for b

( b

b

theorem Th29: :: MSUALG_6:29

for S being non empty non void ManySortedSign

for A being non-empty MSAlgebra over S

for R being ManySortedRelation of the Sorts of A

for s being SortSymbol of S

for a, b being Element of A,s holds

( [a,b] in (InvCl R) . s iff ex s9 being SortSymbol of S ex x, y being Element of A,s9 ex t being Translation of A,s9,s st

( TranslationRel S reduces s9,s & [x,y] in R . s9 & a = t . x & b = t . y ) )

for A being non-empty MSAlgebra over S

for R being ManySortedRelation of the Sorts of A

for s being SortSymbol of S

for a, b being Element of A,s holds

( [a,b] in (InvCl R) . s iff ex s9 being SortSymbol of S ex x, y being Element of A,s9 ex t being Translation of A,s9,s st

( TranslationRel S reduces s9,s & [x,y] in R . s9 & a = t . x & b = t . y ) )

proof end;

theorem Th30: :: MSUALG_6:30

for S being non empty non void ManySortedSign

for A being non-empty MSAlgebra over S

for R being stable ManySortedRelation of A holds InvCl R is stable

for A being non-empty MSAlgebra over S

for R being stable ManySortedRelation of A holds InvCl R is stable

proof end;

Lm2: now :: thesis: 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

( S_{2}[f,s9,s] & [x,y] in R . s9 & a = f . x & b = f . y ) ) ) holds

( S_{1}[Q] & R c= Q & ( for P being ManySortedRelation of A st S_{1}[P] & R c= P holds

Q c= P ) )

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

( S

( S

Q c= P ) )

let S be non empty non void ManySortedSign ; :: thesis: 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

( S_{2}[f,s9,s] & [x,y] in R . s9 & a = f . x & b = f . y ) ) ) holds

( S_{1}[Q] & R c= Q & ( for P being ManySortedRelation of A st S_{1}[P] & R c= P holds

Q c= P ) )

let A be non-empty MSAlgebra over S; :: thesis: 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

( S_{2}[f,s9,s] & [x,y] in R . s9 & a = f . x & b = f . y ) ) ) holds

( S_{1}[Q] & R c= Q & ( for P being ManySortedRelation of A st S_{1}[P] & R c= P holds

Q c= P ) )

let R, Q be ManySortedRelation of A; :: thesis: ( ( 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

( S_{2}[f,s9,s] & [x,y] in R . s9 & a = f . x & b = f . y ) ) ) implies ( S_{1}[Q] & R c= Q & ( for P being ManySortedRelation of A st S_{1}[P] & R c= P holds

Q c= P ) ) )

defpred S_{1}[ ManySortedRelation of A] means $1 is stable ;

defpred S_{2}[ 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 S_{2}[f1,s1,s2] & S_{2}[f2,s2,s3] holds

S_{2}[f2 * f1,s1,s3]

( S_{1}[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 S_{2}[f,s1,s2] holds

for a, b being set st [a,b] in R . s1 holds

[(f . a),(f . b)] in R . s2 )_{2}[ id ( the Sorts of A . s),s,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

( S_{2}[f,s9,s] & [x,y] in R . s9 & a = f . x & b = f . y ) )
; :: thesis: ( S_{1}[Q] & R c= Q & ( for P being ManySortedRelation of A st S_{1}[P] & R c= P holds

Q c= P ) )

thus ( S_{1}[Q] & R c= Q & ( for P being ManySortedRelation of A st S_{1}[P] & R c= P holds

Q c= P ) ) from MSUALG_6:sch 4(A6, A1, A8, A9); :: thesis: verum

end;
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

( S

( S

Q c= P ) )

let A be non-empty MSAlgebra over S; :: thesis: 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

( S

( S

Q c= P ) )

let R, Q be ManySortedRelation of A; :: thesis: ( ( 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

( S

Q c= P ) ) )

defpred S

defpred S

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 S

S

proof

A6:
for R being ManySortedRelation of A holds
let s1, s2, s3 be SortSymbol of S; :: thesis: 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 S_{2}[f1,s1,s2] & S_{2}[f2,s2,s3] holds

S_{2}[f2 * f1,s1,s3]

let f1 be Function of ( the Sorts of A . s1),( the Sorts of A . s2); :: thesis: for f2 being Function of ( the Sorts of A . s2),( the Sorts of A . s3) st S_{2}[f1,s1,s2] & S_{2}[f2,s2,s3] holds

S_{2}[f2 * f1,s1,s3]

let f2 be Function of ( the Sorts of A . s2),( the Sorts of A . s3); :: thesis: ( S_{2}[f1,s1,s2] & S_{2}[f2,s2,s3] implies S_{2}[f2 * f1,s1,s3] )

assume A2: s1 = s2 ; :: thesis: ( for h being Endomorphism of A holds not f1 = h . s1 or not S_{2}[f2,s2,s3] or S_{2}[f2 * f1,s1,s3] )

given h1 being Endomorphism of A such that A3: f1 = h1 . s1 ; :: thesis: ( not S_{2}[f2,s2,s3] or S_{2}[f2 * f1,s1,s3] )

assume A4: s2 = s3 ; :: thesis: ( for h being Endomorphism of A holds not f2 = h . s2 or S_{2}[f2 * f1,s1,s3] )

given h2 being Endomorphism of A such that A5: f2 = h2 . s2 ; :: thesis: S_{2}[f2 * f1,s1,s3]

thus s1 = s3 by A2, A4; :: thesis: ex h being Endomorphism of A st f2 * f1 = h . s1

reconsider h = h2 ** h1 as Endomorphism of A ;

take h ; :: thesis: f2 * f1 = h . s1

thus f2 * f1 = h . s1 by A2, A3, A5, MSUALG_3:2; :: thesis: verum

end;
for f2 being Function of ( the Sorts of A . s2),( the Sorts of A . s3) st S

S

let f1 be Function of ( the Sorts of A . s1),( the Sorts of A . s2); :: thesis: for f2 being Function of ( the Sorts of A . s2),( the Sorts of A . s3) st S

S

let f2 be Function of ( the Sorts of A . s2),( the Sorts of A . s3); :: thesis: ( S

assume A2: s1 = s2 ; :: thesis: ( for h being Endomorphism of A holds not f1 = h . s1 or not S

given h1 being Endomorphism of A such that A3: f1 = h1 . s1 ; :: thesis: ( not S

assume A4: s2 = s3 ; :: thesis: ( for h being Endomorphism of A holds not f2 = h . s2 or S

given h2 being Endomorphism of A such that A5: f2 = h2 . s2 ; :: thesis: S

thus s1 = s3 by A2, A4; :: thesis: ex h being Endomorphism of A st f2 * f1 = h . s1

reconsider h = h2 ** h1 as Endomorphism of A ;

take h ; :: thesis: f2 * f1 = h . s1

thus f2 * f1 = h . s1 by A2, A3, A5, MSUALG_3:2; :: thesis: verum

( S

for f being Function of ( the Sorts of A . s1),( the Sorts of A . s2) st S

for a, b being set st [a,b] in R . s1 holds

[(f . a),(f . b)] in R . s2 )

proof

A8:
for s being SortSymbol of S holds S
let R be ManySortedRelation of A; :: thesis: ( S_{1}[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 S_{2}[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; :: thesis: ( ( for s1, s2 being SortSymbol of S

for f being Function of ( the Sorts of A . s1),( the Sorts of A . s2) st S_{2}[f,s1,s2] holds

for a, b being set st [a,b] in R . s1 holds

[(f . a),(f . b)] in R . s2 ) implies S_{1}[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 S_{2}[f,s1,s2] holds

for a, b being set st [a,b] in R . s1 holds

[(f . a),(f . b)] in R . s2 ; :: thesis: S_{1}[R]

thus R is stable :: thesis: verum

end;
for f being Function of ( the Sorts of A . s1),( the Sorts of A . s2) st S

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; :: thesis: ( ( for s1, s2 being SortSymbol of S

for f being Function of ( the Sorts of A . s1),( the Sorts of A . s2) st S

for a, b being set st [a,b] in R . s1 holds

[(f . a),(f . b)] in R . s2 ) implies S

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 S

for a, b being set st [a,b] in R . s1 holds

[(f . a),(f . b)] in R . s2 ; :: thesis: S

thus R is stable :: thesis: verum

proof

let h be Endomorphism of A; :: according to MSUALG_6:def 9 :: thesis: 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

let s be SortSymbol of S; :: thesis: for a, b being set st [a,b] in R . s holds

[((h . s) . a),((h . s) . b)] in R . s

thus for a, b being set st [a,b] in R . s holds

[((h . s) . a),((h . s) . b)] in R . s by A7; :: thesis: verum

end;
for a, b being set st [a,b] in R . s holds

[((h . s) . a),((h . s) . b)] in R . s

let s be SortSymbol of S; :: thesis: for a, b being set st [a,b] in R . s holds

[((h . s) . a),((h . s) . b)] in R . s

thus for a, b being set st [a,b] in R . s holds

[((h . s) . a),((h . s) . b)] in R . s by A7; :: thesis: verum

proof

assume A9:
for s being SortSymbol of S
reconsider h = id the Sorts of A as Endomorphism of A by Th4;

let s be SortSymbol of S; :: thesis: S_{2}[ id ( the Sorts of A . s),s,s]

thus s = s ; :: thesis: ex h being Endomorphism of A st id ( the Sorts of A . s) = h . s

take h ; :: thesis: id ( the Sorts of A . s) = h . s

thus id ( the Sorts of A . s) = h . s by MSUALG_3:def 1; :: thesis: verum

end;
let s be SortSymbol of S; :: thesis: S

thus s = s ; :: thesis: ex h being Endomorphism of A st id ( the Sorts of A . s) = h . s

take h ; :: thesis: id ( the Sorts of A . s) = h . s

thus id ( the Sorts of A . s) = h . s by MSUALG_3:def 1; :: thesis: verum

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

( S

Q c= P ) )

thus ( S

Q c= P ) ) from MSUALG_6:sch 4(A6, A1, A8, A9); :: thesis: verum

definition

let S be non empty non void ManySortedSign ;

let A be non-empty MSAlgebra over S;

let R be ManySortedRelation of the Sorts of A;

for b_{1}, b_{2} being stable ManySortedRelation of A st R c= b_{1} & ( for Q being stable ManySortedRelation of A st R c= Q holds

b_{1} c= Q ) & R c= b_{2} & ( for Q being stable ManySortedRelation of A st R c= Q holds

b_{2} c= Q ) holds

b_{1} = b_{2}

ex b_{1} being stable ManySortedRelation of A st

( R c= b_{1} & ( for Q being stable ManySortedRelation of A st R c= Q holds

b_{1} c= Q ) )

end;
let A be non-empty MSAlgebra over S;

let R be ManySortedRelation of the Sorts of A;

func StabCl R -> stable ManySortedRelation of A means :Def12: :: MSUALG_6:def 12

( R c= it & ( for Q being stable ManySortedRelation of A st R c= Q holds

it c= Q ) );

uniqueness ( R c= it & ( for Q being stable ManySortedRelation of A st R c= Q holds

it c= Q ) );

for b

b

b

b

proof end;

existence ex b

( R c= b

b

proof end;

:: deftheorem Def12 defines StabCl MSUALG_6:def 12 :

for S being non empty non void ManySortedSign

for A being non-empty MSAlgebra over S

for R being ManySortedRelation of the Sorts of A

for b_{4} being stable ManySortedRelation of A holds

( b_{4} = StabCl R iff ( R c= b_{4} & ( for Q being stable ManySortedRelation of A st R c= Q holds

b_{4} c= Q ) ) );

for S being non empty non void ManySortedSign

for A being non-empty MSAlgebra over S

for R being ManySortedRelation of the Sorts of A

for b

( b

b

theorem Th31: :: MSUALG_6:31

for S being non empty non void ManySortedSign

for A being non-empty MSAlgebra over S

for R being ManySortedRelation of the Sorts of A

for s being SortSymbol of S

for a, b being Element of A,s holds

( [a,b] in (StabCl R) . s iff ex x, y being Element of A,s ex h being Endomorphism of A st

( [x,y] in R . s & a = (h . s) . x & b = (h . s) . y ) )

for A being non-empty MSAlgebra over S

for R being ManySortedRelation of the Sorts of A

for s being SortSymbol of S

for a, b being Element of A,s holds

( [a,b] in (StabCl R) . s iff ex x, y being Element of A,s ex h being Endomorphism of A st

( [x,y] in R . s & a = (h . s) . x & b = (h . s) . y ) )

proof end;

theorem :: MSUALG_6:32

definition

let S be non empty non void ManySortedSign ;

let A be non-empty MSAlgebra over S;

let R be ManySortedRelation of the Sorts of A;

for b_{1}, b_{2} being invariant stable ManySortedRelation of A st R c= b_{1} & ( for Q being invariant stable ManySortedRelation of A st R c= Q holds

b_{1} c= Q ) & R c= b_{2} & ( for Q being invariant stable ManySortedRelation of A st R c= Q holds

b_{2} c= Q ) holds

b_{1} = b_{2}

ex b_{1} being invariant stable ManySortedRelation of A st

( R c= b_{1} & ( for Q being invariant stable ManySortedRelation of A st R c= Q holds

b_{1} c= Q ) )

end;
let A be non-empty MSAlgebra over S;

let R be ManySortedRelation of the Sorts of A;

func TRS R -> invariant stable ManySortedRelation of A means :Def13: :: MSUALG_6:def 13

( R c= it & ( for Q being invariant stable ManySortedRelation of A st R c= Q holds

it c= Q ) );

uniqueness ( R c= it & ( for Q being invariant stable ManySortedRelation of A st R c= Q holds

it c= Q ) );

for b

b

b

b

proof end;

existence ex b

( R c= b

b

proof end;

:: deftheorem Def13 defines TRS MSUALG_6:def 13 :

for S being non empty non void ManySortedSign

for A being non-empty MSAlgebra over S

for R being ManySortedRelation of the Sorts of A

for b_{4} being invariant stable ManySortedRelation of A holds

( b_{4} = TRS R iff ( R c= b_{4} & ( for Q being invariant stable ManySortedRelation of A st R c= Q holds

b_{4} c= Q ) ) );

for S being non empty non void ManySortedSign

for A being non-empty MSAlgebra over S

for R being ManySortedRelation of the Sorts of A

for b

( b

b

registration

let S be non empty non void ManySortedSign ;

let A be non-empty MSAlgebra over S;

let R be V16() ManySortedRelation of A;

coherence

InvCl R is non-empty

StabCl R is non-empty

TRS R is non-empty

end;
let A be non-empty MSAlgebra over S;

let R be V16() ManySortedRelation of A;

coherence

InvCl R is non-empty

proof end;

coherence StabCl R is non-empty

proof end;

coherence TRS R is non-empty

proof end;

theorem :: MSUALG_6:33

for S being non empty non void ManySortedSign

for A being non-empty MSAlgebra over S

for R being invariant ManySortedRelation of A holds InvCl R = R

for A being non-empty MSAlgebra over S

for R being invariant ManySortedRelation of A holds InvCl R = R

proof end;

theorem :: MSUALG_6:34

for S being non empty non void ManySortedSign

for A being non-empty MSAlgebra over S

for R being stable ManySortedRelation of A holds StabCl R = R

for A being non-empty MSAlgebra over S

for R being stable ManySortedRelation of A holds StabCl R = R

proof end;

theorem :: MSUALG_6:35

for S being non empty non void ManySortedSign

for A being non-empty MSAlgebra over S

for R being invariant stable ManySortedRelation of A holds TRS R = R

for A being non-empty MSAlgebra over S

for R being invariant stable ManySortedRelation of A holds TRS R = R

proof end;

theorem :: MSUALG_6:36

for S being non empty non void ManySortedSign

for A being non-empty MSAlgebra over S

for R being ManySortedRelation of the Sorts of A holds

( StabCl R c= TRS R & InvCl R c= TRS R & StabCl (InvCl R) c= TRS R )

for A being non-empty MSAlgebra over S

for R being ManySortedRelation of the Sorts of A holds

( StabCl R c= TRS R & InvCl R c= TRS R & StabCl (InvCl R) c= TRS R )

proof end;

theorem Th37: :: MSUALG_6:37

for S being non empty non void ManySortedSign

for A being non-empty MSAlgebra over S

for R being ManySortedRelation of the Sorts of A holds InvCl (StabCl R) = TRS R

for A being non-empty MSAlgebra over S

for R being ManySortedRelation of the Sorts of A holds InvCl (StabCl R) = TRS R

proof end;

theorem :: MSUALG_6:38

for S being non empty non void ManySortedSign

for A being non-empty MSAlgebra over S

for R being ManySortedRelation of the Sorts of A

for s being SortSymbol of S

for a, b being Element of A,s holds

( [a,b] in (TRS R) . s iff ex s9 being SortSymbol of S st

( TranslationRel S reduces s9,s & ex l, r being Element of A,s9 ex h being Endomorphism of A ex t being Translation of A,s9,s st

( [l,r] in R . s9 & a = t . ((h . s9) . l) & b = t . ((h . s9) . r) ) ) )

for A being non-empty MSAlgebra over S

for R being ManySortedRelation of the Sorts of A

for s being SortSymbol of S

for a, b being Element of A,s holds

( [a,b] in (TRS R) . s iff ex s9 being SortSymbol of S st

( TranslationRel S reduces s9,s & ex l, r being Element of A,s9 ex h being Endomorphism of A ex t being Translation of A,s9,s st

( [l,r] in R . s9 & a = t . ((h . s9) . l) & b = t . ((h . s9) . r) ) ) )

proof end;

begin

theorem Th39: :: MSUALG_6:39

for A being set

for R, E being Relation of A st ( for a, b being set st a in A & b in A holds

( [a,b] in E iff a,b are_convertible_wrt R ) ) holds

( E is total & E is symmetric & E is transitive )

for R, E being Relation of A st ( for a, b being set st a in A & b in A holds

( [a,b] in E iff a,b are_convertible_wrt R ) ) holds

( E is total & E is symmetric & E is transitive )

proof end;

theorem Th40: :: MSUALG_6:40

for A being set

for R being Relation of A

for E being Equivalence_Relation of A st R c= E holds

for a, b being set st a in A & a,b are_convertible_wrt R holds

[a,b] in E

for R being Relation of A

for E being Equivalence_Relation of A st R c= E holds

for a, b being set st a in A & a,b are_convertible_wrt R holds

[a,b] in E

proof end;

theorem Th41: :: MSUALG_6:41

for A being non empty set

for R being Relation of A

for a, b being Element of A holds

( [a,b] in EqCl R iff a,b are_convertible_wrt R )

for R being Relation of A

for a, b being Element of A holds

( [a,b] in EqCl R iff a,b are_convertible_wrt R )

proof end;

theorem Th42: :: MSUALG_6:42

for S being non empty set

for A being V16() ManySortedSet of S

for R being ManySortedRelation of A

for s being Element of S

for a, b being Element of A . s holds

( [a,b] in (EqCl R) . s iff a,b are_convertible_wrt R . s )

for A being V16() ManySortedSet of S

for R being ManySortedRelation of A

for s being Element of S

for a, b being Element of A . s holds

( [a,b] in (EqCl R) . s iff a,b are_convertible_wrt R . s )

proof end;

definition

let S be non empty non void ManySortedSign ;

let A be non-empty MSAlgebra over S;

mode EquationalTheory of A is MSEquivalence-like invariant stable ManySortedRelation of A;

let R be ManySortedRelation of A;

coherence

EqCl R is MSEquivalence-like ManySortedRelation of A by MSUALG_4:def 3;

end;
let A be non-empty MSAlgebra over S;

mode EquationalTheory of A is MSEquivalence-like invariant stable ManySortedRelation of A;

let R be ManySortedRelation of A;

coherence

EqCl R is MSEquivalence-like ManySortedRelation of A by MSUALG_4:def 3;

:: deftheorem defines EqCl MSUALG_6:def 14 :

for S being non empty non void ManySortedSign

for A being non-empty MSAlgebra over S

for R being ManySortedRelation of A holds EqCl (R,A) = EqCl R;

for S being non empty non void ManySortedSign

for A being non-empty MSAlgebra over S

for R being ManySortedRelation of A holds EqCl (R,A) = EqCl R;

theorem Th43: :: MSUALG_6:43

for S being non empty non void ManySortedSign

for A being non-empty MSAlgebra over S

for R being ManySortedRelation of A holds R c= EqCl (R,A)

for A being non-empty MSAlgebra over S

for R being ManySortedRelation of A holds R c= EqCl (R,A)

proof end;

theorem Th44: :: MSUALG_6:44

for S being non empty non void ManySortedSign

for A being non-empty MSAlgebra over S

for R being ManySortedRelation of A

for E being MSEquivalence-like ManySortedRelation of A st R c= E holds

EqCl (R,A) c= E

for A being non-empty MSAlgebra over S

for R being ManySortedRelation of A

for E being MSEquivalence-like ManySortedRelation of A st R c= E holds

EqCl (R,A) c= E

proof end;

theorem Th45: :: MSUALG_6:45

for S being non empty non void ManySortedSign

for A being non-empty MSAlgebra over S

for R being stable ManySortedRelation of A

for s being SortSymbol of S

for a, b being Element of A,s st a,b are_convertible_wrt R . s holds

for h being Endomorphism of A holds (h . s) . a,(h . s) . b are_convertible_wrt R . s

for A being non-empty MSAlgebra over S

for R being stable ManySortedRelation of A

for s being SortSymbol of S

for a, b being Element of A,s st a,b are_convertible_wrt R . s holds

for h being Endomorphism of A holds (h . s) . a,(h . s) . b are_convertible_wrt R . s

proof end;

theorem Th46: :: MSUALG_6:46

for S being non empty non void ManySortedSign

for A being non-empty MSAlgebra over S

for R being stable ManySortedRelation of A holds EqCl (R,A) is stable

for A being non-empty MSAlgebra over S

for R being stable ManySortedRelation of A holds EqCl (R,A) is stable

proof end;

registration

let S be non empty non void ManySortedSign ;

let A be non-empty MSAlgebra over S;

let R be stable ManySortedRelation of A;

coherence

EqCl (R,A) is stable by Th46;

end;
let A be non-empty MSAlgebra over S;

let R be stable ManySortedRelation of A;

coherence

EqCl (R,A) is stable by Th46;

theorem Th47: :: MSUALG_6:47

for S being non empty non void ManySortedSign

for A being non-empty MSAlgebra over S

for R being invariant ManySortedRelation of A

for s1, s2 being SortSymbol of S

for a, b being Element of A,s1 st a,b are_convertible_wrt R . s1 holds

for t being Function st t is_e.translation_of A,s1,s2 holds

t . a,t . b are_convertible_wrt R . s2

for A being non-empty MSAlgebra over S

for R being invariant ManySortedRelation of A

for s1, s2 being SortSymbol of S

for a, b being Element of A,s1 st a,b are_convertible_wrt R . s1 holds

for t being Function st t is_e.translation_of A,s1,s2 holds

t . a,t . b are_convertible_wrt R . s2

proof end;

theorem Th48: :: MSUALG_6:48

for S being non empty non void ManySortedSign

for A being non-empty MSAlgebra over S

for R being invariant ManySortedRelation of A holds EqCl (R,A) is invariant

for A being non-empty MSAlgebra over S

for R being invariant ManySortedRelation of A holds EqCl (R,A) is invariant

proof end;

registration

let S be non empty non void ManySortedSign ;

let A be non-empty MSAlgebra over S;

let R be invariant ManySortedRelation of A;

coherence

EqCl (R,A) is invariant by Th48;

end;
let A be non-empty MSAlgebra over S;

let R be invariant ManySortedRelation of A;

coherence

EqCl (R,A) is invariant by Th48;

theorem Th49: :: MSUALG_6:49

for S being non empty set

for A being V16() ManySortedSet of S

for R, E being ManySortedRelation of A st ( for s being Element of S

for a, b being Element of A . s holds

( [a,b] in E . s iff a,b are_convertible_wrt R . s ) ) holds

E is MSEquivalence_Relation-like

for A being V16() ManySortedSet of S

for R, E being ManySortedRelation of A st ( for s being Element of S

for a, b being Element of A . s holds

( [a,b] in E . s iff a,b are_convertible_wrt R . s ) ) holds

E is MSEquivalence_Relation-like

proof end;

theorem Th50: :: MSUALG_6:50

for S being non empty non void ManySortedSign

for A being non-empty MSAlgebra over S

for R, E being ManySortedRelation of A st ( for s being SortSymbol of S

for a, b being Element of A,s holds

( [a,b] in E . s iff a,b are_convertible_wrt (TRS R) . s ) ) holds

E is EquationalTheory of A

for A being non-empty MSAlgebra over S

for R, E being ManySortedRelation of A st ( for s being SortSymbol of S

for a, b being Element of A,s holds

( [a,b] in E . s iff a,b are_convertible_wrt (TRS R) . s ) ) holds

E is EquationalTheory of A

proof end;

theorem Th51: :: MSUALG_6:51

for S being non empty set

for A being V16() ManySortedSet of S

for R being ManySortedRelation of A

for E being MSEquivalence_Relation-like ManySortedRelation of A st R c= E holds

for s being Element of S

for a, b being Element of A . s st a,b are_convertible_wrt R . s holds

[a,b] in E . s

for A being V16() ManySortedSet of S

for R being ManySortedRelation of A

for E being MSEquivalence_Relation-like ManySortedRelation of A st R c= E holds

for s being Element of S

for a, b being Element of A . s st a,b are_convertible_wrt R . s holds

[a,b] in E . s

proof end;

definition

let S be non empty non void ManySortedSign ;

let A be non-empty MSAlgebra over S;

let R be ManySortedRelation of the Sorts of A;

for b_{1}, b_{2} being EquationalTheory of A st R c= b_{1} & ( for Q being EquationalTheory of A st R c= Q holds

b_{1} c= Q ) & R c= b_{2} & ( for Q being EquationalTheory of A st R c= Q holds

b_{2} c= Q ) holds

b_{1} = b_{2}

ex b_{1} being EquationalTheory of A st

( R c= b_{1} & ( for Q being EquationalTheory of A st R c= Q holds

b_{1} c= Q ) )

end;
let A be non-empty MSAlgebra over S;

let R be ManySortedRelation of the Sorts of A;

func EqTh R -> EquationalTheory of A means :Def15: :: MSUALG_6:def 15

( R c= it & ( for Q being EquationalTheory of A st R c= Q holds

it c= Q ) );

uniqueness ( R c= it & ( for Q being EquationalTheory of A st R c= Q holds

it c= Q ) );

for b

b

b

b

proof end;

existence ex b

( R c= b

b

proof end;

:: deftheorem Def15 defines EqTh MSUALG_6:def 15 :

for S being non empty non void ManySortedSign

for A being non-empty MSAlgebra over S

for R being ManySortedRelation of the Sorts of A

for b_{4} being EquationalTheory of A holds

( b_{4} = EqTh R iff ( R c= b_{4} & ( for Q being EquationalTheory of A st R c= Q holds

b_{4} c= Q ) ) );

for S being non empty non void ManySortedSign

for A being non-empty MSAlgebra over S

for R being ManySortedRelation of the Sorts of A

for b

( b

b

theorem :: MSUALG_6:52

for S being non empty non void ManySortedSign

for A being non-empty MSAlgebra over S

for R being ManySortedRelation of A holds

( EqCl (R,A) c= EqTh R & InvCl R c= EqTh R & StabCl R c= EqTh R & TRS R c= EqTh R )

for A being non-empty MSAlgebra over S

for R being ManySortedRelation of A holds

( EqCl (R,A) c= EqTh R & InvCl R c= EqTh R & StabCl R c= EqTh R & TRS R c= EqTh R )

proof end;

theorem :: MSUALG_6:53

for S being non empty non void ManySortedSign

for A being non-empty MSAlgebra over S

for R being ManySortedRelation of A

for s being SortSymbol of S

for a, b being Element of A,s holds

( [a,b] in (EqTh R) . s iff a,b are_convertible_wrt (TRS R) . s )

for A being non-empty MSAlgebra over S

for R being ManySortedRelation of A

for s being SortSymbol of S

for a, b being Element of A,s holds

( [a,b] in (EqTh R) . s iff a,b are_convertible_wrt (TRS R) . s )

proof end;

theorem :: MSUALG_6:54

for S being non empty non void ManySortedSign

for A being non-empty MSAlgebra over S

for R being ManySortedRelation of A holds EqTh R = EqCl ((TRS R),A)

for A being non-empty MSAlgebra over S

for R being ManySortedRelation of A holds EqTh R = EqCl ((TRS R),A)

proof end;