:: Technical Preliminaries to Algebraic Specifications
:: by Grzegorz Bancerek
::
:: Received September 7, 1999
:: Copyright (c) 1999-2021 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 FUNCT_1, RELAT_1, XBOOLE_0, TARSKI, FUNCT_4, PARTFUN1, SUBSET_1,
PBOOLE, STRUCT_0, MSUALG_1, MARGREL1, CATALG_1, PUA2MSS1, TREES_1,
FINSEQ_1, INSTALG1, FUNCSDOM, MSUALG_6, PROB_2, CARD_3, ALGSPEC1;
notations TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, MSAFREE1, FINSEQ_1,
PBOOLE, RELSET_1, PARTFUN1, FINSEQ_2, FUNCT_4, LANG1, FUNCT_2, STRUCT_0,
CARD_3, MSUALG_1, PROB_2, PUA2MSS1, CIRCCOMB, MSUALG_6, INSTALG1,
CATALG_1;
constructors MSAFREE1, CIRCCOMB, PUA2MSS1, MSUALG_6, CATALG_1, RELSET_1;
registrations XBOOLE_0, RELAT_1, FUNCT_1, FUNCT_2, PBOOLE, STRUCT_0, MSUALG_1,
MSUALG_2, CIRCCOMB, MSUALG_6, INSTALG1, CATALG_1, RELSET_1, FINSEQ_1,
FUNCT_4;
requirements SUBSET, BOOLE;
definitions TARSKI, FUNCT_1, PARTFUN1, STRUCT_0, CIRCCOMB, PUA2MSS1, INSTALG1,
XBOOLE_0, FUNCT_2;
equalities MSUALG_1;
expansions TARSKI, FUNCT_1, CIRCCOMB, PUA2MSS1, XBOOLE_0, FUNCT_2;
theorems RELAT_1, FUNCT_1, FUNCT_2, FUNCT_3, FUNCT_4, PARTFUN1, GRFUNC_1,
FINSEQ_1, PBOOLE, LANG1, PUA2MSS1, FRECHET, INSTALG1, FUNCT_7, CIRCCOMB,
RELSET_1, PROB_2, MSAFREE1, XBOOLE_0, XBOOLE_1, FINSEQ_2;
schemes FUNCT_1;
begin :: Preliminaries
theorem Th1:
for f,g,h being Function st dom f /\ dom g c= dom h holds f+*g+*h = g+*f+*h
proof
let f,g,h be Function;
A1: dom (g+*f+*h) = dom (g+*f) \/ dom h by FUNCT_4:def 1;
A2: dom (f+*g) = dom f \/ dom g by FUNCT_4:def 1;
assume
A3: dom f /\ dom g c= dom h;
A4: now
let x be object;
assume
A5: x in dom f \/ dom g \/ dom h;
per cases;
suppose
A6: x in dom h;
then (f+*g+*h).x = h.x by FUNCT_4:13;
hence (f+*g+*h).x = (g+*f+*h).x by A6,FUNCT_4:13;
end;
suppose
A7: not x in dom h;
then not x in dom f /\ dom g by A3;
then
A8: not x in dom f or not x in dom g by XBOOLE_0:def 4;
A9: (f+*g+*h).x = (f+*g).x by A7,FUNCT_4:11;
x in dom g \/ dom f by A5,A7,XBOOLE_0:def 3;
then x in dom f or x in dom g by XBOOLE_0:def 3;
then (f+*g).x = f.x & (g+*f).x = f.x or (f+*g).x = g.x & (g+*f).x = g.x
by A8,FUNCT_4:11,13;
hence (f+*g+*h).x = (g+*f+*h).x by A7,A9,FUNCT_4:11;
end;
end;
A10: dom (g+*f) = dom g \/ dom f by FUNCT_4:def 1;
dom (f+*g+*h) = dom (f+*g) \/ dom h by FUNCT_4:def 1;
hence thesis by A1,A2,A10,A4;
end;
theorem Th2:
for f,g,h being Function st f c= g & (rng h) /\ dom g c= dom f
holds g*h = f*h
proof
let f,g,h be Function;
assume that
A1: f c= g and
A2: (rng h) /\ dom g c= dom f;
A3: dom (f*h) = dom (g*h)
proof
f*h c= g*h by A1,RELAT_1:29;
hence dom (f*h) c= dom (g*h) by RELAT_1:11;
let x be object;
assume
A4: x in dom (g*h);
then
A5: h.x in dom g by FUNCT_1:11;
A6: x in dom h by A4,FUNCT_1:11;
then h.x in rng h by FUNCT_1:def 3;
then h.x in (rng h) /\ dom g by A5,XBOOLE_0:def 4;
hence thesis by A2,A6,FUNCT_1:11;
end;
now
let x be object;
assume
A7: x in dom (f*h);
then
A8: x in dom h by FUNCT_1:11;
then
A9: (g*h).x = g.(h.x) by FUNCT_1:13;
A10: (f*h).x = f.(h.x) by A8,FUNCT_1:13;
h.x in dom f by A7,FUNCT_1:11;
hence (g*h).x = (f*h).x by A1,A9,A10,GRFUNC_1:2;
end;
hence thesis by A3;
end;
theorem Th3:
for f,g,h being Function st dom f misses rng h & g.:dom h misses
dom f holds f*(g+*h) = f*g
proof
let f,g,h be Function such that
A1: dom f misses rng h and
A2: g.:dom h misses dom f;
A3: dom (f*g) = dom (f*(g+*h))
proof
hereby
let x be object;
assume
A4: x in dom (f*g);
then
A5: x in dom g by FUNCT_1:11;
A6: g.x in dom f by A4,FUNCT_1:11;
now
assume x in dom h;
then g.x in g.:dom h by A5,FUNCT_1:def 6;
hence contradiction by A2,A6,XBOOLE_0:3;
end;
then
A7: g.x = (g+*h).x by FUNCT_4:11;
x in dom (g+*h) by A5,FUNCT_4:12;
hence x in dom (f*(g+*h)) by A6,A7,FUNCT_1:11;
end;
let x be object;
assume
A8: x in dom (f*(g+*h));
then x in dom (g+*h) by FUNCT_1:11;
then x in dom g & not x in dom h or x in dom h by FUNCT_4:12;
then
A9: x in dom g & (g+*h).x = g.x or (g+*h).x = h.x & h.x in rng h by
FUNCT_1:def 3,FUNCT_4:11,13;
(g+*h).x in dom f by A8,FUNCT_1:11;
hence thesis by A1,A9,FUNCT_1:11,XBOOLE_0:3;
end;
now
let x be object;
assume
A10: x in dom (f*g);
then
A11: x in dom g by FUNCT_1:11;
A12: g.x in dom f by A10,FUNCT_1:11;
now
assume x in dom h;
then g.x in g.:dom h by A11,FUNCT_1:def 6;
hence contradiction by A2,A12,XBOOLE_0:3;
end;
then
A13: g.x = (g+*h).x by FUNCT_4:11;
x in dom (g+*h) by A11,FUNCT_4:12;
hence (f*(g+*h)).x = f.(g.x) by A13,FUNCT_1:13
.= (f*g).x by A11,FUNCT_1:13;
end;
hence thesis by A3;
end;
theorem Th4:
for f1,f2,g1,g2 being Function st f1 tolerates f2 & g1 tolerates
g2 holds f1*g1 tolerates f2*g2
proof
let f1,f2,g1,g2 be Function such that
A1: for x being object st x in dom f1 /\ dom f2 holds f1.x = f2.x and
A2: for x being object st x in dom g1 /\ dom g2 holds g1.x = g2.x;
let x be object;
assume
A3: x in dom (f1*g1) /\ dom (f2*g2);
then
A4: x in dom (f1*g1) by XBOOLE_0:def 4;
then
A5: x in dom g1 by FUNCT_1:11;
then
A6: (f1*g1).x = f1.(g1.x) by FUNCT_1:13;
A7: x in dom (f2*g2) by A3,XBOOLE_0:def 4;
then
A8: x in dom g2 by FUNCT_1:11;
then
A9: (f2*g2).x = f2.(g2 .x) by FUNCT_1:13;
x in dom g1 /\ dom g2 by A5,A8,XBOOLE_0:def 4;
then
A10: g1.x = g2.x by A2;
A11: g2.x in dom f2 by A7,FUNCT_1:11;
g1.x in dom f1 by A4,FUNCT_1:11;
then g1.x in dom f1 /\ dom f2 by A11,A10,XBOOLE_0:def 4;
hence thesis by A1,A10,A6,A9;
end;
theorem Th5:
for X1,Y1, X2,Y2 being non empty set for f being Function of X1,
X2, g being Function of Y1,Y2 st f c= g holds f* c= g*
proof
let X1,Y1, X2,Y2 be non empty set;
let f be Function of X1,X2, g be Function of Y1,Y2;
A1: dom g = Y1 by FUNCT_2:def 1;
assume
A2: f c= g;
A3: dom f = X1 by FUNCT_2:def 1;
then
A4: X1* c= Y1* by A1,A2,FINSEQ_1:62,RELAT_1:11;
A5: now
let x be object;
assume x in X1*;
then reconsider p = x as Element of X1*;
A6: (f*).p = f*p by LANG1:def 13;
(rng p) /\ Y1 c= X1;
then
A7: f*p = g*p by A3,A1,A2,Th2;
p in X1*;
hence (f*).x = (g*).x by A4,A6,A7,LANG1:def 13;
end;
A8: dom (g*) = Y1* by FUNCT_2:def 1;
dom (f*) = X1* by FUNCT_2:def 1;
hence thesis by A8,A4,A5,GRFUNC_1:2;
end;
theorem Th6:
for X1,Y1, X2,Y2 be non empty set for f being Function of X1,X2,
g being Function of Y1,Y2 st f tolerates g holds f* tolerates g*
proof
let X1,Y1, X2,Y2 be non empty set;
let f be Function of X1,X2, g be Function of Y1,Y2;
A1: dom g = Y1 by FUNCT_2:def 1;
assume
A2: for x being object st x in dom f /\ dom g holds f.x = g.x;
let x be object;
assume
A3: x in dom (f*) /\ dom (g*);
then reconsider q = x as Element of Y1*;
A4: g*.x = g*q by LANG1:def 13;
x in dom (f*) by A3,XBOOLE_0:def 4;
then reconsider p = x as Element of X1*;
A5: dom f = X1 by FUNCT_2:def 1;
A6: now
let i be object;
assume
A7: i in dom p;
then
A8: q.i in rng q by FUNCT_1:def 3;
p.i in rng p by A7,FUNCT_1:def 3;
then p.i in dom f /\ dom g by A5,A1,A8,XBOOLE_0:def 4;
then f.(p.i) = g.(q.i) by A2
.= (g*q).i by A7,FUNCT_1:13;
hence (f*p).i = (g*q).i by A7,FUNCT_1:13;
end;
rng q c= Y1;
then
A9: dom (g*q) = dom q by A1,RELAT_1:27;
rng p c= X1;
then
A10: dom (f*p) = dom p by A5,RELAT_1:27;
f*.x = f*p by LANG1:def 13;
hence thesis by A4,A10,A9,A6;
end;
definition
let X be set, f be Function;
func X-indexing(f) -> ManySortedSet of X equals
(id X) +* (f|X);
coherence
proof
dom id X = X;
then dom ((id X) +* f|X) = X \/ dom (f|X) by FUNCT_4:def 1;
then dom ((id X) +* f|X) = X by RELAT_1:58,XBOOLE_1:12;
hence thesis by PARTFUN1:def 2,RELAT_1:def 18;
end;
end;
theorem Th7:
for X being set, f being Function holds rng (X-indexing f) = (X \
dom f) \/ f.:X
proof
let X be set, f be Function;
dom id X = X;
hence rng (X-indexing f) = (id X).:(X\dom (f|X)) \/ rng (f|X) by FRECHET:12
.= (id X).:(X\dom (f|X)) \/ f.:X by RELAT_1:115
.= (X\dom (f|X)) \/ f.:X by FUNCT_1:92
.= (X\(dom f /\ X)) \/ f.:X by RELAT_1:61
.= (X \ dom f) \/ f.:X by XBOOLE_1:47;
end;
theorem Th8:
for X being non empty set, f being Function, x being Element of X
holds (X-indexing f).x = ((id X) +* f).x
proof
let X be non empty set, f be Function, x be Element of X;
((id X) +* f)|X = (id X)|X +* f|X by FUNCT_4:71
.= (id X)|(dom id X) +* f|X
.= X-indexing f;
hence thesis by FUNCT_1:49;
end;
theorem Th9:
for X,x being set, f being Function st x in X holds (x in dom f
implies (X-indexing f).x = f.x) & (not x in dom f implies (X-indexing f).x = x)
proof
let X,x be set, f be Function;
assume
A1: x in X;
then
A2: (id X).x = x by FUNCT_1:18;
(X-indexing f).x = ((id X) +* f).x by A1,Th8;
hence thesis by A2,FUNCT_4:11,13;
end;
theorem Th10:
for X being set, f being Function st dom f = X holds X-indexing f = f
proof
let X be set, f be Function;
A1: dom id X = X;
assume
A2: dom f = X;
thus thesis by A2,A1,FUNCT_4:19;
end;
theorem Th11:
for X being set, f being Function holds X-indexing (X-indexing f
) = X-indexing f
proof
let X be set, f be Function;
dom (X-indexing f) = X by PARTFUN1:def 2;
then for x being object st x in X holds (X-indexing (X-indexing f)).x = (X
-indexing f).x by Th9;
hence thesis by PBOOLE:3;
end;
theorem Th12:
for X being set, f being Function holds X-indexing ((id X)+*f) = X-indexing f
proof
let X be set, f be Function;
thus X-indexing ((id X)+*f) = (id X)+*(((id X)|X)+*(f|X)) by FUNCT_4:71
.= (id X)+*((id X)+*(f|X))
.= (id X)+*(id X)+*(f|X) by FUNCT_4:14
.= X-indexing f;
end;
theorem
for X being set, f being Function st f c= id X holds X-indexing f = id X
proof
let X be set, f be Function;
assume f c= id X;
then (id X)+*f = id X by FUNCT_4:98;
hence X-indexing f = X-indexing id X by Th12
.= id X;
end;
theorem
for X being set holds X-indexing {} = id X;
theorem
for X being set, f being Function st X c= dom f holds X-indexing f = f |X
proof
let X be set, f be Function;
assume X c= dom f;
then
A1: dom (f|X) = X by RELAT_1:62;
thus X-indexing f = X-indexing (f|X)
.= f|X by A1,Th10;
end;
theorem
for f being Function holds {}-indexing f = {};
theorem Th17:
for X,Y being set, f being Function st X c= Y holds (Y-indexing
f)|X = X-indexing f
proof
let X,Y be set, f be Function;
assume
A1: X c= Y;
then
A2: (f|Y)|X = f|X by RELAT_1:74;
(id Y)|X = id X by A1,FUNCT_3:1;
hence thesis by A2,FUNCT_4:71;
end;
theorem Th18:
for X,Y being set, f being Function holds (X \/ Y)-indexing f =
(X-indexing f) +* (Y-indexing f)
proof
let X,Y be set, f be Function;
set Z = X \/ Y;
A1: f|Y c= f by RELAT_1:59;
f|X c= f by RELAT_1:59;
then f|X tolerates f|Y by A1,PARTFUN1:52;
then
A2: (f|X) \/ (f|Y) = (f|X)+*(f|Y) by FUNCT_4:30;
dom (f|X) = dom f /\ X by RELAT_1:61;
then
A3: dom (f|X) c= dom f by XBOOLE_1:17;
dom (f|Y) = dom f /\ Y by RELAT_1:61;
then
A4: dom (f|X) /\ dom id Y c= dom (f|Y) by A3,XBOOLE_1:27;
thus Z-indexing f = ((id X)+*id Y)+*(f|Z) by FUNCT_4:22
.= ((id X)+*id Y)+*((f|X)+*(f|Y)) by A2,RELAT_1:78
.= (id X)+*((id Y)+*((f|X)+*(f|Y))) by FUNCT_4:14
.= (id X)+*((id Y)+*(f|X)+*(f|Y)) by FUNCT_4:14
.= (id X)+*((f|X)+*(id Y)+*(f|Y)) by A4,Th1
.= (id X)+*((f|X)+*((id Y)+*(f|Y))) by FUNCT_4:14
.= (X-indexing f)+*(Y-indexing f) by FUNCT_4:14;
end;
theorem Th19:
for X,Y being set, f being Function holds X-indexing f tolerates Y-indexing f
proof
let X,Y be set, f be Function;
Y-indexing f = ((X \/ Y)-indexing f)|Y by Th17,XBOOLE_1:7;
then
A1: Y-indexing f c= (X \/ Y) -indexing f by RELAT_1:59;
X-indexing f = ((X \/ Y)-indexing f)|X by Th17,XBOOLE_1:7;
then X-indexing f c= (X \/ Y)-indexing f by RELAT_1:59;
hence thesis by A1,PARTFUN1:52;
end;
theorem Th20:
for X,Y being set, f being Function holds (X \/ Y)-indexing f =
(X-indexing f) \/ (Y-indexing f)
proof
let X,Y be set, f be Function;
A1: X-indexing f tolerates Y-indexing f by Th19;
(X \/ Y)-indexing f = (X-indexing f) +* (Y-indexing f) by Th18;
hence thesis by A1,FUNCT_4:30;
end;
theorem Th21:
for X being non empty set, f,g being Function st rng g c= X
holds (X-indexing f)*g = ((id X) +* f)*g
proof
let X be non empty set, f,g be Function such that
A1: rng g c= X;
rng g c= dom (X-indexing f) by A1,PARTFUN1:def 2;
then
A2: dom ((X-indexing f)*g) = dom g by RELAT_1:27;
A3: now
let x be object;
assume
A4: x in dom g;
then
A5: (((id X) +* f)*g).x = ((id X) +* f).(g.x) by FUNCT_1:13;
A6: g.x in rng g by A4,FUNCT_1:def 3;
((X-indexing f)*g).x = (X-indexing f).(g.x) by A4,FUNCT_1:13;
hence ((X-indexing f)*g).x = (((id X) +* f)*g).x by A1,A5,A6,Th8;
end;
dom id X = X;
then
A7: dom ((id X) +* f) = X \/ dom f by FUNCT_4:def 1;
X c= X \/ dom f by XBOOLE_1:7;
then dom (((id X) +* f)*g) = dom g by A1,A7,RELAT_1:27,XBOOLE_1:1;
hence thesis by A2,A3;
end;
theorem
for f,g being Function st dom f misses dom g & rng g misses dom f for
X being set holds f*(X-indexing g) = f|X
proof
let f,g be Function such that
A1: dom f misses dom g and
A2: rng g misses dom f;
let X be set;
A3: dom(f|X) c= dom f by RELAT_1:60;
A4: (id X).:dom (g|X) c= dom (g|X)
proof
let x be object;
assume x in (id X).:dom (g|X);
then ex y being object st y in dom id X & y in dom (g|X) & x = ( id X).y
by FUNCT_1:def 6;
hence thesis by FUNCT_1:18;
end;
dom(g|X) c= dom g by RELAT_1:60;
then dom (f|X) misses dom (g|X) by A1,A3,XBOOLE_1:64;
then
A5: (id X).:dom (g|X) misses dom (f|X) by A4,XBOOLE_1:64;
A6: dom (f|X) c= X by RELAT_1:58;
rng (g|X) c= rng g by RELAT_1:70;
then
A7: dom (f|X) misses rng (g|X) by A2,A3,XBOOLE_1:64;
g.:X c= rng g by RELAT_1:111;
then g.:X misses dom f by A2,XBOOLE_1:64;
then
A8: (g.:X) /\ dom f = {};
rng (X-indexing g) = (X \ dom g) \/ g.:X by Th7;
then
(rng (X-indexing g)) /\ dom f = (X \ dom g) /\ (dom f) \/ (g.:X) /\ dom
f by XBOOLE_1:23
.= (X \ dom g) /\ (dom f) by A8;
then (rng (X-indexing g)) /\ dom f c= X /\ dom f by XBOOLE_1:26;
then (rng (X-indexing g)) /\ dom f c= dom (f|X) by RELAT_1:61;
hence f*(X-indexing g) = (f|X)*((id X)+*(g|X)) by Th2,RELAT_1:59
.= (f|X)*id X by A7,A5,Th3
.= f|X by A6,RELAT_1:51;
end;
definition
let f be Function;
mode rng-retract of f -> Function means
: Def2:
dom it = rng f & f*it = id rng f;
existence
proof
defpred P[object,object] means f.$2 = $1;
A1: for o being object st o in rng f
ex y being object st y in dom f & P[o,y]
by FUNCT_1:def 3;
consider g being Function such that
A2: dom g = rng f & rng g c= dom f and
A3: for o being object st o in rng f holds P[o,g.o] from FUNCT_1:sch 6(
A1);
A4: now
let x be object;
assume
A5: x in rng f;
then
A6: (f*g).x = f.(g.x) by A2,FUNCT_1:13;
f.(g.x) = x by A3,A5;
hence (f*g).x = (id rng f).x by A5,A6,FUNCT_1:18;
end;
take g;
thus dom g = rng f by A2;
dom (f*g) = rng f by A2,RELAT_1:27;
hence thesis by A4;
end;
end;
theorem Th23:
for f being Function, g being rng-retract of f holds rng g c= dom f
proof
let f,g be Function;
assume that
A1: dom g = rng f and
A2: f*g = id rng f;
dom g = dom (f*g) by A1,A2;
hence thesis by FUNCT_1:15;
end;
theorem Th24:
for f being Function, g being rng-retract of f for x being set
st x in rng f holds g.x in dom f & f.(g.x) = x
proof
let f be Function, g be rng-retract of f, x be set such that
A1: x in rng f;
A2: rng g c= dom f by Th23;
A3: dom g = rng f by Def2;
then g.x in rng g by A1,FUNCT_1:def 3;
hence g.x in dom f by A2;
thus f.(g.x) = (f*g).x by A1,A3,FUNCT_1:13
.= (id rng f).x by Def2
.= x by A1,FUNCT_1:18;
end;
theorem
for f being Function st f is one-to-one holds f" is rng-retract of f
proof
let f be Function;
assume f is one-to-one;
hence dom (f") = rng f & f*(f") = id rng f by FUNCT_1:32,39;
end;
theorem
for f being Function st f is one-to-one for g being rng-retract of f
holds g = f"
proof
let f be Function such that
A1: f is one-to-one;
let g be rng-retract of f;
A2: rng f = dom g by Def2;
A3: rng g = dom f
proof
thus rng g c= dom f by Th23;
let x be object;
assume
A4: x in dom f;
then
A5: f.x in rng f by FUNCT_1:def 3;
then
A6: g.(f.x) in dom f by Th24;
f.(g.(f.x)) = f.x by A5,Th24;
then x = g.(f.x) by A1,A4,A6;
hence thesis by A2,A5,FUNCT_1:def 3;
end;
now
let x,y be object;
assume that
A7: x in dom f and
A8: y in dom g;
A9: g.y in rng g by A8,FUNCT_1:def 3;
f.(g.y) = y by A2,A8,Th24;
hence f.x = y iff g.y = x by A1,A3,A7,A9;
end;
hence thesis by A1,A2,A3,FUNCT_1:38;
end;
theorem Th27:
for f1,f2 being Function st f1 tolerates f2 for g1 being
rng-retract of f1, g2 being rng-retract of f2 holds g1+*g2 is rng-retract of f1
+*f2
proof
let f1,f2 be Function;
assume
A1: f1 tolerates f2;
then
A2: f1+*f2 = f1 \/ f2 by FUNCT_4:30;
let g1 be rng-retract of f1, g2 be rng-retract of f2;
A3: dom g1 = rng f1 by Def2;
A4: dom g2 = rng f2 by Def2;
thus dom (g1+*g2) = dom g1 \/ dom g2 by FUNCT_4:def 1
.= rng (f1+*f2) by A2,A3,A4,RELAT_1:12;
A5: rng g2 c= dom f2 by Th23;
rng g1 c= dom f1 by Th23;
hence (f1+*f2)*(g1+*g2) = (f1*g1)+*(f2*g2) by A1,A5,FUNCT_4:69
.= (id rng f1)+*(f2*g2) by Def2
.= (id rng f1)+*(id rng f2) by Def2
.= id (rng f1 \/ rng f2) by FUNCT_4:22
.= id rng (f1+*f2) by A2,RELAT_1:12;
end;
theorem
for f1,f2 being Function st f1 c= f2 for g1 being rng-retract of f1 ex
g2 being rng-retract of f2 st g1 c= g2
proof
let f1,f2 be Function such that
A1: f1 c= f2;
A2: f2+*f1 = f2 by A1,FUNCT_4:98;
set g = the rng-retract of f2;
let g1 be rng-retract of f1;
f1 tolerates f2 by A1,PARTFUN1:52;
then reconsider g2 = g+*g1 as rng-retract of f2 by A2,Th27;
take g2;
thus thesis by FUNCT_4:25;
end;
begin :: Replacement in signature
definition
let S be non empty non void ManySortedSign;
let f,g be Function;
pred f,g form_a_replacement_in S means
for o1,o2 being OperSymbol of
S st ((id the carrier' of S) +* g).o1 = ((id the carrier' of S) +* g).o2 holds
((id the carrier of S) +* f)*the_arity_of o1 = ((id the carrier of S) +* f)*
the_arity_of o2 & ((id the carrier of S) +* f).the_result_sort_of o1 = ((id the
carrier of S) +* f).the_result_sort_of o2;
end;
theorem Th29:
for S being non empty non void ManySortedSign, f,g being
Function holds f,g form_a_replacement_in S iff for o1,o2 being OperSymbol of S
st ((the carrier' of S)-indexing g).o1 = ((the carrier' of S)-indexing g).o2
holds ((the carrier of S)-indexing f)*the_arity_of o1 = ((the carrier of S)
-indexing f)*the_arity_of o2 & ((the carrier of S)-indexing f).
the_result_sort_of o1 = ((the carrier of S)-indexing f).the_result_sort_of o2
proof
let S be non empty non void ManySortedSign;
let f,g be Function;
hereby
assume
A1: f,g form_a_replacement_in S;
let o1,o2 be OperSymbol of S;
A2: rng the_arity_of o1 c= the carrier of S;
A3: rng the_arity_of o2 c= the carrier of S;
assume
((the carrier' of S)-indexing g).o1 = ((the carrier' of S) -indexing g).o2;
then
A4: ((id the carrier' of S) +* g).o1 = ((the carrier' of S)-indexing g).o2
by Th8
.= ((id the carrier' of S) +* g).o2 by Th8;
then
((id the carrier of S) +* f)*the_arity_of o1 = ((id the carrier of S)
+* f)*the_arity_of o2 by A1;
hence
((the carrier of S)-indexing f)*the_arity_of o1 = ((id the carrier of
S) +* f)*the_arity_of o2 by A2,Th21
.= ((the carrier of S)-indexing f)*the_arity_of o2 by A3,Th21;
thus ((the carrier of S)-indexing f).the_result_sort_of o1 = ((id the
carrier of S) +* f).the_result_sort_of o1 by Th8
.= ((id the carrier of S) +* f).the_result_sort_of o2 by A1,A4
.= ((the carrier of S)-indexing f).the_result_sort_of o2 by Th8;
end;
assume
A5: for o1,o2 being OperSymbol of S st ((the carrier' of S)-indexing g).
o1 = ((the carrier' of S)-indexing g).o2 holds ((the carrier of S)-indexing f)*
the_arity_of o1 = ((the carrier of S)-indexing f)*the_arity_of o2 & ((the
carrier of S)-indexing f).the_result_sort_of o1 = ((the carrier of S)-indexing
f).the_result_sort_of o2;
let o1,o2 be OperSymbol of S;
A6: rng the_arity_of o1 c= the carrier of S;
A7: rng the_arity_of o2 c= the carrier of S;
assume ((id the carrier' of S) +* g).o1 = ((id the carrier' of S) +* g).o2;
then
A8: ((the carrier' of S)-indexing g).o1 = ((id the carrier' of S) +* g).o2
by Th8
.= ((the carrier' of S)-indexing g).o2 by Th8;
then ((the carrier of S)-indexing f)*the_arity_of o1 = ((the carrier of S)
-indexing f)*the_arity_of o2 by A5;
hence ((id the carrier of S) +* f)*the_arity_of o1 = ((the carrier of S)
-indexing f)*the_arity_of o2 by A6,Th21
.= ((id the carrier of S) +* f)*the_arity_of o2 by A7,Th21;
thus ((id the carrier of S) +* f).the_result_sort_of o1 = ((the carrier of S
)-indexing f).the_result_sort_of o1 by Th8
.= ((the carrier of S)-indexing f).the_result_sort_of o2 by A5,A8
.= ((id the carrier of S) +* f).the_result_sort_of o2 by Th8;
end;
theorem Th30:
for S being non empty non void ManySortedSign, f,g being
Function holds f,g form_a_replacement_in S iff (the carrier of S)-indexing f, (
the carrier' of S)-indexing g form_a_replacement_in S
proof
let S be non empty non void ManySortedSign;
let f,g be Function;
(id the carrier' of S)+*id the carrier' of S = id the carrier' of S;
then
A1: (id the carrier' of S)+* ((id the carrier' of S)+*(g|the carrier' of S))
= ((id the carrier' of S)+*(g|the carrier' of S)) by FUNCT_4:14;
(id the carrier of S)+*id the carrier of S = id the carrier of S;
then
A2: (id the carrier of S)+* ((id the carrier of S)+*(f|the carrier of S) ) =
((id the carrier of S)+*(f|the carrier of S)) by FUNCT_4:14;
f,g form_a_replacement_in S iff for o1,o2 being OperSymbol of S st ((the
carrier' of S)-indexing g).o1 = ((the carrier' of S)-indexing g).o2 holds ((the
carrier of S)-indexing f)*the_arity_of o1 = ((the carrier of S)-indexing f)*
the_arity_of o2 & ((the carrier of S)-indexing f).the_result_sort_of o1 = ((the
carrier of S)-indexing f).the_result_sort_of o2 by Th29;
hence thesis by A1,A2;
end;
reserve S,S9 for non void Signature,
f,g for Function;
theorem Th31:
f,g form_morphism_between S,S9 implies f,g form_a_replacement_in S
proof
A1: dom id the carrier of S = the carrier of S;
A2: dom id the carrier' of S = the carrier' of S;
assume
A3: f,g form_morphism_between S,S9;
then dom g = the carrier' of S;
then
A4: (id the carrier' of S) +* g = g by A2,FUNCT_4:19;
let o1,o2 be OperSymbol of S;
assume
A5: ((id the carrier' of S)+*g).o1 = ((id the carrier' of S)+*g).o2;
dom f = the carrier of S by A3;
then
A6: (id the carrier of S) +* f = f by A1,FUNCT_4:19;
hence
((id the carrier of S) +* f)*the_arity_of o1 = (the Arity of S9).(g.o1)
by A3
.= ((id the carrier of S) +* f)*the_arity_of o2 by A3,A6,A4,A5;
reconsider g9 = g as Function of the carrier' of S, the carrier' of S9 by A3,
INSTALG1:9;
thus ((id the carrier of S) +* f).the_result_sort_of o1 = (f*the ResultSort
of S).o1 by A6,FUNCT_2:15
.= ((the ResultSort of S9)*g).o1 by A3
.= (the ResultSort of S9).(g9.o1) by FUNCT_2:15
.= ((the ResultSort of S9)*g9).o2 by A4,A5,FUNCT_2:15
.= (f*the ResultSort of S).o2 by A3
.= ((id the carrier of S) +* f).the_result_sort_of o2 by A6,FUNCT_2:15;
end;
theorem
f, {} form_a_replacement_in S;
theorem Th33:
g is one-to-one & (the carrier' of S) /\ rng g c= dom g implies
f,g form_a_replacement_in S
proof
assume that
A1: g is one-to-one and
A2: (the carrier' of S) /\ rng g c= dom g;
let o1,o2 be OperSymbol of S;
assume
A3: ((id the carrier' of S)+*g).o1 = ((id the carrier' of S)+*g).o2;
A4: (id the carrier' of S).o1 = o1;
A5: (id the carrier' of S).o2 = o2;
per cases;
suppose
A6: o1 in dom g;
then
A7: g.o1 in rng g by FUNCT_1:def 3;
A8: ((id the carrier' of S)+*g).o1 = g.o1 by A6,FUNCT_4:13;
then not o2 in dom g implies g.o1 = o2 by A3,A5,FUNCT_4:11;
then
A9: not o2 in dom g implies o2 in (the carrier' of S) /\ rng g by A7,
XBOOLE_0:def 4;
then ((id the carrier' of S)+*g).o2 = g.o2 by A2,FUNCT_4:13;
hence thesis by A1,A2,A3,A6,A8,A9;
end;
suppose
A10: not o1 in dom g;
then
A11: not o1 in (the carrier' of S) /\ rng g by A2;
A12: ((id the carrier' of S)+*g).o1 = o1 by A4,A10,FUNCT_4:11;
then o2 in dom g implies o1 = g.o2 & g.o2 in rng g by A3,FUNCT_1:def 3
,FUNCT_4:13;
hence thesis by A3,A5,A12,A11,FUNCT_4:11,XBOOLE_0:def 4;
end;
end;
theorem
g is one-to-one & rng g misses the carrier' of S implies f,g
form_a_replacement_in S
proof
assume
A1: g is one-to-one;
assume rng g misses the carrier' of S;
then (the carrier' of S) /\ rng g = {};
then (the carrier' of S) /\ rng g c= dom g;
hence thesis by A1,Th33;
end;
registration
let X be set, Y be non empty set;
let a be Function of Y, X*;
let r be Function of Y, X;
cluster ManySortedSign(#X, Y, a, r#) -> non void;
coherence;
end;
definition
let S be non empty non void ManySortedSign;
let f,g be Function such that
A1: f,g form_a_replacement_in S;
func S with-replacement (f,g) -> strict non empty non void ManySortedSign
means
:Def4:
(the carrier of S)-indexing f, (the carrier' of S)-indexing g
form_morphism_between S, it & the carrier of it = rng ((the carrier of S)
-indexing f) & the carrier' of it = rng ((the carrier' of S)-indexing g);
uniqueness
proof
set g1 = (the carrier' of S)-indexing g, g2 = g1;
set f1 = (the carrier of S)-indexing f, f2 = f1;
let S1,S2 be strict non empty non void ManySortedSign;
assume that
A2: f1, g1 form_morphism_between S, S1 and
A3: the carrier of S1 = rng f1 and
A4: the carrier' of S1 = rng g1 and
A5: f2, g2 form_morphism_between S, S2 and
A6: the carrier of S2 = rng f2 and
A7: the carrier' of S2 = rng g2;
A8: the ResultSort of S1 = the ResultSort of S2
proof
thus the carrier' of S1 = the carrier' of S2 by A4,A7;
let o be OperSymbol of S1;
consider o1 being object such that
A9: o1 in dom g1 and
A10: o = g1.o1 by A4,FUNCT_1:def 3;
consider o2 being object such that
A11: o2 in dom g2 and
A12: o = g2.o2 by A4,FUNCT_1:def 3;
reconsider o1,o2 as OperSymbol of S by A9,A11;
thus (the ResultSort of S1).o = ((the ResultSort of S1)*g1).o1 by A9,A10,
FUNCT_1:13
.= (f1*the ResultSort of S).o1 by A2
.= f1.the_result_sort_of o1 by FUNCT_2:15
.= f2.the_result_sort_of o2 by A1,A10,A12,Th29
.= (f2*the ResultSort of S).o2 by FUNCT_2:15
.= ((the ResultSort of S2)*g2).o2 by A5
.= (the ResultSort of S2).o by A11,A12,FUNCT_1:13;
end;
the Arity of S1 = the Arity of S2
proof
thus the carrier' of S1 = the carrier' of S2 by A4,A7;
let o be OperSymbol of S1;
consider o2 being object such that
A13: o2 in dom g2 and
A14: o = g2.o2 by A4,FUNCT_1:def 3;
reconsider o2 as OperSymbol of S by A13;
thus (the Arity of S1).o = f2*the_arity_of o2 by A2,A14
.= (the Arity of S2).o by A5,A14;
end;
hence thesis by A3,A6,A8;
end;
existence
proof
set g9 = (the carrier' of S)-indexing g, gg = g9;
set f9 = (the carrier of S)-indexing f, ff = f9;
A15: dom g9 = the carrier' of S by PARTFUN1:def 2;
reconsider X = rng f9, Y = rng g9 as non empty set;
reconsider g9 as Function of the carrier' of S, Y by A15,FUNCT_2:1;
set G = the rng-retract of g9;
A16: rng G c= the carrier' of S by A15,Th23;
dom G = rng g9 by Def2;
then reconsider G as Function of Y, the carrier' of S by A16,FUNCT_2:def 1
,RELSET_1:4;
dom f9 = the carrier of S by PARTFUN1:def 2;
then reconsider f9 as Function of the carrier of S, X by FUNCT_2:1;
set r = f9*(the ResultSort of S)*G;
take R = ManySortedSign(#X, Y, f9**(the Arity of S)*G, r#);
thus ff, gg form_morphism_between S, R
proof
thus dom ff = the carrier of S & dom gg = the carrier' of S by
PARTFUN1:def 2;
thus rng ff c= the carrier of R & rng gg c= the carrier' of R;
now
let x be OperSymbol of S;
A17: g9.(G.(g9.x)) = g9.x by Th24;
thus (r*g9).x = (the ResultSort of R).(g9.x) by FUNCT_2:15
.= (f9*the ResultSort of S).(G.(g9.x)) by FUNCT_2:15
.= f9.(the_result_sort_of (G.(g9.x))) by FUNCT_2:15
.= f9.(the_result_sort_of x) by A1,A17,Th29
.= (f9*the ResultSort of S).x by FUNCT_2:15;
end;
hence ff*the ResultSort of S = (the ResultSort of R)*gg by FUNCT_2:63;
let o be set, p be Function;
assume that
A18: o in the carrier' of S and
A19: p = (the Arity of S).o;
reconsider x = o as OperSymbol of S by A18;
g9.(G.(g9.x)) = g9.x by Th24;
then f9*the_arity_of x = f9*the_arity_of (G.(g9.x)) by A1,Th29;
hence ff*p = f9*.the_arity_of (G.(g9.x)) by A19,LANG1:def 13
.= (f9**(the Arity of S)).(G.(g9.x)) by FUNCT_2:15
.= (the Arity of R).(gg.o) by FUNCT_2:15;
end;
thus thesis;
end;
end;
theorem Th35:
for S1,S2 being non void Signature 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 holds f**the Arity of S1 = (the Arity of S2)*g
proof
let S1,S2 be non void Signature;
let f be Function of the carrier of S1, the carrier of S2;
let g be Function;
A1: dom the Arity of S2 = the carrier' of S2 by FUNCT_2:def 1;
A2: dom ((f*)*the Arity of S1) = the carrier' of S1 by FUNCT_2:def 1;
assume
A3: f,g form_morphism_between S1,S2;
then
A4: dom g = the carrier' of S1;
A5: dom the Arity of S1 = the carrier' of S1 by FUNCT_2:def 1;
A6: now
let c be object;
assume
A7: c in the carrier' of S1;
then
A8: (the Arity of S1).c in rng the Arity of S1 by A5,FUNCT_1:def 3;
then reconsider
p = (the Arity of S1).c as FinSequence of the carrier of S1 by
FINSEQ_1:def 11;
thus (f**the Arity of S1).c = f* .p by A5,A7,FUNCT_1:13
.= f*p by A8,LANG1:def 13
.= (the Arity of S2).(g.c) by A3,A7
.= ((the Arity of S2)*g).c by A4,A7,FUNCT_1:13;
end;
rng g c= the carrier' of S2 by A3;
then dom ((the Arity of S2)*g) = the carrier' of S1 by A4,A1,RELAT_1:27;
hence thesis by A2,A6;
end;
theorem Th36:
f,g form_a_replacement_in S implies (the carrier of S)-indexing
f is Function of the carrier of S, the carrier of S with-replacement (f,g)
proof
assume f,g form_a_replacement_in S;
then (the carrier of S)-indexing f, (the carrier' of S)-indexing g
form_morphism_between S, S with-replacement (f,g) by Def4;
hence thesis by INSTALG1:9;
end;
theorem Th37:
f,g form_a_replacement_in S implies for f9 being Function of the
carrier of S, the carrier of S with-replacement (f,g) st f9 = (the carrier of S
)-indexing f for g9 being rng-retract of (the carrier' of S)-indexing g holds
the Arity of S with-replacement (f,g) = f9* *(the Arity of S)*g9
proof
set ff = (the carrier of S)-indexing f;
set gg = (the carrier' of S)-indexing g;
set T = S with-replacement (f,g);
assume
A1: f,g form_a_replacement_in S;
then
A2: ff, gg form_morphism_between S, T by Def4;
let f9 be Function of the carrier of S, the carrier of S with-replacement (f
,g) such that
A3: f9 = (the carrier of S)-indexing f;
let g9 be rng-retract of gg;
the carrier' of T = rng gg by A1,Def4;
hence the Arity of T = (the Arity of T)*id rng gg by FUNCT_2:17
.= (the Arity of T)*(gg*g9) by Def2
.= (the Arity of T)*gg*g9 by RELAT_1:36
.= f9* *(the Arity of S)*g9 by A2,A3,Th35;
end;
theorem Th38:
f,g form_a_replacement_in S implies for g9 being rng-retract of
(the carrier' of S)-indexing g holds the ResultSort of S with-replacement (f,g)
= ((the carrier of S)-indexing f)*(the ResultSort of S)*g9
proof
set ff = (the carrier of S)-indexing f;
set gg = (the carrier' of S)-indexing g;
set T = S with-replacement (f,g);
assume
A1: f,g form_a_replacement_in S;
then
A2: ff, gg form_morphism_between S, T by Def4;
let g9 be rng-retract of gg;
the carrier' of T = rng gg by A1,Def4;
hence the ResultSort of T = (the ResultSort of T)*id rng gg by FUNCT_2:17
.= (the ResultSort of T)*(gg*g9) by Def2
.= (the ResultSort of T)*gg*g9 by RELAT_1:36
.= ff*(the ResultSort of S)*g9 by A2;
end;
theorem Th39:
f,g form_morphism_between S,S9 implies S with-replacement (f,g)
is Subsignature of S9
proof
set R = S with-replacement (f,g);
set F = id the carrier of R;
set G = id the carrier' of R;
set f9 = (the carrier of S)-indexing f;
set g9 = (the carrier' of S)-indexing g;
A1: dom the ResultSort of S9 = the carrier' of S9 by FUNCT_2:def 1;
A2: dom the ResultSort of R = the carrier' of R by FUNCT_2:def 1;
assume
A3: f,g form_morphism_between S,S9;
then dom f = the carrier of S;
then
A4: f9 = f by Th10;
A5: f,g form_a_replacement_in S by A3,Th31;
then
A6: the carrier' of R = rng g9 by Def4;
thus dom F = the carrier of R & dom G = the carrier' of R;
dom g = the carrier' of S by A3;
then
A7: g9 = g by Th10;
A8: f9, g9 form_morphism_between S, R by A5,Def4;
A9: now
let x be object;
assume
A10: x in the carrier' of R;
then consider a being object such that
A11: a in dom g and
A12: x = g.a by A6,A7,FUNCT_1:def 3;
reconsider a as OperSymbol of S by A3,A11;
(the ResultSort of R)*g = f*the ResultSort of S by A8,A4,A7;
then
A13: (the ResultSort of R).x = (f*the ResultSort of S).a by A11,A12,FUNCT_1:13;
(the ResultSort of S9)*g = f*the ResultSort of S by A3;
then (the ResultSort of S9).x = (f*the ResultSort of S).a by A11,A12,
FUNCT_1:13;
hence
(the ResultSort of R).x = ((the ResultSort of S9)|the carrier' of R).
x by A10,A13,FUNCT_1:49;
end;
rng g c= the carrier' of S9 by A3;
then dom ((the ResultSort of S9)|the carrier' of R) = the carrier' of R by A6
,A7,A1,RELAT_1:62;
then
A14: the ResultSort of R = (the ResultSort of S9)|the carrier' of R by A2,A9;
the carrier of R = rng f9 by A5,Def4;
hence rng F c= the carrier of S9 & rng G c= the carrier' of S9 by A3,A6,A4,A7
;
rng the ResultSort of R c= the carrier of R;
hence F*the ResultSort of R = the ResultSort of R by RELAT_1:53
.= (the ResultSort of S9)*G by A14,RELAT_1:65;
let o be set, p be Function;
assume that
A15: o in the carrier' of R and
A16: p = (the Arity of R).o;
consider a being object such that
A17: a in dom g and
A18: o = g.a by A6,A7,A15,FUNCT_1:def 3;
reconsider a as OperSymbol of S by A3,A17;
A19: f*the_arity_of a = (the Arity of S9).o by A3,A18;
p in (the carrier of R)* by A15,A16,FUNCT_2:5;
then p is FinSequence of the carrier of R by FINSEQ_1:def 11;
then
A20: rng p c= the carrier of R by FINSEQ_1:def 4;
f*the_arity_of a = p by A8,A4,A7,A16,A18;
hence F*p = (the Arity of S9).o by A20,A19,RELAT_1:53
.= (the Arity of S9).(G.o) by A15,FUNCT_1:18;
end;
theorem Th40:
f,g form_a_replacement_in S iff (the carrier of S)-indexing f, (
the carrier' of S)-indexing g form_morphism_between S, S with-replacement (f,g)
by Th30,Th31,Def4;
theorem Th41:
dom f c= the carrier of S & dom g c= the carrier' of S & f,g
form_a_replacement_in S implies (id the carrier of S) +* f, (id the carrier' of
S) +* g form_morphism_between S, S with-replacement (f,g)
proof
assume that
A1: dom f c= the carrier of S and
A2: dom g c= the carrier' of S;
A3: (the carrier' of S)-indexing g = (id the carrier' of S) +* g by A2,
RELAT_1:68;
(the carrier of S)-indexing f = (id the carrier of S) +* f by A1,RELAT_1:68;
hence thesis by A3,Th40;
end;
theorem
dom f = the carrier of S & dom g = the carrier' of S & f,g
form_a_replacement_in S implies f,g form_morphism_between S, S with-replacement
(f,g)
proof
assume that
A1: dom f = the carrier of S and
A2: dom g = the carrier' of S;
dom g = dom id the carrier' of S by A2;
then
A3: (id the carrier' of S) +* g = g by FUNCT_4:19;
dom f = dom id the carrier of S by A1;
then (id the carrier of S) +* f = f by FUNCT_4:19;
hence thesis by A1,A2,A3,Th41;
end;
theorem Th43:
f,g form_a_replacement_in S implies S with-replacement ((the
carrier of S)-indexing f, g) = S with-replacement (f,g)
proof
set X = the carrier of S, Y = the carrier' of S;
set S2 = S with-replacement (X-indexing f, g);
A1: X-indexing (X-indexing f) = X-indexing f by Th11;
assume
A2: f,g form_a_replacement_in S;
then X-indexing f, Y-indexing g form_a_replacement_in S by Th30;
then
A3: X-indexing f, g form_a_replacement_in S by A1,Th30;
then
A4: the carrier of S2 = rng (X-indexing f) by A1,Def4;
A5: the carrier' of S2 = rng (Y-indexing g) by A3,Def4;
X-indexing f, Y-indexing g form_morphism_between S, S2 by A1,A3,Def4;
hence thesis by A2,A4,A5,Def4;
end;
theorem Th44:
f,g form_a_replacement_in S implies S with-replacement (f, (the
carrier' of S)-indexing g) = S with-replacement (f,g)
proof
set X = the carrier of S, Y = the carrier' of S;
set S2 = S with-replacement (f, Y-indexing g);
A1: Y-indexing (Y-indexing g) = Y-indexing g by Th11;
assume
A2: f,g form_a_replacement_in S;
then X-indexing f, Y-indexing g form_a_replacement_in S by Th30;
then
A3: f, Y-indexing g form_a_replacement_in S by A1,Th30;
then
A4: the carrier' of S2 = rng (Y-indexing g) by A1,Def4;
A5: the carrier of S2 = rng (X-indexing f) by A3,Def4;
X-indexing f, Y-indexing g form_morphism_between S, S2 by A1,A3,Def4;
hence thesis by A2,A5,A4,Def4;
end;
begin :: Signature extensions
definition
let S be Signature;
mode Extension of S -> Signature means
: Def5:
S is Subsignature of it;
existence
proof
take S;
thus thesis by INSTALG1:15;
end;
end;
theorem Th45:
for S being Signature holds S is Extension of S
proof
let S be Signature;
thus S is Subsignature of S by INSTALG1:15;
end;
theorem Th46:
for S1 being Signature, S2 being Extension of S1, S3 being
Extension of S2 holds S3 is Extension of S1
proof
let S1 be Signature, S2 be Extension of S1, S3 be Extension of S2;
A1: S2 is Subsignature of S3 by Def5;
S1 is Subsignature of S2 by Def5;
then S1 is Subsignature of S3 by A1,INSTALG1:16;
hence thesis by Def5;
end;
theorem Th47:
for S1,S2 being non empty Signature st S1 tolerates S2 holds S1
+*S2 is Extension of S1
proof
let S1,S2 be non empty Signature such that
A1: the Arity of S1 tolerates the Arity of S2 and
A2: the ResultSort of S1 tolerates the ResultSort of S2;
set S = S1+*S2;
the ResultSort of S = (the ResultSort of S1)+*the ResultSort of S2 by
CIRCCOMB:def 2;
then
A3: the ResultSort of S1 c= the ResultSort of S by A2,FUNCT_4:28;
set f1 = id the carrier of S1, g1 = id the carrier' of S1;
thus dom f1 = the carrier of S1 & dom g1 = the carrier' of S1;
dom the ResultSort of S1 = the carrier' of S1 by FUNCT_2:def 1;
then the ResultSort of S1 = (the ResultSort of S)|the carrier' of S1 by A3,
GRFUNC_1:23;
then
A4: the ResultSort of S1 = (the ResultSort of S)*g1 by RELAT_1:65;
A5: the carrier' of S = (the carrier' of S1) \/ the carrier' of S2 by
CIRCCOMB:def 2;
A6: the carrier of S = (the carrier of S1) \/ the carrier of S2 by
CIRCCOMB:def 2;
thus rng f1 c= the carrier of S & rng g1 c= the carrier' of S by A6,A5,
XBOOLE_1:7;
rng the ResultSort of S1 c= the carrier of S1;
hence f1*the ResultSort of S1 = (the ResultSort of S)*g1 by A4,RELAT_1:53;
let o be set, p be Function such that
A7: o in the carrier' of S1 and
A8: p = (the Arity of S1).o;
A9: dom the Arity of S1 = the carrier' of S1 by FUNCT_2:def 1;
then p in rng the Arity of S1 by A7,A8,FUNCT_1:def 3;
then p is FinSequence of the carrier of S1 by FINSEQ_1:def 11;
then rng p c= the carrier of S1 by FINSEQ_1:def 4;
hence f1*p = p by RELAT_1:53
.= ((the Arity of S1)+*the Arity of S2).o by A1,A7,A8,A9,FUNCT_4:15
.= (the Arity of S).o by CIRCCOMB:def 2
.= (the Arity of S).(g1.o) by A7,FUNCT_1:18;
end;
theorem Th48:
for S1, S2 being non empty Signature holds S1+*S2 is Extension of S2
proof
let S1,S2 be non empty Signature;
set S = S1+*S2;
set f1 = id the carrier of S2, g1 = id the carrier' of S2;
thus dom f1 = the carrier of S2 & dom g1 = the carrier' of S2;
A1: the carrier of S = (the carrier of S1) \/ the carrier of S2 by
CIRCCOMB:def 2;
A2: the carrier' of S = (the carrier' of S1) \/ the carrier' of S2 by
CIRCCOMB:def 2;
thus rng f1 c= the carrier of S & rng g1 c= the carrier' of S by A1,A2,
XBOOLE_1:7;
A3: the ResultSort of S = (the ResultSort of S1)+*the ResultSort of S2 by
CIRCCOMB:def 2;
dom the ResultSort of S2 = the carrier' of S2 by FUNCT_2:def 1;
then the ResultSort of S2 = (the ResultSort of S)|the carrier' of S2 by A3;
then
A4: the ResultSort of S2 = (the ResultSort of S)*g1 by RELAT_1:65;
rng the ResultSort of S2 c= the carrier of S2;
hence f1*the ResultSort of S2 = (the ResultSort of S)*g1 by A4,RELAT_1:53;
let o be set, p be Function such that
A5: o in the carrier' of S2 and
A6: p = (the Arity of S2).o;
A7: dom the Arity of S2 = the carrier' of S2 by FUNCT_2:def 1;
then p in rng the Arity of S2 by A5,A6,FUNCT_1:def 3;
then p is FinSequence of the carrier of S2 by FINSEQ_1:def 11;
then rng p c= the carrier of S2 by FINSEQ_1:def 4;
hence f1*p = p by RELAT_1:53
.= ((the Arity of S1)+*the Arity of S2).o by A5,A6,A7,FUNCT_4:13
.= (the Arity of S).o by CIRCCOMB:def 2
.= (the Arity of S).(g1.o) by A5,FUNCT_1:18;
end;
theorem Th49:
for S1,S2,S being non empty ManySortedSign for f1,g1, f2,g2
being Function st f1 tolerates f2 & f1, g1 form_morphism_between S1, S & f2, g2
form_morphism_between S2, S holds f1+*f2, g1+*g2 form_morphism_between S1+*S2,
S
proof
let S1,S2,E be non empty ManySortedSign;
let f1,g1, f2,g2 be Function such that
A1: f1 tolerates f2 and
A2: dom f1 = the carrier of S1 and
A3: dom g1 = the carrier' of S1 and
A4: rng f1 c= the carrier of E and
A5: rng g1 c= the carrier' of E and
A6: f1*the ResultSort of S1 = (the ResultSort of E)*g1 and
A7: for o being set, p being Function st o in the carrier' of S1 & p = (
the Arity of S1).o holds f1*p = (the Arity of E).(g1.o) and
A8: dom f2 = the carrier of S2 and
A9: dom g2 = the carrier' of S2 and
A10: rng f2 c= the carrier of E and
A11: rng g2 c= the carrier' of E and
A12: f2*the ResultSort of S2 = (the ResultSort of E)*g2 and
A13: for o being set, p being Function st o in the carrier' of S2 & p =
(the Arity of S2).o holds f2*p = (the Arity of E).(g2.o);
set f = f1+*f2, g = g1+*g2, S = S1+*S2;
the carrier of S = (the carrier of S1) \/ the carrier of S2 by CIRCCOMB:def 2
;
hence dom f = the carrier of S by A2,A8,FUNCT_4:def 1;
A14: the carrier' of S = (the carrier' of S1) \/ the carrier' of S2 by
CIRCCOMB:def 2;
hence dom g = the carrier' of S by A3,A9,FUNCT_4:def 1;
A15: rng f c= (rng f1) \/ rng f2 by FUNCT_4:17;
(rng f1) \/ rng f2 c= the carrier of E by A4,A10,XBOOLE_1:8;
hence rng f c= the carrier of E by A15;
A16: rng g c= (rng g1) \/ rng g2 by FUNCT_4:17;
(rng g1) \/ rng g2 c= the carrier' of E by A5,A11,XBOOLE_1:8;
hence rng g c= the carrier' of E by A16;
A17: rng the ResultSort of S1 c= the carrier of S1;
A18: rng the ResultSort of S2 c= the carrier of S2;
A19: dom the ResultSort of E = the carrier' of E by FUNCT_2:def 1;
(the ResultSort of S1)+*the ResultSort of S2 = the ResultSort of S1+*S2
by CIRCCOMB:def 2;
hence f*the ResultSort of S = (f1*the ResultSort of S1)+*(f2*the ResultSort
of S2) by A1,A2,A8,A17,A18,FUNCT_4:69
.= (the ResultSort of E)*g by A6,A11,A12,A19,FUNCT_7:9;
let o be set, p be Function such that
A20: o in the carrier' of S and
A21: p = (the Arity of S).o;
A22: (the Arity of S1)+*the Arity of S2 = the Arity of S1+*S2 by CIRCCOMB:def 2
;
A23: dom the Arity of S1 = the carrier' of S1 by FUNCT_2:def 1;
A24: dom the Arity of S2 = the carrier' of S2 by FUNCT_2:def 1;
per cases;
suppose
A25: o in the carrier' of S2;
then
A26: p = (the Arity of S2).o by A21,A22,A24,FUNCT_4:13;
then p in rng the Arity of S2 by A24,A25,FUNCT_1:def 3;
then p is FinSequence of the carrier of S2 by FINSEQ_1:def 11;
then rng p c= dom f2 by A8,FINSEQ_1:def 4;
then
A27: dom (f2*p) = dom p by RELAT_1:27;
A28: dom (f1*p) c= dom p by RELAT_1:25;
thus f*p = (f1*p)+*(f2*p) by FUNCT_7:10
.= f2*p by A28,A27,FUNCT_4:19
.= (the Arity of E).(g2.o) by A13,A25,A26
.= (the Arity of E).(g.o) by A9,A25,FUNCT_4:13;
end;
suppose
A29: not o in the carrier' of S2;
A30: dom (f2*p) c= dom p by RELAT_1:25;
A31: o in the carrier' of S1 by A14,A20,A29,XBOOLE_0:def 3;
A32: p = (the Arity of S1).o by A21,A22,A24,A29,FUNCT_4:11;
then p in rng the Arity of S1 by A23,A31,FUNCT_1:def 3;
then p is FinSequence of the carrier of S1 by FINSEQ_1:def 11;
then rng p c= dom f1 by A2,FINSEQ_1:def 4;
then
A33: dom (f1*p) = dom p by RELAT_1:27;
thus f*p = (f2+*f1)*p by A1,FUNCT_4:34
.= (f2*p)+*(f1*p) by FUNCT_7:10
.= f1*p by A33,A30,FUNCT_4:19
.= (the Arity of E).(g1.o) by A7,A31,A32
.= (the Arity of E).(g.o) by A9,A29,FUNCT_4:11;
end;
end;
theorem
for S1,S2,E being non empty Signature holds E is Extension of S1 & E
is Extension of S2 iff S1 tolerates S2 & E is Extension of S1+*S2
proof
let S1,S2,E be non empty Signature;
set f1 = id the carrier of S1, g1 = id the carrier' of S1;
set f2 = id the carrier of S2, g2 = id the carrier' of S2;
A1: E is Extension of S1 & E is Extension of S2 implies S1 tolerates S2
proof
assume that
A2: S1 is Subsignature of E and
A3: S2 is Subsignature of E;
A4: the Arity of S2 c= the Arity of E by A3,INSTALG1:11;
the Arity of S1 c= the Arity of E by A2,INSTALG1:11;
hence the Arity of S1 tolerates the Arity of S2 by A4,PARTFUN1:52;
A5: the ResultSort of S2 c= the ResultSort of E by A3,INSTALG1:11;
the ResultSort of S1 c= the ResultSort of E by A2,INSTALG1:11;
hence thesis by A5,PARTFUN1:52;
end;
A6: the carrier of S1+*S2 = (the carrier of S1) \/ the carrier of S2 by
CIRCCOMB:def 2;
the carrier of S2 c= (the carrier of S1) \/ the carrier of S2 by XBOOLE_1:7;
then
A7: f2 c= id ((the carrier of S1) \/ the carrier of S2) by FUNCT_4:3;
A8: the carrier' of S1+*S2 = (the carrier' of S1) \/ the carrier' of S2 by
CIRCCOMB:def 2;
the carrier of S1 c= (the carrier of S1) \/ the carrier of S2 by XBOOLE_1:7;
then f1 c= id ((the carrier of S1) \/ the carrier of S2) by FUNCT_4:3;
then
A9: f1 tolerates f2 by A7,PARTFUN1:52;
E is Extension of S1 & E is Extension of S2 implies E is Extension of S1+*S2
proof
assume that
A10: f1, g1 form_morphism_between S1, E and
A11: f2, g2 form_morphism_between S2, E;
f1+*f2, g1+*g2 form_morphism_between S1+*S2, E by A9,A10,A11,Th49;
then id the carrier of S1+*S2, g1+*g2 form_morphism_between S1+*S2, E by A6
,FUNCT_4:22;
hence id the carrier of S1+*S2, id the carrier' of S1+*S2
form_morphism_between S1+*S2, E by A8,FUNCT_4:22;
end;
hence
E is Extension of S1 & E is Extension of S2 implies S1 tolerates S2 & E
is Extension of S1+*S2 by A1;
assume S1 tolerates S2;
then
A12: S1+*S2 is Extension of S1 by Th47;
S1+*S2 is Extension of S2 by Th48;
hence thesis by A12,Th46;
end;
registration
let S be non empty Signature;
cluster -> non empty for Extension of S;
coherence
proof
set x = the Element of S;
let E be Extension of S;
S is Subsignature of E by Def5;
then
A1: the carrier of S c= the carrier of E by INSTALG1:10;
x in the carrier of S;
hence the carrier of E is non empty by A1;
end;
end;
registration
let S be non void Signature;
cluster -> non void for Extension of S;
coherence
proof
set x = the OperSymbol of S;
let E be Extension of S;
S is Subsignature of E by Def5;
then
A1: the carrier' of S c= the carrier' of E by INSTALG1:10;
x in the carrier' of S;
hence the carrier' of E is non empty by A1;
end;
end;
theorem Th51:
for S,T being Signature st S is empty holds T is Extension of S
proof
let S, T be Signature;
assume
A1: the carrier of S is empty;
then the carrier' of S = {} by INSTALG1:def 1;
then the Arity of S = {};
then
A2: the Arity of S c= the Arity of T;
the ResultSort of S = {} by A1;
then the ResultSort of S c= the ResultSort of T;
hence S is Subsignature of T by A1,A2,INSTALG1:13,XBOOLE_1:2;
end;
registration
let S be Signature;
cluster non empty non void strict for Extension of S;
existence
proof
set S9 = the non void strict Signature;
per cases;
suppose
S is empty;
then S9 is Extension of S by Th51;
hence thesis;
end;
suppose
S is non empty;
then reconsider S1 = S as non empty Signature;
reconsider E = S9+*S1 as Extension of S by Th48;
take E;
thus the carrier of E is non empty;
thus the carrier' of E is non empty;
thus thesis;
end;
end;
end;
theorem Th52:
for S being non void Signature, E being Extension of S st
f,g form_a_replacement_in E holds f,g form_a_replacement_in S
proof
let S be non void Signature, E be Extension of S;
set f9 = (the carrier of E)-indexing f;
set g9 = (the carrier' of E)-indexing g;
set T = E with-replacement (f,g);
A1: S is Subsignature of E by Def5;
then
A2: f9|the carrier of S = (the carrier of S)-indexing f by Th17,INSTALG1:10;
A3: g9|the carrier' of S = (the carrier' of S)-indexing g by A1,Th17,
INSTALG1:10;
assume f,g form_a_replacement_in E;
then f9, g9 form_morphism_between E, T by Th40;
then f9|the carrier of S, g9|the carrier' of S form_a_replacement_in S by A1
,Th31,INSTALG1:18;
hence thesis by A2,A3,Th30;
end;
theorem
for S being non void Signature, E being Extension of S st f,g
form_a_replacement_in E holds E with-replacement(f,g) is Extension of S
with-replacement(f,g)
proof
let S be non void Signature, E be Extension of S;
set f9 = (the carrier of E)-indexing f;
set g9 = (the carrier' of E)-indexing g;
set gg = (the carrier' of S)-indexing g;
set T = E with-replacement (f,g);
A1: (the carrier' of S)-indexing gg = gg by Th11;
assume
A2: f,g form_a_replacement_in E;
then f,g form_a_replacement_in S by Th52;
then (the carrier of S)-indexing f,gg form_a_replacement_in S by Th30;
then
A3: f,gg form_a_replacement_in S by A1,Th30;
A4: S is Subsignature of E by Def5;
then
A5: g9|the carrier' of S = (the carrier' of S)-indexing g by Th17,INSTALG1:10;
f9, g9 form_morphism_between E, T by A2,Th40;
then
A6: S with-replacement (f9|the carrier of S, g9|the carrier' of S) is
Subsignature of T by A4,Th39,INSTALG1:18;
f9|the carrier of S = (the carrier of S)-indexing f by A4,Th17,INSTALG1:10;
then S with-replacement (f9|the carrier of S, g9|the carrier' of S) = S
with-replacement (f, (the carrier' of S)-indexing g) by A3,A5,Th43;
hence S with-replacement(f,g) is Subsignature of E with-replacement(f,g) by
A2,A6,Th44,Th52;
end;
theorem
for S1,S2 being non void Signature st S1 tolerates S2 for f,g being
Function st f,g form_a_replacement_in S1+*S2 holds (S1+*S2) with-replacement (f
,g) = (S1 with-replacement (f,g))+*(S2 with-replacement (f,g))
proof
let S1,S2 be non void Signature such that
A1: S1 tolerates S2;
A2: the ResultSort of S1 tolerates the ResultSort of S2 by A1;
A3: rng the Arity of S2 c= (the carrier of S2)*;
A4: rng the ResultSort of S2 c= the carrier of S2;
A5: rng the ResultSort of S1 c= the carrier of S1;
set S = S1+*S2;
let f,g be Function such that
A6: f,g form_a_replacement_in S1+*S2;
deffunc F(non void Signature) = (the carrier of $1)-indexing f;
deffunc T(non void Signature) = $1 with-replacement (f,g);
A7: dom F(S2) = the carrier of S2 by PARTFUN1:def 2;
A8: F(S1) tolerates F(S2) by Th19;
A9: S is Extension of S1 by A1,Th47;
then reconsider
F1 = F(S1) as Function of the carrier of S1, the carrier of T(S1)
by A6,Th36,Th52;
A10: dom (F(S1)*(the ResultSort of S1)) = the carrier' of S1 by PARTFUN1:def 2;
deffunc G(non void Signature) = (the carrier' of $1)-indexing g;
A11: dom F(S1) = the carrier of S1 by PARTFUN1:def 2;
A12: dom G(S1) = the carrier' of S1 by PARTFUN1:def 2;
set g1 = the rng-retract of G(S1),g2 = the rng-retract of G(S2);
A13: the ResultSort of S = (the ResultSort of S1)+*the ResultSort of S2 by
CIRCCOMB:def 2;
A14: rng g2 c= dom G(S2) by Th23;
A15: the carrier' of S = (the carrier' of S1) \/ the carrier' of S2 by
CIRCCOMB:def 2;
then G(S) = G(S1) \/ G(S2) by Th20;
then
A16: rng G(S) = (rng G(S1)) \/ rng G(S2) by RELAT_1:12;
A17: dom G(S2) = the carrier' of S2 by PARTFUN1:def 2;
A18: S is Extension of S2 by Th48;
then reconsider
F2 = F(S2) as Function of the carrier of S2, the carrier of T(S2)
by A6,Th36,Th52;
A19: dom (F(S2)*(the ResultSort of S2)) = the carrier' of S2 by PARTFUN1:def 2;
A20: the carrier of S = (the carrier of S1) \/ the carrier of S2 by
CIRCCOMB:def 2;
then
A21: F(S) = F(S1)+*F(S2) by Th18;
F(S) = F(S1) \/ F(S2) by A20,Th20;
then
A22: rng F(S) = (rng F(S1)) \/ rng F(S2) by RELAT_1:12;
A23: dom (F2**the Arity of S2) = the carrier' of S2 by FUNCT_2:def 1;
A24: dom (F2*) = (the carrier of S2)* by FUNCT_2:def 1;
G(S) = G(S1)+*G(S2) by A15,Th18;
then reconsider gg = g1+*g2 as rng-retract of G(S) by Th19,Th27;
A25: rng g1 c= dom G(S1) by Th23;
A26: the ResultSort of T(S) = F(S)*(the ResultSort of S)*gg by A6,Th38
.= ((F(S1)*the ResultSort of S1)+*(F(S2)*the ResultSort of S2))*gg by A13
,A21,A5,A4,A11,A7,Th19,FUNCT_4:69
.= (F(S1)*(the ResultSort of S1)*g1)+*(F(S2)*(the ResultSort of S2)*g2)
by A8,A25,A14,A12,A17,A10,A19,A2,Th4,FUNCT_4:69
.= (the ResultSort of T(S1))+*(F(S2)*(the ResultSort of S2)*g2) by A6,A9
,Th38,Th52
.= (the ResultSort of T(S1))+*the ResultSort of T(S2) by A6,A18,Th38,Th52;
A27: the carrier of T(S) = rng F(S) by A6,Def4;
A28: dom (F1**the Arity of S1) = the carrier' of S1 by FUNCT_2:def 1;
reconsider FS = F(S) as Function of the carrier of S, the carrier of T(S) by
A6,Th36;
A29: (rng the Arity of S) /\ dom (FS*) c= rng the Arity of S by XBOOLE_1:17;
A30: the Arity of S = (the Arity of S1)+*the Arity of S2 by CIRCCOMB:def 2;
A31: f,g form_a_replacement_in S1 by A6,A9,Th52;
then
A32: the carrier of T(S1) = rng F(S1) by Def4;
A33: the carrier' of T(S1) = rng G(S1) by A31,Def4;
A34: the carrier' of T(S) = rng G(S) by A6,Def4;
A35: dom (F1*) = (the carrier of S1)* by FUNCT_2:def 1;
the Arity of S1 tolerates the Arity of S2 by A1;
then the Arity of S = (the Arity of S1) \/ the Arity of S2 by A30,FUNCT_4:30;
then rng the Arity of S = (rng the Arity of S1) \/ rng the Arity of S2 by
RELAT_1:12;
then rng the Arity of S c= (the carrier of S1)* \/ (the carrier of S2)* by
XBOOLE_1:13;
then rng the Arity of S c= dom (F1*+*(F2*)) by A35,A24,FUNCT_4:def 1;
then
A36: (rng the Arity of S) /\ dom (FS*) c= dom (F1*+*(F2*)) by A29;
A37: f,g form_a_replacement_in S2 by A6,A18,Th52;
then
A38: the carrier of T(S2) = rng F(S2) by Def4;
A39: the carrier' of T(S2) = rng G(S2) by A37,Def4;
A40: F1* tolerates F2* by Th6,Th19;
A41: F1* +* (F2*) c= F1* \/ F2* by FUNCT_4:29;
F2 = FS|the carrier of S2 by A20,Th17,XBOOLE_1:7;
then
A42: F2* c= FS* by Th5,RELAT_1:59;
F1 = FS|the carrier of S1 by A20,Th17,XBOOLE_1:7;
then F1* c= FS* by Th5,RELAT_1:59;
then F1* \/ F2* c= FS* by A42,XBOOLE_1:8;
then
A43: F1* +* (F2*) c= FS* by A41;
A44: the Arity of S1 tolerates the Arity of S2 by A1;
A45: rng the Arity of S1 c= (the carrier of S1)*;
A46: f,g form_a_replacement_in S1 by A6,A9,Th52;
the Arity of T(S) = FS**(the Arity of S)*gg by A6,Th37
.= (F1*+*(F2*))*(the Arity of S)*gg by A43,A36,Th2
.= ((F1**the Arity of S1)+*(F2**the Arity of S2))*gg by A30,A8,A45,A3,A35
,A24,Th6,FUNCT_4:69
.= ((F1**the Arity of S1)*g1)+*((F2**the Arity of S2)*g2) by A25,A14,A12
,A17,A40,A44,A28,A23,Th4,FUNCT_4:69
.= (the Arity of T(S1))+*((F2**the Arity of S2)*g2) by A46,Th37
.= (the Arity of T(S1))+*the Arity of T(S2) by A6,A18,Th37,Th52;
hence thesis by A22,A27,A32,A38,A16,A34,A33,A39,A26,CIRCCOMB:def 2;
end;
begin :: Algebras
definition
mode Algebra -> object means
: Def6:
ex S being non void Signature st it is feasible MSAlgebra over S;
existence
proof
set S = the non void Signature, A = the feasible MSAlgebra over S;
take A, S;
thus thesis;
end;
end;
definition
let S be Signature;
mode Algebra of S -> Algebra means
: Def7:
ex E being non void Extension of S st it is feasible MSAlgebra over E;
existence
proof
set E = the non void Extension of S;
set A = the feasible MSAlgebra over E;
A is Algebra by Def6;
hence thesis;
end;
end;
theorem
for S being non void Signature, A being feasible MSAlgebra over S
holds A is Algebra of S
proof
let S be non void Signature, A be feasible MSAlgebra over S;
A1: S is Extension of S by Th45;
A is Algebra by Def6;
hence thesis by A1,Def7;
end;
theorem
for S being Signature, E being Extension of S, A being Algebra of E
holds A is Algebra of S
proof
let S be Signature, E be Extension of S, A be Algebra of E;
consider E9 be non void Extension of E such that
A1: A is feasible MSAlgebra over E9 by Def7;
E9 is Extension of S by Th46;
hence thesis by A1,Def7;
end;
theorem Th57:
for S being Signature, E being non empty Signature, A being
MSAlgebra over E st A is Algebra of S holds the carrier of S c= the carrier of
E & the carrier' of S c= the carrier' of E
proof
let S be Signature, E be non empty Signature, A be MSAlgebra over E;
A1: dom the Charact of A = the carrier' of E by PARTFUN1:def 2;
assume A is Algebra of S;
then consider ES being non void Extension of S such that
A2: A is feasible MSAlgebra over ES by Def7;
reconsider B = A as MSAlgebra over ES by A2;
A3: dom the Sorts of A = the carrier of E by PARTFUN1:def 2;
A4: S is Subsignature of ES by Def5;
dom the Sorts of B = the carrier of ES by PARTFUN1:def 2;
hence the carrier of S c= the carrier of E by A4,A3,INSTALG1:10;
dom the Charact of B = the carrier' of ES by PARTFUN1:def 2;
hence thesis by A4,A1,INSTALG1:10;
end;
theorem Th58:
for S being non void Signature, E being non empty Signature for
A being MSAlgebra over E st A is Algebra of S for o being OperSymbol of S holds
(the Charact of A).o is Function of (the Sorts of A)#.the_arity_of o, (the
Sorts of A).the_result_sort_of o
proof
let S be non void Signature, E be non empty Signature;
let A be MSAlgebra over E;
A1: dom the Sorts of A = the carrier of E by PARTFUN1:def 2;
assume A is Algebra of S;
then consider ES being non void Extension of S such that
A2: A is feasible MSAlgebra over ES by Def7;
reconsider B = A as MSAlgebra over ES by A2;
let o be OperSymbol of S;
A3: dom the Sorts of B = the carrier of ES by PARTFUN1:def 2;
A4: S is Subsignature of ES by Def5;
then
A5: the carrier' of S c= the carrier' of ES by INSTALG1:10;
the ResultSort of S = (the ResultSort of ES)|the carrier' of S by A4,
INSTALG1:12;
then
A6: the_result_sort_of o = (the ResultSort of ES).o by FUNCT_1:49;
the Arity of S = (the Arity of ES)|the carrier' of S by A4,INSTALG1:12;
then
A7: the_arity_of o = (the Arity of ES).o by FUNCT_1:49;
A8: (the Charact of B).o is Function of ((the Sorts of B)#*the Arity of ES)
.o, ((the Sorts of B)*the ResultSort of ES).o by A5,PBOOLE:def 15;
the carrier' of ES = dom the ResultSort of ES by FUNCT_2:def 1;
then
A9: ((the Sorts of B)*the ResultSort of ES).o = (the Sorts of A).
the_result_sort_of o by A5,A6,FUNCT_1:13;
the carrier' of ES = dom the Arity of ES by FUNCT_2:def 1;
then
((the Sorts of B)#*the Arity of ES).o = (the Sorts of A)#. the_arity_of
o by A5,A3,A1,A7,FUNCT_1:13;
hence thesis by A9,A8;
end;
theorem
for S being non empty Signature, A being Algebra of S for E being non
empty ManySortedSign st A is MSAlgebra over E holds A is MSAlgebra over E+*S
proof
let S be non empty Signature, A be Algebra of S;
let E be non empty ManySortedSign;
set T = E+*S;
A1: dom the ResultSort of S = the carrier' of S by FUNCT_2:def 1;
A2: the ResultSort of T = (the ResultSort of E)+*the ResultSort of S by
CIRCCOMB:def 2;
assume A is MSAlgebra over E;
then reconsider B = A as MSAlgebra over E;
A3: the Arity of T = (the Arity of E)+*the Arity of S by CIRCCOMB:def 2;
B is Algebra of S;
then
A4: the carrier of S c= the carrier of E by Th57;
the carrier of T = (the carrier of E) \/ the carrier of S by CIRCCOMB:def 2;
then
A5: the carrier of T = the carrier of E by A4,XBOOLE_1:12;
then reconsider Ss = the Sorts of B as ManySortedSet of the carrier of T;
B is Algebra of S;
then
A6: the carrier' of S c= the carrier' of E by Th57;
the carrier' of T = (the carrier' of E) \/ the carrier' of S by
CIRCCOMB:def 2;
then
A7: the carrier' of T = the carrier' of E by A6,XBOOLE_1:12;
A8: dom the Arity of S = the carrier' of S by FUNCT_2:def 1;
now
let i be object;
assume
A9: i in the carrier' of T;
then
A10: (Ss*the ResultSort of T).i = Ss.((the ResultSort of T).i) by FUNCT_2:15;
A11: now
assume
A12: i in the carrier' of S;
then reconsider S9 = S as non void Signature;
reconsider o = i as OperSymbol of S9 by A12;
A13: (the Arity of T).o = the_arity_of o by A8,A3,FUNCT_4:13;
(the ResultSort of T).o = the_result_sort_of o by A1,A2,FUNCT_4:13;
hence (the Charact of B).i is Function of (the Sorts of B)#.((the Arity
of T).i), (the Sorts of B).((the ResultSort of T).i) by A13,Th58;
end;
A14: not i in the carrier' of S implies (the Arity of T).i = (the Arity of
E).i & (the ResultSort of T).i = (the ResultSort of E).i by A8,A1,A3,A2,
FUNCT_4:11;
A15: (Ss#*the Arity of E).i = Ss#.((the Arity of E).i) by A7,A9,FUNCT_2:15;
A16: (Ss#*the Arity of T).i = Ss#.((the Arity of T).i) by A9,FUNCT_2:15;
(Ss*the ResultSort of E).i = Ss.((the ResultSort of E).i) by A7,A9,
FUNCT_2:15;
hence (the Charact of B).i is Function of (Ss# * the Arity of T).i, (Ss *
the ResultSort of T).i by A5,A7,A9,A15,A10,A16,A11,A14,PBOOLE:def 15;
end;
then reconsider
C = the Charact of B as ManySortedFunction of Ss# * the Arity of
T, Ss * the ResultSort of T by A7,PBOOLE:def 15;
set B9 = MSAlgebra(#Ss, C#);
the Sorts of B9 = the Sorts of B;
then B is MSAlgebra over T;
hence thesis;
end;
theorem Th60:
for S1,S2 being non empty Signature for A being MSAlgebra over
S1 st A is MSAlgebra over S2 holds the carrier of S1 = the carrier of S2 & the
carrier' of S1 = the carrier' of S2
proof
let S1,S2 be non empty Signature;
let A be MSAlgebra over S1;
assume A is MSAlgebra over S2;
then reconsider B = A as MSAlgebra over S2;
the Sorts of A = the Sorts of B;
then dom the Sorts of A = the carrier of S2 by PARTFUN1:def 2;
hence the carrier of S1 = the carrier of S2 by PARTFUN1:def 2;
the Charact of A = the Charact of B;
then dom the Charact of A = the carrier' of S2 by PARTFUN1:def 2;
hence thesis by PARTFUN1:def 2;
end;
registration
let S be non void Signature, A be non-empty disjoint_valued MSAlgebra over S;
cluster the Sorts of A -> one-to-one;
coherence
proof
let x,y be object;
assume that
A1: x in dom the Sorts of A and
A2: y in dom the Sorts of A;
reconsider a = x, b = y as SortSymbol of S by A1,A2;
assume that
A3: (the Sorts of A).x = (the Sorts of A).y and
A4: x <> y;
the Sorts of A is disjoint_valued by MSAFREE1:def 2;
then (the Sorts of A).a misses (the Sorts of A). b by A4,PROB_2:def 2;
hence thesis by A3;
end;
end;
theorem Th61:
for S being non void Signature for A being disjoint_valued
MSAlgebra over S for C1,C2 being Component of the Sorts of A holds C1 = C2 or
C1 misses C2
proof
let S be non void Signature;
let A be disjoint_valued MSAlgebra over S;
let C1,C2 be Component of the Sorts of A;
A1: ex y being object st y in dom the Sorts of A & C2 = (the Sorts of A).y
by FUNCT_1:def 3;
A2: the Sorts of A is disjoint_valued by MSAFREE1:def 2;
ex x being object st x in dom the Sorts of A & C1 = (the Sorts of A).x
by FUNCT_1:def 3;
hence thesis by A1,A2,PROB_2:def 2;
end;
theorem Th62:
for S,S9 being non void Signature for A being non-empty
disjoint_valued MSAlgebra over S st A is MSAlgebra over S9 holds the
ManySortedSign of S = the ManySortedSign of S9
proof
let S,E be non void Signature;
let A be non-empty disjoint_valued MSAlgebra over S;
A1: dom the Sorts of A = the carrier of S by PARTFUN1:def 2;
assume
A2: A is MSAlgebra over E;
then reconsider B = A as MSAlgebra over E;
A3: the carrier of S = the carrier of E by A2,Th60;
A4: now
let x be object;
assume x in the carrier' of S;
then reconsider o = x as OperSymbol of S;
reconsider e = o as OperSymbol of E by A2,Th60;
set p = the Element of Args(o,A);
Den(e,B) = (the Charact of B).e;
then
A5: rng Den(o,A) c= Result(e,B) by RELAT_1:def 19;
Den(o,A).p in rng Den(o,A) by FUNCT_2:4;
then Result(o,A) meets Result(e,B) by A5,XBOOLE_0:3;
then Result(o,A) = ((the Sorts of B)*the ResultSort of E).x by Th61
.= (the Sorts of B).((the ResultSort of E).e) by FUNCT_2:15;
then (the Sorts of A).((the ResultSort of E).e) = (the Sorts of A).((the
ResultSort of S).o) by FUNCT_2:15;
hence (the ResultSort of S).x = (the ResultSort of E).x by A3,A1,
FUNCT_1:def 4;
end;
A6: now
let x be object;
assume x in the carrier' of S;
then reconsider o = x as OperSymbol of S;
reconsider e = o as OperSymbol of E by A2,Th60;
reconsider p = (the Arity of E).e as Element of (the carrier of E)*;
reconsider q = (the Arity of S).o as Element of (the carrier of S)*;
Den(e,B) = (the Charact of B).e;
then
A7: dom Den(o,A) = Args(e,B) by FUNCT_2:def 1;
dom Den(o,A) = Args(o,A) by FUNCT_2:def 1;
then Args(o,A) = (the Sorts of B)#.p by A7,FUNCT_2:15
.= product ((the Sorts of B)*p) by FINSEQ_2:def 5;
then product ((the Sorts of A)*p) = (the Sorts of A)#.q by FUNCT_2:15
.= product ((the Sorts of A)*q) by FINSEQ_2:def 5;
then
A8: (the Sorts of B)*p = (the Sorts of A)*q by PUA2MSS1:2;
A9: rng q c= the carrier of S;
then
A10: dom ((the Sorts of A)*q) = dom q by A1,RELAT_1:27;
A11: rng p c= the carrier of E;
then dom ((the Sorts of B)*p) = dom p by A3,A1,RELAT_1:27;
hence (the Arity of S).x = (the Arity of E).x by A3,A1,A8,A11,A9,A10,
FUNCT_1:27;
end;
A12: dom the Arity of E = the carrier' of E by FUNCT_2:def 1;
A13: dom the Arity of S = the carrier' of S by FUNCT_2:def 1;
the ResultSort of S = the ResultSort of E by A2,A4,Th60;
hence thesis by A3,A13,A12,A6,FUNCT_1:2;
end;
theorem
for S9 being non void Signature for A being non-empty disjoint_valued
MSAlgebra over S st A is Algebra of S9 holds S is Extension of S9
proof
let S9 be non void Signature;
let A be non-empty disjoint_valued MSAlgebra over S;
assume A is Algebra of S9;
then consider E being non void Extension of S9 such that
A1: A is feasible MSAlgebra over E by Def7;
A2: S9 is Subsignature of E by Def5;
A3: the ManySortedSign of S = the ManySortedSign of E by A1,Th62;
then
A4: the ResultSort of S9 c= the ResultSort of S by A2,INSTALG1:11;
the Arity of S9 c= the Arity of S by A2,A3,INSTALG1:11;
hence S9 is Subsignature of S by A2,A3,A4,INSTALG1:10,13;
end;