:: Institution of Many-sorted Algebras, Part { I } : Signature Reduct
:: of an Algebra
:: by Grzegorz Bancerek
::
:: Received December 30, 1996
:: Copyright (c) 1996-2016 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 XBOOLE_0, STRUCT_0, MSUALG_1, RELAT_1, PBOOLE, MSATERM, MSAFREE,
SUBSET_1, DTCONSTR, FINSEQ_1, TDGROUP, TREES_3, TARSKI, FUNCT_1, NUMBERS,
MARGREL1, PARTFUN1, PZFMISC1, TREES_4, FUNCT_6, MSUALG_3, MSUALG_6,
PUA2MSS1, CARD_3, RLTOPSP1, FUNCT_4, REWRITE1, REALSET1, CAT_1, ZFMISC_1,
NAT_1, MEMBER_1, INSTALG1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, RELAT_1, FUNCT_1,
NUMBERS, FINSEQ_1, STRUCT_0, FINSEQ_2, CARD_3, LANG1, TREES_3, TREES_4,
DTCONSTR, REWRITE1, FUNCT_7, PBOOLE, PZFMISC1, MSUALG_1, PARTFUN1,
FUNCT_2, PRALG_2, MSUALG_3, PUA2MSS1, MSAFREE, MSATERM, MSUALG_6;
constructors NAT_1, REWRITE1, PZFMISC1, FUNCT_7, PRALG_2, MSUALG_3, MSATERM,
PUA2MSS1, MSUALG_6, RELSET_1, NUMBERS;
registrations XBOOLE_0, RELAT_1, FUNCT_1, FUNCT_2, FUNCOP_1, PBOOLE, TREES_3,
STRUCT_0, MSUALG_1, MSUALG_3, MSAFREE, MSATERM, MSUALG_9, RELSET_1,
FINSEQ_1, ORDINAL1;
requirements SUBSET, BOOLE;
definitions TARSKI, STRUCT_0, FUNCT_1, MSUALG_1, MSUALG_3, PUA2MSS1, MSUALG_6,
PBOOLE, PZFMISC1;
equalities MSUALG_1;
expansions FUNCT_1, MSUALG_3, PUA2MSS1, PBOOLE;
theorems ZFMISC_1, RELAT_1, FUNCT_1, GRFUNC_1, FUNCT_2, FINSEQ_1, TARSKI,
TREES_4, PBOOLE, MSUALG_1, MSUALG_3, REWRITE1, PRALG_2, PUA2MSS1,
MSAFREE, MSATERM, EXTENS_1, MSUALG_6, RELSET_1, XBOOLE_0, MSALIMIT,
PARTFUN1, FINSEQ_2, XTUPLE_0;
schemes CLASSES1, MSATERM, MSUALG_6, FUNCT_1;
begin :: Preliminaries
theorem Th1:
for S being non empty non void ManySortedSign for o being
OperSymbol of S for V being non-empty ManySortedSet of the carrier of S for x
being set holds x is ArgumentSeq of Sym(o,V) iff x is Element of Args(o,
FreeMSA V)
proof
let S be non empty non void ManySortedSign;
let o be OperSymbol of S;
let V be non-empty ManySortedSet of the carrier of S;
let x be set;
A1: TS DTConMSA V = S-Terms V by MSATERM:def 1;
A2: FreeMSA V = MSAlgebra(#FreeSort V, FreeOper V#) by MSAFREE:def 14;
hereby
assume x is ArgumentSeq of Sym(o,V);
then reconsider p = x as ArgumentSeq of Sym(o,V);
reconsider p as FinSequence of TS DTConMSA V by MSATERM:def 1;
Sym(o, V) ==> roots p by MSATERM:21;
hence x is Element of Args(o, FreeMSA V) by A2,MSAFREE:10;
end;
assume x is Element of Args(o, FreeMSA V);
then reconsider x as Element of Args(o, FreeMSA V);
rng x c= TS DTConMSA V
proof
let y be object;
assume y in rng x;
then consider z being object such that
A3: z in dom x and
A4: y = x.z by FUNCT_1:def 3;
reconsider z as Element of NAT by A3;
A5: (FreeSort V).((the_arity_of o)/.z) = FreeSort(V,(the_arity_of o)/.z)
by MSAFREE:def 11;
dom x = dom the_arity_of o by MSUALG_6:2;
then y in (FreeSort V).((the_arity_of o)/.z) by A2,A3,A4,MSUALG_6:2;
hence thesis by A5;
end;
then reconsider x as FinSequence of TS DTConMSA V by FINSEQ_1:def 4;
Sym(o, V) ==> roots x by A2,MSAFREE:10;
hence thesis by A1,MSATERM:21;
end;
registration
let S be non empty non void ManySortedSign;
let V be non-empty ManySortedSet of the carrier of S;
let o be OperSymbol of S;
cluster -> DTree-yielding for Element of Args(o, FreeMSA V);
coherence by Th1;
end;
theorem Th2:
for S being non empty non void ManySortedSign for A1,A2 being
MSAlgebra over S st the Sorts of A1 is_transformable_to the Sorts of A2 for o
being OperSymbol of S st Args(o,A1) <> {} holds Args(o,A2) <> {}
proof
let S be non void non empty ManySortedSign;
let A1,A2 be MSAlgebra over S such that
A1: for i be set st i in the carrier of S & (the Sorts of A2).i = {}
holds (the Sorts of A1).i = {};
let o be OperSymbol of S;
assume
A2: Args(o,A1) <> {};
now
let i be Element of NAT;
assume i in dom the_arity_of o;
then (the Sorts of A1).((the_arity_of o)/.i) <> {} by A2,MSUALG_6:3;
hence (the Sorts of A2).((the_arity_of o)/.i) <> {} by A1;
end;
hence thesis by MSUALG_6:3;
end;
theorem Th3:
for S being non empty non void ManySortedSign for o being
OperSymbol of S for V being non-empty ManySortedSet of the carrier of S for x
being Element of Args(o, FreeMSA V) holds Den(o,FreeMSA V).x = [o, the carrier
of S]-tree x
proof
let S be non empty non void ManySortedSign;
let o be OperSymbol of S;
let V be non-empty ManySortedSet of the carrier of S;
let x be Element of Args(o, FreeMSA V);
A1: FreeMSA V = MSAlgebra(#FreeSort(V), FreeOper(V)#) by MSAFREE:def 14;
reconsider p = x as ArgumentSeq of Sym(o,V) by Th1;
A2: Sym(o, V) = [o, the carrier of S] by MSAFREE:def 9;
p is FinSequence of TS DTConMSA V & Sym(o, V) ==> roots p by MSATERM:21,def 1
;
then DenOp(o,V).x = [o, the carrier of S]-tree x by A2,MSAFREE:def 12;
hence thesis by A1,MSAFREE:def 13;
end;
theorem
for S being non empty non void ManySortedSign for A,B being MSAlgebra
over S st the MSAlgebra of A = the MSAlgebra of B for o being OperSymbol of S
holds Den(o,A) = Den(o,B);
theorem Th5:
for S being non empty non void ManySortedSign for A1,A2,B1,B2
being MSAlgebra over S st the MSAlgebra of A1 = the MSAlgebra of B1 & the
MSAlgebra of A2 = the MSAlgebra of B2 for f being ManySortedFunction of A1,A2
for g being ManySortedFunction of B1,B2 st f = g for o being OperSymbol of S st
Args(o,A1) <> {} & Args(o,A2) <> {} for x being Element of Args(o,A1) for y
being Element of Args(o,B1) st x = y holds f#x = g#y
proof
let S be non empty non void ManySortedSign;
let A1,A2,B1,B2 be MSAlgebra over S such that
A1: the MSAlgebra of A1 = the MSAlgebra of B1 & the MSAlgebra of A2 =
the MSAlgebra of B2;
let f be ManySortedFunction of A1,A2;
let g be ManySortedFunction of B1,B2 such that
A2: f = g;
let o be OperSymbol of S such that
A3: Args(o,A1) <> {} & Args(o,A2) <> {};
let x be Element of Args(o,A1);
let y be Element of Args(o,B1);
assume
A4: x = y;
f#x = (Frege(f*the_arity_of o)).x by A3,MSUALG_3:def 5;
hence thesis by A1,A2,A3,A4,MSUALG_3:def 5;
end;
theorem
for S being non empty non void ManySortedSign for A1,A2,B1,B2 being
MSAlgebra over S st the MSAlgebra of A1 = the MSAlgebra of B1 & the MSAlgebra
of A2 = the MSAlgebra of B2 & the Sorts of A1 is_transformable_to the Sorts of
A2 for h being ManySortedFunction of A1,A2 st h is_homomorphism A1,A2 ex h9
being ManySortedFunction of B1,B2 st h9 = h & h9 is_homomorphism B1,B2
proof
let S be non empty non void ManySortedSign;
let A1,A2,B1,B2 be MSAlgebra over S such that
A1: the MSAlgebra of A1 = the MSAlgebra of B1 and
A2: the MSAlgebra of A2 = the MSAlgebra of B2 and
A3: the Sorts of A1 is_transformable_to the Sorts of A2;
let h be ManySortedFunction of A1,A2 such that
A4: h is_homomorphism A1,A2;
reconsider h9 = h as ManySortedFunction of B1,B2 by A1,A2;
take h9;
thus h9 = h;
let o be OperSymbol of S;
assume
A5: Args(o,B1) <> {};
then
A6: Args(o,B2) <> {} by A1,A2,A3,Th2;
let x be Element of Args(o,B1);
reconsider y = x as Element of Args(o,A1) by A1;
thus (h9.(the_result_sort_of o)).(Den(o,B1).x) = (h.(the_result_sort_of o)).
(Den(o,A1).y) by A1
.= Den(o,A2).(h#y) by A1,A4,A5
.= Den(o,B2).(h9#x) by A1,A2,A5,A6,Th5;
end;
definition
let S be ManySortedSign;
attr S is feasible means
: Def1:
the carrier of S = {} implies the carrier' of S = {};
end;
theorem Th7:
for S being ManySortedSign holds
S is feasible iff dom the ResultSort of S = the carrier' of S
by FUNCT_2:def 1;
registration
cluster non empty -> feasible for ManySortedSign;
coherence;
cluster void -> feasible for ManySortedSign;
coherence;
cluster empty feasible -> void for ManySortedSign;
coherence;
cluster non void feasible -> non empty for ManySortedSign;
coherence;
end;
registration
cluster non void non empty for ManySortedSign;
existence
proof
set S = the non void non empty ManySortedSign;
take S;
thus thesis;
end;
end;
theorem Th8:
for S being feasible ManySortedSign holds id the carrier of S, id
the carrier' of S form_morphism_between S,S
proof
let S be feasible ManySortedSign;
per cases;
suppose
S is void;
hence thesis by MSALIMIT:6;
end;
suppose
S is non void;
then reconsider S as non void feasible ManySortedSign;
S is non empty;
hence thesis by PUA2MSS1:28;
end;
end;
theorem Th9:
for S1,S2 being ManySortedSign for f,g being Function st f,g
form_morphism_between S1,S2 holds f is Function of the carrier of S1, the
carrier of S2 & g is Function of the carrier' of S1, the carrier' of S2
by FUNCT_2:2;
begin :: Subsignature
definition
let S be feasible ManySortedSign;
mode Subsignature of S -> ManySortedSign means
: Def2:
id the carrier of it, id the carrier' of it form_morphism_between it,S;
existence
proof
take S;
thus thesis by Th8;
end;
end;
theorem Th10:
for S being feasible ManySortedSign, T being Subsignature of S
holds the carrier of T c= the carrier of S & the carrier' of T c= the carrier'
of S
proof
let S be feasible ManySortedSign, T be Subsignature of S;
set g = id the carrier' of T;
id the carrier of T, g form_morphism_between T,S by Def2;
then rng id the carrier of T c= the carrier of S & rng id the carrier' of T
c= the carrier' of S;
hence thesis;
end;
registration
let S be feasible ManySortedSign;
cluster -> feasible for Subsignature of S;
coherence
proof
let T be Subsignature of S;
set f = id the carrier of T, g = id the carrier' of T;
A1: dom g = the carrier' of T;
f, g form_morphism_between T,S by Def2;
then
A2: f*the ResultSort of T = (the ResultSort of S)*g;
assume the carrier of T = {};
then
A3: {} = (the ResultSort of S)*g by A2;
the carrier' of S = dom the ResultSort of S & rng g = the carrier' of
T by Th7;
hence thesis by A3,A1,Th10,RELAT_1:27;
end;
end;
theorem Th11:
for S being feasible ManySortedSign, T being Subsignature of S
holds the ResultSort of T c= the ResultSort of S & the Arity of T c= the Arity
of S
proof
let S be feasible ManySortedSign, T be Subsignature of S;
set f = id the carrier of T, g = id the carrier' of T;
A1: dom the Arity of T = the carrier' of T by FUNCT_2:def 1;
A2: f, g form_morphism_between T,S by Def2;
A3: now
let x be object;
A4: rng the Arity of T c= (the carrier of T)* by RELAT_1:def 19;
assume
A5: x in dom the Arity of T;
then (the Arity of T).x in rng the Arity of T by FUNCT_1:def 3;
then reconsider
p = (the Arity of T).x as Element of (the carrier of T)* by A4;
g.x = x by A1,A5,FUNCT_1:17;
then rng p c= the carrier of T & f*p = (the Arity of S).x by A2,A1,A5,
FINSEQ_1:def 4;
hence (the Arity of T).x = (the Arity of S).x by RELAT_1:53;
end;
the ResultSort of T = f*the ResultSort of T by FUNCT_2:17
.= (the ResultSort of S)*g by A2;
hence the ResultSort of T c= the ResultSort of S by RELAT_1:50;
dom the Arity of S = the carrier' of S by FUNCT_2:def 1;
then dom the Arity of T c= dom the Arity of S by A1,Th10;
hence thesis by A3,GRFUNC_1:2;
end;
theorem Th12:
for S being feasible ManySortedSign, T being Subsignature of S
holds the Arity of T = (the Arity of S)|the carrier' of T & the ResultSort of T
= (the ResultSort of S)|the carrier' of T
proof
let S be feasible ManySortedSign, T be Subsignature of S;
A1: the Arity of T c= the Arity of S by Th11;
the carrier of T = {} implies the carrier' of T = {} by Def1;
then
A2: dom the ResultSort of T = the carrier' of T by FUNCT_2:def 1;
dom the Arity of T = the carrier' of T & the ResultSort of T c= the
ResultSort of S by Th11,FUNCT_2:def 1;
hence thesis by A2,A1,GRFUNC_1:23;
end;
theorem Th13:
for S,T being feasible ManySortedSign st the carrier of T c= the
carrier of S & the Arity of T c= the Arity of S & the ResultSort of T c= the
ResultSort of S holds T is Subsignature of S
proof
let S,T be feasible ManySortedSign;
assume that
A1: the carrier of T c= the carrier of S and
A2: the Arity of T c= the Arity of S and
A3: the ResultSort of T c= the ResultSort of S;
set f = id the carrier of T, g = id the carrier' of T;
thus dom f = the carrier of T & dom g = the carrier' of T;
thus rng f c= the carrier of S by A1;
A4: dom the Arity of T = the carrier' of T by FUNCT_2:def 1;
dom the Arity of S = the carrier' of S & rng g = the carrier' of T by
FUNCT_2:def 1;
hence rng g c= the carrier' of S by A2,A4,GRFUNC_1:2;
A5: dom the ResultSort of T = the carrier' of T by Th7;
rng the ResultSort of T c= the carrier of T by RELAT_1:def 19;
hence f*the ResultSort of T = the ResultSort of T by RELAT_1:53
.= (the ResultSort of S)|the carrier' of T by A3,A5,GRFUNC_1:23
.= (the ResultSort of S)*g by RELAT_1:65;
let o be set, p be Function;
assume that
A6: o in the carrier' of T and
A7: p = (the Arity of T).o;
reconsider q = p as Element of (the carrier of T)* by A6,A7,FUNCT_2:5;
rng q c= the carrier of T by FINSEQ_1:def 4;
hence f*p = p by RELAT_1:53
.= (the Arity of S).o by A2,A4,A6,A7,GRFUNC_1:2
.= (the Arity of S).(g.o) by A6,FUNCT_1:17;
end;
theorem
for S,T being feasible ManySortedSign st the carrier of T c= the
carrier of S & the Arity of T = (the Arity of S)|the carrier' of T & the
ResultSort of T = (the ResultSort of S)|the carrier' of T holds T is
Subsignature of S
proof
let S,T be feasible ManySortedSign such that
A1: the carrier of T c= the carrier of S;
assume that
A2: the Arity of T = (the Arity of S)|the carrier' of T and
A3: the ResultSort of T = (the ResultSort of S)|the carrier' of T;
the Arity of T c= the Arity of S by A2,RELAT_1:59;
hence thesis by A1,A3,Th13,RELAT_1:59;
end;
theorem Th15:
for S being feasible ManySortedSign holds S is Subsignature of S
proof
let S be feasible ManySortedSign;
thus id the carrier of S, id the carrier' of S form_morphism_between S,S by
Th8;
end;
theorem
for S1 being feasible ManySortedSign for S2 being Subsignature of S1
for S3 being Subsignature of S2 holds S3 is Subsignature of S1
proof
let S1 be feasible ManySortedSign;
let S2 be Subsignature of S1, S3 be Subsignature of S2;
rng id the carrier of S3 = the carrier of S3;
then
A1: (id the carrier of S2)*id the carrier of S3 = id the carrier of S3 by Th10,
RELAT_1:53;
rng id the carrier' of S3 = the carrier' of S3;
then
A2: (id the carrier' of S2)*id the carrier' of S3 = id the carrier' of S3 by
Th10,RELAT_1:53;
id the carrier of S3,id the carrier' of S3 form_morphism_between S3,S2 &
id the carrier of S2,id the carrier' of S2 form_morphism_between S2,S1 by Def2;
hence id the carrier of S3,id the carrier' of S3 form_morphism_between S3,
S1 by A1,A2,PUA2MSS1:29;
end;
theorem
for S1 being feasible ManySortedSign for S2 being Subsignature of S1
st S1 is Subsignature of S2 holds the ManySortedSign of S1 = the ManySortedSign
of S2
proof
let S1 be feasible ManySortedSign;
let S2 be Subsignature of S1;
A1: the carrier of S2 c= the carrier of S1 by Th10;
assume
A2: S1 is Subsignature of S2;
then the carrier of S1 c= the carrier of S2 by Th10;
then
A3: the carrier of S1 = the carrier of S2 by A1,XBOOLE_0:def 10;
A4: the carrier' of S2 c= the carrier' of S1 by Th10;
the carrier' of S1 c= the carrier' of S2 by A2,Th10;
then
A5: the carrier' of S1 = the carrier' of S2 by A4,XBOOLE_0:def 10;
A6: the Arity of S2 c= the Arity of S1 by Th11;
A7: the ResultSort of S2 c= the ResultSort of S1 by Th11;
the ResultSort of S1 c= the ResultSort of S2 by A2,Th11;
then
A8: the ResultSort of S1 = the ResultSort of S2 by A7,XBOOLE_0:def 10;
the Arity of S1 c= the Arity of S2 by A2,Th11;
hence thesis by A6,A3,A5,A8,XBOOLE_0:def 10;
end;
registration
let S be non empty ManySortedSign;
cluster non empty for Subsignature of S;
existence
proof
reconsider T = S as Subsignature of S by Th15;
take T;
thus thesis;
end;
end;
registration
let S be non void feasible ManySortedSign;
cluster non void for Subsignature of S;
existence
proof
reconsider T = S as Subsignature of S by Th15;
take T;
thus thesis;
end;
end;
theorem
for S being feasible ManySortedSign, S9 being Subsignature of S for T
being ManySortedSign, f,g being Function st f,g form_morphism_between S,T holds
f|the carrier of S9, g|the carrier' of S9 form_morphism_between S9,T
proof
let S be feasible ManySortedSign, S9 be Subsignature of S;
let T be ManySortedSign, f,g be Function;
A1: g|the carrier' of S9 = g*id the carrier' of S9 by RELAT_1:65;
id the carrier of S9, id the carrier' of S9 form_morphism_between S9,S &
f| the carrier of S9 = f*id the carrier of S9 by Def2,RELAT_1:65;
hence thesis by A1,PUA2MSS1:29;
end;
theorem
for S being ManySortedSign, T being feasible ManySortedSign for T9
being Subsignature of T, f,g being Function st f,g form_morphism_between S,T9
holds f,g form_morphism_between S,T
proof
let S be ManySortedSign, T be feasible ManySortedSign;
let T9 be Subsignature of T, f,g be Function such that
A1: f,g form_morphism_between S,T9;
rng f c= the carrier of T9 by A1;
then
A2: (id the carrier of T9)*f = f by RELAT_1:53;
rng g c= the carrier' of T9 by A1;
then
A3: (id the carrier' of T9)*g = g by RELAT_1:53;
id the carrier of T9, id the carrier' of T9 form_morphism_between T9,T
by Def2;
hence thesis by A1,A2,A3,PUA2MSS1:29;
end;
theorem
for S being ManySortedSign, T being feasible ManySortedSign for T9
being Subsignature of T, f,g being Function st f,g form_morphism_between S,T &
rng f c= the carrier of T9 & rng g c= the carrier' of T9 holds f,g
form_morphism_between S,T9
proof
let S be ManySortedSign, T be feasible ManySortedSign;
let T9 be Subsignature of T, f,g be Function;
assume that
A1: dom f = the carrier of S and
A2: dom g = the carrier' of S and
rng f c= the carrier of T and
rng g c= the carrier' of T and
A3: f*the ResultSort of S = (the ResultSort of T)*g and
A4: for o being set, p being Function st o in the carrier' of S & p = (
the Arity of S).o holds f*p = (the Arity of T).(g.o) and
A5: rng f c= the carrier of T9 and
A6: rng g c= the carrier' of T9;
thus dom f = the carrier of S & dom g = the carrier' of S by A1,A2;
thus rng f c= the carrier of T9 & rng g c= the carrier' of T9 by A5,A6;
thus f*the ResultSort of S = (the ResultSort of T)*((id the carrier' of T9)*
g) by A3,A6,RELAT_1:53
.= (the ResultSort of T)*(id the carrier' of T9)*g by RELAT_1:36
.= ((the ResultSort of T)|the carrier' of T9)*g by RELAT_1:65
.= (the ResultSort of T9)*g by Th12;
let o be set, p be Function;
assume that
A7: o in the carrier' of S and
A8: p = (the Arity of S).o;
A9: the Arity of T9 c= the Arity of T & dom the Arity of T9 = the carrier'
of T9 by Th11,FUNCT_2:def 1;
g.o in rng g by A2,A7,FUNCT_1:def 3;
then (the Arity of T9).(g.o) = (the Arity of T).(g.o) by A6,A9,GRFUNC_1:2;
hence thesis by A4,A7,A8;
end;
begin :: Signature reduct
definition
let S1,S2 be non empty ManySortedSign;
let A be MSAlgebra over S2;
let f,g be Function such that
A1: f,g form_morphism_between S1,S2;
func A|(S1,f,g) -> strict MSAlgebra over S1 means
: Def3:
the Sorts of it =
(the Sorts of A)*f & the Charact of it = (the Charact of A)*g;
existence
proof
dom f = the carrier of S1 & rng f c= the carrier of S2 by A1;
then reconsider
f9 = f as Function of the carrier of S1,the carrier of S2 by FUNCT_2:def 1
,RELSET_1:4;
A2: rng g c= the carrier' of S2 by A1;
A3: dom g = the carrier' of S1 by A1;
then reconsider
g9 = g as Function of the carrier' of S1,the carrier' of S2 by A2,FUNCT_2:2
;
dom the Charact of A = the carrier' of S2 by PARTFUN1:def 2;
then dom ((the Charact of A)*g9) = the carrier' of S1 by A3,A2,RELAT_1:27;
then reconsider
C = (the Charact of A)*g9 as ManySortedSet of the carrier' of
S1 by PARTFUN1:def 2;
C is ManySortedFunction of ((the Sorts of A)*f9)#*the Arity of S1, (
the Sorts of A)*f9*the ResultSort of S1
proof
let o be object;
assume
A4: o in the carrier' of S1;
then reconsider
p1 = (the Arity of S1).o as Element of (the carrier of S1 )*
by FUNCT_2:5;
A5: g.o in rng g by A3,A4,FUNCT_1:def 3;
then reconsider
p2 = (the Arity of S2).(g.o) as Element of (the carrier of S2
)* by A2,FUNCT_2:5;
reconsider o as OperSymbol of S1 by A4;
A6: C.o = (the Charact of A).(g9.o) by A2,A4,A5,FUNCT_2:15;
(the Sorts of A)*f9*the ResultSort of S1 = (the Sorts of A)*(f9*the
ResultSort of S1) by RELAT_1:36
.= (the Sorts of A)*((the ResultSort of S2)*g) by A1
.= (the Sorts of A)*(the ResultSort of S2)*g by RELAT_1:36;
then
A7: ((the Sorts of A)*f9*the ResultSort of S1).o = ((the Sorts of A)*(
the ResultSort of S2)).(g9.o) by A2,A4,A5,FUNCT_2:15;
A8: (the Sorts of A)*f9*p1 = (the Sorts of A)*(f9*p1) by RELAT_1:36
.= (the Sorts of A)*p2 by A1,A4;
(((the Sorts of A)*f9)#*the Arity of S1).o = ((the Sorts of A)*f9)#
.p1 by A4,FUNCT_2:15
.= product((the Sorts of A)*f9*p1) by FINSEQ_2:def 5
.= (the Sorts of A)#.p2 by A8,FINSEQ_2:def 5
.= ((the Sorts of A)#*the Arity of S2).(g9.o) by A2,A5,FUNCT_2:15;
hence thesis by A2,A5,A7,A6,PBOOLE:def 15;
end;
then reconsider
C as ManySortedFunction of ((the Sorts of A)*f9)#*the Arity of
S1, (the Sorts of A)*f9*the ResultSort of S1;
take MSAlgebra(#(the Sorts of A)*f9, C#);
thus thesis;
end;
correctness;
end;
definition
let S2,S1 be non empty ManySortedSign;
let A be MSAlgebra over S2;
func A|S1 -> strict MSAlgebra over S1 equals
A|(S1, id the carrier of S1, id
the carrier' of S1);
correctness;
end;
theorem
for S1,S2 being non empty ManySortedSign for A,B being MSAlgebra over
S2 st the MSAlgebra of A = the MSAlgebra of B for f,g being Function st f,g
form_morphism_between S1,S2 holds A|(S1,f,g) = B|(S1,f,g)
proof
let S1,S2 be non empty ManySortedSign;
let A,B be MSAlgebra over S2 such that
A1: the MSAlgebra of A = the MSAlgebra of B;
let f,g be Function;
assume
A2: f,g form_morphism_between S1,S2;
then
the Sorts of A|(S1,f,g) = (the Sorts of A)*f & the Charact of A|(S1,f,g)
= ( the Charact of A)*g by Def3;
hence thesis by A1,A2,Def3;
end;
theorem Th22:
for S1,S2 being non empty ManySortedSign for A being non-empty
MSAlgebra over S2 for f,g being Function st f,g form_morphism_between S1,S2
holds A|(S1,f,g) is non-empty
proof
let S1,S2 be non empty ManySortedSign;
let A be non-empty MSAlgebra over S2;
let f,g be Function;
assume f,g form_morphism_between S1,S2;
then the Sorts of (A|(S1,f,g)) = (the Sorts of A)*f by Def3;
hence the Sorts of (A|(S1,f,g)) is non-empty;
end;
registration
let S2 be non empty ManySortedSign;
let S1 be non empty Subsignature of S2;
let A be non-empty MSAlgebra over S2;
cluster A|S1 -> non-empty;
coherence
by Def2,Th22;
end;
theorem Th23:
for S1,S2 being non void non empty ManySortedSign for f,g being
Function st f,g form_morphism_between S1,S2 for A being MSAlgebra over S2 for
o1 being OperSymbol of S1, o2 being OperSymbol of S2 st o2 = g.o1 holds Den(o1,
A|(S1,f,g)) = Den(o2,A)
proof
let S1,S2 be non void non empty ManySortedSign;
let f,g be Function;
assume
A1: f,g form_morphism_between S1,S2;
then reconsider
g9 = g as Function of the carrier' of S1, the carrier' of S2 by Th9;
let A be MSAlgebra over S2;
let o1 be OperSymbol of S1, o2 be OperSymbol of S2;
assume o2 = g.o1;
then (the Charact of A).o2 = ((the Charact of A)*g9).o1 by FUNCT_2:15
.= (the Charact of A|(S1,f,g)).o1 by A1,Def3;
hence thesis;
end;
theorem Th24:
for S1,S2 being non void non empty ManySortedSign for f,g being
Function st f,g form_morphism_between S1,S2 for A being MSAlgebra over S2 for
o1 being OperSymbol of S1, o2 being OperSymbol of S2 st o2 = g.o1 holds Args(o2
,A) = Args(o1,A|(S1,f,g)) & Result(o1,A|(S1,f,g)) = Result(o2,A)
proof
let S1,S2 be non void non empty ManySortedSign;
let f,g be Function such that
A1: f,g form_morphism_between S1,S2;
A2: dom f = the carrier of S1 by A1;
let A be MSAlgebra over S2;
let o1 be OperSymbol of S1, o2 be OperSymbol of S2;
assume
A3: o2 = g.o1;
thus Args(o2,A) = product ((the Sorts of A)*the_arity_of o2) by PRALG_2:3
.= product ((the Sorts of A)*(f*the_arity_of o1)) by A1,A3
.= product ((the Sorts of A)*f*the_arity_of o1) by RELAT_1:36
.= product ((the Sorts of A|(S1,f,g))*the_arity_of o1) by A1,Def3
.= Args(o1,A|(S1,f,g)) by PRALG_2:3;
dom g = the carrier' of S1 by A1;
then the_result_sort_of o2 = ((the ResultSort of S2)*g).o1 by A3,FUNCT_1:13
.= (f*the ResultSort of S1).o1 by A1
.= f.the_result_sort_of o1 by FUNCT_2:15;
hence Result(o2,A) = (the Sorts of A).(f.the_result_sort_of o1) by PRALG_2:3
.= ((the Sorts of A)*f).the_result_sort_of o1 by A2,FUNCT_1:13
.= (the Sorts of A|(S1,f,g)).the_result_sort_of o1 by A1,Def3
.= Result(o1,A|(S1,f,g)) by PRALG_2:3;
end;
theorem Th25:
for S being non empty ManySortedSign for A being MSAlgebra over
S holds A|(S, id the carrier of S, id the carrier' of S) = the MSAlgebra of A
proof
let S be non empty ManySortedSign;
let A be MSAlgebra over S;
set f = id the carrier of S, g = id the carrier' of S;
dom the Charact of A = the carrier' of S by PARTFUN1:def 2;
then
A1: the Charact of the MSAlgebra of A = (the Charact of A)*g by RELAT_1:52;
dom the Sorts of A = the carrier of S by PARTFUN1:def 2;
then
A2: the Sorts of the MSAlgebra of A = (the Sorts of A)*f by RELAT_1:52;
f,g form_morphism_between S,S by Th8;
hence thesis by A2,A1,Def3;
end;
theorem
for S being non empty ManySortedSign for A being MSAlgebra over S
holds A|S = the MSAlgebra of A by Th25;
theorem Th27:
for S1,S2,S3 being non empty ManySortedSign for f1,g1 being
Function st f1,g1 form_morphism_between S1,S2 for f2,g2 being Function st f2,g2
form_morphism_between S2,S3 for A being MSAlgebra over S3 holds A|(S1,f2*f1,g2*
g1) = (A|(S2,f2,g2))|(S1,f1,g1)
proof
let S1,S2,S3 be non empty ManySortedSign;
let f1,g1 be Function such that
A1: f1,g1 form_morphism_between S1,S2;
let f2,g2 be Function such that
A2: f2,g2 form_morphism_between S2,S3;
A3: f2*f1, g2*g1 form_morphism_between S1,S3 by A1,A2,PUA2MSS1:29;
let A be MSAlgebra over S3;
A4: the Charact of (A|(S2,f2,g2))|(S1,f1,g1) = (the Charact of A|(S2,f2,g2))
*g1 by A1,Def3
.= (the Charact of A)*g2*g1 by A2,Def3
.= (the Charact of A)*(g2*g1) by RELAT_1:36;
the Sorts of (A|(S2,f2,g2))|(S1,f1,g1) = (the Sorts of A|(S2,f2,g2))*f1
by A1,Def3
.= (the Sorts of A)*f2*f1 by A2,Def3
.= (the Sorts of A)*(f2*f1) by RELAT_1:36;
hence thesis by A3,A4,Def3;
end;
theorem
for S1 being non empty feasible ManySortedSign for S2 being non empty
Subsignature of S1 for S3 being non empty Subsignature of S2 for A being
MSAlgebra over S1 holds A|S3 = (A|S2)|S3
proof
let S1 be non empty feasible ManySortedSign;
let S2 be non empty Subsignature of S1;
let S3 be non empty Subsignature of S2;
let A be MSAlgebra over S1;
set f1 = id the carrier of S2, g1 = id the carrier' of S2;
set f2 = id the carrier of S3, g2 = id the carrier' of S3;
rng f2 = the carrier of S3;
then
A1: f1*f2 = f2 by Th10,RELAT_1:53;
rng g2 = the carrier' of S3;
then
A2: g1*g2 = g2 by Th10,RELAT_1:53;
f1,g1 form_morphism_between S2,S1 & f2,g2 form_morphism_between S3,S2 by Def2
;
hence thesis by A1,A2,Th27;
end;
theorem Th29:
for S1,S2 being non empty ManySortedSign for f being Function of
the carrier of S1, the carrier of S2 for g being Function st f,g
form_morphism_between S1,S2 for A1,A2 being MSAlgebra over S2 for h being
ManySortedFunction of the Sorts of A1, the Sorts of A2 holds h*f is
ManySortedFunction of the Sorts of A1|(S1,f,g), the Sorts of A2|(S1,f,g)
proof
let S1,S2 be non empty ManySortedSign;
let f be Function of the carrier of S1, the carrier of S2;
let g be Function such that
A1: f,g form_morphism_between S1,S2;
let A1,A2 be MSAlgebra over S2;
let h be ManySortedFunction of the Sorts of A1,the Sorts of A2;
set B1 = A1|(S1,f,g), B2 = A2|(S1,f,g);
let x be object;
assume x in the carrier of S1;
then reconsider s = x as SortSymbol of S1;
reconsider fs = f.s as SortSymbol of S2;
A2: (h*f).s = h.fs & (the Sorts of A1).fs = ((the Sorts of A1)*f).s by
FUNCT_2:15;
A3: (the Sorts of A2).fs = ((the Sorts of A2)*f).s by FUNCT_2:15;
(the Sorts of A1)*f = the Sorts of B1 & (the Sorts of A2)*f = the Sorts
of B2 by A1,Def3;
hence thesis by A2,A3;
end;
theorem
for S1 being non empty ManySortedSign for S2 being non empty
Subsignature of S1 for A1,A2 being MSAlgebra over S1 for h being
ManySortedFunction of the Sorts of A1, the Sorts of A2 holds h|the carrier of
S2 is ManySortedFunction of the Sorts of A1|S2, the Sorts of A2|S2
proof
let S1 be non empty ManySortedSign;
let S2 be non empty Subsignature of S1;
set f = id the carrier of S2, g = id the carrier' of S2;
let A1,A2 be MSAlgebra over S1;
let h be ManySortedFunction of the Sorts of A1, the Sorts of A2;
A1: f,g form_morphism_between S2,S1 by Def2;
then reconsider f as Function of the carrier of S2, the carrier of S1 by Th9;
h*f is ManySortedFunction of the Sorts of A1|(S2,f,g), the Sorts of A2|(
S2,f,g) by A1,Th29;
hence thesis by RELAT_1:65;
end;
theorem Th31:
for S1,S2 being non empty ManySortedSign for f,g being Function
st f,g form_morphism_between S1,S2 for A being MSAlgebra over S2 holds (id the
Sorts of A)*f = id the Sorts of A|(S1,f,g)
proof
let S1,S2 be non empty ManySortedSign;
let f,g be Function such that
A1: f,g form_morphism_between S1,S2;
dom f = the carrier of S1 & rng f c= the carrier of S2 by A1;
then reconsider f as Function of the carrier of S1, the carrier of S2 by
FUNCT_2:def 1,RELSET_1:4;
let A be MSAlgebra over S2;
now
let i be object;
assume i in the carrier of S1;
then reconsider s = i as SortSymbol of S1;
thus ((id the Sorts of A)*f).i = (id the Sorts of A).(f.s) by FUNCT_2:15
.= id ((the Sorts of A).(f.s)) by MSUALG_3:def 1
.= id (((the Sorts of A)*f).s) by FUNCT_2:15
.= id ((the Sorts of A|(S1,f,g)).s) by A1,Def3
.= (id the Sorts of A|(S1,f,g)).i by MSUALG_3:def 1;
end;
hence thesis by PBOOLE:3;
end;
theorem
for S1 being non empty ManySortedSign for S2 being non empty
Subsignature of S1 for A being MSAlgebra over S1 holds (id the Sorts of A)|the
carrier of S2 = id the Sorts of A|S2
proof
let S1 be non empty ManySortedSign;
let S2 be non empty Subsignature of S1;
set f = id the carrier of S2, g = id the carrier' of S2;
let A be MSAlgebra over S1;
f,g form_morphism_between S2,S1 by Def2;
then (id the Sorts of A)*f = id the Sorts of A|S2 by Th31;
hence thesis by RELAT_1:65;
end;
theorem Th33:
for S1,S2 being non void non empty ManySortedSign for f,g being
Function st f,g form_morphism_between S1,S2 for A,B being MSAlgebra over S2 for
h2 being ManySortedFunction of A,B for h1 being ManySortedFunction of A|(S1,f,g
),B|(S1,f,g) st h1 = h2*f for o1 being OperSymbol of S1, o2 being OperSymbol of
S2 st o2 = g.o1 & Args(o2,A) <> {} & Args(o2,B) <> {} for x2 being Element of
Args(o2,A) for x1 being Element of Args(o1,A|(S1,f,g)) st x2 = x1 holds h1#x1 =
h2#x2
proof
let S1,S2 be non void non empty ManySortedSign;
let f,g be Function such that
A1: f,g form_morphism_between S1,S2;
let A2,B2 be MSAlgebra over S2;
set A1 = A2|(S1,f,g), B1 = B2|(S1,f,g);
let h2 be ManySortedFunction of A2,B2;
let h1 be ManySortedFunction of A1,B1 such that
A2: h1 = h2*f;
let o1 be OperSymbol of S1, o2 be OperSymbol of S2 such that
A3: o2 = g.o1;
assume that
A4: Args(o2,A2) <> {} and
A5: Args(o2,B2) <> {};
let x2 be Element of Args(o2,A2);
let x1 be Element of Args(o1,A1);
assume
A6: x2 = x1;
then reconsider f1 = x1, f2 = x2, g2 = h2#x2 as Function by A4,A5,MSUALG_6:1;
A7: Args(o2,A2) = Args(o1,A1) by A1,A3,Th24;
then
A8: dom f1 = dom the_arity_of o1 by A4,MSUALG_3:6;
A9: dom f2 = dom the_arity_of o2 by A4,MSUALG_3:6;
A10: now
let i be Nat;
assume
A11: i in dom f1;
dom f = the carrier of S1 by A1;
then h1.((the_arity_of o1)/.i) = h2.(f.((the_arity_of o1)/.i)) by A2,
FUNCT_1:13
.= h2.(f.((the_arity_of o1).i)) by A8,A11,PARTFUN1:def 6
.= h2.((f*the_arity_of o1).i) by A8,A11,FUNCT_1:13
.= h2.((the_arity_of o2).i) by A1,A3
.= h2.((the_arity_of o2)/.i) by A6,A9,A11,PARTFUN1:def 6;
hence g2.i = (h1.((the_arity_of o1)/.i)).(f1.i) by A4,A5,A6,A11,MSUALG_3:24
;
end;
Args(o2,B2) = Args(o1,B1) by A1,A3,Th24;
hence thesis by A4,A5,A7,A10,MSUALG_3:24;
end;
theorem Th34:
for S,S9 being non empty non void ManySortedSign for A1,A2 being
MSAlgebra over S st the Sorts of A1 is_transformable_to the Sorts of A2 for h
being ManySortedFunction of A1,A2 st h is_homomorphism A1,A2 for f being
Function of the carrier of S9, the carrier of S for g being Function st f,g
form_morphism_between S9,S ex h9 being ManySortedFunction of A1|(S9,f,g), A2|(
S9,f,g) st h9 = h*f & h9 is_homomorphism A1|(S9,f,g), A2|(S9,f,g)
proof
let S,S9 be non empty non void ManySortedSign;
let A1,A2 be MSAlgebra over S such that
A1: the Sorts of A1 is_transformable_to the Sorts of A2;
let h be ManySortedFunction of A1,A2 such that
A2: h is_homomorphism A1,A2;
let f be Function of the carrier of S9, the carrier of S;
let g be Function such that
A3: f,g form_morphism_between S9,S;
A4: dom g = the carrier' of S9 & rng g c= the carrier' of S by A3;
set B1 = A1|(S9,f,g), B2 = A2|(S9,f,g);
reconsider g as Function of the carrier' of S9, the carrier' of S by A4,
FUNCT_2:def 1,RELSET_1:4;
A5: f*the ResultSort of S9 = (the ResultSort of S)*g by A3;
reconsider h9 = h*f as ManySortedFunction of B1,B2 by A3,Th29;
take h9;
thus h9 = h*f;
let o be OperSymbol of S9;
set go = g.o;
assume
A6: Args(o,B1) <> {};
let x be Element of Args(o,B1);
reconsider y = x as Element of Args(go,A1) by A3,Th24;
A7: h9.the_result_sort_of o = h.(f.the_result_sort_of o) by FUNCT_2:15
.= h.(((the ResultSort of S)*g).o) by A5,FUNCT_2:15
.= h.the_result_sort_of go by FUNCT_2:15;
A8: Den(o,B1) = Den(go,A1) & Den(o,B2) = Den(go,A2) by A3,Th23;
A9: Args(o,B1) = Args(g.o,A1) by A3,Th24;
A10: Args(o,B2) = Args(g.o,A2) by A3,Th24;
then Args(o,B2) <> {} by A1,A6,A9,Th2;
then h9#x = h#y by A3,A6,A9,A10,Th33;
hence thesis by A2,A6,A9,A8,A7;
end;
theorem
for S being non void feasible ManySortedSign for S9 being non void
Subsignature of S for A1,A2 being MSAlgebra over S st the Sorts of A1
is_transformable_to the Sorts of A2 for h being ManySortedFunction of A1,A2 st
h is_homomorphism A1,A2 ex h9 being ManySortedFunction of A1|S9, A2|S9 st h9 =
h|the carrier of S9 & h9 is_homomorphism A1|S9, A2|S9
proof
let S be non void feasible ManySortedSign;
let S9 be non void Subsignature of S;
let A1,A2 be MSAlgebra over S such that
A1: the Sorts of A1 is_transformable_to the Sorts of A2;
set f = id the carrier of S9, g = id the carrier' of S9;
A2: f,g form_morphism_between S9,S by Def2;
then reconsider f as Function of the carrier of S9, the carrier of S by Th9;
let h be ManySortedFunction of A1,A2;
assume h is_homomorphism A1,A2;
then consider
h9 being ManySortedFunction of A1|(S9,f,g), A2|(S9,f,g) such that
A3: h9 = h*f and
A4: h9 is_homomorphism A1|(S9,f,g), A2|(S9,f,g) by A1,A2,Th34;
consider k being ManySortedFunction of A1|S9, A2|S9 such that
A5: k = h9 and
k is_homomorphism A1|S9, A2|S9 by A4;
take k;
thus thesis by A3,A4,A5,RELAT_1:65;
end;
theorem Th36:
for S,S9 being non empty non void ManySortedSign for A being
non-empty MSAlgebra over S for f being Function of the carrier of S9, the
carrier of S for g being Function st f,g form_morphism_between S9,S for B being
non-empty MSAlgebra over S9 st B = A|(S9,f,g) for s1,s2 being SortSymbol of S9,
t being Function st t is_e.translation_of B, s1, s2 holds t is_e.translation_of
A, f.s1, f.s2
proof
let S,S9 be non empty non void ManySortedSign;
let A be non-empty MSAlgebra over S;
let f be Function of the carrier of S9, the carrier of S;
let g be Function such that
A1: f,g form_morphism_between S9,S;
A2: dom g = the carrier' of S9 & rng g c= the carrier' of S by A1;
let B be non-empty MSAlgebra over S9 such that
A3: B = A|(S9,f,g);
reconsider g as Function of the carrier' of S9, the carrier' of S by A2,
FUNCT_2:def 1,RELSET_1:4;
let s1,s2 be SortSymbol of S9, t be Function;
given o being OperSymbol of S9 such that
A4: the_result_sort_of o = s2 and
A5: 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,B) & t = transl(o,i,a,B);
A6: f*the_arity_of o = the_arity_of (g.o) by A1;
take g.o;
f*the ResultSort of S9 = (the ResultSort of S)*g by A1;
hence the_result_sort_of (g.o) = (f*the ResultSort of S9).o by FUNCT_2:15
.= f.s2 by A4,FUNCT_2:15;
consider i being (Element of NAT), a being Function such that
A7: i in dom the_arity_of o and
A8: (the_arity_of o)/.i = s1 and
A9: a in Args(o,B) and
A10: t = transl(o,i,a,B) by A5;
take i;
rng the_arity_of o c= the carrier of S9 & dom f = the carrier of S9 by
FINSEQ_1:def 4,FUNCT_2:def 1;
hence i in dom the_arity_of (g.o) by A7,A6,RELAT_1:27;
hence
A11: (the_arity_of (g.o))/.i = (the_arity_of (g.o)).i by PARTFUN1:def 6
.= f.((the_arity_of o).i) by A7,A6,FUNCT_1:13
.= f.s1 by A7,A8,PARTFUN1:def 6;
then
A12: dom transl(g.o, i, a, A) = (the Sorts of A).(f.s1) by MSUALG_6:def 4;
A13: the Sorts of B = (the Sorts of A)*f by A1,A3,Def3;
then
A14: (the Sorts of B).s1 = (the Sorts of A).(f.s1) by FUNCT_2:15;
A15: now
let x be object;
assume x in (the Sorts of B).s1;
then
t.x = Den(o,B).(a+*(i,x)) & transl(g.o,i,a,A).x = Den(g.o,A).(a+*(i,x
) ) by A8,A10,A11,A14,MSUALG_6:def 4;
hence t.x = transl(g.o,i,a,A).x by A1,A3,Th23;
end;
take a;
thus a in Args(g.o,A) by A1,A3,A9,Th24;
dom t = (the Sorts of B).s1 by A8,A10,MSUALG_6:def 4;
hence thesis by A12,A13,A15,FUNCT_2:15;
end;
Lm1: for S,S9 being non empty non void ManySortedSign for A being non-empty
MSAlgebra over S for f being Function of the carrier of S9, the carrier of S
for g being Function st f,g form_morphism_between S9,S for B being non-empty
MSAlgebra over S9 st B = A|(S9,f,g) for s1,s2 being SortSymbol of S9 st
TranslationRel S9 reduces s1,s2 holds TranslationRel S reduces f.s1, f.s2 & for
t being Translation of B, s1, s2 holds t is Translation of A, f.s1, f.s2
proof
let S,S9 be non void non empty ManySortedSign;
let A be non-empty MSAlgebra over S;
let f be Function of the carrier of S9, the carrier of S;
let g be Function such that
A1: f,g form_morphism_between S9,S;
defpred P[set, SortSymbol of S9, SortSymbol of S9] means TranslationRel S
reduces f.$2, f.$3 & $1 is Translation of A, f.$2,f.$3;
let B be non-empty MSAlgebra over S9 such that
A2: B = A|(S9,f,g);
A3: for s1,s2,s3 being SortSymbol of S9 st TranslationRel S9 reduces s1,s2
for t being Translation of B,s1,s2 st P[t,s1,s2] for h being Function st h
is_e.translation_of B,s2,s3 holds P[h*t,s1,s3]
proof
let s1,s2,s3 be SortSymbol of S9 such that
TranslationRel S9 reduces s1,s2;
let t be Translation of B,s1,s2 such that
A4: P[t,s1,s2];
let h be Function;
assume
A5: h is_e.translation_of B,s2,s3;
then [f.s2, f.s3] in TranslationRel S by A1,A2,Th36,MSUALG_6:12;
then
A6: TranslationRel S reduces f.s2, f.s3 by REWRITE1:15;
h is_e.translation_of A, f.s2, f.s3 by A1,A2,A5,Th36;
hence thesis by A4,A6,MSUALG_6:19,REWRITE1:16;
end;
let s1,s2 be SortSymbol of S9;
assume
A7: TranslationRel S9 reduces s1,s2;
A8: for s being SortSymbol of S9 holds P[id ((the Sorts of B).s),s,s]
proof
let s be SortSymbol of S9;
thus TranslationRel S reduces f.s, f.s by REWRITE1:12;
the Sorts of B = (the Sorts of A)*f by A1,A2,Def3;
then (the Sorts of B).s = (the Sorts of A).(f.s) by FUNCT_2:15;
hence thesis by MSUALG_6:16;
end;
for s1,s2 being SortSymbol of S9 st TranslationRel S9 reduces s1,s2 for
t being Translation of B,s1,s2 holds P[t,s1,s2] from MSUALG_6:sch 1(A8,A3);
hence thesis by A7;
end;
theorem
for S,S9 being non empty non void ManySortedSign for f being Function
of the carrier of S9, the carrier of S for g being Function st f,g
form_morphism_between S9,S for s1,s2 being SortSymbol of S9 st TranslationRel
S9 reduces s1,s2 holds TranslationRel S reduces f.s1, f.s2
proof
let S,S9 be non empty non void ManySortedSign;
set A = the non-empty MSAlgebra over S;
let f be Function of the carrier of S9, the carrier of S;
let g be Function;
assume
A1: f,g form_morphism_between S9,S;
then A|(S9,f,g) is non-empty MSAlgebra over S9 by Th22;
hence thesis by A1,Lm1;
end;
theorem
for S,S9 being non void non empty ManySortedSign for A being non-empty
MSAlgebra over S for f being Function of the carrier of S9, the carrier of S
for g being Function st f,g form_morphism_between S9,S for B being non-empty
MSAlgebra over S9 st B = A|(S9,f,g) for s1,s2 being SortSymbol of S9 st
TranslationRel S9 reduces s1,s2 for t being Translation of B, s1, s2 holds t is
Translation of A, f.s1, f.s2 by Lm1;
begin :: Translating homomorphism
scheme
GenFuncEx{S() -> non empty non void ManySortedSign, A() -> non-empty
MSAlgebra over S(), X() -> non-empty ManySortedSet of the carrier of S(),
F(object,object) -> set}:
ex h being ManySortedFunction of FreeMSA X(), A() st h
is_homomorphism FreeMSA X(), A() & for s being SortSymbol of S() for x being
Element of X().s holds h.s.root-tree [x,s] = F(x,s)
provided
A1: for s being SortSymbol of S() for x being Element of X().s holds F(x
,s) in (the Sorts of A()).s
proof
defpred P[object,object] means
ex f being Function of (FreeGen X()).$1, (the Sorts
of A()).$1 st $2 = f & for x being Element of X().$1 holds f.root-tree [x,$1] =
F(x,$1);
A2: for a being object st a in the carrier of S() ex y being object st P[a,y]
proof
let a be object;
assume a in the carrier of S();
then reconsider s = a as SortSymbol of S();
defpred P[object,object] means
ex x being Element of X().s st $1 = root-tree [x,s] & $2 = F(x,s);
A3: (FreeGen X()).s = FreeGen(s, X()) by MSAFREE:def 16;
A4: for y being object st y in (FreeGen X()).s
ex z being object st z in (the Sorts of A()).s & P[y,z]
proof
let y be object;
assume y in (FreeGen X()).s;
then consider a be set such that
A5: a in X().s and
A6: y = root-tree [a,s] by A3,MSAFREE:def 15;
reconsider a as Element of X().s by A5;
take z = F(a,s);
thus z in (the Sorts of A()).s by A1;
take a;
thus thesis by A6;
end;
consider f being Function such that
A7: dom f = (FreeGen X()).s & rng f c= (the Sorts of A()).s and
A8: for y being object st y in (FreeGen X()).s holds P[y,f.y] from
FUNCT_1:sch 6(A4);
reconsider f as Function of (FreeGen X()).a, (the Sorts of A()).a by A7,
FUNCT_2:2;
take y = f, f;
thus y = f;
let x be Element of X().a;
root-tree [x,s] in (FreeGen X()).s by A3,MSAFREE:def 15;
then consider z being Element of X().s such that
A9: root-tree [x,s] = root-tree [z,s] and
A10: f.root-tree [x,s] = F(z,s) by A8;
[x,s] = [z,s] by A9,TREES_4:4;
hence thesis by A10,XTUPLE_0:1;
end;
consider h being Function such that
A11: dom h = the carrier of S() and
A12: for a being object st a in the carrier of S() holds P[a,h.a] from
CLASSES1:sch 1(A2);
reconsider h as ManySortedSet of the carrier of S() by A11,PARTFUN1:def 2
,RELAT_1:def 18;
h is ManySortedFunction of FreeGen X(), the Sorts of A()
proof
let a be object;
assume a in the carrier of S();
then
ex f being Function of (FreeGen X()).a, (the Sorts of A()).a st h.a =
f & for x being Element of X().a holds f.root-tree [x,a] = F(x,a) by A12;
hence thesis;
end;
then reconsider h as ManySortedFunction of FreeGen X(), the Sorts of A();
consider H being ManySortedFunction of FreeMSA X(), A() such that
A13: H is_homomorphism FreeMSA X(), A() and
A14: H||FreeGen X() = h by MSAFREE:def 5;
take H;
thus H is_homomorphism FreeMSA X(), A() by A13;
let s be SortSymbol of S(), x be Element of X().s;
A15: ex f being Function of (FreeGen X()).s, (the Sorts of A()).s st h.s = f
& for x being Element of X().s holds f.root-tree [x,s] = F(x,s) by A12;
reconsider t = root-tree [x,s] as Term of S(), X() by MSATERM:4;
(FreeGen X()).s = FreeGen(s,X()) by MSAFREE:def 16;
then
A16: t in (FreeGen X()).s by MSAFREE:def 15;
h.s = (H.s)|((FreeGen X()).s) by A14,MSAFREE:def 1;
then H.s.root-tree [x,s] = h.s.root-tree [x,s] by A16,FUNCT_1:49;
hence thesis by A15;
end;
theorem Th39:
for I being set, A,B being ManySortedSet of I for C being
ManySortedSubset of A for F being ManySortedFunction of A,B for i being set st
i in I for f,g being Function st f = F.i & g = (F||C).i for x being set st x in
C.i holds g.x = f.x
proof
let I be set, A,B be ManySortedSet of I;
let C be ManySortedSubset of A;
let F be ManySortedFunction of A,B;
let i be set;
assume
A1: i in I;
then reconsider Fi = F.i as Function of A.i, B.i by PBOOLE:def 15;
let f,g be Function;
assume that
A2: f = F.i and
A3: g = (F||C).i;
let x be set;
g = Fi|(C.i) by A1,A3,MSAFREE:def 1;
hence thesis by A2,FUNCT_1:49;
end;
registration
let S be non void non empty ManySortedSign;
let X be non-empty ManySortedSet of the carrier of S;
cluster FreeGen X -> non-empty;
coherence;
end;
definition
let S1,S2 be non empty non void ManySortedSign;
let X be non-empty ManySortedSet of the carrier of S2;
let f be Function of the carrier of S1, the carrier of S2;
let g be Function such that
A1: f,g form_morphism_between S1,S2;
func hom(f,g,X,S1,S2) -> ManySortedFunction of FreeMSA(X*f), (FreeMSA X)|(S1
,f,g) means
: Def5:
it is_homomorphism FreeMSA(X*f), (FreeMSA X)|(S1,f,g) & for
s being SortSymbol of S1, x being Element of (X*f).s holds it.s.root-tree [x,s]
= root-tree [x,f.s];
existence
proof
set A = (FreeMSA X)|(S1,f,g);
the Sorts of A = (the Sorts of FreeMSA X)*f by A1,Def3;
then reconsider A as non-empty MSAlgebra over S1 by MSUALG_1:def 3;
deffunc F(set,set)=root-tree [$1,f.$2];
A2: now
let s be SortSymbol of S1, x be Element of (X*f).s;
reconsider fs = f.s as SortSymbol of S2;
reconsider y = x as Element of X.fs by FUNCT_2:15;
reconsider t = root-tree [y,fs] as Term of S2,X by MSATERM:4;
the_sort_of t = fs by MSATERM:14;
then t in FreeSort(X,fs) by MSATERM:def 5;
then
A3: t in (FreeSort X).fs by MSAFREE:def 11;
FreeMSA X = MSAlgebra(#FreeSort X,FreeOper X#) & the Sorts of A = (
the Sorts of FreeMSA X)*f by A1,Def3,MSAFREE:def 14;
hence F(x,s) in (the Sorts of A).s by A3,FUNCT_2:15;
end;
consider H being ManySortedFunction of FreeMSA(X*f), A such that
A4: H is_homomorphism FreeMSA(X*f), A & for s being SortSymbol of S1
for x being Element of (X*f).s holds H.s.root-tree [x,s] = F(x,s) from
GenFuncEx(A2);
reconsider G = H as ManySortedFunction of FreeMSA(X*f), (FreeMSA X)|(S1,f,
g);
take G;
thus thesis by A4;
end;
uniqueness
proof
reconsider A1 = (FreeMSA X)|(S1,f,g) as non-empty MSAlgebra over S1 by A1
,Th22;
let G1,G2 be ManySortedFunction of the Sorts of FreeMSA(X*f), the Sorts of
(FreeMSA X)|(S1,f,g) such that
A5: G1 is_homomorphism FreeMSA(X*f), (FreeMSA X)|(S1,f,g) and
A6: for s being SortSymbol of S1, x being Element of (X*f).s holds G1
.s.root-tree [x,s] = root-tree [x,f.s] and
A7: G2 is_homomorphism FreeMSA(X*f), (FreeMSA X)|(S1,f,g) and
A8: for s being SortSymbol of S1, x being Element of (X*f).s holds G2
.s.root-tree [x,s] = root-tree [x,f.s];
set H1 = G1, H2 = G2;
A9: now
let x be object;
assume x in the carrier of S1;
then reconsider s = x as SortSymbol of S1;
reconsider g1 = (H1||FreeGen (X*f)).s, g2 = (H2||FreeGen (X*f)).s as
Function of (FreeGen (X*f)).s, (the Sorts of A1).s;
now
let z be Element of (FreeGen (X*f)).s;
FreeGen(s,X*f) = (FreeGen(X*f)).s by MSAFREE:def 16;
then consider a being set such that
A10: a in (X*f).s and
A11: z = root-tree [a,s] by MSAFREE:def 15;
reconsider a as Element of (X*f).s by A10;
thus g1.z = H1.s.z by Th39
.= root-tree [a,f.s] by A6,A11
.= H2.s.z by A8,A11
.= g2.z by Th39;
end;
hence (H1||FreeGen (X*f)).x = (H2||FreeGen (X*f)).x by FUNCT_2:63;
end;
A1 = (FreeMSA X)|(S1,f,g);
hence thesis by A5,A7,A9,EXTENS_1:14,PBOOLE:3;
end;
end;
theorem Th40:
for S1,S2 being non void non empty ManySortedSign for X being
non-empty ManySortedSet of the carrier of S2 for f being Function of the
carrier of S1, the carrier of S2 for g being Function st f,g
form_morphism_between S1,S2 for o being OperSymbol of S1, p being Element of
Args(o,FreeMSA(X*f)) for q being FinSequence st q = hom(f,g,X,S1,S2)#p holds (
hom(f,g,X,S1,S2).the_result_sort_of o).([o,the carrier of S1]-tree p) = [g.o,
the carrier of S2]-tree q
proof
let S1,S2 be non void non empty ManySortedSign;
let X be non-empty ManySortedSet of the carrier of S2;
let f be Function of the carrier of S1, the carrier of S2;
let g be Function;
set F = hom(f,g,X,S1,S2);
assume
A1: f,g form_morphism_between S1,S2;
then reconsider
h = g as Function of the carrier' of S1, the carrier' of S2 by Th9;
let o be OperSymbol of S1, p be Element of Args(o,FreeMSA(X*f));
let q be FinSequence;
assume
A2: q = F#p;
then
A3: q is Element of Args(h.o,FreeMSA X) by A1,Th24;
F is_homomorphism FreeMSA(X*f), (FreeMSA X)|(S1,f,g) by A1,Def5;
then
(F.(the_result_sort_of o)).(Den(o,FreeMSA(X*f)).p) = Den(o,(FreeMSA X)|(
S1,f,g)).q by A2;
hence (F.the_result_sort_of o).([o,the carrier of S1]-tree p) = Den(o,(
FreeMSA X)|(S1,f,g)).q by Th3
.= Den(h.o, FreeMSA X).q by A1,Th23
.= [g.o, the carrier of S2]-tree q by A3,Th3;
end;
theorem Th41:
for S1,S2 being non void non empty ManySortedSign for X being
non-empty ManySortedSet of the carrier of S2 for f being Function of the
carrier of S1, the carrier of S2 for g being Function st f,g
form_morphism_between S1,S2 for t being Term of S1, X*f holds (hom(f,g,X,S1,S2)
.the_sort_of t).t is CompoundTerm of S2, X iff t is CompoundTerm of S1, X*f
proof
let S1,S2 be non void non empty ManySortedSign;
let X be non-empty ManySortedSet of the carrier of S2;
let f be Function of the carrier of S1, the carrier of S2;
let g be Function;
assume
A1: f,g form_morphism_between S1,S2;
then reconsider
h = g as Function of the carrier' of S1, the carrier' of S2 by Th9;
let t be Term of S1, X*f;
hereby
assume (hom(f,g,X,S1,S2).the_sort_of t).t is CompoundTerm of S2, X;
then reconsider
w = (hom(f,g,X,S1,S2).the_sort_of t).t as CompoundTerm of S2,X;
assume t is not CompoundTerm of S1, X*f;
then not t.{} in [:the carrier' of S1, {the carrier of S1}:] by
MSATERM:def 6;
then consider
s being SortSymbol of S1, v being Element of (X*f).s such that
A2: t.{} = [v,s] by MSATERM:2;
t = root-tree [v,s] by A2,MSATERM:5;
then hom(f,g,X,S1,S2).s.t = root-tree [v,f.s] & the_sort_of t = s by A1
,Def5,MSATERM:14;
then w.{} in [:the carrier' of S2, {the carrier of S2}:] & w.{} = [v,f.s]
by MSATERM:def 6,TREES_4:3;
then
A3: f.s = the carrier of S2 by ZFMISC_1:106;
f.s in the carrier of S2;
hence contradiction by A3;
end;
assume t is CompoundTerm of S1, X*f;
then reconsider t as CompoundTerm of S1, X*f;
t.{} in [:the carrier' of S1, {the carrier of S1}:] by MSATERM:def 6;
then consider o,r being object such that
A4: o in the carrier' of S1 and
A5: r in {the carrier of S1} and
A6: t.{} = [o,r] by ZFMISC_1:def 2;
reconsider o as OperSymbol of S1 by A4;
r = the carrier of S1 by A5,TARSKI:def 1;
then consider a being ArgumentSeq of Sym(o,X*f) such that
A7: t = [o,the carrier of S1]-tree a by A6,MSATERM:10;
reconsider a as Element of Args(o, FreeMSA(X*f)) by Th1;
reconsider b = hom(f,g,X,S1,S2)#a as Element of Args(h.o, FreeMSA X) by A1
,Th24;
A8: (hom(f,g,X,S1,S2).the_result_sort_of o).([o,the carrier of S1]-tree a)
= [g.o,the carrier of S2]-tree b by A1,Th40;
t.{} = [o,the carrier of S1] by A7,TREES_4:def 4;
then
A9: the_sort_of t = the_result_sort_of o by MSATERM:17;
reconsider b as ArgumentSeq of Sym(h.o, X) by Th1;
Sym(h.o, X)-tree b = [h.o,the carrier of S2]-tree b by MSAFREE:def 9;
then reconsider T = [h.o,the carrier of S2]-tree b as Term of S2, X;
T.{} = [g.o,the carrier of S2] & [h.o,the carrier of S2] in [:the
carrier' of S2, {the carrier of S2 } :] by TREES_4:def 4,ZFMISC_1:106;
hence thesis by A7,A9,A8,MSATERM:def 6;
end;
theorem
for S1,S2 being non void non empty ManySortedSign for X being
non-empty ManySortedSet of the carrier of S2 for f being Function of the
carrier of S1, the carrier of S2 for g being one-to-one Function st f,g
form_morphism_between S1,S2 holds hom(f,g,X,S1,S2) is_monomorphism FreeMSA(X*f)
, (FreeMSA X)|(S1,f,g)
proof
let S1,S2 be non void non empty ManySortedSign;
let X be non-empty ManySortedSet of the carrier of S2;
let f be Function of the carrier of S1, the carrier of S2;
let g be one-to-one Function;
set A = (FreeMSA X)|(S1,f,g);
set H = hom(f,g,X,S1,S2);
defpred P[set] means ex t1 being Term of S1, X*f st t1 = $1 & for t2 being
Term of S1, X*f st the_sort_of t1 = the_sort_of t2 & (H.the_sort_of t1).t1 = (H
.the_sort_of t1).t2 holds t1 = t2;
A1: FreeMSA (X*f) = MSAlgebra(#FreeSort(X*f), FreeOper(X*f)#) by MSAFREE:def 14
;
assume
A2: f,g form_morphism_between S1,S2;
then reconsider
h = g as Function of the carrier' of S1, the carrier' of S2 by Th9;
reconsider B = A as non-empty MSAlgebra over S1 by A2,Th22;
reconsider H9 = H as ManySortedFunction of FreeMSA(X*f), B;
A3: for o being OperSymbol of S1, p being ArgumentSeq of Sym(o,X*f) st for
t being Term of S1,X*f st t in rng p holds P[t] holds P[[o,the carrier of S1]
-tree p]
proof
let o be OperSymbol of S1, p be ArgumentSeq of Sym(o,X*f) such that
A4: for t being Term of S1,X*f st t in rng p holds P[t];
A5: dom p = dom the_arity_of o by MSATERM:22;
reconsider a = p as Element of Args(o, FreeMSA(X*f)) by Th1;
A6: [h.o,the carrier of S2] in [:the carrier' of S2, {the carrier of S2}
:] by ZFMISC_1:106;
reconsider q = H#a as Element of Args(h.o, FreeMSA X) by A2,Th24;
take t1 = Sym(o,X*f)-tree p;
thus
A7: t1 = [o,the carrier of S1]-tree p by MSAFREE:def 9;
reconsider b = q as ArgumentSeq of Sym(h.o, X) by Th1;
let t2 be Term of S1, X*f such that
A8: the_sort_of t1 = the_sort_of t2 & (H.the_sort_of t1).t1 = (H.
the_sort_of t1) .t2;
the_sort_of t1 = the_result_sort_of o by MSATERM:20;
then
A9: (H.the_sort_of t1).t1 = [g.o,the carrier of S2]-tree q by A2,A7,Th40;
(Sym(h.o, X)-tree b).{} = Sym(h.o, X) & Sym(h.o, X) = [h.o,the
carrier of S2 ] by MSAFREE:def 9,TREES_4:def 4;
then [h.o, the carrier of S2]-tree b is CompoundTerm of S2, X by A6,
MSATERM:def 6;
then t2 is CompoundTerm of S1, X*f by A2,A8,A9,Th41;
then t2.{} in [:the carrier' of S1, {the carrier of S1}:] by MSATERM:def 6;
then consider o9,s9 being object such that
A10: o9 in the carrier' of S1 and
A11: s9 in {the carrier of S1} & t2.{} = [o9, s9] by ZFMISC_1:def 2;
reconsider o9 as OperSymbol of S1 by A10;
A12: t2.{} = [o9, the carrier of S1] by A11,TARSKI:def 1;
then consider r being ArgumentSeq of Sym(o9, X*f) such that
A13: t2 = [o9, the carrier of S1]-tree r by MSATERM:10;
reconsider c = r as Element of Args(o9, FreeMSA(X*f)) by Th1;
reconsider R = H#c as Element of Args(h.o9, FreeMSA X) by A2,Th24;
the_result_sort_of o9 = the_sort_of t2 by A12,MSATERM:17;
then
A14: (H.the_sort_of t1).t1 = [g.o9,the carrier of S2]-tree R by A2,A8,A13,Th40;
then [g.o9, the carrier of S2] = [g.o,the carrier of S2] by A9,TREES_4:15;
then h.o = h.o9 by XTUPLE_0:1;
then
A15: o = o9 by FUNCT_2:19;
then
A16: dom r = dom the_arity_of o by MSATERM:22;
A17: q = R by A9,A14,TREES_4:15;
now
let i be Nat;
A18: R = H9#c;
assume
A19: i in dom the_arity_of o;
then reconsider w1 = p.i, w2 = r.i as Term of S1,X*f by A5,A16,MSATERM:22
;
A20: the_sort_of w1 = (the_arity_of o)/.i by A5,A19,MSATERM:23;
q = H9#a;
then q.i = (H.the_sort_of w1).w1 by A5,A19,A20,MSUALG_3:def 6;
then
A21: (H.the_sort_of w1).w1 = (H.the_sort_of w1).w2 by A17,A15,A16,A19,A20,A18,
MSUALG_3:def 6;
w1 in rng p by A5,A19,FUNCT_1:def 3;
then
A22: P[w1] by A4;
the_sort_of w2 = (the_arity_of o)/.i by A15,A16,A19,MSATERM:23;
hence p.i = r.i by A22,A20,A21;
end;
hence thesis by A7,A13,A15,A5,A16,FINSEQ_1:13;
end;
thus H is_homomorphism FreeMSA(X*f), A by A2,Def5;
let i be set, h be Function;
assume i in dom H;
then reconsider s = i as SortSymbol of S1 by PARTFUN1:def 2;
assume
A23: H.i = h;
then
A24: dom h = dom (H9.s) .= (FreeSort(X*f)).s by A1,FUNCT_2:def 1
.= FreeSort(X*f,s) by MSAFREE:def 11;
let x,y be object;
assume
A25: x in dom h & y in dom h;
FreeSort(X*f,s) c= S1-Terms (X*f) by MSATERM:12;
then reconsider t1 = x, t2 = y as Term of S1, X*f by A24,A25;
A26: for s being SortSymbol of S1, v being Element of (X*f).s holds P[
root-tree [v,s]]
proof
let s be SortSymbol of S1, v be Element of (X*f).s;
reconsider t1 = root-tree [v,s] as Term of S1, X*f by MSATERM:4;
take t1;
thus t1 = root-tree [v,s];
let t2 be Term of S1, X*f such that
A27: the_sort_of t1 = the_sort_of t2 and
A28: (H.the_sort_of t1).t1 = (H.the_sort_of t1).t2;
A29: the_sort_of t1 = s by MSATERM:14;
A30: H.s.root-tree [v,s] = root-tree [v,f.s] by A2,Def5;
now
assume t2.{} in [:the carrier' of S1,{the carrier of S1}:];
then t2 is CompoundTerm of S1, X*f by MSATERM:def 6;
then (root-tree [v,f.s]).{} = [v,f.s] & root-tree [v,f.s] is
CompoundTerm of S2, X by A2,A27,A28,A30,A29,Th41,TREES_4:3;
then [v,f.s] in [:the carrier' of S2, {the carrier of S2}:] by
MSATERM:def 6;
then
A31: f.s = the carrier of S2 by ZFMISC_1:106;
f.s in the carrier of S2;
hence contradiction by A31;
end;
then consider
s2 being SortSymbol of S1, v2 being Element of (X*f).s2 such that
A32: t2.{} = [v2,s2] by MSATERM:2;
A33: t2 = root-tree [v2,s2] by A32,MSATERM:5;
then
A34: s = s2 by A27,A29,MSATERM:14;
then H.s.t2 = root-tree [v2,f.s] by A2,A33,Def5;
then [v,f.s] = [v2,f.s] by A28,A30,A29,TREES_4:4;
hence thesis by A33,A34,XTUPLE_0:1;
end;
for t being Term of S1,X*f holds P[t] from MSATERM:sch 1(A26,A3);
then
A35: P[t1];
the_sort_of t1 = s & the_sort_of t2 = s by A24,A25,MSATERM:def 5;
hence thesis by A23,A35;
end;
theorem
for S being non void non empty ManySortedSign for X being non-empty
ManySortedSet of the carrier of S holds hom(id the carrier of S, id the
carrier' of S, X, S, S) = id the Sorts of FreeMSA X
proof
let S be non void non empty ManySortedSign;
let X be non-empty ManySortedSet of the carrier of S;
set f = id the carrier of S;
set h = hom(f, id the carrier' of S, X, S, S);
set I = id the Sorts of FreeMSA X, g = id the carrier' of S;
A1: f, g form_morphism_between S,S by PUA2MSS1:28;
dom X = the carrier of S by PARTFUN1:def 2;
then
A2: X*f = X by RELAT_1:52;
A3: (FreeMSA X)|(S,f,g) = FreeMSA X by Th25;
A4: now
let i be object;
assume i in the carrier of S;
then reconsider s = i as SortSymbol of S;
FreeGen X c= the Sorts of FreeMSA X by PBOOLE:def 18;
then
A5: (FreeGen X).s c= (the Sorts of FreeMSA X).s;
then (I.s)|((FreeGen X).s) is Function of (FreeGen X).s, (the Sorts of
FreeMSA X).s by FUNCT_2:32;
then
A6: dom ((I.s)|((FreeGen X).s)) = (FreeGen X).s by FUNCT_2:def 1;
A7: now
let a be object;
assume
A8: a in (FreeGen X).s;
then reconsider b = a as Element of FreeMSA X,s by A5;
b in FreeGen(s,X) by A8,MSAFREE:def 16;
then consider x being set such that
A9: x in X.s and
A10: b = root-tree [x,s] by MSAFREE:def 15;
thus ((I.s)|((FreeGen X).s)).a = I.s.b by A8,FUNCT_1:49
.= (id ((the Sorts of FreeMSA X).s)).b by MSUALG_3:def 1
.= b
.= root-tree [x,f.s] by A10
.= h.s.b by A1,A2,A9,A10,Def5
.= ((h.s)|((FreeGen X).s)).a by A8,FUNCT_1:49;
end;
(h.s)|((FreeGen X).s) is Function of (FreeGen X).s, (the Sorts of
FreeMSA X).s by A2,A3,A5,FUNCT_2:32;
then
A11: dom ((h.s)|((FreeGen X).s)) = (FreeGen X).s by FUNCT_2:def 1;
(I||FreeGen X).s = (I.s)|((FreeGen X).s) & (h||FreeGen (X*f)).s = (h.s
)|(( FreeGen (X*f)).s) by MSAFREE:def 1;
hence (I||FreeGen X).i = (h||FreeGen (X*f)).i by A2,A6,A11,A7;
end;
I is_homomorphism FreeMSA X, FreeMSA X & h is_homomorphism FreeMSA (X*f)
, ( FreeMSA X)|(S,f,g) by A1,Def5,MSUALG_3:9;
hence thesis by A2,A3,A4,EXTENS_1:19,PBOOLE:3;
end;
theorem
for S1,S2,S3 being non void non empty ManySortedSign for X being
non-empty ManySortedSet of the carrier of S3 for f1 being Function of the
carrier of S1, the carrier of S2 for g1 being Function st f1,g1
form_morphism_between S1,S2 for f2 being Function of the carrier of S2, the
carrier of S3 for g2 being Function st f2,g2 form_morphism_between S2,S3 holds
hom(f2*f1,g2*g1,X,S1,S3) = (hom(f2,g2,X,S2,S3)*f1)**hom(f1,g1,X*f2,S1,S2)
proof
let S1,S2,S3 be non void non empty ManySortedSign;
let X be non-empty ManySortedSet of the carrier of S3;
let f1 be Function of the carrier of S1, the carrier of S2;
let g1 be Function such that
A1: f1,g1 form_morphism_between S1,S2;
let f2 be Function of the carrier of S2, the carrier of S3;
let g2 be Function;
set f = f2*f1, g = g2*g1;
assume
A2: f2,g2 form_morphism_between S2,S3;
then reconsider
Af = (FreeMSA X)|(S1,f,g), Af1 = (FreeMSA(X*f2))|(S1,f1,g1) as
non-empty MSAlgebra over S1 by A1,Th22,PUA2MSS1:29;
A3: hom(f2,g2,X,S2,S3) is_homomorphism FreeMSA(X*f2), (FreeMSA X)|(S2,f2,g2)
by A2,Def5;
A4: the Sorts of FreeMSA(X*f2) is_transformable_to the Sorts of (FreeMSA X)|
(S2,f2,g2)
proof
let i be set;
assume i in the carrier of S2;
then reconsider s = i as SortSymbol of S2;
(the Sorts of (FreeMSA X)|(S2,f2,g2)).s = ((the Sorts of FreeMSA X)*f2
).s by A2,Def3;
hence thesis;
end;
(FreeMSA X)|(S1,f,g) = ((FreeMSA X)|(S2,f2,g2))|(S1,f1,g1) by A1,A2,Th27;
then consider hf1 being ManySortedFunction of Af1, Af such that
A5: hf1 = hom(f2,g2,X,S2,S3)*f1 and
A6: hf1 is_homomorphism Af1, Af by A1,A3,A4,Th34;
reconsider hh = hom(f1,g1,X*f2,S1,S2) as ManySortedFunction of FreeMSA(X*f),
Af1 by RELAT_1:36;
reconsider hf1h = hf1**hh as ManySortedFunction of FreeMSA(X*f), (FreeMSA X)
|(S1,f,g);
A7: X*f = X*f2*f1 by RELAT_1:36;
A8: now
let s be SortSymbol of S1, x be Element of (X*f).s;
reconsider t = root-tree [x,s] as Term of S1, X*f by MSATERM:4;
A9: FreeMSA (X*f) = MSAlgebra(#FreeSort (X*f), FreeOper (X*f)#) by
MSAFREE:def 14;
the_sort_of t = s & (FreeSort (X*f)).s = FreeSort(X*f,s) by MSAFREE:def 11
,MSATERM:14;
then
A10: root-tree [x,s] in (the Sorts of FreeMSA(X*f)).s by A9,MSATERM:def 5;
A11: (X*f).s = (X*f2).(f1.s) by A7,FUNCT_2:15;
hf1h.s.root-tree [x,s] = ((hf1.s)*(hom(f1,g1,X*f2,S1,S2).s)).
root-tree [x,s] by MSUALG_3:2
.= (hf1.s).(hom(f1,g1,X*f2,S1,S2).s.root-tree [x,s]) by A7,A10,FUNCT_2:15
.= (hf1.s).root-tree [x,f1.s] by A1,A7,Def5;
hence
hf1h.s.root-tree [x,s] = (hom(f2,g2,X,S2,S3).(f1.s)).root-tree [x,f1.
s] by A5,FUNCT_2:15
.= root-tree [x,f2.(f1.s)] by A2,A11,Def5
.= root-tree [x,f.s] by FUNCT_2:15;
end;
A12: f, g form_morphism_between S1,S3 by A1,A2,PUA2MSS1:29;
hom(f1,g1,X*f2,S1,S2) is_homomorphism FreeMSA(X*f2*f1), (FreeMSA (X*f2))
|(S1,f1,g1) by A1,Def5;
then hf1**hh is_homomorphism FreeMSA(X*f), Af by A6,A7,MSUALG_3:10;
hence thesis by A12,A5,A8,Def5;
end;