Volume 8, 1996

University of Bialystok

Copyright (c) 1996 Association of Mizar Users

### The abstract of the Mizar article:

### Translations, Endomorphisms, and Stable Equational Theories

**by****Grzegorz Bancerek**- Received February 9, 1996
- MML identifier: MSUALG_6

- [ Mizar article, MML identifier index ]

environ vocabulary MSUALG_1, FUNCT_1, PBOOLE, PRALG_1, MSUALG_3, RELAT_1, BOOLE, AMI_1, CARD_3, QC_LANG1, ZF_REFLE, MOD_4, ALG_1, TDGROUP, FUNCT_4, REWRITE1, FINSEQ_1, FUNCT_7, FUNCT_2, MSUALG_4, CIRCUIT2, EQREL_1, MCART_1, MSUALG_5, MSUALG_6, FINSEQ_4, PARTFUN1, RELAT_2; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, XREAL_0, NAT_1, MCART_1, STRUCT_0, RELAT_1, RELAT_2, RELSET_1, EQREL_1, REWRITE1, FUNCT_1, PARTFUN1, FUNCT_2, FINSEQ_1, CARD_3, FINSEQ_4, PBOOLE, PRALG_1, MSUALG_1, MSUALG_3, MSUALG_4, MSUALG_5, FUNCT_7; constructors NAT_1, MCART_1, REWRITE1, MSUALG_3, MSUALG_5, FUNCT_7, FINSEQ_4, MEMBERED, EQREL_1, PARTFUN1; clusters FUNCT_1, PBOOLE, PRALG_1, RELSET_1, STRUCT_0, MSUALG_1, REWRITE1, MSUALG_3, MSUALG_4, MSUALG_5, ALTCAT_1, FUNCT_7, FINSEQ_1, XREAL_0, ARYTM_3, FUNCT_2, NUMBERS, EQREL_1, PARTFUN1; requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM; begin :: Endomorphisms and translations 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; definition let I be set; let A be ManySortedSet of I; let h1,h2 be ManySortedFunction of A,A; redefine func h2**h1 -> ManySortedFunction of A,A; end; theorem :: MSUALG_6:1 for S being non empty non void ManySortedSign for A being MSAlgebra over S for o being OperSymbol of S, a being set st a in Args(o,A) holds a is Function; theorem :: MSUALG_6:2 for S being non empty non void ManySortedSign for A being MSAlgebra over S for o being OperSymbol of S, 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); definition let S be non empty non void ManySortedSign; let A be MSAlgebra over S; attr A is feasible means :: MSUALG_6:def 1 for o being OperSymbol of S st Args(o,A) <> {} holds Result(o,A) <> {}; end; theorem :: 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 Nat st i in dom the_arity_of o holds (the Sorts of A).((the_arity_of o)/.i) <> {}; definition let S be non empty non void ManySortedSign; cluster non-empty -> feasible MSAlgebra over S; end; definition let S be non empty non void ManySortedSign; cluster non-empty MSAlgebra over S; end; definition let S be non empty non void ManySortedSign; let A be MSAlgebra over S; mode Endomorphism of A -> ManySortedFunction of A,A means :: MSUALG_6:def 2 it is_homomorphism A,A; end; reserve S for non empty non void ManySortedSign, A for MSAlgebra over S; theorem :: MSUALG_6:4 id the Sorts of A is Endomorphism of A; theorem :: MSUALG_6:5 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; theorem :: MSUALG_6:6 for h1,h2 being Endomorphism of A holds h2**h1 is Endomorphism of A; definition let S be non empty non void ManySortedSign; let A be MSAlgebra over S; let h1,h2 be Endomorphism of A; redefine func h2**h1 -> Endomorphism of A; end; definition let S be non empty non void ManySortedSign; func TranslationRel S -> Relation of the carrier of S means :: 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 Nat st i in dom the_arity_of o & (the_arity_of o)/.i = s1; end; theorem :: MSUALG_6:7 for S being non empty non void ManySortedSign, o being OperSymbol of S for A being MSAlgebra over S, a being Function st a in Args(o,A) for i being Nat, x being Element of A,(the_arity_of o)/.i holds a+*(i,x) in Args(o,A); theorem :: MSUALG_6:8 for A1,A2 being MSAlgebra over S, h being ManySortedFunction of A1,A2 for o being OperSymbol of S st Args(o,A1) <> {} & Args(o,A2) <> {} for i being Nat st i in dom the_arity_of o 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); theorem :: MSUALG_6:9 for S being non empty non void ManySortedSign, o being OperSymbol of S for i being Nat st i in dom the_arity_of o 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) for f,g1,g2 being Function st f = a & g1 = h#a & g2 = h#b 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, o be OperSymbol of S; let i be Nat; let A be MSAlgebra over S; let a be Function; func transl(o,i,a,A) -> Function means :: 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)); end; theorem :: MSUALG_6:10 for S being non empty non void ManySortedSign, o being OperSymbol of S for i being Nat st i in dom the_arity_of o for A being feasible MSAlgebra over S, 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; definition let S be non empty non void ManySortedSign, 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 :: MSUALG_6:def 5 ex o being OperSymbol of S st the_result_sort_of o = s2 & ex i being 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); end; theorem :: MSUALG_6:11 for S being non empty non void ManySortedSign, s1,s2 being SortSymbol of S for A being feasible MSAlgebra over S, 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 <> {}; theorem :: MSUALG_6:12 for S being non empty non void ManySortedSign, s1,s2 being SortSymbol of S for A being MSAlgebra over S, f being Function st f is_e.translation_of A,s1,s2 holds [s1,s2] in TranslationRel S; theorem :: MSUALG_6:13 for S being non empty non void ManySortedSign, s1,s2 being SortSymbol of S for A being non-empty MSAlgebra over S st [s1,s2] in TranslationRel S ex f being Function st f is_e.translation_of A,s1,s2; theorem :: 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 st TranslationRel S reduces s1,s2 for q being RedSequence of TranslationRel S, p being Function-yielding FinSequence st len q = len p+1 & s1 = q.1 & s2 = q.len q & for i being Nat, f being Function, 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 <> {}); definition let S be non empty non void ManySortedSign; let A be non-empty MSAlgebra over S; let s1,s2 be SortSymbol of S such that TranslationRel S reduces s1,s2; mode Translation of A,s1,s2 -> Function of (the Sorts of A).s1,(the Sorts of A).s2 means :: MSUALG_6:def 6 ex q being RedSequence of TranslationRel S, 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 Nat, f being Function, 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; 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 for q being RedSequence of TranslationRel S, p being Function-yielding FinSequence st len q = len p+1 & s1 = q.1 & s2 = q.len q & for i being Nat, f being Function, 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; reserve A for non-empty MSAlgebra over S; theorem :: MSUALG_6:16 for s being SortSymbol of S holds id ((the Sorts of A).s) is Translation of A,s,s; theorem :: MSUALG_6:17 for s1,s2 being SortSymbol of S, 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; theorem :: MSUALG_6:18 for s1,s2,s3 being SortSymbol of S st TranslationRel S reduces s1,s2 & TranslationRel S reduces s2,s3 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 :: MSUALG_6:19 for s1,s2,s3 being SortSymbol of S st TranslationRel S reduces s1,s2 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; theorem :: MSUALG_6:20 for s1,s2,s3 being SortSymbol of S st TranslationRel S reduces s2,s3 for f being Function st f is_e.translation_of A,s1,s2 for t being Translation of A,s2,s3 holds t*f is Translation of A,s1,s3; scheme TranslationInd {S() -> non empty non void ManySortedSign, A() -> non-empty MSAlgebra over S(), P[set,set,set]}: for s1,s2 being SortSymbol of S() st TranslationRel S() reduces s1,s2 for t being Translation of A(),s1,s2 holds P[t,s1,s2] provided for s being SortSymbol of S() holds P[id ((the Sorts of A()).s),s,s] and for s1,s2,s3 being SortSymbol of S() st TranslationRel S() reduces s1,s2 for t being Translation of A(),s1,s2 st P[t,s1,s2] for f being Function st f is_e.translation_of A(),s2,s3 holds P[f*t,s1,s3]; theorem :: MSUALG_6:21 for A1,A2 being non-empty MSAlgebra over S for h being ManySortedFunction of A1,A2 st h is_homomorphism A1,A2 for o being OperSymbol of S, i being Nat st i in dom the_arity_of o 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 :: MSUALG_6:22 for h being Endomorphism of A for o being OperSymbol of S, i being Nat st i in dom the_arity_of o 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)); theorem :: MSUALG_6:23 for A1,A2 being non-empty MSAlgebra over S for h being ManySortedFunction of A1,A2 st h is_homomorphism A1,A2 for s1,s2 being SortSymbol of S, t being Function st t is_e.translation_of A1,s1,s2 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; theorem :: MSUALG_6:24 for h being Endomorphism of A for s1,s2 being SortSymbol of S, t being Function st t is_e.translation_of A,s1,s2 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; theorem :: MSUALG_6:25 for A1,A2 being non-empty MSAlgebra over S for h being ManySortedFunction of A1,A2 st h is_homomorphism A1,A2 for s1,s2 being SortSymbol of S st TranslationRel S reduces s1,s2 for t being Translation of A1,s1,s2 ex T being Translation of A2,s1,s2 st T*(h.s1) = (h.s2)*t; theorem :: MSUALG_6:26 for h being Endomorphism of A for s1,s2 being SortSymbol of S st TranslationRel S reduces s1,s2 for t being Translation of A,s1,s2 ex T being Translation of A,s1,s2 st T*(h.s1) = (h.s2)*t; begin :: Compatibility, invariantness, and stability definition let S be non empty non void ManySortedSign; let A be MSAlgebra over S; let R be ManySortedRelation of A; attr R is compatible means :: MSUALG_6:def 7 for o being OperSymbol of S, a,b being Function st a in Args(o,A) & b in Args(o,A) & (for n be 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 :: MSUALG_6:def 8 for s1,s2 being SortSymbol of S for t being Function st t is_e.translation_of A,s1,s2 for a,b being set st [a,b] in R.s1 holds [t.a, t.b] in R.s2; attr R is stable means :: MSUALG_6:def 9 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; theorem :: MSUALG_6:27 for R being MSEquivalence-like ManySortedRelation of A holds R is compatible iff R is MSCongruence of A; theorem :: MSUALG_6:28 for R being ManySortedRelation of A holds R is invariant iff for s1,s2 being SortSymbol of S st TranslationRel S reduces s1,s2 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; definition let S be non empty non void ManySortedSign; let A be non-empty MSAlgebra over S; cluster invariant -> compatible (MSEquivalence-like ManySortedRelation of A); cluster compatible -> invariant (MSEquivalence-like ManySortedRelation of A); end; definition let X be non empty set; cluster id X -> non empty; end; scheme MSRExistence {I() -> non empty set, A() -> non-empty ManySortedSet of I(), P[set,set,set]}: ex R being ManySortedRelation of A() st for i being Element of I() for a,b being Element of A().i holds [a,b] in R.i iff P[i,a,b]; scheme MSRLambdaU{I() -> set, A() -> ManySortedSet of I(), F(set) -> set}: (ex R being ManySortedRelation of A() st for i being set st i in I() holds R.i = F(i)) & for R1,R2 being ManySortedRelation of A() st (for i being set st i in I() holds R1.i = F(i)) & (for i being set st i in I() holds R2.i = F(i)) holds R1 = R2 provided for i being set st i in I() holds F(i) is Relation of A().i, A().i; definition let I be set, A be ManySortedSet of I; func id(I,A) -> ManySortedRelation of A means :: MSUALG_6:def 10 for i being set st i in I holds it.i = id (A.i); end; definition let S be non empty non void ManySortedSign; let A be non-empty MSAlgebra over S; cluster MSEquivalence-like -> non-empty ManySortedRelation of A; end; definition let S be non empty non void ManySortedSign; let A be non-empty MSAlgebra over S; cluster invariant stable MSEquivalence-like ManySortedRelation of A; end; begin :: Invariant, stable, and invariant stable closure reserve S for non empty non void ManySortedSign, A for non-empty MSAlgebra over S, R for ManySortedRelation of the Sorts of A; scheme MSRelCl {S() -> non empty non void ManySortedSign, A() -> non-empty MSAlgebra over S(), P[set,set,set], R[set], R,Q() -> ManySortedRelation of A()}: R[Q()] & R() c= Q() & for P being ManySortedRelation of A() st R[P] & R() c= P holds Q() c= P provided for R being ManySortedRelation of A() holds R[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 P[f,s1,s2] for a,b being set st [a,b] in R.s1 holds [f.a,f.b] in R.s2 and 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 P[f1,s1,s2] & P[f2,s2,s3] holds P[f2*f1,s1,s3] and for s being SortSymbol of S() holds P[id ((the Sorts of A()).s),s,s] and for s being SortSymbol of S(), a,b being Element of A(),s holds [a,b] in Q().s iff ex s' being SortSymbol of S(), f being Function of (the Sorts of A()).s',(the Sorts of A()).s, x,y being Element of A(),s' st P[f,s',s] & [x,y] in R().s' & a = f.x & b = f.y; 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; func InvCl R -> invariant ManySortedRelation of A means :: MSUALG_6:def 11 R c= it & for Q being invariant ManySortedRelation of A st R c= Q holds it c= Q; end; theorem :: MSUALG_6:29 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 s' being SortSymbol of S, x,y being Element of A,s' st ex t being Translation of A,s',s st TranslationRel S reduces s',s & [x,y] in R.s' & a = t.x & b = t.y; theorem :: MSUALG_6:30 for R being stable ManySortedRelation of A holds InvCl R is stable; 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; func StabCl R -> stable ManySortedRelation of A means :: MSUALG_6:def 12 R c= it & for Q being stable ManySortedRelation of A st R c= Q holds it c= Q; end; theorem :: MSUALG_6:31 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, h being Endomorphism of A st [x,y] in R.s & a = h.s.x & b = h.s.y; theorem :: MSUALG_6:32 InvCl StabCl R is stable; 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; func TRS R -> invariant stable ManySortedRelation of A means :: MSUALG_6:def 13 R c= it & for Q being invariant stable ManySortedRelation of A st R c= Q holds it c= Q; end; definition let S be non empty non void ManySortedSign; let A be non-empty MSAlgebra over S; let R be non-empty ManySortedRelation of A; cluster InvCl R -> non-empty; cluster StabCl R -> non-empty; cluster TRS R -> non-empty; end; theorem :: MSUALG_6:33 for R being invariant ManySortedRelation of A holds InvCl R = R; theorem :: MSUALG_6:34 for R being stable ManySortedRelation of A holds StabCl R = R; theorem :: MSUALG_6:35 for R being invariant stable ManySortedRelation of A holds TRS R = R; theorem :: MSUALG_6:36 StabCl R c= TRS R & InvCl R c= TRS R & StabCl InvCl R c= TRS R; theorem :: MSUALG_6:37 InvCl StabCl R = TRS R; theorem :: MSUALG_6:38 for R being ManySortedRelation of the Sorts of A for s being SortSymbol of S, a,b being Element of A,s holds [a,b] in (TRS R).s iff ex s' being SortSymbol of S st TranslationRel S reduces s', s & ex l,r being Element of A,s', h being Endomorphism of A, t being Translation of A, s', s st [l,r] in R.s' & a = t.(h.s'.l) & b = t.(h.s'.r); begin :: Equational theory theorem :: 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 symmetric transitive; theorem :: MSUALG_6:40 for A being set, R being Relation of A for E being Equivalence_Relation of A st R c= E for a,b being set st a in A & b in A & a,b are_convertible_wrt R holds [a,b] in E; theorem :: MSUALG_6:41 for A being non empty set, 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; theorem :: MSUALG_6:42 for S being non empty set, A being non-empty 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; definition let S be non empty non void ManySortedSign; let A be non-empty MSAlgebra over S; mode EquationalTheory of A is stable invariant MSEquivalence-like ManySortedRelation of A; let R be ManySortedRelation of A; func EqCl(R,A) -> MSEquivalence-like ManySortedRelation of A equals :: MSUALG_6:def 14 EqCl R; end; theorem :: MSUALG_6:43 for R being ManySortedRelation of A holds R c= EqCl(R,A); theorem :: MSUALG_6:44 for R being ManySortedRelation of A for E being MSEquivalence-like ManySortedRelation of A st R c= E holds EqCl(R,A) c= E; theorem :: MSUALG_6:45 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 for h being Endomorphism of A holds h.s.a, h.s.b are_convertible_wrt R.s; theorem :: MSUALG_6:46 for R being stable ManySortedRelation of A holds EqCl(R,A) is stable; definition let S,A; let R be stable ManySortedRelation of A; cluster EqCl(R,A) -> stable; end; theorem :: MSUALG_6:47 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 for t being Function st t is_e.translation_of A,s1,s2 holds t.a, t.b are_convertible_wrt R.s2; theorem :: MSUALG_6:48 for R being invariant ManySortedRelation of A holds EqCl(R,A) is invariant; definition let S,A; let R be invariant ManySortedRelation of A; cluster EqCl(R,A) -> invariant; end; theorem :: MSUALG_6:49 for S being non empty set, A being non-empty 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; theorem :: MSUALG_6:50 for R,E being ManySortedRelation of A st for s being SortSymbol of S, 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; theorem :: MSUALG_6:51 for S being non empty set, A being non-empty ManySortedSet of S for R being ManySortedRelation of A for E being MSEquivalence_Relation-like ManySortedRelation of A st R c= E 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; 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; func EqTh R -> EquationalTheory of A means :: MSUALG_6:def 15 R c= it & for Q being EquationalTheory of A st R c= Q holds it c= Q; end; theorem :: MSUALG_6:52 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; theorem :: MSUALG_6:53 for R being ManySortedRelation of A for s being SortSymbol of S, a,b being Element of A,s holds [a,b] in (EqTh R).s iff a,b are_convertible_wrt (TRS R).s; theorem :: MSUALG_6:54 for R being ManySortedRelation of A holds EqTh R = EqCl(TRS R,A);

Back to top