:: Translations, Endomorphisms, and Stable Equational Theories
:: by Grzegorz Bancerek
::
:: Received February 9, 1996
:: Copyright (c) 1996-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, XBOOLE_0, MSUALG_1, SUBSET_1, FUNCT_1, PBOOLE, MEMBER_1,
RELAT_1, STRUCT_0, CARD_3, MARGREL1, PARTFUN1, MOD_4, MSUALG_3, NAT_1,
FUNCT_4, RLTOPSP1, TARSKI, REWRITE1, FUNCOP_1, FINSEQ_1, ARYTM_3,
FUNCT_7, CARD_1, XXREAL_0, ORDINAL4, MSUALG_4, CIRCUIT2, MCART_1,
ZFMISC_1, EQREL_1, RELAT_2, MSUALG_5, MSUALG_6;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0,
NAT_1, XTUPLE_0, MCART_1, STRUCT_0, RELAT_1, RELAT_2, RELSET_1, EQREL_1,
REWRITE1, FUNCT_1, PBOOLE, PARTFUN1, FUNCT_2, FINSEQ_1, CARD_3, FUNCOP_1,
MSUALG_1, MSUALG_3, MSUALG_4, MSUALG_5, FUNCT_7, XXREAL_0;
constructors NAT_1, NAT_D, REWRITE1, FUNCT_7, MSUALG_3, MSUALG_5, RELSET_1,
XTUPLE_0;
registrations XBOOLE_0, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, FUNCOP_1,
XXREAL_0, XREAL_0, NAT_1, FINSEQ_1, PBOOLE, REWRITE1, FUNCT_7, STRUCT_0,
MSUALG_1, MSUALG_3, MSUALG_4, MSUALG_5, ORDINAL1, CARD_1, RELSET_1,
XTUPLE_0;
requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
definitions TARSKI, RELAT_1, REWRITE1, PBOOLE, MSUALG_3, MSUALG_4, FUNCT_7,
FUNCOP_1;
expansions TARSKI, REWRITE1, FUNCT_1, PBOOLE, MSUALG_3;
theorems TARSKI, NAT_1, ZFMISC_1, RELAT_1, RELSET_1, EQREL_1, FUNCT_1,
FINSEQ_1, FINSEQ_3, FUNCT_2, CARD_3, FUNCT_7, REWRITE1, PBOOLE, PRALG_2,
MSUALG_3, MSUALG_4, MSUALG_5, FINSEQ_5, XBOOLE_0, PARTFUN1, RELAT_2,
ORDERS_1, XREAL_1, XXREAL_0, ORDINAL1;
schemes NAT_1, RECDEF_1, RELSET_1, FUNCT_1, FINSEQ_1, CARD_3, CLASSES1,
PBOOLE, PUA2MSS1;
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; :: redefines ** (PBOOLE, definition)
coherence
proof
set h = h2**h1;
A1: dom h2 = I by PARTFUN1:def 2;
dom h1 = I by PARTFUN1:def 2;
then
A2: dom h = I /\ I by A1,PBOOLE:def 19
.= I;
then reconsider h as ManySortedSet of I by PARTFUN1:def 2,RELAT_1:def 18;
h is ManySortedFunction of A,A
proof
let i be object;
assume
A3: i in I;
then reconsider f = h1.i, g = h2.i as Function of A.i, A.i by
PBOOLE:def 15;
h.i = g*f by A2,A3,PBOOLE:def 19;
hence thesis;
end;
hence thesis;
end;
end;
theorem Th1:
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
proof
let S be non empty non void ManySortedSign;
let A be MSAlgebra over S;
let o be OperSymbol of S;
let x be set;
assume x in Args(o,A);
then x in product((the Sorts of A)*the_arity_of o) by PRALG_2:3;
then ex f being Function st x = f & dom f = dom ((the Sorts of A)*
the_arity_of o) &
for y be object st y in dom ((the Sorts of A)*the_arity_of o)
holds f.y in ((the Sorts of A)*the_arity_of o).y by CARD_3:def 5;
hence thesis;
end;
theorem Th2:
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)
proof
let S be non empty non void ManySortedSign;
let A be MSAlgebra over S;
let o be OperSymbol of S;
let x be Function;
assume x in Args(o,A);
then x in product((the Sorts of A) * (the_arity_of o)) by PRALG_2:3;
then
A1: ex f being Function st x = f & dom f = dom ((the Sorts of A)*
the_arity_of o) &
for y be object st y in dom ((the Sorts of A)*the_arity_of o)
holds f.y in ((the Sorts of A)*the_arity_of o).y by CARD_3:def 5;
hence
A2: dom x = dom the_arity_of o by PARTFUN1:def 2;
let y be set;
assume
A3: y in dom the_arity_of o;
then
A4: (the_arity_of o).y = (the_arity_of o)/.y by PARTFUN1:def 6;
x.y in ((the Sorts of A)*the_arity_of o).y by A1,A2,A3;
hence thesis by A3,A4,FUNCT_1:13;
end;
definition
let S be non empty non void ManySortedSign;
let A be MSAlgebra over S;
attr A is feasible means
: Def1:
for o being OperSymbol of S st Args(o,A) <> {} holds Result(o,A) <> {};
end;
theorem Th3:
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) <> {}
proof
let S be non empty non void ManySortedSign;
let o be OperSymbol of S;
let A be MSAlgebra over S;
A1: dom ((the Sorts of A)*the_arity_of o) = dom the_arity_of o by PRALG_2:3;
A2: Args(o,A) = product ((the Sorts of A)*the_arity_of o) by PRALG_2:3;
hereby
assume
A3: Args(o,A) <> {};
let i be Element of NAT;
assume
A4: i in dom the_arity_of o;
then
A5: (the Sorts of A).((the_arity_of o).i) = ((the Sorts of A)*the_arity_of
o ).i by FUNCT_1:13;
A6: (the_arity_of o)/.i = (the_arity_of o).i by A4,PARTFUN1:def 6;
((the Sorts of A)*the_arity_of o).i in rng ((the Sorts of A)*
the_arity_of o) by A1,A4,FUNCT_1:def 3;
hence (the Sorts of A).((the_arity_of o)/.i) <> {} by A2,A3,A5,A6,CARD_3:26
;
end;
assume
A7: for i being Element of NAT st i in dom the_arity_of o holds (the
Sorts of A).((the_arity_of o)/.i) <> {};
assume Args(o,A) = {};
then {} in rng ((the Sorts of A)*the_arity_of o) by A2,CARD_3:26;
then consider x being object such that
A8: x in dom the_arity_of o and
A9: {} = ((the Sorts of A)*the_arity_of o).x by A1,FUNCT_1:def 3;
reconsider x as Element of NAT by A8;
A10: (the_arity_of o)/.x = (the_arity_of o).x by A8,PARTFUN1:def 6;
(the Sorts of A).((the_arity_of o)/.x) <> {} by A7,A8;
hence thesis by A8,A9,A10,FUNCT_1:13;
end;
registration
let S be non empty non void ManySortedSign;
cluster non-empty -> feasible for MSAlgebra over S;
coherence;
end;
registration
let S be non empty non void ManySortedSign;
cluster non-empty for MSAlgebra over S;
existence
proof
set A = the non-empty MSAlgebra over S;
take A;
thus thesis;
end;
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
: Def2:
it is_homomorphism A,A;
existence
proof
take id the Sorts of A;
thus thesis by MSUALG_3:9;
end;
end;
reserve S for non empty non void ManySortedSign,
A for MSAlgebra over S;
theorem Th4:
id the Sorts of A is Endomorphism of A
proof
thus id the Sorts of A is_homomorphism A,A by MSUALG_3:9;
end;
theorem Th5:
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
let h1,h2 be ManySortedFunction of A,A;
set h = h2**h1;
let o be OperSymbol of S;
let a be Element of Args(o,A);
assume
A1: a in Args(o,A);
then reconsider f = a, b = h1#a, c = h2#(h1#a) as Function by Th1;
A2: dom f = dom the_arity_of o by A1,Th2;
now
A3: dom ((the Sorts of A)*the_arity_of o) = dom the_arity_of o by PRALG_2:3;
A4: Args(o,A) = product ((the Sorts of A)*the_arity_of o) by PRALG_2:3;
let i be Nat;
reconsider f1 = h1.((the_arity_of o)/.i), f2 = h2.((the_arity_of o)/.i) as
Function of (the Sorts of A).((the_arity_of o)/.i), (the Sorts of A).((
the_arity_of o)/.i);
A5: h.((the_arity_of o)/.i) = f2*f1 by MSUALG_3:2;
assume
A6: i in dom f;
then
A7: f1.(f.i) = b.i by A1,MSUALG_3:24;
dom b = dom the_arity_of o by A1,Th2;
then
A8: f2.(b.i) = c.i by A1,A2,A6,MSUALG_3:24;
A9: (the Sorts of A).((the_arity_of o).i) = ((the Sorts of A)*
the_arity_of o).i by A2,A6,FUNCT_1:13;
(the_arity_of o)/.i = (the_arity_of o).i by A2,A6,PARTFUN1:def 6;
then f.i in (the Sorts of A).((the_arity_of o)/.i) by A1,A2,A6,A4,A3,A9,
CARD_3:9;
hence c.i = (h.((the_arity_of o)/.i)).(f.i) by A5,A7,A8,FUNCT_2:15;
end;
hence thesis by A1,MSUALG_3:24;
end;
theorem Th6:
for h1,h2 being Endomorphism of A holds h2**h1 is Endomorphism of A
proof
let h1,h2 be Endomorphism of A;
let o be OperSymbol of S such that
A1: Args (o,A) <> {};
set h = h2**h1;
let x be Element of Args(o,A);
A2: Result(o,A) = (the Sorts of A).the_result_sort_of o by PRALG_2:3;
A3: h2 is_homomorphism A,A by Def2;
reconsider f1 = h1.the_result_sort_of o, f2 = h2.the_result_sort_of o, f = h
.the_result_sort_of o as Function of (the Sorts of A).the_result_sort_of o, (
the Sorts of A).the_result_sort_of o;
A4: h1 is_homomorphism A,A by Def2;
per cases;
suppose
A5: (the Sorts of A).the_result_sort_of o = {};
then dom f = {};
then
A6: f.(Den(o,A).x) = {} by FUNCT_1:def 2;
dom Den(o,A) = {} by A2,A5;
hence thesis by A6,FUNCT_1:def 2;
end;
suppose
A7: (the Sorts of A).the_result_sort_of o <> {};
h.the_result_sort_of o = f2*f1 by MSUALG_3:2;
then
(h.(the_result_sort_of o)).(Den(o,A).x) = f2.(f1.(Den(o,A).x)) by A1,A2,A7,
FUNCT_2:5,15
.= (h2.(the_result_sort_of o)).(Den(o,A).(h1#x)) by A4,A1
.= Den(o,A).(h2#(h1#x)) by A3,A1;
hence thesis by A1,Th5;
end;
end;
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; :: redefines ** (PBOOLE, definition)
coherence by Th6;
end;
definition
let S be non empty non void ManySortedSign;
func TranslationRel S -> Relation of the carrier of S means
: Def3:
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
proof
defpred P[set,set] means ex o being OperSymbol of S st the_result_sort_of
o = $2 & ex i being Element of NAT st i in dom the_arity_of o & (the_arity_of o
)/.i = $1;
ex R being Relation of the carrier of S,the carrier of S st for x
being SortSymbol of S, y being SortSymbol of S holds [x,y] in R iff P[x,y] from
RELSET_1:sch 2;
hence thesis;
end;
correctness
proof
defpred P[set,set] means ex o being OperSymbol of S st the_result_sort_of
o = $2 & ex i being Element of NAT st i in dom the_arity_of o & (the_arity_of o
)/.i = $1;
for R1, R2 being Relation of the carrier of S, the carrier of S st (
for x being SortSymbol of S, y being SortSymbol of S holds [x,y] in R1 iff P[x,
y]) & (for x being SortSymbol of S, y being SortSymbol of S holds [x,y] in R2
iff P[x,y]) holds R1 = R2 from PUA2MSS1:sch 2;
hence thesis;
end;
end;
theorem Th7:
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)
proof
let S be non empty non void ManySortedSign, o be OperSymbol of S;
let A be MSAlgebra over S;
A1: dom ((the Sorts of A)*the_arity_of o) = dom the_arity_of o by PRALG_2:3;
let a be Function such that
A2: a in Args(o,A);
A3: dom a = dom the_arity_of o by A2,Th2;
let i be Nat;
let x be Element of A,(the_arity_of o)/.i;
A4: Args(o,A) = product ((the Sorts of A)*the_arity_of o) by PRALG_2:3;
A5: now
let j be object;
assume
A6: j in dom a;
then reconsider k = j as Element of NAT by A3;
A7: ((the Sorts of A)*the_arity_of o).k = (the Sorts of A).((the_arity_of
o) .k) by A3,A6,FUNCT_1:13;
A8: (the_arity_of o)/.k = (the_arity_of o).k by A3,A6,PARTFUN1:def 6;
then
A9: ((the Sorts of A)*the_arity_of o).j <> {} by A2,A3,A6,A7,Th3;
per cases;
suppose
A10: j = i;
then (a+*(i,x)).j = x by A6,FUNCT_7:31;
hence (a+*(i,x)).j in ((the Sorts of A)*the_arity_of o).j by A8,A7,A9,A10
;
end;
suppose
j <> i;
then (a+*(i,x)).j = a.j by FUNCT_7:32;
hence
(a+*(i,x)).j in ((the Sorts of A)*the_arity_of o).j by A2,A4,A1,A3,A6,
CARD_3:9;
end;
end;
dom (a+*(i,x)) = dom a by FUNCT_7:30;
hence thesis by A4,A1,A3,A5,CARD_3:9;
end;
theorem Th8:
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 Element of 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)
proof
let A1,A2 be MSAlgebra over S, h be ManySortedFunction of A1,A2;
let o be OperSymbol of S such that
A1: Args(o,A1) <> {} and
A2: Args(o,A2) <> {};
let i be Element of NAT;
assume
A3: i in dom the_arity_of o;
then
A4: (the Sorts of A2).((the_arity_of o)/.i) <> {} by A2,Th3;
(the Sorts of A1).((the_arity_of o)/.i) <> {} by A1,A3,Th3;
hence thesis by A4,FUNCT_2:5;
end;
theorem Th9:
for S being non empty non void ManySortedSign, o being OperSymbol
of S for i being Element of 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)
proof
let S be non empty non void ManySortedSign, o be OperSymbol of S;
let i be Element of NAT such that
A1: i in dom the_arity_of o;
let A1,A2 be MSAlgebra over S;
let h be ManySortedFunction of A1,A2;
let a,b be Element of Args(o,A1) such that
A2: a in Args(o,A1) and
A3: h#a in Args(o,A2);
reconsider f2 = b as Function by A2,Th1;
A4: dom f2 = dom the_arity_of o by A2,Th2;
let f,g1,g2 be Function such that
A5: f = a and
A6: g1 = h#a and
A7: g2 = h#b;
reconsider g3 = g1+*(i,g2.i) as Function;
A8: dom f = dom the_arity_of o by A2,A5,Th2;
let x be Element of A1,((the_arity_of o)/.i) such that
A9: b = f+*(i,x);
f2.i = x by A1,A9,A8,FUNCT_7:31;
hence g2.i = h.((the_arity_of o)/.i).x by A1,A2,A3,A7,A4,MSUALG_3:24;
then g2.i in (the Sorts of A2).((the_arity_of o)/.i) by A1,A2,A3,Th8;
then g1+*(i,g2.i) in Args(o,A2) by A3,A6,Th7;
then
A10: dom g3 = dom the_arity_of o by Th2;
A11: now
let z be set;
assume that
A12: z in dom the_arity_of o and
A13: z <> i;
reconsider j = z as Element of NAT by A12;
A14: f2.j = f.j by A9,A13,FUNCT_7:32;
g2.j = h.((the_arity_of o)/.j).(f2.j) by A2,A3,A7,A4,A12,MSUALG_3:24;
hence g2.z = g1.z by A2,A3,A5,A6,A8,A12,A14,MSUALG_3:24;
end;
A15: dom g1 = dom the_arity_of o by A3,A6,Th2;
A16: now
let z be object;
assume
A17: z in dom the_arity_of o;
per cases;
suppose
z = i;
hence g2.z = (g1+*(i,g2.i)).z by A1,A15,FUNCT_7:31;
end;
suppose
A18: z <> i;
then g2.z = g1.z by A11,A17;
hence g2.z = (g1+*(i,g2.i)).z by A18,FUNCT_7:32;
end;
end;
dom g2 = dom the_arity_of o by A3,A7,Th2;
hence thesis by A7,A10,A16,FUNCT_1:2;
end;
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
: Def4:
dom it = (the Sorts of A).((the_arity_of o)/.i) &
for x being object st x in (the Sorts of A).((the_arity_of o
)/.i) holds it.x = Den(o,A).(a+*(i,x));
existence
proof
deffunc F(object)= Den(o,A).(a+*(i,$1));
ex f being Function st dom f = (the Sorts of A).((the_arity_of o)/.i)
& for x be object st x in (the Sorts of A).((the_arity_of o)/.i)
holds f.x = F(x)
from FUNCT_1:sch 3;
hence thesis;
end;
uniqueness
proof
let f1,f2 be Function such that
A1: dom f1 = (the Sorts of A).((the_arity_of o)/.i) and
A2: for x being object st x in (the Sorts of A).((the_arity_of o)/.i)
holds f1.x = Den(o,A).(a+*(i,x)) and
A3: dom f2 = (the Sorts of A).((the_arity_of o)/.i) and
A4: for x being object st x in (the Sorts of A).((the_arity_of o)/.i)
holds f2.x = Den(o,A).(a+*(i,x));
now
let x be object;
assume
A5: x in (the Sorts of A).((the_arity_of o)/.i);
then f1.x = Den(o,A).(a+*(i,x)) by A2;
hence f1.x = f2.x by A4,A5;
end;
hence thesis by A1,A3;
end;
end;
theorem Th10:
for S being non empty non void ManySortedSign, o being
OperSymbol of S for i being Element of NAT 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
proof
let S be non empty non void ManySortedSign, o be OperSymbol of S;
let i be Element of NAT;
let A be feasible MSAlgebra over S;
let a be Function;
assume
A1: a in Args(o,A);
then
A2: Result(o,A) <> {} by Def1;
A3: dom transl(o,i,a,A) = (the Sorts of A).((the_arity_of o)/.i) by Def4;
A4: rng transl(o,i,a,A) c= (the Sorts of A).the_result_sort_of o
proof
let x be object;
assume x in rng transl(o,i,a,A);
then consider y being object such that
A5: y in dom transl(o,i,a,A) and
A6: x = transl(o,i,a,A).y by FUNCT_1:def 3;
reconsider y as Element of A,((the_arity_of o)/.i) by A5,Def4;
set b = a+*(i,y);
A7: Den(o,A).b in Result(o,A) by A1,A2,Th7,FUNCT_2:5;
x = Den(o,A).b by A3,A5,A6,Def4;
hence thesis by A7,PRALG_2:3;
end;
Result(o,A) = (the Sorts of A).(the_result_sort_of o) by PRALG_2:3;
hence thesis by A2,A3,A4,FUNCT_2:def 1,RELSET_1:4;
end;
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
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);
end;
theorem Th11:
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 <> {}
proof
let S be non empty non void ManySortedSign, s1,s2 be SortSymbol of S;
let A be feasible MSAlgebra over S;
let f be Function;
assume f is_e.translation_of A,s1,s2;
then consider o being OperSymbol of S such that
A1: the_result_sort_of o = s2 and
A2: 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);
Result(o,A) = (the Sorts of A).the_result_sort_of o by PRALG_2:3;
hence thesis by A1,A2,Def1,Th3,Th10;
end;
theorem Th12:
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
by Def3;
theorem
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
proof
let S be non empty non void ManySortedSign, s1,s2 be SortSymbol of S;
let A be non-empty MSAlgebra over S;
assume [s1,s2] in TranslationRel S;
then consider o being OperSymbol of S such that
A1: the_result_sort_of o = s2 and
A2: ex i being Element of NAT st i in dom the_arity_of o & (the_arity_of
o)/.i = s1 by Def3;
set a = the Element of Args(o,A);
consider i being Element of NAT such that
A3: i in dom the_arity_of o and
A4: (the_arity_of o)/.i = s1 by A2;
take transl(o,i,a,A), o;
thus thesis by A1,A3,A4;
end;
theorem Th14:
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, p being Function-yielding FinSequence st len q
= len p+1 & s1 = q.1 & s2 = q.len q & for i being (Element of 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 <> {})
proof
let S be non empty non void ManySortedSign;
let A be feasible MSAlgebra over S;
let s1,s2 be SortSymbol of S;
let q be RedSequence of TranslationRel S, p be Function-yielding FinSequence
such that
A1: len q = len p+1 and
A2: s1 = q.1 and
A3: s2 = q.len q and
A4: for i being (Element of 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;
per cases;
suppose
A5: p = {};
then
A6: len p = 0;
compose(p, (the Sorts of A).s1) = id ((the Sorts of A).s1) by A5,FUNCT_7:39
;
hence thesis by A1,A2,A3,A6;
end;
suppose
p <> {};
then
A7: rng p <> {};
then
A8: 1 in dom p by FINSEQ_3:32;
then
A9: 1+1 in dom q by A1,FUNCT_7:22;
1 in dom q by A1,A8,FUNCT_7:22;
then [q.1,q.(1+1)] in TranslationRel S by A9,REWRITE1:def 2;
then reconsider q1 = q.1, q2 = q.(1+1) as SortSymbol of S by ZFMISC_1:87;
deffunc F(set) = (the Sorts of A).(q.$1);
reconsider f = p.1 as Function;
A10: dom q = Seg len q by FINSEQ_1:def 3;
consider pp being FinSequence such that
A11: len pp = len q and
A12: for i being Nat st i in dom pp holds pp.i = F(i) from FINSEQ_1:
sch 2;
defpred P[Nat] means $1 in dom pp implies pp.$1 is not empty;
A13: dom pp = Seg len q by A11,FINSEQ_1:def 3;
f is_e.translation_of A,q1,q2 by A4,A7,FINSEQ_3:32;
then
A14: (the Sorts of A).q1 <> {} by Th11;
A15: for i be Nat st P[i] holds P[(i+1)]
proof
let i be Nat such that
i in dom pp implies pp.i is not empty and
A16: i+1 in dom pp;
A17: i <= i+1 by NAT_1:11;
i+1 <= len pp by A16,FINSEQ_3:25;
then
A18: i <= len pp by A17,XXREAL_0:2;
per cases;
suppose
i = 0;
hence thesis by A14,A12,A16;
end;
suppose
i > 0;
then i >= 0+1 by NAT_1:13;
then
A19: i in dom pp by A18,FINSEQ_3:25;
then [q.i,q.(i+1)] in TranslationRel S by A10,A13,A16,REWRITE1:def 2;
then reconsider s1 = q.i, s2 = q.(i+1) as SortSymbol of S by
ZFMISC_1:87;
reconsider f = p.i as Function;
i in dom p by A1,A11,A16,A19,FUNCT_7:22;
then
A20: f is_e.translation_of A,s1,s2 by A4;
pp.(i+1) = (the Sorts of A).s2 by A12,A16;
hence thesis by A20,Th11;
end;
end;
A21: P[ 0 ] by FINSEQ_3:25;
A22: for i being Nat holds P[i] from NAT_1:sch 2(A21,A15);
A23: pp is non-empty
by A22;
A24: dom pp = Seg len q by A11,FINSEQ_1:def 3;
reconsider pp as non empty non-empty FinSequence by A11,A23;
A25: dom p = Seg len p by FINSEQ_1:def 3;
p is FuncSequence of pp
proof
thus len p+1 = len pp by A1,A11;
let j be Nat;
reconsider f = p.j as Function;
assume
A26: j in dom p;
then
A27: j >= 1 by A25,FINSEQ_1:1;
then
A28: j+1 >= 1 by NAT_1:13;
A29: j <= len p by A25,A26,FINSEQ_1:1;
then j <= len q by A1,NAT_1:13;
then
A30: j in Seg len q by A27,FINSEQ_1:1;
j+1 <= len q by A1,A29,XREAL_1:6;
then
A31: j+1 in Seg len q by A28,FINSEQ_1:1;
then [q.j,q.(j+1)] in TranslationRel S by A10,A30,REWRITE1:def 2;
then reconsider s1 = q.j, s2 = q.(j+1) as SortSymbol of S by ZFMISC_1:87;
A32: pp.(j+1) = (the Sorts of A).s2 by A12,A24,A31;
A33: f is_e.translation_of A,s1,s2 by A4,A26;
then
A34: p.j is Function of (the Sorts of A).s1,(the Sorts of A).s2 by Th11;
A35: (the Sorts of A).s2 <> {} by A33,Th11;
pp.j = (the Sorts of A).s1 by A12,A24,A30;
hence thesis by A34,A35,A32,FUNCT_2:8;
end;
then reconsider p9 = p as FuncSequence of pp;
A36: 1 in dom q by FINSEQ_5:6;
then
A37: pp.1 = (the Sorts of A).s1 by A2,A10,A12,A13;
then
A38: dom compose(p9,(the Sorts of A).s1) = (the Sorts of A).s1 by FUNCT_7:67;
A39: len q in dom q by FINSEQ_5:6;
then
A40: pp.len pp = (the Sorts of A).s2 by A3,A10,A11,A12,A13;
then rng compose(p9,(the Sorts of A).s1) c= (the Sorts of A).s2 by A37,
FUNCT_7:67;
hence
compose(p, (the Sorts of A).s1) is Function of (the Sorts of A).s1, (
the Sorts of A).s2 by A10,A11,A13,A39,A40,A38,FUNCT_2:def 1,RELSET_1:4;
thus thesis by A10,A11,A13,A36,A39,A37,A40;
end;
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 such that
A1: TranslationRel S reduces s1,s2;
mode Translation of A,s1,s2 -> Function of (the Sorts of A).s1,(the Sorts of
A).s2 means
: Def6:
ex q being RedSequence of TranslationRel S, 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), 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;
existence
proof
consider q being RedSequence of TranslationRel S such that
A2: q.1 = s1 and
A3: q.len q = s2 by A1;
defpred Z[object,object] means
ex f being Function, s1,s2 being SortSymbol of S,
i being Element of NAT st $2 = f & i = $1 & s1 = q.i & s2 = q.(i+1) & f
is_e.translation_of A,s1,s2;
len q >= 0+1 by NAT_1:13;
then consider n being Nat such that
A4: len q = 1+n by NAT_1:10;
reconsider n as Element of NAT by ORDINAL1:def 12;
A5: dom q = Seg len q by FINSEQ_1:def 3;
A6: for x being object st x in Seg n ex y being object st Z[x,y]
proof
let x be object;
assume
A7: x in Seg n;
then reconsider i = x as Element of NAT;
A8: i <= n by A7,FINSEQ_1:1;
then
A9: i+1 <= len q by A4,XREAL_1:6;
A10: i >= 1 by A7,FINSEQ_1:1;
then i+1 >= 1 by NAT_1:13;
then
A11: i+1 in dom q by A5,A9,FINSEQ_1:1;
i <= n+1 by A8,NAT_1:13;
then i in dom q by A4,A5,A10,FINSEQ_1:1;
then
A12: [q.i, q.(i+1)] in TranslationRel S by A11,REWRITE1:def 2;
then reconsider s1 = q.i, s2 = q.(i+1) as SortSymbol of S by ZFMISC_1:87;
consider o being OperSymbol of S such that
A13: the_result_sort_of o = s2 and
A14: ex i being Element of NAT st i in dom the_arity_of o & (
the_arity_of o)/.i = s1 by A12,Def3;
set a = the Element of Args(o,A);
consider j being Element of NAT such that
A15: j in dom the_arity_of o and
A16: (the_arity_of o)/.j = s1 by A14;
take transl(o,j,a,A);
take transl(o,j,a,A), s1,s2,i;
thus thesis by A13,A15,A16;
end;
consider p being Function such that
A17: dom p = Seg n & for x being object st x in Seg n holds Z[x,p.x] from
CLASSES1:sch 1(A6);
p is Function-yielding
proof
let j be object;
assume j in dom p;
then ex f being Function, s1,s2 being SortSymbol of S, i being Element
of NAT st p.j = f & i = j & s1 = q.i & s2 = q.(i+1) & f is_e.translation_of A,
s1,s2 by A17;
hence thesis;
end;
then reconsider p as Function-yielding FinSequence by A17,FINSEQ_1:def 2;
A18: now
let i be Element of NAT;
let f be Function, s1,s2 be SortSymbol of S;
assume i in dom p;
then ex f being Function, s1,s2 being SortSymbol of S, j being Element
of NAT st p.i = f & j = i & s1 = q.j & s2 = q.(j+1) & f is_e.translation_of A,
s1,s2 by A17;
hence f = p.i & s1 = q.i & s2 = q.(i+1) implies f is_e.translation_of A,
s1,s2;
end;
len p = n by A17,FINSEQ_1:def 3;
then reconsider
t = compose(p, (the Sorts of A).s1) as Function of (the Sorts
of A).s1, (the Sorts of A).s2 by A2,A3,A4,A18,Th14;
take t, q, p;
thus thesis by A2,A3,A4,A17,A18,FINSEQ_1:def 3;
end;
end;
theorem
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 (Element
of 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
proof
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
A1: TranslationRel S reduces s1,s2;
let q be RedSequence of TranslationRel S, p be Function-yielding FinSequence
such that
A2: len q = len p+1 and
A3: s1 = q.1 and
A4: s2 = q.len q and
A5: for i being (Element of 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;
compose(p, (the Sorts of A).s1) is Function of (the Sorts of A).s1, (the
Sorts of A).s2 by A2,A3,A4,A5,Th14;
hence thesis by A1,A2,A3,A4,A5,Def6;
end;
reserve A for non-empty MSAlgebra over S;
theorem Th16:
for s being SortSymbol of S holds id ((the Sorts of A).s) is
Translation of A,s,s
proof
let s be SortSymbol of S;
thus TranslationRel S reduces s,s by REWRITE1:12;
A1: <*s*> is RedSequence of TranslationRel S by REWRITE1:6;
A2: len <*s*> = 0+1 by FINSEQ_1:40;
A3: len {} = 0;
A4: for i being (Element of NAT), f being Function, s1,s2 being SortSymbol
of S st i in dom {} & f = {}.i & s1 = <*s*>.i & s2 = <*s*>.(i+1) holds f
is_e.translation_of A,s1,s2;
A5: <*s*>.1 = s;
id ((the Sorts of A).s) = compose({}, (the Sorts of A).s) by FUNCT_7:39;
hence thesis by A1,A2,A3,A5,A4;
end;
theorem Th17:
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
proof
let s1,s2 be SortSymbol of S, f be Function;
A1: len <*s1,s2*> = 1+1 by FINSEQ_1:44;
A2: len <*f*> = 1 by FINSEQ_1:40;
assume
A3: f is_e.translation_of A,s1,s2;
then reconsider
g = f as Function of (the Sorts of A).s1, (the Sorts of A).s2 by Th11;
A4: <*s1,s2*>.2 = s2;
A5: <*s1,s2*>.1 = s1;
A6: now
let i be Element of NAT;
let g be Function, w1,w2 be SortSymbol of S;
assume i in dom <*f*>;
then i in {1} by FINSEQ_1:2,38;
then i = 1 by TARSKI:def 1;
hence g = <*f*>.i & w1 = <*s1,s2*>.i & w2 = <*s1,s2*>.(i+1) implies g
is_e.translation_of A,w1,w2 by A3;
end;
dom g = (the Sorts of A).s1 by FUNCT_2:def 1;
then
A7: g = compose(<*f*>, (the Sorts of A).s1) by FUNCT_7:46;
A8: [s1,s2] in TranslationRel S by A3,Th12;
hence
A9: TranslationRel S reduces s1,s2 by REWRITE1:15;
<*s1,s2*> is RedSequence of TranslationRel S by A8,REWRITE1:7;
hence thesis by A7,A9,A1,A2,A5,A4,A6,Def6;
end;
theorem Th18:
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
proof
let s1,s2,s3 be SortSymbol of S such that
A1: TranslationRel S reduces s1,s2 and
A2: TranslationRel S reduces s2,s3;
let t1 be Translation of A,s1,s2;
let t2 be Translation of A,s2,s3;
thus TranslationRel S reduces s1,s3 by A1,A2,REWRITE1:16;
consider q1 being RedSequence of TranslationRel S, p1 being
Function-yielding FinSequence such that
A3: t1 = compose(p1, (the Sorts of A).s1) and
A4: len q1 = len p1+1 and
A5: s1 = q1.1 and
A6: s2 = q1.len q1 and
A7: for i being (Element of NAT), f being Function, s1,s2 being
SortSymbol of S st i in dom p1 & f = p1.i & s1 = q1.i & s2 = q1.(i+1) holds f
is_e.translation_of A,s1,s2 by A1,Def6;
consider q2 being RedSequence of TranslationRel S, p2 being
Function-yielding FinSequence such that
A8: t2 = compose(p2, (the Sorts of A).s2) and
A9: len q2 = len p2+1 and
A10: s2 = q2.1 and
A11: s3 = q2.len q2 and
A12: for i being (Element of NAT), f being Function, s1,s2 being
SortSymbol of S st i in dom p2 & f = p2.i & s1 = q2.i & s2 = q2.(i+1) holds f
is_e.translation_of A,s1,s2 by A2,Def6;
reconsider q = q1$^q2 as RedSequence of TranslationRel S by A6,A10,REWRITE1:8
;
take q, p = p1^p2;
rng t1 c= (the Sorts of A).s2 by RELAT_1:def 19;
hence t2*t1 = compose(p, (the Sorts of A).s1) by A3,A8,FUNCT_7:48;
A13: len p = len p1+len p2 by FINSEQ_1:22;
consider x2 being object, r2 being FinSequence such that
A14: q2 = <*x2*>^r2 and
len q2 = len r2+1 by REWRITE1:5;
A15: x2 = s2 by A10,A14,FINSEQ_1:41;
consider r1 being FinSequence, x1 being object such that
A16: q1 = r1^<*x1*> by FINSEQ_1:46;
A17: q = r1^q2 by A16,REWRITE1:2;
len <*x1*> = 1 by FINSEQ_1:40;
then
A18: len q1 = len r1+1 by A16,FINSEQ_1:22;
then
A19: len q = len p1+len q2 by A4,A17,FINSEQ_1:22;
hence len q = len p+1 by A9,A13;
x1 = s2 by A6,A16,A18,FINSEQ_1:42;
then
A20: q = q1^r2 by A16,A14,A17,A15,FINSEQ_1:32;
1 <= len r1 or 0+1 > len r1;
then
1 in Seg len r1 & Seg len r1 = dom r1 or 0 <= len r1 & 0 >= len r1 by
FINSEQ_1:1,def 3,NAT_1:13;
then
A21: q.1 = r1.1 & r1.1 = q1.1 or r1 = {} & {}^q2 = q2 by A16,A17,FINSEQ_1:34
,def 7;
thus s1 = q.1 by A5,A6,A10,A16,A18,A21,REWRITE1:2;
len q2 in dom q2 by FINSEQ_5:6;
hence s3 = q.len q by A4,A11,A18,A17,A19,FINSEQ_1:def 7;
let i be Element of NAT;
let f be Function, s1,s2 be SortSymbol of S;
assume that
A22: i in dom p and
A23: f = p.i and
A24: s1 = q.i and
A25: s2 = q.(i+1);
per cases;
suppose
A26: i in dom p1;
then i+1 in dom q1 by A4,FUNCT_7:22;
then
A27: s2 = q1.(i+1) by A20,A25,FINSEQ_1:def 7;
i in dom q1 by A4,A26,FUNCT_7:22;
then
A28: s1 = q1.i by A20,A24,FINSEQ_1:def 7;
f = p1.i by A23,A26,FINSEQ_1:def 7;
hence thesis by A7,A26,A28,A27;
end;
suppose
not i in dom p1;
then not (i <= len p1 & i >= 1) by FINSEQ_3:25;
then i >= len p1+1 by A22,FINSEQ_3:25,NAT_1:13;
then consider k being Nat such that
A29: i = len p1+1+k by NAT_1:10;
A30: len p1+(k+1+1) = i+1 by A29;
A31: k+1 >= 1 by NAT_1:11;
A32: i = len p1+(1+k) by A29;
i <= len p by A22,FINSEQ_3:25;
then k+1 <= len p2 by A13,A32,XREAL_1:6;
then
A33: k+1 in dom p2 by A31,FINSEQ_3:25;
then k+1 in dom q2 by A9,FUNCT_7:22;
then
A34: s1 = q2.(k+1) by A4,A18,A17,A24,A32,FINSEQ_1:def 7;
k+1+1 in dom q2 by A9,A33,FUNCT_7:22;
then
A35: s2 = q2.(k+1+1) by A4,A18,A17,A25,A30,FINSEQ_1:def 7;
f = p2.(k+1) by A23,A32,A33,FINSEQ_1:def 7;
hence thesis by A12,A33,A34,A35;
end;
end;
theorem Th19:
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
proof
let s1,s2,s3 be SortSymbol of S such that
A1: TranslationRel S reduces s1,s2;
let t be Translation of A,s1,s2;
let f be Function;
assume
A2: f is_e.translation_of A,s2,s3;
then
A3: f is Translation of A,s2,s3 by Th17;
TranslationRel S reduces s2,s3 by A2,Th17;
hence thesis by A1,A3,Th18;
end;
theorem
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
proof
let s1,s2,s3 be SortSymbol of S such that
A1: TranslationRel S reduces s2,s3;
let f be Function;
assume
A2: f is_e.translation_of A,s1,s2;
then
A3: f is Translation of A,s1,s2 by Th17;
TranslationRel S reduces s1,s2 by A2,Th17;
hence thesis by A1,A3,Th18;
end;
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
A1: for s being SortSymbol of S() holds P[id ((the Sorts of A()).s),s,s] and
A2: 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]
proof
set S = S(), A = A();
let s1,s2 be SortSymbol of S such that
A3: TranslationRel S reduces s1,s2;
let t be Translation of A,s1,s2;
consider q being RedSequence of TranslationRel S, p being Function-yielding
FinSequence such that
A4: t = compose(p, (the Sorts of A).s1) and
A5: len q = len p+1 and
A6: s1 = q.1 and
A7: s2 = q.len q and
A8: for i being (Element of 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 by A3,Def6;
defpred Q[Nat] means $1 in dom p implies ex s being SortSymbol of
S, t being Translation of A,s1,s, p9 being Function-yielding FinSequence st p9
= p|Seg $1 & s = q.($1+1) & TranslationRel S reduces s1,s & t = compose(p9, (
the Sorts of A).s1) & P[t,s1,s];
A9: for i being Nat st Q[i] holds Q[i+1]
proof
let i be Nat such that
A10: i in dom p implies ex s being SortSymbol of S, t being
Translation of A,s1,s, p9 being Function-yielding FinSequence st p9 = p|Seg i &
s = q.(i+1) & TranslationRel S reduces s1,s & t = compose(p9, (the Sorts of A).
s1) & P[t,s1,s] and
A11: i+1 in dom p;
A12: i+1+1 in dom q by A5,A11,FUNCT_7:22;
i+1 in dom q by A5,A11,FUNCT_7:22;
then [q.(i+1),q.(i+1+1)] in TranslationRel S by A12,REWRITE1:def 2;
then reconsider v1 = q.(i+1), v2 = q.(i+1+1) as SortSymbol of S by
ZFMISC_1:87;
reconsider f = p.(i+1) as Function;
A13: f is_e.translation_of A,v1,v2 by A8,A11;
then reconsider t = f as Translation of A,v1,v2 by Th17;
per cases;
suppose
A14: i = 0;
then reconsider t as Translation of A,s1,v2 by A6;
reconsider p9 = p|Seg 1 as Function-yielding FinSequence by FINSEQ_1:15;
A15: t*id ((the Sorts of A).s1) = t by FUNCT_2:17;
take v2, t, p9;
thus p9 = p|Seg (i+1) & v2 = q.(i+1+1) by A14;
thus TranslationRel S reduces s1,v2 by A6,A13,A14,Th17;
A16: dom t = (the Sorts of A).s1 by FUNCT_2:def 1;
1 in Seg 1 by FINSEQ_1:2,TARSKI:def 1;
then
A17: p9.1 = t by A14,FUNCT_1:49;
0+1 <= len p by A11,A14,FINSEQ_3:25;
then len p9 = 1 by FINSEQ_1:17;
then p9 = <*t*> by A17,FINSEQ_1:40;
hence t = compose(p9, (the Sorts of A).s1) by A16,FUNCT_7:46;
A18: TranslationRel S reduces s1,s1 by REWRITE1:12;
A19: P[id ((the Sorts of A).s1),s1,s1] by A1;
id ((the Sorts of A).s1) is Translation of A,s1,s1 by Th16;
hence thesis by A2,A6,A8,A11,A14,A18,A15,A19;
end;
suppose
A20: i > 0;
reconsider pp = p|Seg (i+1) as FinSequence by FINSEQ_1:15;
take v2;
A21: i+1 <= len p by A11,FINSEQ_3:25;
then
A22: i <= len p by NAT_1:13;
i >= 0+1 by A20,NAT_1:13;
then consider
s being SortSymbol of S, t9 being Translation of A,s1,s, p9
being Function-yielding FinSequence such that
A23: p9 = p|Seg i and
A24: s = q.(i+1) and
A25: TranslationRel S reduces s1,s and
A26: t9 = compose(p9, (the Sorts of A).s1) and
A27: P[t9,s1,s] by A10,A22,FINSEQ_3:25;
reconsider T = t*t9 as Translation of A,s1,v2 by A8,A11,A24,A25,Th19;
take T, y = p9^<*f*>;
i <= len p by A21,NAT_1:13;
then
A28: len p9 = i by A23,FINSEQ_1:17;
i+1 <= len p by A11,FINSEQ_3:25;
then
A29: dom pp = Seg (i+1) by FINSEQ_1:17;
A30: now
let k be Nat;
assume
A31: k in Seg (i+1);
then k <= i+1 by FINSEQ_1:1;
then k <= i & k >= 1 or k = i+1 by A31,FINSEQ_1:1,NAT_1:8;
then k in dom p9 or k = i+1 by A28,FINSEQ_3:25;
then y.k = p9.k & p9.k = p.k or y.k = p.k by A23,A28,FINSEQ_1:42,def 7
,FUNCT_1:47;
hence y.k = pp.k by A29,A31,FUNCT_1:47;
end;
len <*f*> = 1 by FINSEQ_1:40;
then len y = len p9+1 by FINSEQ_1:22;
then dom y = Seg (i+1) by A28,FINSEQ_1:def 3;
hence y = p|Seg (i+1) by A29,A30;
thus v2 = q.(i+1+1);
TranslationRel S reduces v1,v2 by A13,Th17;
hence TranslationRel S reduces s1,v2 by A24,A25,REWRITE1:16;
thus T = compose(y, (the Sorts of A).s1) by A26,FUNCT_7:41;
thus thesis by A2,A8,A11,A24,A25,A27;
end;
end;
A32: Q[ 0 ] by FINSEQ_3:25;
A33: for i being Nat holds Q[i] from NAT_1:sch 2(A32,A9);
per cases;
suppose
A34: p = {};
then
A35: len p = 0;
t = id ((the Sorts of A).s1) by A4,A34,FUNCT_7:39;
hence thesis by A1,A5,A6,A7,A35;
end;
suppose
p <> {};
then len p >= 0+1 by NAT_1:13;
then
A36: len p in dom p by FINSEQ_3:25;
A37: p|dom p = p;
dom p = Seg len p by FINSEQ_1:def 3;
then ex s being SortSymbol of S, t being Translation of A,s1,s, p9 being
Function-yielding FinSequence st p9 = p & s = q.(len p+1) & TranslationRel S
reduces s1,s & t = compose(p9, (the Sorts of A).s1) & P[t,s1,s] by A33,A36
,A37;
hence thesis by A4,A5,A7;
end;
end;
theorem Th21:
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 Element of 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))
proof
let A1,A2 be non-empty MSAlgebra over S;
let h be ManySortedFunction of A1,A2 such that
A1: h is_homomorphism A1,A2;
let o be OperSymbol of S, i be Element of NAT such that
A2: i in dom the_arity_of o;
let a be Element of Args(o,A1);
set s1 = (the_arity_of o)/.i, s2 = the_result_sort_of o;
reconsider T = transl(o,i,h#a,A2) as Function of (the Sorts of A2).s1, (the
Sorts of A2).s2 by Th10;
reconsider t = transl(o,i,a,A1) as Function of (the Sorts of A1).s1, (the
Sorts of A1).s2 by Th10;
now
let x be Element of A1,s1;
reconsider b = a+*(i,x) as Element of Args(o,A1) by Th7;
A3: h#b = (h#a)+*(i,(h#b).i) by A2,Th9;
h#a in Args(o,A2);
then
A4: (h#b).i = h.s1.x by A2,Th9;
thus ((h.s2)*t).x = h.s2.(t.x) by FUNCT_2:15
.= h.s2.(Den(o,A1).b) by Def4
.= Den(o,A2).(h#a+*(i,(h.s1.x))) by A1,A4,A3
.= T.(h.s1.x) by Def4
.= (T*(h.s1)).x by FUNCT_2:15;
end;
hence thesis by FUNCT_2:63;
end;
theorem
for h being Endomorphism of A for o being OperSymbol of S, i being
Element of 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))
by Def2,Th21;
theorem Th23:
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
proof
let A1,A2 be non-empty MSAlgebra over S;
let h be ManySortedFunction of A1,A2 such that
A1: h is_homomorphism A1,A2;
let s1,s2 be SortSymbol of S, t be Function;
assume t is_e.translation_of A1,s1,s2;
then consider o being OperSymbol of S such that
A2: the_result_sort_of o = s2 and
A3: 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,A1) & t = transl(o,i,a,A1);
consider i being (Element of NAT), a being Function such that
A4: i in dom the_arity_of o and
A5: (the_arity_of o)/.i = s1 and
A6: a in Args(o,A1) and
A7: t = transl(o,i,a,A1) by A3;
reconsider a as Element of Args(o,A1) by A6;
reconsider T = transl(o,i,h#a,A2) as Function of (the Sorts of A2).s1, (the
Sorts of A2).s2 by A2,A5,Th10;
take T;
thus T is_e.translation_of A2,s1,s2 by A2,A4,A5;
thus thesis by A1,A2,A4,A5,A7,Th21;
end;
theorem
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
by Def2,Th23;
theorem Th25:
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
proof
let A1,A2 be non-empty MSAlgebra over S;
let h be ManySortedFunction of A1,A2 such that
A1: h is_homomorphism A1,A2;
defpred P[Function, SortSymbol of S, SortSymbol of S] means ex T being
Translation of A2,$2,$3 st T*(h.$2) = (h.$3)*$1;
A2: for s1,s2,s3 being SortSymbol of S st TranslationRel S reduces s1,s2 for
t being Translation of A1,s1,s2 st P[t,s1,s2] for f being Function st f
is_e.translation_of A1,s2,s3 holds P[f*t,s1,s3]
proof
let s1,s2,s3 be SortSymbol of S such that
A3: TranslationRel S reduces s1,s2;
let t be Translation of A1,s1,s2;
given T being Translation of A2,s1,s2 such that
A4: T*(h.s1) = (h.s2)*t;
let f be Function;
assume f is_e.translation_of A1,s2,s3;
then consider
T1 being Function of (the Sorts of A2).s2, (the Sorts of A2) .s3
such that
A5: T1 is_e.translation_of A2,s2,s3 and
A6: T1*(h.s2) = (h.s3)*f by A1,Th23;
reconsider T2 = T1*T as Translation of A2,s1,s3 by A3,A5,Th19;
take T2;
thus T2*(h.s1) = T1*(T*(h.s1)) by RELAT_1:36
.= (h.s3)*f*t by A4,A6,RELAT_1:36
.= (h.s3)*(f*t) by RELAT_1:36;
end;
A7: for s being SortSymbol of S holds P[id ((the Sorts of A1).s),s,s]
proof
let s be SortSymbol of S;
A8: (id ((the Sorts of A2).s))*(h.s) = h.s by FUNCT_2:17;
A9: (h.s)*(id ((the Sorts of A1).s)) = h.s by FUNCT_2:17;
id ((the Sorts of A2).s) is Translation of A2,s,s by Th16;
hence thesis by A8,A9;
end;
thus for s1,s2 being SortSymbol of S st TranslationRel S reduces s1,s2 for t
being Translation of A1,s1,s2 holds P[t,s1,s2] from TranslationInd(A7,A2);
end;
theorem Th26:
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
by Def2,Th25;
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
for o being OperSymbol of S, a,b being
Function st a in Args(o,A) & b in Args(o,A) & (for n be Element of NAT st n in
dom the_arity_of o holds [a.n,b.n] in R.((the_arity_of o)/.n)) holds [Den(o,A).
a,Den(o,A).b] in R.(the_result_sort_of o);
attr R is invariant means
: Def8:
for s1,s2 being SortSymbol of S for t
being Function st t is_e.translation_of A,s1,s2 for a,b being set st [a,b] in R
.s1 holds [t.a, t.b] in R.s2;
attr R is stable means
: Def9:
for h being Endomorphism of A for s being
SortSymbol of S for a,b being set st [a,b] in R.s holds [(h.s).a, (h.s).b] in R
.s;
end;
theorem
for R being MSEquivalence-like ManySortedRelation of A holds R is
compatible iff R is MSCongruence of A
proof
let R be MSEquivalence-like ManySortedRelation of A;
hereby
assume
A1: R is compatible;
now
let o be OperSymbol of S, x,y be Element of Args(o,A) such that
A2: for n be Nat st n in dom x holds [x.n,y.n] in R.((the_arity_of o )/.n);
now
let n be Element of NAT;
assume n in dom the_arity_of o;
then n in dom x by MSUALG_3:6;
hence [x.n,y.n] in R.((the_arity_of o)/.n) by A2;
end;
hence [Den(o,A).x,Den(o,A).y] in R.(the_result_sort_of o) by A1;
end;
hence R is MSCongruence of A by MSUALG_4:def 4;
end;
assume
A3: R is MSCongruence of A;
let o be OperSymbol of S, x,y be Function such that
A4: x in Args(o,A) and
A5: y in Args(o,A) and
A6: for n be Element of NAT st n in dom the_arity_of o holds [x.n,y.n]
in R.((the_arity_of o)/.n);
reconsider x, y as Element of Args(o,A) by A4,A5;
now
let n be Nat;
assume n in dom x;
then n in dom the_arity_of o by MSUALG_3:6;
hence [x.n,y.n] in R.((the_arity_of o)/.n) by A6;
end;
hence thesis by A3,MSUALG_4:def 4;
end;
theorem Th28:
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
proof
let R be ManySortedRelation of A;
hereby
defpred P[Function,set,set] means for a,b being set st [a,b] in R.$2 holds
[$1.a,$1.b] in R.$3;
deffunc i(SortSymbol of S) = id ((the Sorts of A).$1);
assume
A1: R is invariant;
A2: 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]
proof
let s1,s2,s3 be SortSymbol of S such that
TranslationRel S reduces s1,s2;
let t be Translation of A,s1,s2 such that
A3: for a,b being set st [a,b] in R.s1 holds [t.a,t.b] in R.s2;
let f be Function such that
A4: f is_e.translation_of A,s2,s3;
let a,b be set;
assume
A5: [a,b] in R.s1;
then reconsider a9 = a, b9 = b as Element of A,s1 by ZFMISC_1:87;
[t.a9,t.b9] in R.s2 by A3,A5;
then
A6: [f.(t.a9),f.(t.b9)] in R.s3 by A1,A4;
f.(t.a9) = (f*t).a9 by FUNCT_2:15;
hence thesis by A6,FUNCT_2:15;
end;
A7: for s being SortSymbol of S holds P[id ((the Sorts of A).s),s,s]
proof
let s be SortSymbol of S;
let a,b be set;
assume
A8: [a,b] in R.s;
then a in (the Sorts of A).s by ZFMISC_1:87;
then
A9: i(s).a = a by FUNCT_1:17;
b in (the Sorts of A).s by A8,ZFMISC_1:87;
hence thesis by A8,A9,FUNCT_1:17;
end;
thus 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] from TranslationInd(A7,A2);
end;
assume
A10: 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;
let s1,s2 be SortSymbol of S;
let t be Function;
assume
A11: t is_e.translation_of A,s1,s2;
then t is Translation of A,s1,s2 by Th17;
hence thesis by A10,A11,Th17;
end;
registration
let S be non empty non void ManySortedSign;
let A be non-empty MSAlgebra over S;
cluster invariant -> compatible for
MSEquivalence-like ManySortedRelation of A;
coherence
proof
let R be MSEquivalence-like ManySortedRelation of A such that
A1: 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;
let o be OperSymbol of S, a,b be Function such that
A2: a in Args(o,A) and
A3: b in Args(o,A) and
A4: for n be Element of NAT st n in dom the_arity_of o holds [a.n,b.n]
in R.((the_arity_of o)/.n);
A5: dom the_arity_of o = Seg len the_arity_of o by FINSEQ_1:def 3;
reconsider a9 = a as Element of Args(o,A) by A2;
defpred P[set,set,set] means ex c being Element of Args(o,A) st c = $2 &
$3 = c+*($1,b.$1);
A6: for n being Nat st 1 <= n & n < (len the_arity_of o)+1 for
x being Element of Args(o,A) ex y being Element of Args(o,A) st P[n,x,y]
proof
let n be Nat;
assume that
A7: 1 <= n and
A8: n < (len the_arity_of o)+1;
let x be Element of Args(o,A);
n <= (len the_arity_of o) by A8,NAT_1:13;
then n in dom the_arity_of o by A7,FINSEQ_3:25;
then b.n in (the Sorts of A).((the_arity_of o)/.n) by A3,Th2;
then x+*(n,b.n) in Args(o,A) by Th7;
hence thesis;
end;
consider p being FinSequence of Args(o,A) such that
A9: len p = (len the_arity_of o)+1 and
A10: p.1 = a9 or (len the_arity_of o)+1 = 0 and
A11: for i being Nat st 1 <= i & i < (len the_arity_of o)+1
holds P[i,p.i,p.(i+1)] from RECDEF_1:sch 4(A6);
(len the_arity_of o)+1 >= 1 by NAT_1:11;
then
A12: (len the_arity_of o)+1 in dom p by A9,FINSEQ_3:25;
defpred P[Nat] means $1 <= len the_arity_of o implies ex c
being Element of Args(o,A) st c = p.($1+1) & (for j being Element of NAT st j
in dom the_arity_of o & j > $1 holds c.j = a.j) & for j being Nat st j in Seg
$1 holds c.j = b.j;
A13: dom the_arity_of o = Seg len the_arity_of o by FINSEQ_1:def 3;
A14: for n being Nat st P[n] holds P[n+1]
proof
let i be Nat such that
A15: i <= len the_arity_of o implies ex c being Element of Args(o,A)
st c = p.(i+1) & (for j being Element of NAT st j in dom the_arity_of o & j > i
holds c.j = a.j) & for j being Nat st j in Seg i holds c.j = b.j and
A16: i+1 <= len the_arity_of o;
i+1 < (len the_arity_of o)+1 by A16,NAT_1:13;
then consider c being Element of Args(o,A) such that
A17: c = p.(i+1) and
A18: p.(i+1+1) = c+*(i+1,b.(i+1)) by A11,NAT_1:11;
i+1 >= 1 by NAT_1:11;
then i+1 in dom the_arity_of o by A16,FINSEQ_3:25;
then b.(i+1) in (the Sorts of A).((the_arity_of o)/.(i+1)) by A3,Th2;
then reconsider d = p.(i+1+1) as Element of Args(o,A) by A18,Th7;
take d;
thus d = p.(i+1+1);
Seg (i+1) c= dom the_arity_of o by A13,A16,FINSEQ_1:5;
then
A19: Seg (i+1) c= dom c by MSUALG_3:6;
i <= i+1 by NAT_1:11;
then consider ci being Element of Args(o,A) such that
A20: ci = p.(i+1) and
A21: for j being Element of NAT st j in dom the_arity_of o & j > i
holds ci.j = a.j and
A22: for j being Nat st j in Seg i holds ci.j = b.j by A15,A16,XXREAL_0:2;
hereby
let j be Element of NAT;
assume that
A23: j in dom the_arity_of o and
A24: j > i+1;
j > i by A24,NAT_1:13;
then ci.j = a.j by A21,A23;
hence d.j = a.j by A20,A17,A18,A24,FUNCT_7:32;
end;
let j be Nat;
assume
A25: j in Seg (i+1);
then j in Seg i \/ {i+1} by FINSEQ_1:9;
then
A26: j in Seg i or j in {i+1} by XBOOLE_0:def 3;
per cases;
suppose
j = i+1;
hence thesis by A18,A25,A19,FUNCT_7:31;
end;
suppose
A27: j <> i+1;
then d.j = c.j by A18,FUNCT_7:32;
hence thesis by A20,A22,A17,A26,A27,TARSKI:def 1;
end;
end;
A28: P[ 0 ]
proof
assume 0 <= len the_arity_of o;
take a9;
thus thesis by A10;
end;
A29: for i being Nat holds P[i] from NAT_1:sch 2(A28,A14);
then consider c being Element of Args(o,A) such that
A30: c = p.((len the_arity_of o)+1) and
for j being Element of NAT st j in dom the_arity_of o & j > len
the_arity_of o holds c.j = a.j and
A31: for j being Nat st j in Seg len the_arity_of o holds c.j = b.j;
defpred P[Nat] means $1 in dom p implies [Den(o,A).a9,Den(o,A).
(p.$1)] in R.(the_result_sort_of o);
A32: for k be Nat st P[k] holds P[k+1]
proof
A33: Result(o,A) = (the Sorts of A).the_result_sort_of o by PRALG_2:3;
let i be Nat such that
A34: i in dom p implies [Den(o,A).a9,Den(o,A).(p.i)] in R.(
the_result_sort_of o) and
A35: i+1 in dom p;
A36: i+1 <= len p by A35,FINSEQ_3:25;
i <= i+1 by NAT_1:11;
then
A37: i <= len p by A36,XXREAL_0:2;
per cases;
suppose
i = 0;
hence thesis by A10,A33,EQREL_1:5;
end;
suppose
i > 0;
then
A38: i >= 0+1 by NAT_1:13;
then consider j being Nat such that
A39: i = 1+j by NAT_1:10;
reconsider j as Element of NAT by ORDINAL1:def 12;
i < (len the_arity_of o)+1 by A9,A36,NAT_1:13;
then consider c being Element of Args(o,A) such that
A40: c = p.i and
A41: p.(i+1) = c+*(i,b.i) by A11,A38;
A42: i <= len the_arity_of o by A9,A36,XREAL_1:6;
then
A43: i in dom the_arity_of o by A38,FINSEQ_3:25;
then reconsider
bi = b.i, ci = c.i as Element of A,((the_arity_of o)/.i) by A3,Th2;
j <= i by A39,NAT_1:11;
then
A44: ex c being Element of Args(o,A) st c = p.(j+1) & (for k being
Element of NAT st k in dom the_arity_of o & k > j holds c.k = a.k) & for k
being Nat st k in Seg j holds c.k = b.k by A29,A42,XXREAL_0:2;
j < i by A39,NAT_1:13;
then c.i = a.i by A40,A43,A39,A44;
then
A45: [ci,bi] in R.((the_arity_of o)/.i) by A4,A43;
reconsider d = c+*(i,bi) as Element of Args(o,A) by Th7;
A46: Den(o,A).d = transl(o,i,c,A).bi by Def4;
c = c+*(i,ci) by FUNCT_7:35;
then
A47: Den(o,A).c = transl(o,i,c,A).ci by Def4;
transl(o,i,c,A) is_e.translation_of A, (the_arity_of o)/.i,
the_result_sort_of o by A43;
then
[Den(o,A).c,Den(o,A).d] in R.(the_result_sort_of o) by A1,A46,A47,A45;
hence thesis by A34,A37,A38,A40,A41,EQREL_1:7,FINSEQ_3:25;
end;
end;
A48: dom b = dom the_arity_of o by A3,MSUALG_3:6;
A49: P[ 0 ] by FINSEQ_3:25;
A50: for i being Nat holds P[i] from NAT_1:sch 2(A49,A32);
A51: dom c = dom the_arity_of o by MSUALG_3:6;
c = b by A31,A51,A48,A5;
hence [Den(o,A).a,Den(o,A).b] in R.(the_result_sort_of o) by A50,A30,A12;
end;
cluster compatible -> invariant for
MSEquivalence-like ManySortedRelation of A;
coherence
proof
let R be MSEquivalence-like ManySortedRelation of A such that
A52: for o be OperSymbol of S, a,b be Function st a in Args(o,A) & b
in Args(o,A) & (for n be 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);
let s1,s2 be SortSymbol of S;
let f be Function;
given o being OperSymbol of S such that
A53: the_result_sort_of o = s2 and
A54: 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);
consider i being (Element of NAT), a being Function such that
i in dom the_arity_of o and
A55: ((the_arity_of o)/.i) = s1 and
A56: a in Args(o,A) and
A57: f = transl(o,i,a,A) by A54;
let x,y be set;
assume
A58: [x,y] in R.s1;
then
A59: y in (the Sorts of A).s1 by ZFMISC_1:87;
A60: x in (the Sorts of A).s1 by A58,ZFMISC_1:87;
then reconsider
ax = a+*(i,x), ay = a+*(i,y) as Element of Args(o,A) by A55,A56,A59,Th7;
A61: f.y = Den(o,A).ay by A55,A57,A59,Def4;
A62: dom a = dom the_arity_of o by A56,MSUALG_3:6;
A63: now
let n be Element of NAT;
A64: dom ((the Sorts of A)*the_arity_of o) = dom the_arity_of o by
PARTFUN1:def 2;
assume
A65: n in dom the_arity_of o;
then (the_arity_of o)/.n = (the_arity_of o).n by PARTFUN1:def 6;
then
A66: (the Sorts of A).((the_arity_of o)/.n) = ((the Sorts of A)*
the_arity_of o).n by A65,FUNCT_1:13;
n = i or n <> i;
then ax.n = x & ay.n = y & n = i or ax.n = a.n & ay.n = a.n by A62,A65,
FUNCT_7:31,32;
hence [ax.n,ay.n] in R.((the_arity_of o)/.n) by A55,A58,A65,A64,A66,
EQREL_1:5,MSUALG_3:6;
end;
f.x = Den(o,A).ax by A55,A57,A60,Def4;
hence [f.x, f.y] in R.s2 by A52,A53,A61,A63;
end;
end;
registration
let X be non empty set;
cluster id X -> non empty;
coherence;
end;
scheme
MSRExistence {I() -> non empty set, A() -> non-empty ManySortedSet of I(),
P[object,object,object]}:
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] proof
defpred Q[object,object] means P[$1,$2`1,$2`2];
deffunc F(object)=[:A().$1,A().$1:];
consider R being Function such that
A1: dom R = I() and
A2: for i being object st i in I()
for a being object holds a in R.i iff a in
F(i) & Q[i,a] from CARD_3:sch 2;
reconsider R as ManySortedSet of I() by A1,PARTFUN1:def 2,RELAT_1:def 18;
R is ManySortedRelation of A()
proof
let i be set;
assume
A3: i in I();
R.i c= [:A().i,A().i:]
by A2,A3;
hence thesis;
end;
then reconsider R as ManySortedRelation of A();
take R;
let i be Element of I();
let a,b be Element of A().i;
A4: [a,b]`2 = b;
A5: [a,b] in [:A().i,A().i:] by ZFMISC_1:87;
[a,b]`1 = a;
hence thesis by A2,A4,A5;
end;
scheme
MSRLambdaU{I() -> set, A() -> ManySortedSet of I(), F(object) -> set}:
(ex R
being ManySortedRelation of A() st
for i being object st i in I() holds R.i = F(i)
) & for R1,R2 being ManySortedRelation of A() st
(for i being object st i in I()
holds R1.i = F(i)) &
(for i being object st i in I() holds R2.i = F(i)) holds R1 =
R2
provided
A1: for i being set st i in I() holds F(i) is Relation of A().i, A().i
proof
consider R being ManySortedSet of I() such that
A2: for i being object st i in I() holds R.i = F(i) from PBOOLE:sch 4;
R is ManySortedRelation of A()
proof
let i be set;
assume
A3: i in I();
then F(i) is Relation of A().i, A().i by A1;
hence thesis by A2,A3;
end;
hence ex R being ManySortedRelation of A() st
for i being object st i in I()
holds R.i = F(i) by A2;
let R1,R2 be ManySortedRelation of A() such that
A4: for i being object st i in I() holds R1.i = F(i) and
A5: for i being object st i in I() holds R2.i = F(i);
now
let i be object;
assume
A6: i in I();
then R1.i = F(i) by A4;
hence R1.i = R2.i by A5,A6;
end;
hence thesis;
end;
definition
let I be set, A be ManySortedSet of I;
func id(I,A) -> ManySortedRelation of A means
: Def10:
for i being object st i in I holds it.i = id (A.i);
correctness
proof
deffunc F(object) = id (A.$1);
A1: for i being set st i in I holds F(i) is Relation of A.i, A.i;
(ex R being ManySortedRelation of A st
for i being object st i in I holds
R.i = F(i)) & for R1,R2 being ManySortedRelation of A st
(for i being object st i
in I holds R1.i = F(i)) &
(for i being object st i in I holds R2.i = F(i)) holds
R1 = R2 from MSRLambdaU(A1);
hence thesis;
end;
end;
registration
let S be non empty non void ManySortedSign;
let A be non-empty MSAlgebra over S;
cluster MSEquivalence-like -> non-empty for ManySortedRelation of A;
coherence
proof
let R be ManySortedRelation of A;
assume
A1: for i be object, P be Relation of (the Sorts of A).i st i in the
carrier of S & R.i = P holds P is Equivalence_Relation of (the Sorts of A).i;
let i be object;
assume i in the carrier of S;
then reconsider i as SortSymbol of S;
R.i is Equivalence_Relation of (the Sorts of A).i by A1;
hence thesis;
end;
end;
registration
let S be non empty non void ManySortedSign;
let A be non-empty MSAlgebra over S;
cluster invariant stable MSEquivalence-like for ManySortedRelation of A;
existence
proof
reconsider R = id(the carrier of S, the Sorts of A) as ManySortedRelation
of A;
take R;
thus R is invariant
proof
let s1,s2 be SortSymbol of S;
let t be Function;
assume t is_e.translation_of A,s1,s2;
then reconsider
f = t as Function of (the Sorts of A).s1, (the Sorts of A) .
s2 by Th11;
let a,b be set;
assume
A1: [a,b] in R.s1;
then a in (the Sorts of A).s1 by ZFMISC_1:87;
then
A2: f.a in (the Sorts of A).s2 by FUNCT_2:5;
R.s1 = id ((the Sorts of A).s1) by Def10;
then
A3: a = b by A1,RELAT_1:def 10;
R.s2 = id ((the Sorts of A).s2) by Def10;
hence thesis by A3,A2,RELAT_1:def 10;
end;
thus R is stable
proof
let h be Endomorphism of A;
let s be SortSymbol of S;
let a,b be set;
A4: R.s = id ((the Sorts of A).s) by Def10;
assume
A5: [a,b] in R.s;
then a in (the Sorts of A).s by A4,RELAT_1:def 10;
then
A6: h.s.a in (the Sorts of A).s by FUNCT_2:5;
a = b by A4,A5,RELAT_1:def 10;
hence thesis by A4,A6,RELAT_1:def 10;
end;
let i be object, P be Relation of (the Sorts of A).i;
assume i in the carrier of S;
then reconsider s = i as SortSymbol of S;
assume R.i = P;
then P = id ((the Sorts of A).s) by Def10;
hence thesis;
end;
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
A1: 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
A2: 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
A3: for s being SortSymbol of S() holds P[id ((the Sorts of A()).s),s,s] and
A4: for s being SortSymbol of S(), a,b being Element of A(),s holds [a,b
] in Q().s iff ex s9 being SortSymbol of S(), f being Function of (the Sorts of
A()).s9,(the Sorts of A()).s, x,y being Element of A(),s9 st P[f,s9,s] & [x,y]
in R().s9 & a = f.x & b = f.y
proof
now
let s1,s2 be SortSymbol of S();
set R = Q();
let f be Function of (the Sorts of A()).s1,(the Sorts of A()).s2;
assume
A5: P[f,s1,s2];
let a,b be set;
assume
A6: [a,b] in R.s1;
then
A7: b in (the Sorts of A()).s1 by ZFMISC_1:87;
a in (the Sorts of A()).s1 by A6,ZFMISC_1:87;
then consider
s9 being SortSymbol of S(), f9 being Function of (the Sorts of A(
)).s9,(the Sorts of A()).s1, x,y being Element of A(),s9 such that
A8: P[f9,s9,s1] and
A9: [x,y] in R().s9 and
A10: a = f9.x and
A11: b = f9.y by A4,A6,A7;
A12: f.a = (f*f9).x by A10,FUNCT_2:15;
A13: f.b = (f*f9).y by A11,FUNCT_2:15;
P[f*f9,s9,s2] by A2,A5,A8;
hence [f.a,f.b] in R.s2 by A4,A9,A12,A13;
end;
hence R[Q()] by A1;
thus R() c= Q()
proof
let i be object;
assume i in the carrier of S();
then reconsider s = i as SortSymbol of S();
R().s c= Q().s
proof
set f = id ((the Sorts of A()).s);
let x,y be object;
assume
A14: [x,y] in R().s;
then reconsider a = x, b = y as Element of A(),s by ZFMISC_1:87;
A15: f.b = b;
A16: P[f,s,s] by A3;
f.a = a;
hence thesis by A4,A14,A16,A15;
end;
hence thesis;
end;
let P be ManySortedRelation of A();
assume that
A17: R[P] and
A18: R() c= P;
let i be object;
assume i in the carrier of S();
then reconsider s = i as SortSymbol of S();
Q().s c= P.s
proof
let x,y be object;
assume
A19: [x,y] in Q().s;
then reconsider a = x, b = y as Element of A(),s by ZFMISC_1:87;
consider s9 being SortSymbol of S(), f being Function of (the Sorts of A()
).s9,(the Sorts of A()).s, u,v being Element of A(),s9 such that
A20: P[f,s9,s] and
A21: [u,v] in R().s9 and
A22: a = f.u and
A23: b = f.v by A4,A19;
R().s9 c= P.s9 by A18;
hence thesis by A1,A17,A20,A21,A22,A23;
end;
hence thesis;
end;
Lm1: now
let S be non empty non void ManySortedSign;
let A be non-empty MSAlgebra over S;
let R,Q be ManySortedRelation of A;
defpred R[ManySortedRelation of A] means $1 is invariant;
defpred P[Function, SortSymbol of S, SortSymbol of S] means TranslationRel S
reduces $2,$3 & $1 is Translation of A,$2,$3;
assume that
A1: for s being SortSymbol of S, a,b being Element of A,s holds [a,b] in
Q.s iff ex s9 being SortSymbol of S, f being Function of (the Sorts of A).s9,(
the Sorts of A).s, x,y being Element of A,s9 st P[f,s9,s] & [x,y] in R.s9 & a =
f.x & b = f.y;
A2: for s being SortSymbol of S holds P[id ((the Sorts of A).s),s,s] by Th16,
REWRITE1:12;
A3: now
let R be ManySortedRelation of A;
thus R[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 P[f,s1,s2] for a,b being set st [a,b
] in R.s1 holds [f.a,f.b] in R.s2 by Th28;
assume 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;
then
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;
hence R[R] by Th28;
end;
A4: for s1,s2,s3 being SortSymbol of S for f1 being Function of (the Sorts
of A).s1,(the Sorts of A).s2 for f2 being Function of (the Sorts of A).s2,(the
Sorts of A).s3 st P[f1,s1,s2] & P[f2,s2,s3] holds P[f2*f1,s1,s3] by Th18,
REWRITE1:16;
thus R[Q] & R c= Q & for P being ManySortedRelation of A st R[P] & R c= P
holds Q c= P from MSRelCl(A3,A4,A2,A1);
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;
func InvCl R -> invariant ManySortedRelation of A means
: Def11:
R c= it &
for Q being invariant ManySortedRelation of A st R c= Q holds it c= Q;
uniqueness
proof
let Q1,Q2 be invariant ManySortedRelation of A such that
A1: R c= Q1 and
A2: for Q being invariant ManySortedRelation of A st R c= Q holds Q1 c= Q and
A3: R c= Q2 and
A4: for Q being invariant ManySortedRelation of A st R c= Q holds Q2 c= Q;
Q1 c= Q2 & Q2 c= Q1 by A1,A2,A3,A4;
hence thesis by PBOOLE:146;
end;
existence
proof
defpred P[Function, SortSymbol of S, SortSymbol of S] means TranslationRel
S reduces $2,$3 & $1 is Translation of A,$2,$3;
defpred Z[SortSymbol of S,set,set] means ex s9 being SortSymbol of S, f
being Function of (the Sorts of A).s9,(the Sorts of A).$1, x,y being Element of
A,s9 st P[f,s9,$1] & [x,y] in R.s9 & $2 = f.x & $3 = f.y;
consider Q being ManySortedRelation of the Sorts of A such that
A5: for s being SortSymbol of S, a,b being Element of A,s holds [a,b]
in Q.s iff Z[s,a,b] from MSRExistence;
reconsider Q as ManySortedRelation of A;
reconsider Q as invariant ManySortedRelation of A by A5,Lm1;
take Q;
thus thesis by A5,Lm1;
end;
end;
theorem Th29:
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, x,y being Element of A,s9 st 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
let P be ManySortedRelation of the Sorts of A;
defpred Z[SortSymbol of S,set,set] means ex s9 being SortSymbol of S, f
being Function of (the Sorts of A).s9,(the Sorts of A).$1, x,y being Element of
A,s9 st TranslationRel S reduces s9,$1 & f is Translation of A,s9,$1 & [x,y] in
P.s9 & $2 = f.x & $3 = f.y;
let s be SortSymbol of S;
let a,b be Element of A,s;
consider Q being ManySortedRelation of the Sorts of A such that
A1: for s being SortSymbol of S, a,b being Element of A,s holds [a,b] in
Q.s iff Z[s,a,b] from MSRExistence;
reconsider R = P,Q as ManySortedRelation of A;
A2: R c= Q by A1,Lm1;
reconsider Q as invariant ManySortedRelation of A by A1,Lm1;
R c= InvCl R by Def11;
then
A3: Q c= InvCl R by A1,Lm1;
InvCl R c= Q by A2,Def11;
then
A4: InvCl R = Q by A3,PBOOLE:146;
hereby
assume [a,b] in (InvCl P).s;
then
ex s9 being SortSymbol of S, f being Function of (the Sorts of A).s9,(
the Sorts of A).s, x,y being Element of A,s9 st TranslationRel S reduces s9,s &
f is Translation of A,s9,s & [x,y] in P.s9 & a = f.x & b = f.y by A1,A4;
hence ex s9 being SortSymbol of S, x,y being Element of A,s9 st ex t being
Translation of A,s9,s st TranslationRel S reduces s9,s & [x,y] in P.s9 & a = t.
x & b = t.y;
end;
thus thesis by A1,A4;
end;
theorem Th30:
for R being stable ManySortedRelation of A holds InvCl R is stable
proof
let R be stable ManySortedRelation of A;
let h be Endomorphism of A;
let s be SortSymbol of S;
let a,b be set;
assume
A1: [a,b] in (InvCl R).s;
then
A2: b in (the Sorts of A).s by ZFMISC_1:87;
a in (the Sorts of A).s by A1,ZFMISC_1:87;
then consider s9 being SortSymbol of S, x,y being Element of A,s9, t being
Translation of A,s9,s such that
A3: TranslationRel S reduces s9,s and
A4: [x,y] in R.s9 and
A5: a = t.x and
A6: b = t.y by A1,A2,Th29;
consider T being Translation of A,s9,s such that
A7: T*(h.s9) = (h.s)*t by A3,Th26;
(T*(h.s9)).y = T.(h.s9.y) by FUNCT_2:15;
then
A8: T.(h.s9.y) = h.s.b by A6,A7,FUNCT_2:15;
(T*(h.s9)).x = T.(h.s9.x) by FUNCT_2:15;
then
A9: T.(h.s9.x) = h.s.a by A5,A7,FUNCT_2:15;
[h.s9.x,h.s9.y] in R.s9 by A4,Def9;
hence thesis by A3,A9,A8,Th29;
end;
Lm2: now
let S be non empty non void ManySortedSign;
let A be non-empty MSAlgebra over S;
let R,Q be ManySortedRelation of A;
defpred R[ManySortedRelation of A] means $1 is stable;
defpred P[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 P[f1,s1,s2] & P[f2,s2,s3] holds P[f2*f1,s1,s3]
proof
let s1,s2,s3 be SortSymbol of S;
let f1 be Function of (the Sorts of A).s1,(the Sorts of A).s2;
let f2 be Function of (the Sorts of A).s2,(the Sorts of A).s3;
assume
A2: s1 = s2;
given h1 being Endomorphism of A such that
A3: f1 = h1.s1;
assume
A4: s2 = s3;
given h2 being Endomorphism of A such that
A5: f2 = h2.s2;
thus s1 = s3 by A2,A4;
reconsider h = h2**h1 as Endomorphism of A;
take h;
thus thesis by A2,A3,A5,MSUALG_3:2;
end;
A6: 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
proof
let R be ManySortedRelation of A;
thus R is stable implies for s1,s2 be SortSymbol of S for f be 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;
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 P[f,s1,s2] for a,b being set st [a,b] in R.s1
holds [f.a,f.b] in R.s2;
thus R is stable
by A7;
end;
A8: for s being SortSymbol of S holds P[id ((the Sorts of A).s),s,s]
proof
reconsider h = id the Sorts of A as Endomorphism of A by Th4;
let s be SortSymbol of S;
thus s = s;
take h;
thus thesis by MSUALG_3:def 1;
end;
assume that
A9: for s being SortSymbol of S, a,b being Element of A,s holds [a,b] in
Q.s iff ex s9 being SortSymbol of S, f being Function of (the Sorts of A).s9,(
the Sorts of A).s, x,y being Element of A,s9 st P[f,s9,s] & [x,y] in R.s9 & a =
f.x & b = f.y;
thus R[Q] & R c= Q & for P being ManySortedRelation of A st R[P] & R c= P
holds Q c= P from MSRelCl(A6,A1,A8,A9);
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;
func StabCl R -> stable ManySortedRelation of A means
: Def12:
R c= it & for Q being stable ManySortedRelation of A st R c= Q holds it c= Q;
uniqueness
proof
let Q1,Q2 be stable ManySortedRelation of A such that
A1: R c= Q1 and
A2: for Q being stable ManySortedRelation of A st R c= Q holds Q1 c= Q and
A3: R c= Q2 and
A4: for Q being stable ManySortedRelation of A st R c= Q holds Q2 c= Q;
Q1 c= Q2 & Q2 c= Q1 by A1,A2,A3,A4;
hence thesis by PBOOLE:146;
end;
existence
proof
defpred P[Function, SortSymbol of S, SortSymbol of S] means $2 = $3 & ex h
being Endomorphism of A st $1 = h.$2;
defpred Z[SortSymbol of S,set,set] means ex s9 being SortSymbol of S, f
being Function of (the Sorts of A).s9,(the Sorts of A).$1, x,y being Element of
A,s9 st P[f,s9,$1] & [x,y] in R.s9 & $2 = f.x & $3 = f.y;
consider Q being ManySortedRelation of the Sorts of A such that
A5: for s being SortSymbol of S, a,b being Element of A,s holds [a,b]
in Q.s iff Z[s,a,b] from MSRExistence;
reconsider Q as ManySortedRelation of A;
reconsider Q as stable ManySortedRelation of A by A5,Lm2;
take Q;
thus thesis by A5,Lm2;
end;
end;
theorem Th31:
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
proof
let P be ManySortedRelation of the Sorts of A;
defpred Z[SortSymbol of S,set,set] means ex s9 being SortSymbol of S, f
being Function of (the Sorts of A).s9,(the Sorts of A).$1, x,y being Element of
A,s9 st s9 = $1 & (ex h being Endomorphism of A st f = h.s9) & [x,y] in P.s9 &
$2 = f.x & $3 = f.y;
let s be SortSymbol of S;
let a,b be Element of A,s;
consider Q being ManySortedRelation of the Sorts of A such that
A1: for s being SortSymbol of S, a,b being Element of A,s holds [a,b] in
Q.s iff Z[s,a,b] from MSRExistence;
reconsider R = P,Q as ManySortedRelation of A;
A2: R c= Q by A1,Lm2;
reconsider Q as stable ManySortedRelation of A by A1,Lm2;
R c= StabCl R by Def12;
then
A3: Q c= StabCl R by A1,Lm2;
StabCl R c= Q by A2,Def12;
then
A4: StabCl R = Q by A3,PBOOLE:146;
hereby
assume [a,b] in (StabCl P).s;
then
ex s9 being SortSymbol of S, f being Function of (the Sorts of A).s9,(
the Sorts of A).s, x,y being Element of A,s9 st s9 = s & (ex h being
Endomorphism of A st f = h.s9) & [x,y] in P.s9 & a = f.x & b = f.y by A1,A4;
hence
ex x,y being Element of A,s, h being Endomorphism of A st [x,y] in P.
s & a = h.s.x & b = h.s.y;
end;
thus thesis by A1,A4;
end;
theorem
InvCl StabCl R is stable by Th30;
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
: Def13:
R c=
it & for Q being invariant stable ManySortedRelation of A st R c= Q holds it c=
Q;
uniqueness
proof
let Q1,Q2 be invariant stable ManySortedRelation of A such that
A1: R c= Q1 and
A2: for Q being invariant stable ManySortedRelation of A st R c= Q
holds Q1 c= Q and
A3: R c= Q2 and
A4: for Q being invariant stable ManySortedRelation of A st R c= Q
holds Q2 c= Q;
Q1 c= Q2 & Q2 c= Q1 by A1,A2,A3,A4;
hence thesis by PBOOLE:146;
end;
existence
proof
reconsider Q = InvCl StabCl R as invariant stable ManySortedRelation of A
by Th30;
take Q;
A5: StabCl R c= InvCl StabCl R by Def11;
R c= StabCl R by Def12;
hence R c= Q by A5,PBOOLE:13;
let P be invariant stable ManySortedRelation of A;
assume R c= P;
then StabCl R c= P by Def12;
hence thesis by Def11;
end;
end;
registration
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;
coherence
proof
let i be object;
assume i in the carrier of S;
then reconsider s = i as SortSymbol of S;
set x = the Element of R.s;
R c= InvCl R by Def11;
then
A1: R.s c= (InvCl R).s;
x in R.s;
hence thesis by A1;
end;
cluster StabCl R -> non-empty;
coherence
proof
let i be object;
assume i in the carrier of S;
then reconsider s = i as SortSymbol of S;
set x = the Element of R.s;
R c= StabCl R by Def12;
then
A2: R.s c= (StabCl R).s;
x in R.s;
hence thesis by A2;
end;
cluster TRS R -> non-empty;
coherence
proof
let i be object;
assume i in the carrier of S;
then reconsider s = i as SortSymbol of S;
set x = the Element of R.s;
R c= TRS R by Def13;
then
A3: R.s c= (TRS R).s;
x in R.s;
hence thesis by A3;
end;
end;
theorem
for R being invariant ManySortedRelation of A holds InvCl R = R
proof
let R be invariant ManySortedRelation of A;
InvCl R c= R & R c= InvCl R by Def11;
hence thesis by PBOOLE:146;
end;
theorem
for R being stable ManySortedRelation of A holds StabCl R = R
proof
let R be stable ManySortedRelation of A;
StabCl R c= R & R c= StabCl R by Def12;
hence thesis by PBOOLE:146;
end;
theorem
for R being invariant stable ManySortedRelation of A holds TRS R = R
proof
let R be invariant stable ManySortedRelation of A;
TRS R c= R & R c= TRS R by Def13;
hence thesis by PBOOLE:146;
end;
theorem
StabCl R c= TRS R & InvCl R c= TRS R & StabCl InvCl R c= TRS R
proof
R c= TRS R by Def13;
hence StabCl R c= TRS R & InvCl R c= TRS R by Def11,Def12;
hence thesis by Def12;
end;
theorem Th37:
InvCl StabCl R = TRS R
proof
A1: StabCl R c= InvCl StabCl R by Def11;
R c= TRS R by Def13;
then StabCl R c= TRS R by Def12;
then
A2: InvCl StabCl R c= TRS R by Def11;
A3: InvCl StabCl R is invariant stable ManySortedRelation of A by Th30;
R c= StabCl R by Def12;
then R c= InvCl StabCl R by A1,PBOOLE:13;
then TRS R c= InvCl StabCl R by A3,Def13;
hence thesis by A2,PBOOLE:146;
end;
theorem
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 s9
being SortSymbol of S st TranslationRel S reduces s9, s & ex l,r being Element
of A,s9, h being Endomorphism of A, t being Translation of A, s9, s st [l,r] in
R.s9 & a = t.(h.s9.l) & b = t.(h.s9.r)
proof
let R be ManySortedRelation of the Sorts of A;
let s be SortSymbol of S, a,b be Element of A,s;
A1: InvCl StabCl R = TRS R by Th37;
hereby
assume [a,b] in (TRS R).s;
then consider s9 being SortSymbol of S, x,y being Element of A,s9, t being
Translation of A,s9,s such that
A2: TranslationRel S reduces s9,s and
A3: [x,y] in (StabCl R).s9 and
A4: a = t.x and
A5: b = t.y by A1,Th29;
take s9;
thus TranslationRel S reduces s9,s by A2;
reconsider t as Translation of A,s9,s;
consider u,v being Element of A,s9, h being Endomorphism of A such that
A6: [u,v] in R.s9 and
A7: x = h.s9.u and
A8: y = h.s9.v by A3,Th31;
take u,v,h;
take t;
thus [u,v] in R.s9 & a = t.((h.s9).u) & b = t.((h.s9).v) by A4,A5,A6,A7,A8;
end;
given s9 being SortSymbol of S such that
A9: TranslationRel S reduces s9, s and
A10: ex l,r being Element of A,s9, h being Endomorphism of A, t being
Translation of A, s9, s st [l,r] in R.s9 & a = t.((h.s9).l) & b = t.((h.s9).r);
consider l,r being Element of A,s9, h being Endomorphism of A, t being
Translation of A, s9, s such that
A11: [l,r] in R.s9 and
A12: a = t.((h.s9).l) and
A13: b = t.((h.s9).r) by A10;
[h.s9.l,h.s9.r] in (StabCl R).s9 by A11,Th31;
hence thesis by A1,A9,A12,A13,Th29;
end;
begin :: Equational theory
theorem Th39:
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
proof
let A be set;
let R,E be Relation of A;
set X = A;
assume
A1: for a,b being set st a in A & b in A holds [a,b] in E iff a,b
are_convertible_wrt R;
now
let x be object;
x,x are_convertible_wrt R by REWRITE1:26;
hence x in X implies [x,x] in E by A1;
end;
then
A2: E is_reflexive_in X by RELAT_2:def 1;
then
A3: field E = X by ORDERS_1:13;
dom E = X by A2,ORDERS_1:13;
hence E is total by PARTFUN1:def 2;
now
let x,y be object;
assume that
A4: x in X and
A5: y in X;
assume [x,y] in E;
then x,y are_convertible_wrt R by A1,A4,A5;
then y,x are_convertible_wrt R by REWRITE1:31;
hence [y,x] in E by A1,A4,A5;
end;
then E is_symmetric_in X by RELAT_2:def 3;
hence E is symmetric by A3,RELAT_2:def 11;
now
let x,y,z be object;
assume that
A6: x in X and
A7: y in X and
A8: z in X;
assume that
A9: [x,y] in E and
A10: [y,z] in E;
A11: y,z are_convertible_wrt R by A1,A7,A8,A10;
x,y are_convertible_wrt R by A1,A6,A7,A9;
then x,z are_convertible_wrt R by A11,REWRITE1:30;
hence [x,z] in E by A1,A6,A8;
end;
then E is_transitive_in X by RELAT_2:def 8;
hence thesis by A3,RELAT_2:def 16;
end;
theorem Th40:
for A being set, R being Relation of A for E being
Equivalence_Relation of A st R c= E for a,b being object st a in A & a,b
are_convertible_wrt R holds [a,b] in E
proof
let A be set, R be Relation of A;
let E be Equivalence_Relation of A such that
A1: R c= E;
let a,b be object such that
A2: a in A;
assume R \/ R~ reduces a,b;
then consider p being RedSequence of R \/ R~ such that
A3: p.1 = a and
A4: p.len p = b;
defpred Q[Nat] means $1 in dom p implies [a,p.$1] in E;
A5: for k be Nat st Q[k] holds Q[k+1]
proof
let i be Nat such that
A6: i in dom p implies [a,p.i] in E and
A7: i+1 in dom p;
A8: i <= i+1 by NAT_1:11;
i+1 <= len p by A7,FINSEQ_3:25;
then
A9: i <= len p by A8,XXREAL_0:2;
per cases;
suppose
i = 0;
hence thesis by A2,A3,EQREL_1:5;
end;
suppose
i > 0;
then
A10: i >= 0+1 by NAT_1:13;
then i in dom p by A9,FINSEQ_3:25;
then
A11: [p.i, p.(i+1)] in R \/ R~ by A7,REWRITE1:def 2;
then reconsider ppi = p.i, pj = p.(i+1) as Element of A by ZFMISC_1:87;
[p.i, p.(i+1)] in R or [p.i, p.(i+1)] in R~ by A11,XBOOLE_0:def 3;
then [p.i, p.(i+1)] in R or [p.(i+1), p.i] in R by RELAT_1:def 7;
then [ppi, pj] in E by A1,EQREL_1:6;
hence thesis by A6,A9,A10,EQREL_1:7,FINSEQ_3:25;
end;
end;
A12: len p in dom p by FINSEQ_5:6;
A13: Q[ 0 ] by FINSEQ_3:25;
for i being Nat holds Q[i] from NAT_1:sch 2(A13,A5);
hence thesis by A4,A12;
end;
theorem Th41:
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
proof
let A be non empty set, R be Relation of A;
defpred Z[object,object] means $1,$2 are_convertible_wrt R;
consider Q being Relation of A such that
A1: for a,b being object holds [a,b] in Q iff a in A & b in A & Z[a,b] from
RELSET_1:sch 1;
for a,b being set st a in A & b in A holds [a,b] in Q iff a,b
are_convertible_wrt R by A1;
then reconsider Q as Equivalence_Relation of A by Th39;
A2: now
let E be Equivalence_Relation of A;
assume
A3: R c= E;
thus Q c= E
proof
let x,y be object;
assume
A4: [x,y] in Q;
then
A5: x,y are_convertible_wrt R by A1;
x in A by A1,A4;
hence thesis by A3,A5,Th40;
end;
end;
R c= Q
proof
let a,b be object;
assume
A6: [a,b] in R;
then
A7: b in A by ZFMISC_1:87;
A8: a,b are_convertible_wrt R by A6,REWRITE1:29;
a in A by A6,ZFMISC_1:87;
hence thesis by A1,A7,A8;
end;
then Q = EqCl R by A2,MSUALG_5:def 1;
hence thesis by A1;
end;
theorem Th42:
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
proof
let S be non empty set, A be non-empty ManySortedSet of S;
let R be ManySortedRelation of A;
let s be Element of S;
(EqCl R).s = EqCl (R.s) by MSUALG_5:def 3;
hence thesis by Th41;
end;
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
EqCl R;
coherence by MSUALG_4:def 3;
end;
theorem Th43:
for R being ManySortedRelation of A holds R c= EqCl(R,A)
proof
let R be ManySortedRelation of A;
let i be object;
assume i in the carrier of S;
then reconsider s = i as SortSymbol of S;
EqCl(R,A).s = EqCl (R.s) by MSUALG_5:def 3;
hence thesis by MSUALG_5:def 1;
end;
theorem Th44:
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
let R be ManySortedRelation of A;
let E be MSEquivalence-like ManySortedRelation of A such that
A1: R c= E;
let i be object;
assume i in the carrier of S;
then reconsider s = i as SortSymbol of S;
A2: EqCl(R,A).s = EqCl (R.s) by MSUALG_5:def 3;
R.s c= E.s by A1;
hence thesis by A2,MSUALG_5:def 1;
end;
theorem Th45:
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
proof
let R be stable ManySortedRelation of A;
let s be SortSymbol of S;
let a,b be Element of A,s;
assume (R.s) \/ (R.s)~ reduces a,b;
then consider p being RedSequence of (R.s) \/ (R.s)~ such that
A1: p.1 = a and
A2: p.len p = b;
let h be Endomorphism of A;
defpred P[Nat] means $1 in dom p implies h.s.a, h.s.(p.$1)
are_convertible_wrt R.s;
A3: for i be Nat st P[i] holds P[i+1]
proof
let i be Nat such that
A4: i in dom p implies h.s.a, h.s.(p.i) are_convertible_wrt R.s and
A5: i+1 in dom p;
A6: i <= i+1 by NAT_1:11;
i+1 <= len p by A5,FINSEQ_3:25;
then
A7: i <= len p by A6,XXREAL_0:2;
per cases;
suppose
i = 0;
hence thesis by A1,REWRITE1:26;
end;
suppose
i > 0;
then
A8: i >= 0+1 by NAT_1:13;
then i in dom p by A7,FINSEQ_3:25;
then
A9: [p.i, p.(i+1)] in (R.s) \/ (R.s)~ by A5,REWRITE1:def 2;
then reconsider ppi = p.i, pj = p.(i+1) as Element of A,s by ZFMISC_1:87;
[p.i, p.(i+1)] in R.s or [p.i, p.(i+1)] in (R.s)~ by A9,XBOOLE_0:def 3;
then [p.i, p.(i+1)] in R.s or [p.(i+1), p.i] in R.s by RELAT_1:def 7;
then [h.s.ppi, h.s.pj] in R.s or [h.s.pj, h.s.ppi] in R.s by Def9;
then h.s.ppi, h.s.pj are_convertible_wrt R.s or h.s.pj, h.s.ppi
are_convertible_wrt R.s by REWRITE1:29;
then h.s.ppi, h.s.pj are_convertible_wrt R.s by REWRITE1:31;
hence thesis by A4,A7,A8,FINSEQ_3:25,REWRITE1:30;
end;
end;
A10: len p in dom p by FINSEQ_5:6;
A11: P[ 0 ] by FINSEQ_3:25;
for i being Nat holds P[i] from NAT_1:sch 2(A11,A3);
hence thesis by A2,A10;
end;
theorem Th46:
for R being stable ManySortedRelation of A holds EqCl(R,A) is stable
proof
let R be stable ManySortedRelation of A;
let h be Endomorphism of A;
let s be SortSymbol of S;
let a,b be set;
assume
A1: [a,b] in EqCl(R,A).s;
then reconsider a, b as Element of A,s by ZFMISC_1:87;
a,b are_convertible_wrt R.s by A1,Th42;
then h.s.a, h.s.b are_convertible_wrt R.s by Th45;
hence thesis by Th42;
end;
registration
let S,A;
let R be stable ManySortedRelation of A;
cluster EqCl(R,A) -> stable;
coherence by Th46;
end;
theorem Th47:
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
proof
let R be invariant ManySortedRelation of A;
let s1,s2 be SortSymbol of S;
let a,b be Element of A,s1;
assume (R.s1) \/ (R.s1)~ reduces a,b;
then consider p being RedSequence of (R.s1) \/ (R.s1)~ such that
A1: p.1 = a and
A2: p.len p = b;
let t be Function such that
A3: t is_e.translation_of A,s1,s2;
defpred P[Nat] means $1 in dom p implies t.a, t.(p.$1)
are_convertible_wrt R.s2;
A4: for i be Nat st P[i] holds P[i+1]
proof
let i be Nat such that
A5: i in dom p implies t.a, t.(p.i) are_convertible_wrt R.s2 and
A6: i+1 in dom p;
A7: i <= i+1 by NAT_1:11;
i+1 <= len p by A6,FINSEQ_3:25;
then
A8: i <= len p by A7,XXREAL_0:2;
per cases;
suppose
i = 0;
hence thesis by A1,REWRITE1:26;
end;
suppose
i > 0;
then
A9: i >= 0+1 by NAT_1:13;
then i in dom p by A8,FINSEQ_3:25;
then
A10: [p.i, p.(i+1)] in (R.s1) \/ (R.s1)~ by A6,REWRITE1:def 2;
then reconsider ppi = p.i, pj = p.(i+1) as Element of A,s1 by ZFMISC_1:87
;
[p.i, p.(i+1)] in R.s1 or [p.i, p.(i+1)] in (R.s1)~ by A10,XBOOLE_0:def 3
;
then [p.i, p.(i+1)] in R.s1 or [p.(i+1), p.i] in R.s1 by RELAT_1:def 7;
then [t.ppi, t.pj] in R.s2 or [t.pj, t.ppi] in R.s2 by A3,Def8;
then t.ppi, t.pj are_convertible_wrt R.s2 or t.pj, t.ppi
are_convertible_wrt R.s2 by REWRITE1:29;
then t.ppi, t.pj are_convertible_wrt R.s2 by REWRITE1:31;
hence thesis by A5,A8,A9,FINSEQ_3:25,REWRITE1:30;
end;
end;
A11: len p in dom p by FINSEQ_5:6;
A12: P[ 0 ] by FINSEQ_3:25;
for i being Nat holds P[i] from NAT_1:sch 2(A12,A4);
hence thesis by A2,A11;
end;
theorem Th48:
for R being invariant ManySortedRelation of A holds EqCl(R,A) is invariant
proof
let R be invariant ManySortedRelation of A;
let s1,s2 be SortSymbol of S;
let t be Function;
assume
A1: t is_e.translation_of A,s1,s2;
then reconsider
t as Function of (the Sorts of A).s1, (the Sorts of A).s2 by Th11;
let a,b be set;
assume
A2: [a,b] in EqCl(R,A).s1;
then reconsider a, b as Element of A,s1 by ZFMISC_1:87;
a,b are_convertible_wrt R.s1 by A2,Th42;
then t.a, t.b are_convertible_wrt R.s2 by A1,Th47;
hence thesis by Th42;
end;
registration
let S,A;
let R be invariant ManySortedRelation of A;
cluster EqCl(R,A) -> invariant;
coherence by Th48;
end;
theorem Th49:
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
proof
let S be non empty set, A be non-empty ManySortedSet of S;
let R,E be ManySortedRelation of A;
assume
A1: 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;
let i be object, P be Relation of A.i;
assume i in S;
then reconsider s = i as Element of S;
for a,b being set st a in A.s & b in A.s holds [a,b] in E.s iff a,b
are_convertible_wrt R.s by A1;
hence thesis by Th39;
end;
theorem Th50:
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
proof
let R,E be ManySortedRelation of A;
assume
A1: 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;
A2: E is stable
proof
let h be Endomorphism of A;
let s be SortSymbol of S;
let a,b be set;
assume
A3: [a,b] in E.s;
then reconsider x = a, y = b as Element of A,s by ZFMISC_1:87;
reconsider a9 = h.s.x, b9 = h.s.y as Element of A,s;
x,y are_convertible_wrt (TRS R).s by A1,A3;
then a9, b9 are_convertible_wrt (TRS R).s by Th45;
hence thesis by A1;
end;
A4: E is invariant
proof
let s1,s2 be SortSymbol of S;
let t be Function;
assume
A5: t is_e.translation_of A,s1,s2;
then reconsider
f = t as Function of (the Sorts of A).s1, (the Sorts of A ).s2
by Th11;
let a,b be set;
assume
A6: [a,b] in E.s1;
then reconsider x = a, y = b as Element of A,s1 by ZFMISC_1:87;
x,y are_convertible_wrt (TRS R).s1 by A1,A6;
then
A7: t.x,t.y are_convertible_wrt (TRS R).s2 by A5,Th47;
A8: t.y = f.y;
t.x = f.x;
hence thesis by A1,A8,A7;
end;
E is MSEquivalence_Relation-like by A1,Th49;
hence thesis by A2,A4,MSUALG_4:def 3;
end;
theorem Th51:
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
proof
let S be non empty set, A be non-empty ManySortedSet of S;
let R be ManySortedRelation of A;
let E be MSEquivalence_Relation-like ManySortedRelation of A such that
A1: R c= E;
let s be Element of S;
A2: E.s is Equivalence_Relation of A.s by MSUALG_4:def 2;
R.s c= E.s by A1;
hence thesis by A2,Th40;
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;
func EqTh R -> EquationalTheory of A means
: Def15:
R c= it & for Q being EquationalTheory of A st R c= Q holds it c= Q;
uniqueness
proof
let Q1,Q2 be EquationalTheory of A such that
A1: R c= Q1 and
A2: for Q being EquationalTheory of A st R c= Q holds Q1 c= Q and
A3: R c= Q2 and
A4: for Q being EquationalTheory of A st R c= Q holds Q2 c= Q;
Q1 c= Q2 & Q2 c= Q1 by A1,A2,A3,A4;
hence thesis by PBOOLE:146;
end;
existence
proof
defpred Z[SortSymbol of S,set,set] means $2,$3 are_convertible_wrt (TRS R)
.$1;
consider P being ManySortedRelation of the Sorts of A such that
A5: for s being SortSymbol of S for a,b being Element of A,s holds [a,
b] in P.s iff Z[s,a,b] from MSRExistence;
reconsider P as ManySortedRelation of A;
reconsider P as EquationalTheory of A by A5,Th50;
take P;
thus R c= P
proof
let i be object;
assume i in the carrier of S;
then reconsider s = i as SortSymbol of S;
R.s c= P.s
proof
let x,y be object;
assume
A6: [x,y] in R.s;
then reconsider a = x, b = y as Element of A,s by ZFMISC_1:87;
R c= TRS R by Def13;
then R.s c= (TRS R).s;
then a,b are_convertible_wrt (TRS R).s by A6,REWRITE1:29;
hence thesis by A5;
end;
hence thesis;
end;
let Q be EquationalTheory of A;
assume
A7: R c= Q;
let i be object;
assume i in the carrier of S;
then reconsider s = i as SortSymbol of S;
A8: TRS R c= Q by A7,Def13;
P.s c= Q.s
proof
let x,y be object;
assume
A9: [x,y] in P.s;
then reconsider a = x, b = y as Element of A,s by ZFMISC_1:87;
a,b are_convertible_wrt (TRS R).s by A5,A9;
hence thesis by A8,Th51;
end;
hence thesis;
end;
end;
theorem
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
let R be ManySortedRelation of A;
A1: R c= EqTh R by Def15;
hence EqCl(R,A) c= EqTh R by Th44;
thus thesis by A1,Def11,Def12,Def13;
end;
theorem
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
proof
let R be ManySortedRelation of A;
let s be SortSymbol of S, a,b be Element of A,s;
defpred Z[SortSymbol of S,set,set] means $2,$3 are_convertible_wrt (TRS R).
$1;
consider P being ManySortedRelation of the Sorts of A such that
A1: for s being SortSymbol of S for a,b being Element of A,s holds [a,b]
in P.s iff Z[s,a,b] from MSRExistence;
reconsider P as ManySortedRelation of A;
reconsider P as EquationalTheory of A by A1,Th50;
R c= P
proof
let i be object;
assume i in the carrier of S;
then reconsider s = i as SortSymbol of S;
R.s c= P.s
proof
let x,y be object;
assume
A2: [x,y] in R.s;
then reconsider a = x, b = y as Element of A,s by ZFMISC_1:87;
R c= TRS R by Def13;
then R.s c= (TRS R).s;
then a,b are_convertible_wrt (TRS R).s by A2,REWRITE1:29;
hence thesis by A1;
end;
hence thesis;
end;
then EqTh R c= P by Def15;
then (EqTh R).s c= P.s;
hence [a,b] in (EqTh R).s implies a,b are_convertible_wrt (TRS R).s by A1;
R c= EqTh R by Def15;
then TRS R c= EqTh R by Def13;
hence thesis by Th51;
end;
theorem
for R being ManySortedRelation of A holds EqTh R = EqCl(TRS R,A)
proof
let R be ManySortedRelation of A;
A1: TRS R c= EqCl(TRS R,A) by Th43;
R c= TRS R by Def13;
then R c= EqCl(TRS R,A) by A1,PBOOLE:13;
then
A2: EqTh R c= EqCl(TRS R,A) by Def15;
R c= EqTh R by Def15;
then TRS R c= EqTh R by Def13;
then EqCl(TRS R,A) c= EqTh R by Th44;
hence thesis by A2,PBOOLE:146;
end;