:: Minimal Manysorted Signature for Partial Algebra
:: by Grzegorz Bancerek
::
:: Received October 1, 1995
:: Copyright (c) 1995-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies FINSEQ_1, FUNCT_1, RELAT_1, XBOOLE_0, TARSKI, SETFAM_1, UNIALG_1,
FUNCT_2, PARTFUN1, SUBSET_1, NAT_1, STRUCT_0, CARD_3, MSUALG_1, UNIALG_2,
EQREL_1, ZFMISC_1, NUMBERS, FINSEQ_2, PBOOLE, CARD_1, ARYTM_3, INCPROJ,
ORDINAL4, RELAT_2, NEWTON, MCART_1, MARGREL1, PUA2MSS1;
notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, SUBSET_1, ORDINAL1, NUMBERS,
XCMPLX_0, NAT_1, SETFAM_1, RELAT_1, STRUCT_0, FUNCT_1, PBOOLE, RELSET_1,
PARTFUN1, MCART_1, FINSEQ_1, FINSEQ_2, FUNCT_2, RELAT_2, EQREL_1, CARD_3,
MARGREL1, MSUALG_1, UNIALG_1;
constructors NAT_1, EQREL_1, MSUALG_1, RELSET_1, DOMAIN_1, MARGREL1, XTUPLE_0,
NUMBERS;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, NAT_1,
FINSEQ_1, EQREL_1, FINSEQ_2, CARD_3, STRUCT_0, UNIALG_1, MSUALG_1,
ORDINAL1, CARD_1, RELSET_1, PBOOLE, MARGREL1, XTUPLE_0, XCMPLX_0;
requirements NUMERALS, BOOLE, SUBSET, ARITHM;
definitions STRUCT_0, XBOOLE_0, TARSKI, SETFAM_1, RELAT_2, EQREL_1, PBOOLE,
RELAT_1, FUNCT_1, UNIALG_1, MARGREL1;
equalities MSUALG_1;
expansions XBOOLE_0, TARSKI, SETFAM_1, RELAT_2, PBOOLE, FUNCT_1;
theorems TARSKI, ZFMISC_1, RELAT_1, RELSET_1, FUNCT_1, FINSEQ_1, FINSEQ_2,
EQREL_1, CARD_3, FUNCT_2, PARTFUN1, CARD_5, FUNCT_6, MSUALG_1, XBOOLE_0,
XBOOLE_1, ORDERS_1, CARD_1, XTUPLE_0;
schemes NAT_1, RELSET_1, PARTFUN1, FUNCT_1, PBOOLE;
begin :: Preliminary
::-------------------------------------------------------------------
:: Acknowledgements:
:: ================
::
:: I would like to thank Professor Andrzej Trybulec for suggesting me
:: the problem solved here.
::-------------------------------------------------------------------
Lm1: for p being FinSequence, f being Function st dom f = dom p holds
f is FinSequence
proof
let p be FinSequence;
dom p = Seg len p by FINSEQ_1:def 3;
hence thesis by FINSEQ_1:def 2;
end;
Lm2: for X being set, Y being non empty set
for p being FinSequence of X, f being Function of X,Y holds
f*p is FinSequence of Y
proof
let X be set, Y be non empty set;
let p be FinSequence of X, f be Function of X,Y;
A1: rng p c= X;
dom f = X by FUNCT_2:def 1;
then dom (f*p) = dom p by A1,RELAT_1:27;
then
A2: f*p is FinSequence by Lm1;
rng (f*p) c= Y;
hence thesis by A2,FINSEQ_1:def 4;
end;
registration
let X be with_non-empty_elements set;
cluster -> non-empty for FinSequence of X;
coherence
proof
let p be FinSequence of X;
let x be object;
assume x in dom p;
then p.x in rng p by FUNCT_1:def 3;
hence thesis;
end;
end;
registration
let A be non empty set;
cluster homogeneous quasi_total non-empty non empty for
PFuncFinSequence of A;
existence
proof set a = the homogeneous quasi_total non empty PartFunc of A*,A;
reconsider a as Element of PFuncs(A*,A) by PARTFUN1:45;
take <*a*>;
hereby
let n be Nat, h be PartFunc of A*,A;
assume n in dom <*a*>;
then n in Seg 1 by FINSEQ_1:38;
then n = 1 by FINSEQ_1:2,TARSKI:def 1;
hence h = <*a*>.n implies h is homogeneous;
end;
hereby
let n be Nat, h be PartFunc of A*,A;
assume n in dom <*a*>;
then n in Seg 1 by FINSEQ_1:38;
then n = 1 by FINSEQ_1:2,TARSKI:def 1;
hence h = <*a*>.n implies h is quasi_total;
end;
hereby
let n be object;
assume n in dom <*a*>;
then n in Seg 1 by FINSEQ_1:38;
then n = 1 by FINSEQ_1:2,TARSKI:def 1;
hence <*a*>.n is non empty;
end;
thus thesis;
end;
end;
registration
cluster non-empty -> non empty for UAStr;
coherence
proof
let A be UAStr;
assume that
A1: the charact of A <> {} and
A2: the charact of A is non-empty;
reconsider f = the charact of A as non empty Function by A1;
set x = the Element of dom f;
reconsider y = f.x as non empty set by A2;
A3: y in rng f by FUNCT_1:def 3;
rng f c= PFuncs((the carrier of A)*, the carrier of A) by FINSEQ_1:def 4;
then
A4: y is PartFunc of (the carrier of A)*, the carrier of A by A3,PARTFUN1:47;
reconsider y as non empty Function;
thus the carrier of A is non empty by A4;
end;
end;
theorem Th1:
for f,g being non-empty Function st product f c= product g holds
dom f = dom g & for x being set st x in dom f holds f.x c= g.x
proof
let f,g be non-empty Function;
assume
A1: product f c= product g;
set h = the Element of product f;
h in product f;
then
A2: ex i being Function st h = i & dom i = dom g &
for x being object st x in
dom g holds i.x in g.x by A1,CARD_3:def 5;
A3: ex i being Function st h = i & dom i = dom f &
for x being object st x in
dom f holds i.x in f.x by CARD_3:def 5;
hence dom f = dom g by A2;
let x be set;
assume
A4: x in dom f;
let z be object;
reconsider zz=z as set by TARSKI:1;
set k = the Element of product f;
reconsider k as Function;
defpred P[object] means $1 = x;
deffunc F1(object) = zz;
deffunc F2(object) = k.$1;
consider h being Function such that
A5: dom h = dom f & for y being object st y in dom f holds
(P[y] implies h.y = F1(y)) & (not P[y] implies h.y = F2(y)) from
PARTFUN1:sch 1;
assume
A6: z in f.x;
now
let y be object;
assume
A7: y in dom f;
then y <> x implies h.y = k.y by A5;
hence h.y in f.y by A5,A6,A7,CARD_3:9;
end;
then h in product f by A5,CARD_3:9;
then h.x in g.x by A1,A2,A3,A4,CARD_3:9;
hence thesis by A4,A5;
end;
theorem Th2:
for f,g being non-empty Function st product f = product g holds f = g
proof
let f,g be non-empty Function;
assume
A1: product f = product g;
set h = the Element of product f;
A2: ex i being Function st h = i & dom i = dom g &
for x being object st x in
dom g holds i.x in g.x by A1,CARD_3:def 5;
A3: ex i being Function st h = i & dom i = dom f &
for x being object st x in dom f holds i.x in f.x by CARD_3:def 5;
then for x be object st x in dom f holds f.x = g.x by A1,A2,Th1;
hence thesis by A2,A3;
end;
definition
let A be non empty set;
let f be PFuncFinSequence of A;
redefine func rng f -> Subset of PFuncs(A*, A); :: redefines rng (FUNCT_1, redefinition) → rng (RELAT_1, synonym) → proj2 (XTUPLE_0, definition)
coherence by FINSEQ_1:def 4;
end;
definition
let A,B be non empty set;
let S be non empty Subset of PFuncs(A, B);
redefine mode Element of S -> PartFunc of A,B; :: redefines Element (SUBSET_1, definition)
coherence
proof
let s be Element of S;
thus thesis by PARTFUN1:46;
end;
end;
definition
let A be non-empty UAStr;
mode OperSymbol of A is Element of dom the charact of A;
mode operation of A is Element of rng the charact of A;
end;
definition
let A be non-empty UAStr;
let o be OperSymbol of A;
func Den(o, A) -> operation of A equals
(the charact of A).o;
correctness by FUNCT_1:def 3;
end;
begin :: Partitions
::$CT
Lm3:
for X being set, P being a_partition of X, x,a,b being set
st x in a & a in P & x in b & b in P holds a = b by EQREL_1:70;
theorem Th3:
for X,Y being set st X is_finer_than Y
for p being FinSequence of X ex q being FinSequence of Y st
product p c= product q
proof
let X,Y be set;
assume
A1: for a being set st a in X ex b being set st b in Y & a c= b;
let p be FinSequence of X;
defpred P[object,object] means ex D2 being set st D2 = $2 & p.$1 c= D2;
A2: for i being object st i in dom p ex y being object st y in Y & P[i,y]
proof
let i be object;
assume
A3: i in dom p;
reconsider i as set by TARSKI:1;
p.i in rng p by FUNCT_1:def 3,A3;
then p.i in X;
then consider b being set such that
A4: b in Y & p.i c= b by A1;
take b;
thus thesis by A4;
end;
consider q being Function such that
A5: dom q = dom p & rng q c= Y &
for i being object st i in dom p holds P[i,q.i]
from FUNCT_1:sch 6(A2);
dom p = Seg len p by FINSEQ_1:def 3;
then q is FinSequence by A5,FINSEQ_1:def 2;
then
A6: q is FinSequence of Y by A5,FINSEQ_1:def 4;
for i being object st i in dom p holds p.i c= q.i
proof let i being object;
assume i in dom p;
then P[i,q.i] by A5;
hence thesis;
end;
then product p c= product q by A5,CARD_3:27;
hence thesis by A6;
end;
theorem Th4:
for X being set, P,Q being a_partition of X
for f being Function of P,Q st for a being set st a in P holds a c= f.a
for p being FinSequence of P, q being FinSequence of Q holds
product p c= product q iff f*p = q
proof
let X be set, P,Q be a_partition of X;
let f be Function of P,Q such that
A1: for a being set st a in P holds a c= f.a;
let p be FinSequence of P, q be FinSequence of Q;
A2: rng p c= P;
now
assume P <> {};
then reconsider X as non empty set;
Q is a_partition of X;
hence Q <> {};
end;
then dom f = P by FUNCT_2:def 1;
then
A3: dom (f*p) = dom p by A2,RELAT_1:27;
hereby
assume
A4: product p c= product q;
then
A5: dom p = dom q by Th1;
now
let x be object;
assume
A6: x in dom p;
then
A7: p.x c= q.x by A4,Th1;
A8: p.x in rng p by A6,FUNCT_1:def 3;
A9: q.x in rng q by A5,A6,FUNCT_1:def 3;
reconsider Y = X as non empty set by A8;
reconsider P9 = P, Q9 = Q as a_partition of Y;
reconsider a = p.x as Element of P9 by A8;
set z = the Element of a;
A10: a c= f.a by A1;
A11: z in a;
f.a in Q9 by FUNCT_2:5;
then q.x = f.a by A7,A9,A10,A11,Lm3;
hence (f*p).x = q.x by A6,FUNCT_1:13;
end;
hence f*p = q by A3,A5;
end;
assume
A12: f*p = q;
now
let x be object;
assume
A13: x in dom p;
then
A14: q.x = f.(p.x) by A12,FUNCT_1:13;
p.x in rng p by A13,FUNCT_1:def 3;
hence p.x c= q.x by A1,A14;
end;
hence thesis by A3,A12,CARD_3:27;
end;
theorem Th5:
for P being set, f being Function st rng f c= union P
ex p being Function st dom p = dom f & rng p c= P & f in product p
proof
let P be set, f be Function;
assume
A1: rng f c= union P;
defpred P[object,object] means ex D2 being set st D2 = $2 & f.$1 in D2;
A2: for x being object st x in dom f ex a being object st a in P & P[x,a]
proof
let x be object;
assume x in dom f;
then f.x in rng f by FUNCT_1:def 3;
then ex a being set st f.x in a & a in P by A1,TARSKI:def 4;
hence thesis;
end;
consider p being Function such that
A3: dom p = dom f & rng p c= P and
A4: for x being object st x in dom f holds P[x,p.x] from FUNCT_1:sch 6(A2);
take p;
for x being object st x in dom f holds f.x in p.x
proof let x be object;
assume x in dom f;
then P[x,p.x] by A4;
hence f.x in p.x;
end;
hence thesis by A3,CARD_3:def 5;
end;
theorem Th6:
for X be set, P being a_partition of X, f being FinSequence of X
ex p being FinSequence of P st f in product p
proof
let X be set, P be a_partition of X, f be FinSequence of X;
A1: rng f c= X;
union P = X by EQREL_1:def 4;
then consider p being Function such that
A2: dom p = dom f and
A3: rng p c= P and
A4: f in product p by A1,Th5;
dom p = Seg len f by A2,FINSEQ_1:def 3;
then p is FinSequence by FINSEQ_1:def 2;
then p is FinSequence of P by A3,FINSEQ_1:def 4;
hence thesis by A4;
end;
theorem
for X,Y being non empty set
for P being a_partition of X, Q being a_partition of Y holds
the set of all [:p,q:] where p is Element of P, q is Element of Q
is a_partition of [:X,Y:]
proof
let X,Y be non empty set;
let P be a_partition of X, Q be a_partition of Y;
set PQ = the set of all [:p,q:] where p is Element of P, q is Element of Q;
PQ c= bool [:X,Y:]
proof
let x be object;
assume x in PQ;
then ex p being Element of P, q being Element of Q st ( x = [:p,q :]);
hence thesis;
end;
then reconsider PQ as Subset-Family of [:X,Y:];
PQ is a_partition of [:X,Y:]
proof
thus union PQ = [:X,Y:]
proof
let x,y be object;
thus [x,y] in union PQ implies [x,y] in [:X,Y:];
assume
A1: [x,y] in [:X,Y:];
then
A2: x in X by ZFMISC_1:87;
A3: y in Y by A1,ZFMISC_1:87;
X = union P by EQREL_1:def 4;
then consider p being set such that
A4: x in p and
A5: p in P by A2,TARSKI:def 4;
Y = union Q by EQREL_1:def 4;
then consider q being set such that
A6: y in q and
A7: q in Q by A3,TARSKI:def 4;
A8: [x,y] in [:p,q:] by A4,A6,ZFMISC_1:87;
[:p,q:] in PQ by A5,A7;
hence thesis by A8,TARSKI:def 4;
end;
let A be Subset of [:X,Y:];
assume A in PQ;
then consider p being Element of P, q being Element of Q such that
A9: A = [:p,q:];
thus A <> {} by A9;
let B be Subset of [:X,Y:];
assume B in PQ;
then consider p1 being Element of P, q1 being Element of Q such that
A10: B = [:p1,q1:];
assume A <> B;
then p <> p1 or q <> q1 by A9,A10;
then p misses p1 or q misses q1 by EQREL_1:def 4;
then p /\ p1 = {} or q /\ q1 = {};
then A /\ B = [:{}, q /\ q1:] or A /\ B = [:p /\
p1,{}:] by A9,A10,ZFMISC_1:100;
then A /\ B = {};
hence thesis;
end;
hence thesis;
end;
theorem Th8:
for X being non empty set for P being a_partition of X holds
the set of all product p where p is Element of P* is a_partition of X*
proof
let X be non empty set;
let P be a_partition of X;
set PP = the set of all product p where p is Element of P*;
PP c= bool (X*)
proof
let x be object;
reconsider xx=x as set by TARSKI:1;
assume x in PP;
then consider p being Element of P* such that
A1: x = product p;
xx c= X*
proof
let y be object;
assume y in xx;
then consider f being Function such that
A2: y = f and
A3: dom f = dom p and
A4: for z being object st z in dom p holds f.z in p.z by A1,CARD_3:def 5;
dom p = Seg len p by FINSEQ_1:def 3;
then
A5: y is FinSequence by A2,A3,FINSEQ_1:def 2;
rng f c= X
proof
let z be object;
assume z in rng f;
then consider v being object such that
A6: v in dom p and
A7: z = f.v by A3,FUNCT_1:def 3;
p.v in rng p by A6,FUNCT_1:def 3;
then
A8: p.v in P;
z in p.v by A4,A6,A7;
hence thesis by A8;
end;
then y is FinSequence of X by A2,A5,FINSEQ_1:def 4;
hence thesis by FINSEQ_1:def 11;
end;
hence thesis;
end;
then reconsider PP as Subset-Family of X*;
PP is a_partition of X*
proof
thus union PP c= X*;
thus X* c= union PP
proof
let x be object;
assume x in X*;
then reconsider x as FinSequence of X by FINSEQ_1:def 11;
A9: rng x c= X;
union P = X by EQREL_1:def 4;
then consider p being Function such that
A10: dom p = dom x and
A11: rng p c= P and
A12: x in product p by A9,Th5;
dom p = Seg len x by A10,FINSEQ_1:def 3;
then reconsider p as FinSequence by FINSEQ_1:def 2;
reconsider p as FinSequence of P by A11,FINSEQ_1:def 4;
reconsider p as Element of P* by FINSEQ_1:def 11;
product p in PP;
hence thesis by A12,TARSKI:def 4;
end;
let A be Subset of X*;
assume A in PP;
then consider p being Element of P* such that
A13: A = product p;
thus A <> {} by A13;
let B be Subset of X*;
assume B in PP;
then consider q being Element of P* such that
A14: B = product q;
assume
A15: A <> B;
assume A meets B;
then consider x being object such that
A16: x in A and
A17: x in B by XBOOLE_0:3;
consider f being Function such that
A18: x = f and
A19: dom f = dom p and
A20: for z being object st z in dom p holds f.z in p.z
by A13,A16,CARD_3:def 5;
A21: ex g being Function st ( x = g)&( dom g = dom q)&( for z
being object st z in dom q holds g.z in q.z) by A14,A17,CARD_3:def 5;
now
let z be object;
assume
A22: z in dom p;
then
A23: f.z in p.z by A20;
A24: f.z in q.z by A18,A19,A21,A22;
A25: p.z in rng p by A22,FUNCT_1:def 3;
A26: q.z in rng q by A18,A19,A21,A22,FUNCT_1:def 3;
A27: p.z meets q.z by A23,A24,XBOOLE_0:3;
A28: p.z in P by A25;
q.z in P by A26;
hence p.z = q.z by A27,A28,EQREL_1:def 4;
end;
hence contradiction by A13,A14,A15,A18,A19,A21,FUNCT_1:2;
end;
hence thesis;
end;
theorem
for X being non empty set, n be Element of NAT
for P being a_partition of X holds
the set of all product p where p is Element of n-tuples_on P
is a_partition of n-tuples_on X
proof
let X be non empty set, n be Element of NAT;
let P be a_partition of X;
set nP = n-tuples_on P, nX = n-tuples_on X;
set PP = the set of all product p where p is Element of nP;
PP c= bool nX
proof
let x be object;
reconsider xx=x as set by TARSKI:1;
assume x in PP;
then consider p being Element of nP such that
A1: x = product p;
xx c= nX
proof
let y be object;
assume y in xx;
then consider f being Function such that
A2: y = f and
A3: dom f = dom p and
A4: for z being object st z in dom p holds f.z in p.z by A1,CARD_3:def 5;
A5: dom p = Seg len p by FINSEQ_1:def 3;
then reconsider y as FinSequence by A2,A3,FINSEQ_1:def 2;
rng f c= X
proof
let z be object;
assume z in rng f;
then consider v being object such that
A6: v in dom p and
A7: z = f.v by A3,FUNCT_1:def 3;
p.v in rng p by A6,FUNCT_1:def 3;
then
A8: p.v in P;
z in p.v by A4,A6,A7;
hence thesis by A8;
end;
then
A9: y is FinSequence of X by A2,FINSEQ_1:def 4;
A10: len y = len p by A2,A3,A5,FINSEQ_1:def 3;
len p = n by CARD_1:def 7;
then y is Element of nX by A9,A10,FINSEQ_2:92;
hence thesis;
end;
hence thesis;
end;
then reconsider PP as Subset-Family of nX;
PP is a_partition of nX
proof
thus union PP c= nX;
thus nX c= union PP
proof
let x be object;
assume x in nX;
then reconsider x as Element of nX;
A11: rng x c= X;
union P = X by EQREL_1:def 4;
then consider p being Function such that
A12: dom p = dom x and
A13: rng p c= P and
A14: x in product p by A11,Th5;
A15: dom p = Seg len x by A12,FINSEQ_1:def 3;
then reconsider p as FinSequence by FINSEQ_1:def 2;
reconsider p as FinSequence of P by A13,FINSEQ_1:def 4;
A16: len p = len x by A15,FINSEQ_1:def 3;
len x = n by CARD_1:def 7;
then reconsider p as Element of nP by A16,FINSEQ_2:92;
product p in PP;
hence thesis by A14,TARSKI:def 4;
end;
let A be Subset of nX;
assume A in PP;
then consider p being Element of nP such that
A17: A = product p;
thus A <> {} by A17;
let B be Subset of nX;
assume B in PP;
then consider q being Element of nP such that
A18: B = product q;
assume
A19: A <> B;
assume A meets B;
then consider x being object such that
A20: x in A and
A21: x in B by XBOOLE_0:3;
consider f being Function such that
A22: x = f and
A23: dom f = dom p and
A24: for z being object st z in dom p holds f.z in p.z
by A17,A20,CARD_3:def 5;
A25: ex g being Function st ( x = g)&( dom g = dom q)&( for z
being object st z in dom q holds g.z in q.z) by A18,A21,CARD_3:def 5;
now
let z be object;
assume
A26: z in dom p;
then
A27: f.z in p.z by A24;
A28: f.z in q.z by A22,A23,A25,A26;
A29: p.z in rng p by A26,FUNCT_1:def 3;
A30: q.z in rng q by A22,A23,A25,A26,FUNCT_1:def 3;
A31: p.z meets q.z by A27,A28,XBOOLE_0:3;
A32: p.z in P by A29;
q.z in P by A30;
hence p.z = q.z by A31,A32,EQREL_1:def 4;
end;
hence contradiction by A17,A18,A19,A22,A23,A25,FUNCT_1:2;
end;
hence thesis;
end;
theorem Th10:
for X being non empty set, Y be set st Y c= X
for P being a_partition of X holds
{a /\ Y where a is Element of P: a meets Y} is a_partition of Y
proof
let X be non empty set, Y be set;
assume
A1: Y c= X;
let P be a_partition of X;
set Q = {a /\ Y where a is Element of P: a meets Y};
Q c= bool Y
proof
let x be object;
reconsider xx=x as set by TARSKI:1;
assume x in Q;
then ex p being Element of P st ( x = p /\ Y)&( p meets Y);
then
A2: xx c= X /\ Y by XBOOLE_1:26;
X /\ Y = Y by A1,XBOOLE_1:28;
hence thesis by A2;
end;
then reconsider Q as Subset-Family of Y;
Q is a_partition of Y
proof
thus union Q c= Y;
thus Y c= union Q
proof
let x be object;
assume
A3: x in Y;
X = union P by EQREL_1:def 4;
then consider p being set such that
A4: x in p and
A5: p in P by A1,A3,TARSKI:def 4;
A6: p meets Y by A3,A4,XBOOLE_0:3;
A7: x in p /\ Y by A3,A4,XBOOLE_0:def 4;
p /\ Y in Q by A5,A6;
hence thesis by A7,TARSKI:def 4;
end;
let A be Subset of Y;
assume A in Q;
then consider p being Element of P such that
A8: A = p /\ Y and
A9: p meets Y;
thus A <> {} by A8,A9;
let B be Subset of Y;
assume B in Q;
then consider p1 being Element of P such that
A10: B = p1 /\ Y and p1 meets Y;
assume A <> B;
then p misses p1 by A8,A10,EQREL_1:def 4;
then A misses p1 by A8,XBOOLE_1:74;
hence thesis by A10,XBOOLE_1:74;
end;
hence thesis;
end;
theorem Th11:
for f being non empty Function, P being a_partition of dom f holds
the set of all f|a where a is Element of P is a_partition of f
proof
let f be non empty Function;
set X = dom f;
let P be a_partition of X;
set Y = f;
set Q = the set of all f|a where a is Element of P;
Q c= bool Y
proof
let x be object;
reconsider xx=x as set by TARSKI:1;
assume x in Q;
then ex p being Element of P st ( x = f|p);
then xx c= f by RELAT_1:59;
hence thesis;
end;
then reconsider Q as Subset-Family of Y;
Q is a_partition of Y
proof
Y c= union Q
proof
let y,z be object;
assume
A1: [y,z] in f;
then
A2: y in X by XTUPLE_0:def 12;
X = union P by EQREL_1:def 4;
then consider p being set such that
A3: y in p and
A4: p in P by A2,TARSKI:def 4;
A5: [y,z] in f|p by A1,A3,RELAT_1:def 11;
f|p in Q by A4;
hence thesis by A5,TARSKI:def 4;
end;
hence Y = union Q;
let A be Subset of Y;
assume A in Q;
then consider p being Element of P such that
A6: A = f|p;
reconsider p as non empty Subset of X;
thus A <> {} by A6;
let B be Subset of Y;
assume B in Q;
then consider p1 being Element of P such that
A7: B = f|p1;
assume A <> B;
then
A8: p misses p1 by A6,A7,EQREL_1:def 4;
assume A meets B;
then consider x being object such that
A9: x in A and
A10: x in B by XBOOLE_0:3;
consider y,z being object such that
A11: x = [y,z] by A9,RELAT_1:def 1;
A12: y in p by A6,A9,A11,RELAT_1:def 11;
y in p1 by A7,A10,A11,RELAT_1:def 11;
hence contradiction by A8,A12,XBOOLE_0:3;
end;
hence thesis;
end;
theorem Th12:
for X being set, p being FinSequence of SmallestPartition X
ex q being FinSequence of X st product p = {q}
proof
let X be set;
set P = SmallestPartition X;
let p be FinSequence of P;
set q = the Element of product p;
A1: dom q = dom p by CARD_3:9;
then reconsider q as FinSequence by Lm1;
A2: q in product p;
A3: product p c= Funcs(dom p, Union p) by FUNCT_6:1;
A4: Union p = union rng p by CARD_3:def 4;
A5: ex f being Function st q = f & dom f = dom p & rng f c= Union p
by A2,A3,FUNCT_2:def 2;
Union p c= union P by A4,ZFMISC_1:77;
then rng q c= union P by A5;
then rng q c= X by EQREL_1:def 4;
then reconsider q as FinSequence of X by FINSEQ_1:def 4;
take q;
thus product p c= {q}
proof
let x be object;
assume x in product p;
then consider g being Function such that
A6: x = g and
A7: dom g = dom p and
A8: for x being object st x in dom p holds g.x in p.x by CARD_3:def 5;
now
let y be object;
assume
A9: y in dom p;
then
A10: g.y in p.y by A8;
A11: q.y in p.y by A9,CARD_3:9;
A12: p.y in rng p by A9,FUNCT_1:def 3;
then
A13: p.y in P;
reconsider X as non empty set by A12;
P = the set of all {z} where z is Element of X by EQREL_1:37;
then consider z being Element of X such that
A14: p.y = {z} by A13;
thus g.y = z by A10,A14,TARSKI:def 1
.= q.y by A11,A14,TARSKI:def 1;
end;
then x = q by A1,A6,A7,FUNCT_1:2;
hence thesis by TARSKI:def 1;
end;
thus thesis by ZFMISC_1:31;
end;
definition
let X be set;
mode IndexedPartition of X -> Function means
:
Def2: rng it is a_partition of X & it is one-to-one;
existence
proof set p = the a_partition of X;
take id p;
thus thesis;
end;
end;
definition
let X be set;
let P be IndexedPartition of X;
redefine func rng P -> a_partition of X; :: redefines rng (FUNCT_1, redefinition) → rng (RELAT_1, synonym) → proj2 (XTUPLE_0, definition)
coherence by Def2;
end;
registration
let X be set;
cluster -> one-to-one non-empty for IndexedPartition of X;
coherence
proof
let P be IndexedPartition of X;
thus P is one-to-one by Def2;
let x be object;
assume x in dom P;
then P.x in rng P by FUNCT_1:def 3;
hence thesis;
end;
end;
registration
let X be non empty set;
cluster -> non empty for IndexedPartition of X;
coherence
proof
let P be IndexedPartition of X;
set a = the Element of rng P;
ex b being object st [b,a] in P by XTUPLE_0:def 13;
hence thesis;
end;
end;
definition
let X be set, P be a_partition of X;
redefine func id P -> IndexedPartition of X; :: redefines id (RELAT_1, definition)
coherence
proof rng id P = P;
hence thesis by Def2;
end;
end;
definition
let X be set;
let P be IndexedPartition of X;
let x be object;
assume
A1: x in X;
A2: union rng P = X by EQREL_1:def 4;
func P-index_of x -> set means
: Def3:
it in dom P & x in P.it;
existence
proof consider a being set such that
A3: x in a and
A4: a in rng P by A1,A2,TARSKI:def 4;
ex y being object st y in dom P & a = P.y by A4,FUNCT_1:def 3;
hence thesis by A3;
end;
correctness
proof
let y1,y2 be set;
assume that
A5: y1 in dom P and
A6: x in P.y1 and
A7: y2 in dom P and
A8: x in P.y2;
A9: P.y1 in rng P by A5,FUNCT_1:def 3;
A10: P.y2 in rng P by A7,FUNCT_1:def 3;
P.y1 meets P.y2 by A6,A8,XBOOLE_0:3;
then P.y1 = P.y2 by A9,A10,EQREL_1:def 4;
hence thesis by A5,A7,FUNCT_1:def 4;
end;
end;
theorem Th13:
for X being set, P being non-empty Function st Union P = X &
for x,y being set st x in dom P & y in dom P & x <> y holds P.x misses P.y
holds P is IndexedPartition of X
proof
let X be set, P be non-empty Function such that
A1: Union P = X and
A2: for x,y being set st x in dom P & y in dom P & x <> y holds P.x misses P.y;
rng P c= bool X
proof
let y be object;
reconsider yy=y as set by TARSKI:1;
assume y in rng P;
then yy c= union rng P by ZFMISC_1:74;
then yy c= X by A1,CARD_3:def 4;
hence thesis;
end;
then reconsider Y = rng P as Subset-Family of X;
Y is a_partition of X
proof
thus union Y = X by A1,CARD_3:def 4;
let A be Subset of X;
assume
A3: A in Y;
then
A4: ex x being object st x in dom P & A = P.x by FUNCT_1:def 3;
thus A<>{} by A3;
let B be Subset of X;
assume B in Y;
then ex y being object st y in dom P & B = P.y by FUNCT_1:def 3;
hence thesis by A2,A4;
end;
hence rng P is a_partition of X;
let x,y be object;
assume that
A5: x in dom P and
A6: y in dom P and
A7: P.x = P.y and
A8: x <> y;
reconsider Px = P.x, Py = P.y as non empty set by A5,A6,FUNCT_1:def 9;
set a = the Element of Px;
P.x misses P.y by A2,A5,A6,A8;
then not a in Py by XBOOLE_0:3;
hence contradiction by A7;
end;
theorem Th14:
for X,Y being non empty set, P being a_partition of Y
for f being Function of X, P st P c= rng f & f is one-to-one
holds f is IndexedPartition of Y
proof
let X,Y be non empty set, P be a_partition of Y;
let f be Function of X, P;
assume P c= rng f;
then rng f = P;
hence thesis by Def2;
end;
begin :: Relations generated by operations of partial algebra
scheme IndRelationEx {A, B() -> non empty set, i() -> Nat,
R0() -> (Relation of A(),B()), RR(set,set) -> Relation of A(),B()}:
ex R being Relation of A(),B(), F being ManySortedSet of NAT st
R = F.i() & F.0 = R0() &
for i being Nat, R being Relation of A(),B() st R = F.i
holds F.(i+1) = RR(R,i)
proof
deffunc G(set,set) = RR($2,$1);
consider F being Function such that
A1: dom F = NAT and
A2: F.0 = R0() & for n being Nat holds F.(n+1) = G(n,F.n) from NAT_1:sch 11;
reconsider F as ManySortedSet of NAT by A1,PARTFUN1:def 2,RELAT_1:def 18;
defpred P[Nat] means F.$1 is Relation of A(),B();
A3: P[ 0 ] by A2;
A4: now
let i be Nat;
assume P[i];
then reconsider R = F.i as Relation of A(),B();
F.(i+1) = RR(R,i) by A2;
hence P[i+1];
end;
for i being Nat holds P[i] from NAT_1:sch 2(A3,A4);
then reconsider R = F.i() as Relation of A(),B();
take R,F;
thus thesis by A2;
end;
scheme RelationUniq {A, B() -> non empty set, P[set,set]}:
for R1, R2 being Relation of A(), B() st
(for x being Element of A(), y being Element of B() holds
[x,y] in R1 iff P[x,y]) &
(for x being Element of A(), y being Element of B() holds
[x,y] in R2 iff P[x,y]) holds R1 = R2
proof
let R1, R2 be Relation of A(), B() such that
A1: for x being Element of A(), y being Element of B() holds
[x,y] in R1 iff P[x,y] and
A2: for x being Element of A(), y being Element of B() holds
[x,y] in R2 iff P[x,y];
let x,y be object;
hereby
assume
A3: [x,y] in R1;
then reconsider a = x as Element of A() by ZFMISC_1:87;
reconsider b = y as Element of B() by A3,ZFMISC_1:87;
P[a,b] by A1,A3;
hence [x,y] in R2 by A2;
end;
assume
A4: [x,y] in R2;
then reconsider a = x as Element of A() by ZFMISC_1:87;
reconsider b = y as Element of B() by A4,ZFMISC_1:87;
P[a,b] by A2,A4;
hence thesis by A1;
end;
scheme IndRelationUniq {A, B() -> non empty set, i() -> Nat,
R0() -> (Relation of A(),B()), RR(set,set) -> Relation of A(),B()}:
for R1, R2 being Relation of A(),B() st (ex F being ManySortedSet of NAT st
R1 = F.i() & F.0 = R0() &
for i being Nat, R being Relation of A(),B() st R = F.i
holds F.(i+1) = RR(R,i)) & (ex F being ManySortedSet of NAT st
R2 = F.i() & F.0 = R0() &
for i being Nat, R being Relation of A(),B() st R = F.i
holds F.(i+1) = RR(R,i)) holds R1 = R2
proof
let R1, R2 be Relation of A(),B();
given F1 being ManySortedSet of NAT such that
A1: R1 = F1.i() and
A2: F1.0 = R0() and
A3: for i being Nat, R being Relation of A(),B() st R = F1.i
holds F1.(i+1) = RR(R,i);
given F2 being ManySortedSet of NAT such that
A4: R2 = F2.i() and
A5: F2.0 = R0() and
A6: for i being Nat, R being Relation of A(),B() st R = F2.i
holds F2.(i+1) = RR(R,i);
defpred P[Nat] means F1.$1 = F2.$1 & F1.$1 is Relation of A(),B();
A7: P[ 0 ] by A2,A5;
A8: now
let i be Nat;
assume
A9: P[i];
then reconsider R = F1.i as Relation of A(),B();
F1.(i+1) = RR(R,i) by A3;
hence P[i+1] by A6,A9;
end;
for i being Nat holds P[i] from NAT_1:sch 2(A7,A8);
hence thesis by A1,A4;
end;
definition
let A be partial non-empty UAStr;
func DomRel A -> Relation of the carrier of A means
:Def4:
for x,y being Element of A holds [x,y] in it iff
for f being operation of A, p,q being FinSequence holds
p^<*x*>^q in dom f iff p^<*y*>^q in dom f;
existence
proof
defpred P[set,set] means for f be operation of A, p,q be FinSequence holds
p^<*$1*>^q in dom f iff p^<*$2*>^q in dom f;
thus ex D be Relation of the carrier of A st
for x,y being Element of A holds [x,y] in D iff P[x,y]
from RELSET_1:sch 2;
end;
uniqueness
proof
defpred P[set,set] means for f be operation of A, p,q be FinSequence holds
p^<*$1*>^q in dom f iff p^<*$2*>^q in dom f;
thus for D1,D2 be Relation of the carrier of A st
(for x,y being Element of A holds [x,y] in D1 iff P[x,y]) &
(for x,y being Element of A holds [x,y] in D2 iff P[x,y])
holds D1 = D2 from RelationUniq;
end;
end;
registration
let A be partial non-empty UAStr;
cluster DomRel A -> total symmetric transitive;
coherence
proof
set X = the carrier of A;
A1: DomRel A is_reflexive_in X
proof
let x be object;
for f being operation of A for a,b be FinSequence holds
a^<*x*>^b in dom f iff a^<*x*>^b in dom f;
hence thesis by Def4;
end;
then
A2: dom DomRel A = X by ORDERS_1:13;
A3: field DomRel A = X by A1,ORDERS_1:13;
thus DomRel A is total by A2,PARTFUN1:def 2;
DomRel A is_symmetric_in X
proof
let x,y be object;
assume that
A4: x in X and
A5: y in X;
reconsider x9 = x, y9 = y as Element of X by A4,A5;
assume [x,y] in DomRel A;
then for f being operation of A for a,b be FinSequence holds
a^<*x9*>^b in dom f iff a^<*y9*>^b in dom f by Def4;
hence thesis by Def4;
end;
hence DomRel A is symmetric by A3;
DomRel A is_transitive_in X
proof
let x,y,z be object;
assume that
A6: x in X and
A7: y in X and
A8: z in X;
reconsider x9 = x, y9 = y, z9 = z as Element of X by A6,A7,A8;
assume that
A9: [x,y] in DomRel A and
A10: [y,z] in DomRel A;
now
let f be operation of A, a,b be FinSequence;
a^<*x9*>^b in dom f iff a^<*y9*>^b in dom f by A9,Def4;
hence a^<*x9*>^b in dom f iff a^<*z9*>^b in dom f by A10,Def4;
end;
hence thesis by Def4;
end;
hence thesis by A3;
end;
end;
definition
let A be non-empty partial UAStr;
let R be Relation of the carrier of A;
func R|^A -> Relation of the carrier of A means
:
Def5: for x,y being Element of A holds [x,y] in it iff [x,y] in R &
for f being operation of A for p,q being FinSequence
st p^<*x*>^q in dom f & p^<*y*>^q in dom f
holds [f.(p^<*x*>^q), f.(p^<*y*>^q)] in R;
existence
proof
defpred P[set,set] means [$1,$2] in R &
for f be operation of A for p,q be FinSequence st p^<*$1*>^q in dom f &
p^<*$2*>^q in dom f holds [f.(p^<*$1*>^q), f.(p^<*$2*>^q)] in R;
thus ex D be Relation of the carrier of A st
for x,y being Element of A holds [x,y] in D iff P[x,y]
from RELSET_1:sch 2;
end;
uniqueness
proof
defpred P[set,set] means [$1,$2] in R &
for f be operation of A for p,q be FinSequence st p^<*$1*>^q in dom f &
p^<*$2*>^q in dom f holds [f.(p^<*$1*>^q), f.(p^<*$2*>^q)] in R;
thus for D1,D2 be Relation of the carrier of A st
(for x,y being Element of A holds [x,y] in D1 iff P[x,y]) &
(for x,y being Element of A holds [x,y] in D2 iff P[x,y])
holds D1 = D2 from RelationUniq;
end;
end;
definition
let A be non-empty partial UAStr;
let R be Relation of the carrier of A;
let i be Nat;
func R|^(A,i) -> Relation of the carrier of A means
:
Def6: ex F being ManySortedSet of NAT st it = F.i & F.0 = R &
for i being Nat, R being Relation of the carrier of A st R = F.i
holds F.(i+1) = R|^A;
existence
proof
deffunc RR(Relation of the carrier of A,the carrier of A,Nat)
= $1 |^ A;
thus ex D be Relation of the carrier of A st
ex F being ManySortedSet of NAT st D = F.i & F.0 = R &
for i being Nat, R being Relation of the carrier of A st R = F.i
holds F.(i+1) = RR(R,i) from IndRelationEx;
end;
uniqueness
proof
deffunc RR(Relation of the carrier of A,the carrier of A,Nat)
= $1 |^ A;
thus for D1,D2 be Relation of the carrier of A st
(ex F being ManySortedSet of NAT st D1 = F.i & F.0 = R &
for i being Nat, R being Relation of the carrier of A st R = F.i
holds F.(i+1) = RR(R,i)) &
(ex F being ManySortedSet of NAT st D2 = F.i & F.0 = R &
for i being Nat, R being Relation of the carrier of A st R = F.i
holds F.(i+1) = RR(R,i)) holds D1 = D2 from IndRelationUniq;
end;
end;
theorem Th15:
for A being non-empty partial UAStr, R being Relation of the carrier of A
holds R|^(A,0) = R & R|^(A,1) = R|^A
proof
let A be non-empty partial UAStr;
let R be Relation of the carrier of A;
consider F being ManySortedSet of NAT such that R|^(A,0) = F.0 and
A1: F.0 = R and
A2: for i being Nat, R being Relation of the carrier of A st
R = F.i holds F.(i+1) = R|^A by Def6;
F.(0+1) = R|^A by A1,A2;
hence thesis by A1,A2,Def6;
end;
theorem Th16:
for A being non-empty partial UAStr, i being Nat,
R being Relation of the carrier of A holds R|^(A,i+1) = R|^(A,i)|^A
proof
let A be non-empty partial UAStr;
let i be Nat;
let R be Relation of the carrier of A;
consider F being ManySortedSet of NAT such that
A1: R|^(A,i) = F.i and
A2: F.0 = R and
A3: for i being Nat, R being Relation of the carrier of A st
R = F.i holds F.(i+1) = R|^A
by Def6;
F.(i+1) = R|^(A,i)|^A by A1,A3;
hence thesis by A2,A3,Def6;
end;
theorem
for A being non-empty partial UAStr, i,j being Element of NAT,
R being Relation of the carrier of A holds R|^(A,i+j) = R|^(A,i)|^(A,j)
proof
let A be non-empty partial UAStr;
let i,j be Element of NAT;
let R be Relation of the carrier of A;
defpred P[Nat] means R|^(A,i+$1) = R|^(A,i)|^(A,$1);
A1: P[ 0 ] by Th15;
A2: now
let j be Nat;
assume
A3: P[j];
R|^(A,i+(j+1)) = R|^(A,(i+j)+1) .= R|^(A,i+j)|^A by Th16
.= R|^(A,i)|^(A,j+1) by A3,Th16;
hence P[j+1];
end;
for j being Nat holds P[j] from NAT_1:sch 2(A1,A2);
hence thesis;
end;
theorem Th18:
for A being non-empty partial UAStr
for R being Equivalence_Relation of the carrier of A st R c= DomRel A
holds R|^A is total symmetric transitive
proof
let A be non-empty partial UAStr;
let R be Equivalence_Relation of the carrier of A;
assume
A1: R c= DomRel A;
now
let x be object;
assume x in the carrier of A;
then reconsider a = x as Element of A;
A2: [a,a] in R by EQREL_1:5;
now
let f be operation of A, p,q be FinSequence;
assume that
A3: p^<*a*>^q in dom f and p^<*a*>^q in dom f;
f.(p^<*a*>^q) in rng f by A3,FUNCT_1:def 3;
hence [f.(p^<*a*>^q), f.(p^<*a*>^q)] in R by EQREL_1:5;
end;
hence [x,x] in R|^A by A2,Def5;
end;
then
A4: R|^A is_reflexive_in the carrier of A;
then
A5: dom(R|^A) = the carrier of A by ORDERS_1:13;
A6: field(R|^A) = the carrier of A by A4,ORDERS_1:13;
thus R|^A is total by A5,PARTFUN1:def 2;
now
let x,y be object;
assume that
A7: x in the carrier of A and
A8: y in the carrier of A;
reconsider a = x, b = y as Element of A by A7,A8;
assume
A9: [x,y] in R|^A;
then
A10: [a,b] in R by Def5;
now
thus [b,a] in R by A10,EQREL_1:6;
let f be operation of A;
let p,q be FinSequence;
assume that
A11: p^<*b*>^q in dom f and
A12: p^<*a*>^q in dom f;
[f.(p^<*a*>^q), f.(p^<*b*>^q)] in R by A9,A11,A12,Def5;
hence [f.(p^<*b*>^q), f.(p^<*a*>^q)] in R by EQREL_1:6;
end;
hence [y,x] in R|^A by Def5;
end;
then R|^A is_symmetric_in the carrier of A;
hence R|^A is symmetric by A6;
now
let x,y,z be object;
assume that
A13: x in the carrier of A and
A14: y in the carrier of A and
A15: z in the carrier of A;
reconsider a = x, b = y, c = z as Element of A by A13,A14,A15;
assume that
A16: [x,y] in R|^A and
A17: [y,z] in R|^A;
A18: now
let f be operation of A;
let p,q be FinSequence;
A19: [a,b] in R by A16,Def5;
A20: p^<*a*>^q in dom f & p^<*b*>^q in dom f implies [f.(p^<*a*>^q), f.(p^
<*b*>^q)] in R by A16,Def5;
p^<*b*>^q in dom f & p^<*c*>^q in dom f implies [f.(p^<*b*>^q), f.(p^
<*c*>^q)] in R by A17,Def5;
hence p^<*a*>^q in dom f & p^<*c*>^q in dom f
implies [f.(p^<*a*>^q), f.(p^<*c*>^q)] in R by A1,A19,A20,Def4,EQREL_1:7;
end;
A21: [a,b] in R by A16,Def5;
[b,c] in R by A17,Def5;
then [a,c] in R by A21,EQREL_1:7;
hence [x,z] in R|^A by A18,Def5;
end;
then R|^A is_transitive_in the carrier of A;
hence thesis by A6;
end;
theorem Th19:
for A being non-empty partial UAStr
for R being Relation of the carrier of A holds R|^A c= R
proof
let A be non-empty partial UAStr;
let R be Relation of the carrier of A;
let x,y be object;
assume
A1: [x,y] in R|^A;
then
A2: x in the carrier of A by ZFMISC_1:87;
y in the carrier of A by A1,ZFMISC_1:87;
hence thesis by A1,A2,Def5;
end;
theorem Th20:
for A being non-empty partial UAStr
for R being Equivalence_Relation of the carrier of A st R c= DomRel A
for i being Element of NAT holds R|^(A,i) is total symmetric transitive
proof
let A be non-empty partial UAStr;
let R be Equivalence_Relation of the carrier of A such that
A1: R c= DomRel A;
defpred P[Nat] means
R|^(A,$1) c= DomRel A & R|^(A,$1) is total symmetric transitive;
A2: P[ 0 ] by A1,Th15;
A3: now
let i be Nat;
assume
A4: P[i];
A5: R|^(A,i)|^A c= R|^(A,i) by Th19;
R|^(A,i)|^A = R|^(A,i+1) by Th16;
hence P[i+1] by A4,A5,Th18,XBOOLE_1:1;
end;
for i being Nat holds P[i] from NAT_1:sch 2(A2,A3);
hence thesis;
end;
definition
let A be non-empty partial UAStr;
defpred P[set,set] means
for i being Element of NAT holds [$1,$2] in (DomRel A)|^(A,i);
func LimDomRel A -> Relation of the carrier of A means
:
Def7: for x,y being Element of A holds
[x,y] in it iff for i being Element of NAT holds [x,y] in (DomRel A)|^(A,i);
existence
proof
thus ex D be Relation of the carrier of A st
for x,y being Element of A holds [x,y] in D iff P[x,y]
from RELSET_1:sch 2;
end;
uniqueness
proof
thus for D1,D2 be Relation of the carrier of A st
(for x,y being Element of A holds [x,y] in D1 iff P[x,y]) &
(for x,y being Element of A holds [x,y] in D2 iff P[x,y])
holds D1 = D2 from RelationUniq;
end;
end;
theorem Th21:
for A being non-empty partial UAStr holds LimDomRel A c= DomRel A
proof
let A be non-empty partial UAStr, x,y be object;
assume
A1: [x,y] in LimDomRel A;
then
A2: x in the carrier of A by ZFMISC_1:87;
y in the carrier of A by A1,ZFMISC_1:87;
then [x,y] in (DomRel A)|^(A,0) by A1,A2,Def7;
hence thesis by Th15;
end;
registration
let A be non-empty partial UAStr;
cluster LimDomRel A -> total symmetric transitive;
coherence
proof
now
let x be object;
assume x in the carrier of A;
then reconsider a = x as Element of A;
now
let i be Element of NAT;
(DomRel A)|^(A,i) is total symmetric transitive by Th20;
hence [a,a] in (DomRel A)|^(A,i) by EQREL_1:5;
end;
hence [x,x] in LimDomRel A by Def7;
end;
then
A1: LimDomRel A is_reflexive_in the carrier of A;
then
A2: dom(LimDomRel A) = the carrier of A by ORDERS_1:13;
A3: field(LimDomRel A) = the carrier of A by A1,ORDERS_1:13;
thus LimDomRel A is total by A2,PARTFUN1:def 2;
now
let x,y be object;
assume that
A4: x in the carrier of A and
A5: y in the carrier of A;
reconsider a = x, b = y as Element of A by A4,A5;
assume
A6: [x,y] in LimDomRel A;
now
let i be Element of NAT;
A7: (DomRel A)|^(A,i) is total symmetric transitive by Th20;
[a,b] in (DomRel A)|^(A,i) by A6,Def7;
hence [b,a] in (DomRel A)|^(A,i) by A7,EQREL_1:6;
end;
hence [y,x] in LimDomRel A by Def7;
end;
then LimDomRel A is_symmetric_in the carrier of A;
hence LimDomRel A is symmetric by A3;
now
let x,y,z be object;
assume that
A8: x in the carrier of A and
A9: y in the carrier of A and
A10: z in the carrier of A;
reconsider a = x, b = y, c = z as Element of A by A8,A9,A10;
assume that
A11: [x,y] in LimDomRel A and
A12: [y,z] in LimDomRel A;
now
let i be Element of NAT;
A13: (DomRel A)|^(A,i) is total symmetric transitive by Th20;
A14: [a,b] in (DomRel A)|^(A,i) by A11,Def7;
[b,c] in (DomRel A)|^(A,i) by A12,Def7;
hence [a,c] in (DomRel A)|^(A,i) by A13,A14,EQREL_1:7;
end;
hence [x,z] in LimDomRel A by Def7;
end;
then LimDomRel A is_transitive_in the carrier of A;
hence thesis by A3;
end;
end;
begin :: Partitability
definition
let X be non empty set;
let f be PartFunc of X*, X;
let P be a_partition of X;
pred f is_partitable_wrt P means
for p being FinSequence of P ex a being Element of P st f.:product p c= a;
end;
definition
let X be non empty set;
let f be PartFunc of X*, X;
let P be a_partition of X;
pred f is_exactly_partitable_wrt P means
f is_partitable_wrt P &
for p being FinSequence of P st product p meets dom f holds
product p c= dom f;
end;
theorem
for A being non-empty partial UAStr for f being operation of A holds
f is_exactly_partitable_wrt SmallestPartition the carrier of A
proof
let A be non-empty partial UAStr;
set P = SmallestPartition the carrier of A;
let f be operation of A;
hereby
let p be FinSequence of P;
consider q being FinSequence of the carrier of A such that
A1: product p = {q} by Th12;
q in dom f & f.q in rng f & rng f c= the carrier of A
or not q in dom f by FUNCT_1:def 3;
then consider x being Element of A such that
A2: q in dom f & x = f.q or not q in dom f;
P = the set of all {z} where z is Element of A by EQREL_1:37;
then {x} in P;
then reconsider a = {x} as Element of P;
take a;
thus f.:product p c= a
proof
let z be object;
assume z in f.:product p;
then consider y being object such that
A3: y in dom f and
A4: y in product p and
A5: z = f.y by FUNCT_1:def 6;
y = q by A1,A4,TARSKI:def 1;
hence thesis by A2,A3,A5,TARSKI:def 1;
end;
end;
let p be FinSequence of P;
consider q being FinSequence of the carrier of A such that
A6: product p = {q} by Th12;
assume product p meets dom f;
then
A7: ex x being object st x in product p & x in dom f by XBOOLE_0:3;
let z be object;
assume z in product p;
then z = q by A6,TARSKI:def 1;
hence thesis by A6,A7,TARSKI:def 1;
end;
scheme FiniteTransitivity {x, y() -> FinSequence, P[set], R[set,set]}: P[y()]
provided
A1: P[x()] and
A2: len x() = len y() and
A3: for p,q being FinSequence, z1,z2 being set
st P[p^<*z1*>^q] & R[z1,z2] holds P[p^<*z2*>^q] and
A4: for i being Element of NAT st i in dom x() holds R[x().i, y().i]
proof
defpred Q[Nat] means for x1,x2, y1,y2 being FinSequence
st len x1 = $1 & x() = x1^x2 & len y1 = $1 & y() = y1^y2 holds P[y1^x2];
A5: Q[ 0 ]
proof
let x1,x2, y1,y2 be FinSequence;
assume that
A6: len x1 = 0 and
A7: x() = x1^x2 and
A8: len y1 = 0 and y() = y1^y2;
A9: x1 = {} by A6;
y1 = {} by A8;
hence thesis by A1,A7,A9;
end;
A10: for i being Nat st Q[i] holds Q[i+1]
proof
let i be Nat such that
A11: for x1,x2, y1,y2 being FinSequence
st len x1 = i & x() = x1^x2 & len y1 = i & y() = y1^y2 holds P[y1^x2];
let x1,x2, y1,y2 be FinSequence such that
A12: len x1 = i+1 and
A13: x() = x1^x2 and
A14: len y1 = i+1 and
A15: y() = y1^y2;
A16: x1 <> {} by A12;
A17: y1 <> {} by A14;
consider x9 being FinSequence, xx being object such that
A18: x1 = x9^<*xx*> by A16,FINSEQ_1:46;
consider y9 being FinSequence, yy being object such that
A19: y1 = y9^<*yy*> by A17,FINSEQ_1:46;
A20: dom x1 = Seg len x1 by FINSEQ_1:def 3;
A21: dom y1 = Seg len y1 by FINSEQ_1:def 3;
A22: len <*xx*> = 1 by FINSEQ_1:40;
A23: len <*yy*> = 1 by FINSEQ_1:40;
A24: len x1 = len x9+1 by A18,A22,FINSEQ_1:22;
A25: len y1 = len y9+1 by A19,A23,FINSEQ_1:22;
A26: x() = x9^(<*xx*>^x2) by A13,A18,FINSEQ_1:32;
A27: y() = y9^(<*yy*>^ y2) by A15,A19,FINSEQ_1:32;
A28: i+1 in dom x1 by A12,A20,FINSEQ_1:4;
A29: dom x1 c= dom x() by A13,FINSEQ_1:26;
A30: x1.(len x9+1) = xx by A18,FINSEQ_1:42;
A31: y1.(len y9+1) = yy by A19,FINSEQ_1:42;
A32: P[y9^(<*xx*>^x2)] by A11,A12,A14,A24,A25,A26,A27;
A33: x().(i+1) = xx by A12,A13,A24,A28,A30,FINSEQ_1:def 7;
A34: y().(i+1) = yy by A12,A14,A15,A20,A21,A25,A28,A31,FINSEQ_1:def 7;
P[y9^<*xx*>^x2] by A32,FINSEQ_1:32;
hence thesis by A3,A4,A19,A28,A29,A33,A34;
end;
A35: for i being Nat holds Q[i] from NAT_1:sch 2(A5,A10);
A36: x() = x()^{} by FINSEQ_1:34;
y() = y()^{} by FINSEQ_1:34;
hence thesis by A2,A35,A36;
end;
theorem Th23:
for A being non-empty partial UAStr for f being operation of A holds
f is_exactly_partitable_wrt Class LimDomRel A
proof
let A be non-empty partial UAStr;
set P = Class LimDomRel A;
let f be operation of A;
hereby
let p be FinSequence of P;
set a0 = the Element of P;
per cases;
suppose product p meets dom f;
then consider x being object such that
A1: x in product p and
A2: x in dom f by XBOOLE_0:3;
f.x in the carrier of A by A2,PARTFUN1:4;
then reconsider a = Class(LimDomRel A, f.x) as Element of P by
EQREL_1:def 3;
take a;
thus f.:product p c= a
proof
let y be object;
assume y in f.:product p;
then consider z being object such that
z in dom f and
A3: z in product p and
A4: y = f.z by FUNCT_1:def 6;
A5: product p c= Funcs(dom p, Union p) by FUNCT_6:1;
then
A6: ex f being Function st x = f & dom f = dom p & rng f c= Union p by A1,
FUNCT_2:def 2;
A7: ex f being Function st z = f & dom f = dom p & rng f c= Union p by A3
,A5,FUNCT_2:def 2;
reconsider x, z as Function by A1,A3;
A8: dom p = Seg len p by FINSEQ_1:def 3;
then reconsider x, z as FinSequence by A6,A7,FINSEQ_1:def 2;
defpred P[set] means $1 in dom f & f.$1 in a;
defpred R[set,set] means [$1,$2] in LimDomRel A;
len x = len p by A6,A8,FINSEQ_1:def 3;
then
A9: len x = len z by A7,A8,FINSEQ_1:def 3;
A10: P[x] by A2,EQREL_1:20,PARTFUN1:4;
A11: for p1,q1 being FinSequence, z1,z2 being set
st P[p1^<*z1*>^q1] & R[z1,z2] holds P[p1^<*z2*>^q1]
proof
let p1,q1 be FinSequence, z1,z2 be set;
assume that
A12: p1^<*z1*>^q1 in dom f and
A13: f.(p1^<*z1*>^q1) in a and
A14: [z1,z2] in LimDomRel A;
A15: [f.(p1^<*z1*>^q1), f.x] in LimDomRel A by A13,EQREL_1:19;
A16: LimDomRel A c= DomRel A by Th21;
A17: z1 in the carrier of A by A14,ZFMISC_1:87;
A18: z2 in the carrier of A by A14,ZFMISC_1:87;
hence
A19: p1^<*z2*>^q1 in dom f by A12,A14,A16,A17,Def4;
A20: f.(p1^<*z1*>^q1) in rng f by A12,FUNCT_1:def 3;
A21: f.(p1^<*z2*>^q1) in rng f by A19,FUNCT_1:def 3;
now
let i be Element of NAT;
[z1,z2] in (DomRel A)|^(A,i+1) by A14,A17,A18,Def7;
then [z1,z2] in (DomRel A)|^(A,i)|^A by Th16;
then
A22: [
f.(p1^<*z1*>^q1),f.(p1^<*z2*>^q1)] in (DomRel A)|^(A,i) by A12,A17,A18,A19,Def5
;
(DomRel A)|^(A,i) is total symmetric transitive by Th20;
hence [f.(p1^<*z2*>^q1),f.(p1^<*z1*>^q1)] in (DomRel A)|^(A,i)
by A22,EQREL_1:6;
end;
then [f.(p1^<*z2*>^q1),f.(p1^<*z1*>^q1)] in LimDomRel A by A20,A21
,Def7;
then [f.(p1^<*z2*>^q1), f.x] in LimDomRel A by A15,EQREL_1:7;
hence thesis by EQREL_1:19;
end;
A23: for i being Element of NAT st i in dom x holds R[x.i, z.i]
proof
let i be Element of NAT;
assume
A24: i in dom x;
then p.i in rng p by A6,FUNCT_1:def 3;
then reconsider a = p.i as Element of P;
A25: ex
g being Function st x = g & dom g = dom p & for x being object st x in
dom p holds g.x in p.x by A1,CARD_3:def 5;
A26: ex
g being Function st z = g & dom g = dom p & for x being object st x in
dom p holds g.x in p.x by A3,CARD_3:def 5;
A27: ex b being object
st b in the carrier of A & a = Class(LimDomRel A, b)
by EQREL_1:def 3;
A28: x.i in a by A24,A25;
z.i in a by A24,A25,A26;
hence thesis by A27,A28,EQREL_1:22;
end;
P[z] from FiniteTransitivity(A10,A9,A11,A23);
hence thesis by A4;
end;
end;
suppose product p misses dom f;
then (product p) /\ dom f = {};
then f.:product p = f.:{} by RELAT_1:112
.= {};
then f.:product p c= a0;
hence ex a being Element of P st f.:product p c= a;
end;
end;
let p be FinSequence of P;
assume product p meets dom f;
then consider x being object such that
A29: x in product p and
A30: x in dom f by XBOOLE_0:3;
let y be object;
assume
A31: y in product p;
A32: product p c= Funcs(dom p, Union p) by FUNCT_6:1;
then
A33: ex f being Function st x = f & dom f = dom p & rng f c= Union p by A29,
FUNCT_2:def 2;
A34: ex f being Function st y = f & dom f = dom p & rng f c= Union p by A31,A32
,FUNCT_2:def 2;
reconsider x, z = y as Function by A29,A31;
A35: dom p = Seg len p by FINSEQ_1:def 3;
then reconsider x, z as FinSequence by A33,A34,FINSEQ_1:def 2;
defpred P[set] means $1 in dom f;
defpred R[set,set] means [$1,$2] in LimDomRel A;
len x = len p by A33,A35,FINSEQ_1:def 3;
then
A36: len x = len z by A34,A35,FINSEQ_1:def 3;
A37: P[x] by A30;
A38: for p1,q1 being FinSequence, z1,z2 being set
st P[p1^<*z1*>^q1] & R[z1,z2] holds P[p1^<*z2*>^q1]
proof
let p1,q1 be FinSequence, z1,z2 be set;
assume that
A39: p1^<*z1*>^q1 in dom f and
A40: [z1,z2] in LimDomRel A;
A41: LimDomRel A c= DomRel A by Th21;
A42: z1 in the carrier of A by A40,ZFMISC_1:87;
z2 in the carrier of A by A40,ZFMISC_1:87;
hence thesis by A39,A40,A41,A42,Def4;
end;
A43: for i being Element of NAT st i in dom x holds R[x.i, z.i]
proof
let i be Element of NAT;
assume
A44: i in dom x;
then p.i in rng p by A33,FUNCT_1:def 3;
then reconsider a = p.i as Element of P;
A45: ex g being Function st x = g & dom g = dom p &
for x being object st x in
dom p holds g.x in p.x by A29,CARD_3:def 5;
A46: ex g being Function st z = g & dom g = dom p &
for x being object st x in
dom p holds g.x in p.x by A31,CARD_3:def 5;
A47: ex b being object st b in the carrier of A & a = Class(LimDomRel A, b)
by EQREL_1:def 3;
A48: x.i in a by A44,A45;
z.i in a by A44,A45,A46;
hence thesis by A47,A48,EQREL_1:22;
end;
P[z] from FiniteTransitivity(A37,A36,A38,A43);
hence thesis;
end;
definition
let A be partial non-empty UAStr;
mode a_partition of A -> a_partition of the carrier of A means
:
Def10: for f being operation of A holds f is_exactly_partitable_wrt it;
existence
proof
for f being operation of A holds
f is_exactly_partitable_wrt Class LimDomRel A by Th23;
hence thesis;
end;
end;
definition
let A be partial non-empty UAStr;
mode IndexedPartition of A -> IndexedPartition of the carrier of A means
:
Def11: rng it is a_partition of A;
existence
proof set P = the a_partition of A;
take id P;
thus thesis;
end;
end;
definition
let A be partial non-empty UAStr;
let P be IndexedPartition of A;
redefine func rng P -> a_partition of A; :: redefines rng (FUNCT_1, redefinition) → rng (RELAT_1, synonym) → proj2 (XTUPLE_0, definition)
coherence by Def11;
end;
theorem
for A being non-empty partial UAStr holds
Class LimDomRel A is a_partition of A
proof
let A be partial non-empty UAStr;
thus for f being operation of A holds
f is_exactly_partitable_wrt Class LimDomRel A by Th23;
end;
theorem Th25:
for X being non empty set, P being a_partition of X
for p being FinSequence of P, q1,q2 being FinSequence, x,y being set
st q1^<*x*>^q2 in product p & ex a being Element of P st x in a & y in a
holds q1^<*y*>^q2 in product p
proof
let X be non empty set, P be a_partition of X;
let pp be FinSequence of P;
let p,q be FinSequence;
let x,y be set;
assume
A1: p^<*x*>^q in product pp;
given a being Element of P such that
A2: x in a and
A3: y in a;
reconsider x,y as Element of a by A2,A3;
now
A4: ex g being Function st p^<*x*>^q = g & dom g = dom pp &
for x being object st x in dom pp holds g.x in pp.x by A1,CARD_3:def 5;
thus dom (p^<*y*>^q) = Seg len (p^<*y*>^q) by FINSEQ_1:def 3
.= Seg (len (p^<*y*>)+len q) by FINSEQ_1:22
.= Seg ((len p+len <*y*>)+len q) by FINSEQ_1:22
.= Seg ((len p+1)+len q) by FINSEQ_1:40
.= Seg ((len p+len <*x*>)+len q) by FINSEQ_1:40
.= Seg (len (p^<*x*>)+len q) by FINSEQ_1:22
.= Seg len (p^<*x*>^q) by FINSEQ_1:22
.= dom pp by A4,FINSEQ_1:def 3;
let i be object;
assume
A5: i in dom pp;
then reconsider ii = i as Element of NAT;
A6: len <*x*> = 1 by FINSEQ_1:40;
A7: len <*y*> = 1 by FINSEQ_1:40;
A8: dom <*x*> = Seg 1 by FINSEQ_1:38;
A9: len (p^<*x*>) = len p+1 by A6,FINSEQ_1:22;
A10: len (p^<*y*>) = len p+1 by A7,FINSEQ_1:22;
A11: dom (p^<*x*>) = Seg (len p+1) by A9,FINSEQ_1:def 3;
A12: dom (p^<*y*>) = Seg (len p+1) by A10,FINSEQ_1:def 3;
A13: ii
in dom (p^<*x*>) or ex n being Nat st n in dom q & ii = len (p^<*x*>)+n
by A4,A5,FINSEQ_1:25;
A14: dom p c= dom (p^<*y*>) by FINSEQ_1:26;
per cases by A13,FINSEQ_1:25;
suppose
A15: ii in dom p;
then
A16: (p^<*y*>).i = p.i by FINSEQ_1:def 7;
A17: (p^<*x*>).i = p.i by A15,FINSEQ_1:def 7;
A18: (p^<*y*>^q).i = p.i by A14,A15,A16,FINSEQ_1:def 7;
(p^<*x*>^q).i = p.i by A11,A12,A14,A15,A17,FINSEQ_1:def 7;
hence (p^<*y*>^q).i in pp.i by A4,A5,A18;
end;
suppose ex n being Nat st n in dom <*x*> & ii = len p+n;
then consider n being Nat such that
A19: n in Seg 1 and
A20: ii = len p+n by A8;
A21: n = 1 by A19,FINSEQ_1:2,TARSKI:def 1;
then
A22: (p^<*x*>).ii = x by A20,FINSEQ_1:42;
A23: (p^<*y*>).ii = y by A20,A21,FINSEQ_1:42;
A24: ii in dom (p^<*y*>) by A12,A20,A21,FINSEQ_1:4;
then
A25: (p^<*x*>^q).ii = x by A11,A12,A22,FINSEQ_1:def 7;
A26: (p^<*y*>^q).ii = y by A23,A24,FINSEQ_1:def 7;
A27: x in pp.i by A4,A5,A25;
pp.i in rng pp by A5,FUNCT_1:def 3;
then
A28: pp.i in P;
a meets pp.i by A27,XBOOLE_0:3;
then pp.i = a by A28,EQREL_1:def 4;
hence (p^<*y*>^q).i in pp.i by A26;
end;
suppose
ex n being Element of NAT st n in dom q & ii = len (p^<*x*>)+n;
then consider n being Element of NAT such that
A29: n in dom q and
A30: ii = len (p^<*x*>)+n;
A31: (p^<*y*>^q).i = q.n by A9,A10,A29,A30,FINSEQ_1:def 7;
(p^<*x*>^q).i = q.n by A29,A30,FINSEQ_1:def 7;
hence (p^<*y*>^q).i in pp.i by A4,A5,A31;
end;
end;
hence thesis by CARD_3:def 5;
end;
theorem Th26:
for A being partial non-empty UAStr, P being a_partition of A holds
P is_finer_than Class LimDomRel A
proof
let A be partial non-empty UAStr;
let P be a_partition of A;
consider EP being Equivalence_Relation of the carrier of A such that
A1: P = Class EP by EQREL_1:34;
let a be set;
assume a in P;
then reconsider aa = a as Element of P;
set x = the Element of aa;
take Class(LimDomRel A, x);
thus Class(LimDomRel A, x) in Class LimDomRel A by EQREL_1:def 3;
let y be object;
assume y in a;
then reconsider y as Element of aa;
reconsider x,y as Element of A;
defpred P[Nat] means EP c= (DomRel A)|^(A,$1);
A2: P[ 0 ]
proof
let x,y be object;
assume
A3: [x,y] in EP;
then reconsider x,y as Element of A by ZFMISC_1:87;
reconsider a = Class(EP, y) as Element of P by A1,EQREL_1:def 3;
A4: x in a by A3,EQREL_1:19;
A5: y in a by EQREL_1:20;
for f being operation of A, p,q being FinSequence holds
p^<*x*>^q in dom f iff p^<*y*>^q in dom f
proof
let f be operation of A, p,q be FinSequence;
A6: f is_exactly_partitable_wrt P by Def10;
now
let p,q be FinSequence, x,y be Element of a;
assume
A7: p^<*x*>^q in dom f;
then p^<*x*>^q is FinSequence of the carrier of A by FINSEQ_1:def 11;
then consider pp being FinSequence of P such that
A8: p^<*x*>^q in product pp by Th6;
product pp meets dom f by A7,A8,XBOOLE_0:3;
then
A9: product pp c= dom f by A6;
p^<*y*>^q in product pp by A8,Th25;
hence p^<*y*>^q in dom f by A9;
end;
hence thesis by A4,A5;
end;
then [x,y] in DomRel A by Def4;
hence thesis by Th15;
end;
A10: for i being Nat st P[i] holds P[i+1]
proof
let i be Nat;
assume
A11: EP c= (DomRel A)|^(A,i);
let x,y be object;
assume
A12: [x,y] in EP;
then reconsider x,y as Element of A by ZFMISC_1:87;
reconsider a = Class(EP, y) as Element of P by A1,EQREL_1:def 3;
now
let f be operation of A, p,q be FinSequence;
assume that
A13: p^<*x*>^q in dom f and
A14: p^<*y*>^q in dom f;
p^<*x*>^q is FinSequence of the carrier of A by A13,FINSEQ_1:def 11;
then consider pp being FinSequence of P such that
A15: p^<*x*>^q in product pp by Th6;
f is_exactly_partitable_wrt P by Def10;
then f is_partitable_wrt P;
then consider c being Element of P such that
A16: f.:product pp c= c;
A17: x in a by A12,EQREL_1:19;
y in a by EQREL_1:20;
then
A18: p^<*y*>^q in product pp by A15,A17,Th25;
A19: f.(p^<*x*>^q) in f.:product pp by A13,A15,FUNCT_1:def 6;
A20: f.(p^<*y*>^q) in f.:product pp by A14,A18,FUNCT_1:def 6;
ex x being object st x in the carrier of A & c = Class(EP,x) by A1,
EQREL_1:def 3;
then [f.(p^<*x*>^q), f.(p^<*y*>^q)] in EP by A16,A19,A20,EQREL_1:22;
hence [f.(p^<*x*>^q), f.(p^<*y*>^q)] in (DomRel A)|^(A,i) by A11;
end;
then [x,y] in (DomRel A)|^(A,i)|^A by A11,A12,Def5;
hence thesis by Th16;
end;
A21: for i being Nat holds P[i] from NAT_1:sch 2(A2,A10);
now
let i be Element of NAT;
ex x being object st x in the carrier of A & aa = Class(EP, x)
by A1,EQREL_1:def 3;
then
A22: [x,y] in EP by EQREL_1:22;
EP c= (DomRel A)|^(A,i) by A21;
hence [x,y] in (DomRel A)|^(A,i) by A22;
end;
then [x,y] in LimDomRel A by Def7;
then [y,x] in LimDomRel A by EQREL_1:6;
hence thesis by EQREL_1:19;
end;
begin :: Morphisms between manysorted signatures
definition
let S1,S2 be ManySortedSign;
let f,g be Function;
pred f,g form_morphism_between S1,S2 means
dom f = the carrier of S1 & dom g = the carrier' of S1 &
rng f c= the carrier of S2 & rng g c= the carrier' of S2 &
f*the ResultSort of S1 = (the ResultSort of S2)*g &
for o being set, p being Function
st o in the carrier' of S1 & p = (the Arity of S1).o
holds f*p = (the Arity of S2).(g.o);
end;
theorem Th27:
for S being non void non empty ManySortedSign holds
id the carrier of S, id the carrier' of S form_morphism_between S,S
proof
let S be non void non empty ManySortedSign;
set f = id the carrier of S, g = id the carrier' of S;
A1: dom the ResultSort of S = the carrier' of S by FUNCT_2:def 1;
rng the ResultSort of S c= the carrier of S;
then f*the ResultSort of S = the ResultSort of S by RELAT_1:53;
hence dom f = the carrier of S & dom g = the carrier' of S &
rng f c= the carrier of S & rng g c= the carrier' of S &
f*the ResultSort of S = (the ResultSort of S)*g by A1,RELAT_1:52;
let o be set, p be Function;
assume that
A2: o in the carrier' of S and
A3: p = (the Arity of S).o;
A4: g.o = o by A2,FUNCT_1:17;
p in (the carrier of S)* by A2,A3,FUNCT_2:5;
then p is FinSequence of the carrier of S by FINSEQ_1:def 11;
then rng p c= the carrier of S by FINSEQ_1:def 4;
hence thesis by A3,A4,RELAT_1:53;
end;
theorem Th28:
for S1,S2,S3 being ManySortedSign for f1,f2, g1,g2 being Function st
f1, g1 form_morphism_between S1,S2 & f2, g2 form_morphism_between S2,S3
holds f2*f1, g2*g1 form_morphism_between S1,S3
proof
let S1,S2,S3 be ManySortedSign;
let f1,f2, g1,g2 be Function such that
A1: dom f1 = the carrier of S1 and
A2: dom g1 = the carrier' of S1 and
A3: rng f1 c= the carrier of S2 and
A4: rng g1 c= the carrier' of S2 and
A5: f1*the ResultSort of S1 = (the ResultSort of S2)*g1 and
A6: 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 S2).(g1.o) and
A7: dom f2 = the carrier of S2 and
A8: dom g2 = the carrier' of S2 and
A9: rng f2 c= the carrier of S3 and
A10: rng g2 c= the carrier' of S3 and
A11: f2*the ResultSort of S2 = (the ResultSort of S3)*g2 and
A12: 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 S3).(g2.o);
set f = f2*f1, g = g2*g1;
thus dom f = the carrier of S1 & dom g = the carrier' of S1
by A1,A2,A3,A4,A7,A8,RELAT_1:27;
A13: rng f c= rng f2 by RELAT_1:26;
rng g c= rng g2 by RELAT_1:26;
hence rng f c= the carrier of S3 & rng g c= the carrier' of S3
by A9,A10,A13;
thus f*the ResultSort of S1 = f2*((the ResultSort of S2)*g1) by A5,RELAT_1:36
.= f2*(the ResultSort of S2)*g1 by RELAT_1:36
.= (the ResultSort of S3)*g by A11,RELAT_1:36;
let o be set, p be Function;
assume that
A14: o in the carrier' of S1 and
A15: p = (the Arity of S1).o;
A16: f1*p = (the Arity of S2).(g1.o) by A6,A14,A15;
A17: g1.o in rng g1 by A2,A14,FUNCT_1:def 3;
A18: f*p = f2*(f1*p) by RELAT_1:36;
g.o = g2.(g1.o) by A2,A14,FUNCT_1:13;
hence thesis by A4,A12,A16,A17,A18;
end;
definition
let S1,S2 be ManySortedSign;
pred S1 is_rougher_than S2 means
ex f,g being Function st f,g form_morphism_between S2,S1 &
rng f = the carrier of S1 & rng g = the carrier' of S1;
end;
definition
let S1,S2 be non void non empty ManySortedSign;
redefine pred S1 is_rougher_than S2; :: redefines is_rougher_than (PUA2MSS1, definition)
reflexivity
proof
let S be non void non empty ManySortedSign;
take f = id the carrier of S, g = id the carrier' of S;
thus f,g form_morphism_between S,S &
rng f = the carrier of S & rng g = the carrier' of S
by Th27;
end;
end;
theorem
for S1,S2,S3 being ManySortedSign
st S1 is_rougher_than S2 & S2 is_rougher_than S3 holds S1 is_rougher_than S3
proof
let S1,S2,S3 be ManySortedSign;
given f1,g1 being Function such that
A1: f1,g1 form_morphism_between S2,S1 and
A2: rng f1 = the carrier of S1 and
A3: rng g1 = the carrier' of S1;
given f2,g2 being Function such that
A4: f2,g2 form_morphism_between S3,S2 and
A5: rng f2 = the carrier of S2 and
A6: rng g2 = the carrier' of S2;
take f = f1*f2, g = g1*g2;
thus f,g form_morphism_between S3,S1 by A1,A4,Th28;
A7: dom f1 = the carrier of S2 by A1;
dom g1 = the carrier' of S2 by A1;
hence thesis by A2,A3,A5,A6,A7,RELAT_1:28;
end;
begin :: Manysorted signature of partital algebra
definition
let A be partial non-empty UAStr;
let P be a_partition of A;
func MSSign(A,P) -> strict ManySortedSign means
:
Def14: the carrier of it = P & the carrier' of it =
{[o,p] where o is OperSymbol of A, p is Element of P*:
product p meets dom Den(o,A)} &
for o being OperSymbol of A, p being Element of P*
st product p meets dom Den(o,A) holds (the Arity of it).[o,p] = p &
Den(o, A).:product p c= (the ResultSort of it).[o,p];
existence
proof
set O = {[f,p] where f is OperSymbol of A, p is Element of P*:
product p meets dom Den(f, A)};
defpred Q[object,object] means
ex f being OperSymbol of A, q being Element of P* st q = $2 & $1 = [f,q];
A1: for o being object st o in O ex p being object st p in P* & Q[o,p]
proof
let o be object;
assume o in O;
then consider f being OperSymbol of A, p being Element of P* such that
A2: o = [f,p] and product p meets dom Den(f,A);
take p;
thus thesis by A2;
end;
defpred S[object,object] means
ex D2 being set, f being OperSymbol of A, p being Element of P*
st D2 = $2 & $1 = [f,p] & Den(f,A).:product p c= D2;
A3: for o being object st o in O ex r being object st r in P & S[o,r]
proof
let o be object;
assume o in O;
then consider f being OperSymbol of A, p being Element of P* such that
A4: o = [f,p] and product p meets dom Den(f,A);
Den(f,A) is_exactly_partitable_wrt P by Def10;
then Den(f,A) is_partitable_wrt P;
then ex a being Element of P st Den(f,A).:product p c= a;
hence thesis by A4;
end;
consider Ar being Function such that
A5: dom Ar = O & rng Ar c= P* and
A6: for o being object st o in O holds Q[o,Ar.o] from FUNCT_1:sch 6(A1);
reconsider Ar as Function of O, P* by A5,FUNCT_2:2;
consider R being Function such that
A7: dom R = O & rng R c= P and
A8: for o being object st o in O holds S[o,R.o] from FUNCT_1:sch 6(A3);
reconsider R as Function of O, P by A7,FUNCT_2:2;
take S = ManySortedSign(#P, O, Ar, R#);
thus the carrier of S = P & the carrier' of S = O;
let f be OperSymbol of A, p be Element of P*;
set o = [f, p];
assume product p meets dom Den(f, A);
then
A9: o in O;
then
A10: ex f1 being OperSymbol of A, q1 being Element of P* st ( q1
= Ar.o)&( o = [f1,q1]) by A6;
S[o,R.o] by A8,A9;
then consider f2 being OperSymbol of A, q2 being Element of P* such that
A11: o = [f2,q2] and
A12: Den(f2,A).:product q2 c= R.o;
q2 = p by A11,XTUPLE_0:1;
hence thesis by A10,A11,A12,XTUPLE_0:1;
end;
correctness
proof
set O = {[f,p] where f is OperSymbol of A, p is Element of P*:
product p meets dom Den(f,A)};
let S1, S2 be strict ManySortedSign such that
A13: the carrier of S1 = P and
A14: the carrier' of S1 = O and
A15: for f being OperSymbol of A, p being Element of P*
st product p meets dom Den(f,A) holds (the Arity of S1).[f,p] = p &
Den(f,A).:product p c= (the ResultSort of S1).[f,p] and
A16: the carrier of S2 = P and
A17: the carrier' of S2 = O and
A18: for f being OperSymbol of A, p being Element of P*
st product p meets dom Den(f,A) holds (the Arity of S2).[f,p] = p &
Den(f,A).:product p c= (the ResultSort of S2).[f,p];
A19: dom the Arity of S1 = O by A14,FUNCT_2:def 1;
A20: dom the Arity of S2 = O by A17,FUNCT_2:def 1;
now
let o be object;
assume o in O;
then consider f being OperSymbol of A, p being Element of P* such that
A21: o = [f,p] and
A22: product p meets dom Den(f,A);
thus (the Arity of S1).o = p by A15,A21,A22
.= (the Arity of S2).o by A18,A21,A22;
end;
then
A23: the Arity of S1 = the Arity of S2 by A19,A20;
A24: dom the ResultSort of S1 = O by A13,A14,FUNCT_2:def 1;
A25: dom the ResultSort of S2 = O by A16,A17,FUNCT_2:def 1;
consider R being Equivalence_Relation of the carrier of A such that
A26: P = Class R by EQREL_1:34;
now
let o be object;
assume
A27: o in O;
then consider f being OperSymbol of A, p being Element of P* such that
A28: o = [f,p] and
A29: product p meets dom Den(f,A);
consider x being object such that
A30: x in product p and
A31: x in dom Den(f,A) by A29,XBOOLE_0:3;
A32: Den(f,A).x in Den(f,A).:product p by A30,A31,FUNCT_1:def 6;
A33: Den(f,A).:product p c= (the ResultSort of S1).o by A15,A28,A29;
A34: Den(f,A).:product p c= (the ResultSort of S2).o by A18,A28,A29;
A35: (the ResultSort of S1).o in P by A13,A14,A27,FUNCT_2:5;
A36: (the ResultSort of S2).o in P by A16,A17,A27,FUNCT_2:5;
A37: ex y being object
st y in the carrier of A & (the ResultSort of S1).o =
Class(R,y) by A26,A35,EQREL_1:def 3;
A38: ex y being object
st y in the carrier of A & (the ResultSort of S2).o =
Class(R,y) by A26,A36,EQREL_1:def 3;
(the ResultSort of S1).o = Class(R,Den(f,A).x) by A32,A33,A37,EQREL_1:23;
hence (the ResultSort of S1).o = (the ResultSort of S2).o by A32,A34,A38,
EQREL_1:23;
end;
hence thesis by A13,A14,A16,A17,A23,A24,A25,FUNCT_1:2;
end;
end;
registration
let A be partial non-empty UAStr;
let P be a_partition of A;
cluster MSSign(A,P) -> non empty non void;
coherence
proof
thus the carrier of MSSign(A,P) is non empty by Def14;
set g = the OperSymbol of A;
set x = the Element of dom Den(g,A);
reconsider x as Element of (the carrier of A)*;
A1: union P = the carrier of A by EQREL_1:def 4;
rng x c= the carrier of A;
then consider q being Function such that
A2: dom q = dom x and
A3: rng q c= P and
A4: x in product q by A1,Th5;
dom x = Seg len x by FINSEQ_1:def 3;
then reconsider q as FinSequence by A2,FINSEQ_1:def 2;
reconsider q as FinSequence of P by A3,FINSEQ_1:def 4;
reconsider q as Element of P* by FINSEQ_1:def 11;
A5: product q meets dom Den(g, A) by A4,XBOOLE_0:3;
the carrier' of MSSign(A,P) = {[f,p] where f is OperSymbol of A, p is
Element of P*: product p meets dom Den(f,A)} by Def14;
then [g,q] in the carrier' of MSSign(A,P) by A5;
hence the carrier' of MSSign(A,P) is non empty;
end;
end;
definition
let A be partial non-empty UAStr;
let P be a_partition of A;
let o be OperSymbol of MSSign(A,P);
redefine func o`1 -> OperSymbol of A; :: redefines `1 (XTUPLE_0, definition)
coherence
proof
A1: o in the carrier' of MSSign(A,P);
the carrier' of MSSign(A,P) = {[f,p] where f is OperSymbol of A, p is
Element of P*: product p meets dom Den(f, A)} by Def14;
then ex f being OperSymbol of A, p being Element of P* st
o = [f,p] & product p meets dom Den(f, A) by A1;
hence thesis;
end;
redefine func o`2 -> Element of P*; :: redefines `2 (XTUPLE_0, definition)
coherence
proof
A2: o in the carrier' of MSSign(A,P);
the carrier' of MSSign(A,P) = {[f,p] where f is OperSymbol of A, p is
Element of P*: product p meets dom Den(f,A)} by Def14;
then ex f being OperSymbol of A, p being Element of P* st
o = [f,p] & product p meets dom Den(f,A) by A2;
hence thesis;
end;
end;
definition
let A be partial non-empty UAStr;
let S be non void non empty ManySortedSign;
let G be MSAlgebra over S;
let P be IndexedPartition of the carrier' of S;
pred A can_be_characterized_by S,G,P means
the Sorts of G is IndexedPartition of A &
dom P = dom the charact of A & for o being OperSymbol of A holds
(the Charact of G)|(P.o) is IndexedPartition of Den(o, A);
end;
definition
let A be partial non-empty UAStr;
let S be non void non empty ManySortedSign;
pred A can_be_characterized_by S means
ex G being MSAlgebra over S, P being IndexedPartition of the carrier' of S st
A can_be_characterized_by S,G,P;
end;
theorem
for A being partial non-empty UAStr, P being a_partition of A
holds A can_be_characterized_by MSSign(A, P)
proof
let A be partial non-empty UAStr;
let P be a_partition of A;
set S = MSSign(A, P);
P = the carrier of S by Def14;
then reconsider Z = id P as ManySortedSet of the carrier of S;
deffunc F1(OperSymbol of S) = Den($1`1, A)|product $1`2;
consider D being ManySortedSet of the carrier' of S such that
A1: for o being OperSymbol of S holds D.o = F1(o) from PBOOLE:sch 5;
deffunc F2(OperSymbol of A) = {a where a is OperSymbol of S: a`1 = $1};
consider Q being ManySortedSet of dom the charact of A such that
A2: for o being OperSymbol of A holds Q.o = F2(o) from PBOOLE:sch 5;
A3: dom Q = dom the charact of A by PARTFUN1:def 2;
A4: the carrier of S = P by Def14;
A5: the carrier' of S = {[o,p] where o is OperSymbol of A, p is Element of P
*: product p meets dom Den(o,A)} by Def14;
Q is non-empty
proof
let x be object;
assume x in dom Q;
then reconsider o = x as OperSymbol of A;
set y = the Element of dom Den(o,A);
reconsider y as Element of (the carrier of A)*;
A6: rng y c= the carrier of A;
the carrier of A = union P by EQREL_1:def 4;
then consider f being Function such that
A7: dom f = dom y and
A8: rng f c= P and
A9: y in product f by A6,Th5;
dom y = Seg len y by FINSEQ_1:def 3;
then f is FinSequence by A7,FINSEQ_1:def 2;
then f is FinSequence of P by A8,FINSEQ_1:def 4;
then reconsider f as Element of P* by FINSEQ_1:def 11;
product f meets dom Den(o,A) by A9,XBOOLE_0:3;
then
A10: [o,f] in the carrier' of S by A5;
A11: [o,f]`1 = o;
Q.o = {a where a is OperSymbol of S: a`1 = o} by A2;
then [o,f] in Q.x by A10,A11;
hence thesis;
end;
then reconsider Q as non-empty Function;
D is ManySortedFunction of Z# * the Arity of S, Z * the ResultSort of S
proof
let x be object;
assume
A12: x in the carrier' of S;
then consider o being OperSymbol of A, p being Element of P* such that
A13: x = [o,p] and
A14: product p meets dom Den(o,A) by A5;
reconsider xx = x as OperSymbol of S by A12;
A15: rng the ResultSort of S c= the carrier of S;
A16: dom the Arity of S = the carrier' of S by FUNCT_2:def 1;
A17: rng p c= P;
A18: (the Arity of S).x = p by A13,A14,Def14;
A19: (Z# ).p = product(Z*p) by A4,FINSEQ_2:def 5;
Z*p = p by A17,RELAT_1:53;
then
A20: (Z# * the Arity of S).x = product p by A12,A16,A18,A19,FUNCT_1:13;
A21: Den(o, A).:product p c= (the ResultSort of S).x by A13,A14,Def14;
A22: xx`2 = p by A13;
A23: xx`1 = o by A13;
A24: rng (Den(o, A)|product p) = Den(o, A).:product p by RELAT_1:115;
A25: D.xx = Den(o, A)|product p by A1,A22,A23;
Den(o,A) is_exactly_partitable_wrt P by Def10;
then
A26: product p c= dom Den(o,A) by A14;
A27: Z * the ResultSort of S = the ResultSort of S by A4,A15,RELAT_1:53;
dom (Den(o, A)|product p) = product p by A26,RELAT_1:62;
hence thesis by A20,A21,A24,A25,A27,FUNCT_2:2;
end;
then reconsider D as ManySortedFunction of
Z# * the Arity of S, Z * the ResultSort of S;
A28: Union Q = the carrier' of S
proof
hereby
let x be object;
assume x in Union Q;
then consider y being object such that
A29: y in dom Q and
A30: x in Q.y by CARD_5:2;
reconsider y as OperSymbol of A by A29,PARTFUN1:def 2;
Q.y = {a where a is OperSymbol of S: a`1 = y} by A2;
then ex a being OperSymbol of S st x = a & a`1 = y by A30;
hence x in the carrier' of S;
end;
let x be object;
assume x in the carrier' of S;
then reconsider b = x as OperSymbol of S;
Q.b`1 = {a where a is OperSymbol of S: a`1 = b`1} by A2;
then b in Q.b`1;
hence thesis by A3,CARD_5:2;
end;
now
let x,y be set;
assume that
A31: x in dom Q and
A32: y in dom Q and
A33: x <> y;
reconsider a = x, b = y as OperSymbol of A by A31,A32,PARTFUN1:def 2;
thus Q.x misses Q.y
proof
assume Q.x meets Q.y;
then consider z being object such that
A34: z in Q.x and
A35: z in Q.y by XBOOLE_0:3;
A36: Q.a = {c where c is OperSymbol of S: c`1 = a} by A2;
A37: Q.b = {c where c is OperSymbol of S: c`1 = b} by A2;
A38: ex c1 being OperSymbol of S st z = c1 & c1`1 = a by A34,A36;
ex c2 being OperSymbol of S st z = c2 & c2`1 = b by A35,A37;
hence contradiction by A33,A38;
end;
end;
then reconsider Q as IndexedPartition of the carrier' of S by A28,Th13;
take G = MSAlgebra(#Z, D#), Q;
rng id P is a_partition of A;
hence the Sorts of G is IndexedPartition of A by Def11;
thus dom Q = dom the charact of A by PARTFUN1:def 2;
let o be OperSymbol of A;
reconsider PP = the set of all product p where p is Element of P*
as a_partition of (the carrier of A)* by Th8;
reconsider QQ = {a /\ dom Den(o,A) where a is Element of PP:
a meets dom Den(o,A)} as a_partition of dom Den(o,A) by Th10;
set F = (the Charact of G)|(Q.o);
A39: Q.o in rng Q by A3,FUNCT_1:def 3;
A40: dom D = the carrier' of S by PARTFUN1:def 2;
then
A41: dom F = Q.o by A39,RELAT_1:62;
reconsider F as non empty Function by A39,A40;
reconsider Qo = Q.o as non empty set;
reconsider RR = the set of all Den(o,A)|a where a is Element of QQ
as a_partition of Den(o,A) by Th11;
A42: Q.o = {a where a is OperSymbol of S: a`1 = o} by A2;
rng F c= RR
proof
let y be object;
assume y in rng F;
then consider x be object such that
A43: x in dom F and
A44: y = F.x by FUNCT_1:def 3;
x in dom (the Charact of G) /\ (Q.o) by A43,RELAT_1:61;
then x in Q.o by XBOOLE_0:def 4;
then consider a being OperSymbol of S such that
A45: x = a and
A46: a`1 = o by A42;
a in the carrier' of S;
then consider s being OperSymbol of A, p being Element of P* such that
A47: a = [s,p] and
A48: product p meets dom Den(s,A) by A5;
A49: s = o by A46,A47;
A50: a`2 = p by A47;
A51: product p in PP;
A52: Den(o,A) is_exactly_partitable_wrt P by Def10;
A53: (product p) /\ dom Den(o,A) in QQ by A48,A49,A51;
product p c= dom Den(o,A) by A48,A49,A52;
then product p in QQ by A53,XBOOLE_1:28;
then
A54: Den(o,A)|product p in RR;
y = D.a by A43,A44,A45,FUNCT_1:47;
hence thesis by A1,A46,A50,A54;
end;
then reconsider F as Function of Qo, RR by A41,FUNCT_2:2;
A55: RR c= rng F
proof
let x be object;
assume x in RR;
then consider a being Element of QQ such that
A56: x = Den(o,A)|a;
a in QQ;
then consider b being Element of PP such that
A57: a = b /\ dom Den(o,A) and
A58: b meets dom Den(o,A);
b in PP;
then consider p being Element of P* such that
A59: b = product p;
Den(o,A) is_exactly_partitable_wrt P by Def10;
then product p c= dom Den(o,A) by A58,A59;
then
A60: b = a by A57,A59,XBOOLE_1:28;
A61: [o,p] in the carrier' of S by A5,A58,A59;
A62: [o,p]`1 = o;
A63: [o,p]`2 = p;
A64: [o,p] in dom D by A61,PARTFUN1:def 2;
A65: [o,p] in Q.o by A42,A61,A62;
D.[o,p] = x by A1,A56,A59,A60,A61,A62,A63;
hence thesis by A64,A65,FUNCT_1:50;
end;
F is one-to-one
proof
let x1,x2 be object;
assume that
A66: x1 in dom F and
A67: x2 in dom F and
A68: F.x1 = F.x2;
consider a1 being OperSymbol of S such that
A69: x1 = a1 and
A70: a1`1 = o by A41,A42,A66;
consider a2 being OperSymbol of S such that
A71: x2 = a2 and
A72: a2`1 = o by A41,A42,A67;
a1 in the carrier' of S;
then consider o1 being OperSymbol of A, p1 being Element of P* such that
A73: a1 = [o1,p1] and
A74: product p1 meets dom Den(o1,A) by A5;
a2 in the carrier' of S;
then consider o2 being OperSymbol of A, p2 being Element of P* such that
A75: a2 = [o2,p2] and
A76: product p2 meets dom Den(o2,A) by A5;
A77: F.x1 = D.a1 by A66,A69,FUNCT_1:47;
A78: F.x1 = D.a2 by A67,A68,A71,FUNCT_1:47;
A79: a1`2 = p1 by A73;
A80: a2`2 = p2 by A75;
A81: F.x1 = Den(o,A)|product p1 by A1,A70,A77,A79;
A82: F.x1 = Den(o,A)|product p2 by A1,A72,A78,A80;
A83: Den(o,A) is_exactly_partitable_wrt P by Def10;
A84: o = o1 by A70,A73;
A85: o = o2 by A72,A75;
A86: product p1 c= dom Den(o,A) by A74,A83,A84;
A87: product p2 c= dom Den(o,A) by A76,A83,A85;
product p1 = dom (Den(o,A)|product p1) by A86,RELAT_1:62;
hence thesis by A69,A71,A73,A75,A81,A82,A84,A85,A87,Th2,RELAT_1:62;
end;
hence thesis by A55,Th14;
end;
theorem Th31:
for A being partial non-empty UAStr
for S being non void non empty ManySortedSign for G being MSAlgebra over S
for Q being IndexedPartition of the carrier' of S
st A can_be_characterized_by S,G,Q
for o being OperSymbol of A, r being FinSequence of rng the Sorts of G
st product r c= dom Den(o,A) ex s being OperSymbol of S st
(the Sorts of G)*the_arity_of s = r & s in Q.o
proof
let A be partial non-empty UAStr;
let S2 be non void non empty ManySortedSign;
let G be MSAlgebra over S2,
Q be IndexedPartition of the carrier' of S2 such that
A1: the Sorts of G is IndexedPartition of A and
A2: dom Q = dom the charact of A and
A3: for o being OperSymbol of A holds
(the Charact of G)|(Q.o) is IndexedPartition of Den(o, A);
reconsider R = the Sorts of G as IndexedPartition of A by A1;
dom R = the carrier of S2 by PARTFUN1:def 2;
then reconsider SG = the Sorts of G as Function of the carrier of S2, rng R
by RELSET_1:4;
let o be OperSymbol of A, r be FinSequence of rng the Sorts of G;
reconsider p = r as Element of (rng R)* by FINSEQ_1:def 11;
assume
A4: product r c= dom Den(o,A);
reconsider P = (the Charact of G)|(Q.o) as IndexedPartition of Den(o, A)
by A3;
set h = the Element of product p;
h in product r;
then
A5: [h,Den(o,A).h] in Den(o, A) by A4,FUNCT_1:def 2;
then
A6: P-index_of [h,Den(o,A).h] in dom P by Def3;
A7: [h,Den(o,A).h] in P.(P-index_of [h,Den(o,A).h]) by A5,Def3;
reconsider Qo = Q.o as Element of rng Q by A2,FUNCT_1:def 3;
A8: dom the Charact of G = the carrier' of S2 by PARTFUN1:def 2;
then
A9: dom P = Qo by RELAT_1:62;
reconsider s = P-index_of [h,Den(o,A).h] as Element of Qo by A6,A8,RELAT_1:62;
reconsider q = SG*the_arity_of s as FinSequence of rng R by Lm2;
reconsider q as Element of (rng R)* by FINSEQ_1:def 11;
reconsider Q = the set of all product t where t is Element of (rng R)*
as a_partition of (the carrier of A)* by Th8;
take s;
dom the Arity of S2 = the carrier' of S2 by FUNCT_2:def 1;
then
A10: Args(s,G) = (the Sorts of G)# .((the Arity of S2).s) by FUNCT_1:13
.= product q by FINSEQ_2:def 5;
A11: product q in Q;
A12: product p in Q;
P.s = (the Charact of G).s by A9,FUNCT_1:47;
then h in dom Den(s,G) by A7,XTUPLE_0:def 12;
hence (the Sorts of G)*the_arity_of s = r by A10,A11,A12,Th2,Lm3;
thus thesis;
end;
theorem
for A being partial non-empty UAStr, P being a_partition of A
st P = Class LimDomRel A
for S being non void non empty ManySortedSign st A can_be_characterized_by S
holds MSSign(A,P) is_rougher_than S
proof
let A be partial non-empty UAStr, P be a_partition of A;
assume
A1: P = Class LimDomRel A;
set S1 = MSSign(A,P);
let S2 be non void non empty ManySortedSign;
given G being MSAlgebra over S2,
Q being IndexedPartition of the carrier' of S2 such that
A2: A can_be_characterized_by S2,G,Q;
A3: the Sorts of G is IndexedPartition of A by A2;
A4: dom Q = dom the charact of A by A2;
reconsider G as non-empty MSAlgebra over S2 by A3,MSUALG_1:def 3;
reconsider R = the Sorts of G as IndexedPartition of A by A2;
A5: dom R = the carrier of S2 by PARTFUN1:def 2;
then reconsider SG = the Sorts of G as Function of the carrier of S2, rng R
by RELSET_1:4;
A6: the carrier' of S1 = {[o,p] where o is OperSymbol of A, p is Element of P*:
product p meets dom Den(o,A)} by Def14;
A7: the carrier of S1 = P by Def14;
defpred Q[object,object] means
ex D1,D2 being set st D1 = $1 & D2 = $2 & D1 c= D2;
A8: rng R is_finer_than P by A1,Th26;
A9: for r being object st r in rng R ex p being object st p in P & Q[r,p]
proof let r be object;
assume
A10: r in rng R;
reconsider r as set by TARSKI:1;
ex p being set st p in P & r c= p by A10,A8;
hence thesis;
end;
consider em being Function such that
A11: dom em = rng R & rng em c= P and
A12: for r being object st r in rng R holds Q[r,em.r] from FUNCT_1:sch 6(A9);
reconsider em as Function of rng R, P by A11,FUNCT_2:2;
A13: for a being set st a in rng R holds a c= em.a
proof let a be set;
assume a in rng R;
then Q[a, em.a] by A12;
hence thesis;
end;
A14: dom (em*R) = dom R by A11,RELAT_1:27;
rng (em*R) = rng em by A11,RELAT_1:28;
then reconsider f = em*R as Function of the carrier of S2, the carrier of S1
by A5,A7,A14,FUNCT_2:2;
take f;
defpred S[object,object] means
ex p being FinSequence of P, o being OperSymbol of S2 st
$2 = [Q-index_of $1, p] & $1 = o & Args(o,G) c= product p;
A15: for s2 being object st s2 in the carrier' of S2
ex s1 being object st s1 in the carrier' of S1 & S[s2,s1]
proof
let s2 be object;
assume s2 in the carrier' of S2;
then reconsider s2 as OperSymbol of S2;
SG*the_arity_of s2 is FinSequence of rng R by Lm2;
then consider p being FinSequence of P such that
A16: product (SG*the_arity_of s2) c= product p by A1,Th3,Th26;
reconsider p as Element of P* by FINSEQ_1:def 11;
take s1 = [Q-index_of s2, p];
reconsider o = Q-index_of s2 as OperSymbol of A by A4,Def3;
set aa = the Element of Args(s2,G);
A17: aa in Args(s2,G);
A18: dom Den(s2,G) = Args(s2,G) by FUNCT_2:def 1;
A19: dom the Arity of S2 = the carrier' of S2 by PARTFUN1:def 2;
A20: dom the Charact of G = the carrier' of S2 by PARTFUN1:def 2;
(the Charact of G)|(Q.o) is IndexedPartition of Den(o, A) by A2;
then rng ((the Charact of G)|(Q.o)) is a_partition of Den(o, A) by Def2;
then
A21: (the Charact of G).:(Q.o) is a_partition of Den(o, A) by RELAT_1:115;
s2 in Q.o by Def3;
then (the Charact of G).s2 in (the Charact of G).:(Q.o) by A20,
FUNCT_1:def 6;
then
A22: dom Den(s2, G) c= dom Den(o, A) by A21,RELAT_1:11;
A23: Args(s2,G) = (the Sorts of G)# .((the Arity of S2).s2) by A19,FUNCT_1:13
.= product(SG*the_arity_of s2) by FINSEQ_2:def 5;
then product p meets dom Den(o,A) by A16,A17,A18,A22,XBOOLE_0:3;
hence s1 in the carrier' of S1 by A6;
take p, s2;
thus thesis by A16,A23;
end;
consider g being Function such that
A24: dom g = the carrier' of S2 & rng g c= the carrier' of S1 &
for s being object st s in the carrier' of S2 holds S[s,g.s]
from FUNCT_1:sch 6(A15);
reconsider g as Function of the carrier' of S2, the carrier' of S1
by A24,FUNCT_2:2;
take g;
thus
A25: dom f = the carrier of S2 & dom g = the carrier' of S2 &
rng f c= the carrier of S1 & rng g c= the carrier' of S1
by FUNCT_2:def 1;
now
let c be OperSymbol of S2;
set s = (the ResultSort of S2).c;
A26: R.s = ((the Sorts of G)*the ResultSort of S2).c by FUNCT_2:15;
A27: (f*the ResultSort of S2).c = f.s by FUNCT_2:15;
R.s in rng R by A5,FUNCT_1:def 3;
then Q[R.s,em.(R.s)] by A12;
then R.s c= em.(R.s);
then
A28: R.s c= f.s by A5,FUNCT_1:13;
consider p being FinSequence of P, o being OperSymbol of S2 such that
A29: g.c = [Q-index_of c, p] and
A30: c = o and
A31: Args(o,G) c= product p by A24;
reconsider p as Element of P* by FINSEQ_1:def 11;
reconsider s2 = Q-index_of c as OperSymbol of A by A4,Def3;
set aa = the Element of Args(o,G);
(the Charact of G)|(Q.s2) is IndexedPartition of Den(s2, A) by A2;
then
A32: rng ((the Charact of G)|(Q.s2)) is a_partition of Den(s2, A) by Def2;
A33: o in Q.s2 by A30,Def3;
A34: dom the Charact of G = the carrier' of S2 by PARTFUN1:def 2;
A35: (the Charact of G).:(Q.s2) is a_partition of Den(s2, A) by A32,RELAT_1:115
;
A36: (the Charact of G).o in (the Charact of G).:(Q.s2) by A33,A34,
FUNCT_1:def 6;
A37: dom Den(o,G) = Args(o,G) by FUNCT_2:def 1;
A38: dom Den(o,G) c= dom Den(s2,A) by A35,A36,RELAT_1:11;
aa in Args(o,G);
then product p meets dom Den(s2,A) by A31,A37,A38,XBOOLE_0:3;
then
A39: Den(s2, A).:product p c= (the ResultSort of S1).(g.c) by A29,Def14;
rng Den(c,G) = Den(c,G).:Args(c,G) by A30,A37,RELAT_1:113;
then
A40: rng Den(c,G) c= Den(c,G).:product p by A30,A31,RELAT_1:123;
Den(c,G).:product p c= Den(s2,A).: product p by A30,A35,A36,RELAT_1:124;
then rng Den(c,G) c= Den(s2,A).:product p by A40;
then
A41: rng Den(c,G) c= (the ResultSort of S1).(g.c) by A39;
A42: Den(c,G).aa in rng Den(c,G) by A30,A37,FUNCT_1:def 3;
then
A43: Den(c,G).aa in ((the Sorts of G)*the ResultSort of S2).c;
Den(c,G).aa in (the ResultSort of S1).(g.c) by A41,A42;
then Den(c,G).aa in ((the ResultSort of S1)*g).c by FUNCT_2:15;
hence (f*the ResultSort of S2).c = ((the ResultSort of S1)*g).c by A7,A26
,A27,A28,A43,Lm3;
end;
hence f*the ResultSort of S2 = (the ResultSort of S1)*g;
hereby
let o be set, p be Function;
assume o in the carrier' of S2;
then reconsider s = o as OperSymbol of S2;
assume
A44: p = (the Arity of S2).o;
reconsider q = (the Arity of S2).s as Element of (the carrier of S2)*;
reconsider r = SG*q as FinSequence of rng R by Lm2;
consider p9 being FinSequence of P, o9 being OperSymbol of S2 such that
A45: g.s = [Q-index_of s, p9] and
A46: s = o9 and
A47: Args(o9,G) c= product p9 by A24;
g.s in the carrier' of S1;
then consider o1 being OperSymbol of A, p1 being Element of P* such that
A48: g.s = [o1,p1] and
A49: product p1 meets dom Den(o1,A) by A6;
p9 = p1 by A45,A48,XTUPLE_0:1;
then
A50: (the Arity of S1).(g.o) = p9 by A48,A49,Def14;
Args(o9,G) = (the Sorts of G)# .q by A46,FUNCT_2:15
.= product r by FINSEQ_2:def 5;
then
A51: product r c= product p9 by A47;
em*r = p9 by Th4,A51,A13;
hence f*p = (the Arity of S1).(g.o) by A44,A50,RELAT_1:36;
end;
thus rng f c= the carrier of S1;
thus the carrier of S1 c= rng f
proof
let s be object;
assume s in the carrier of S1;
then reconsider s as Element of P by Def14;
set a = the Element of s;
A52: R-index_of a in dom R by Def3;
A53: a in R.(R-index_of a) by Def3;
A54: R.(R-index_of a) in rng R by A52,FUNCT_1:def 3;
A55: em.(R.(R-index_of a)) = f.(R-index_of a) by A52,FUNCT_1:13;
Q[R.(R-index_of a),em.(R.(R-index_of a))] by A12,A54;
then
A56: R.(R-index_of a) c= f.(R-index_of a) by A55;
A57: f.(R-index_of a) in rng f by A5,A25,A52,FUNCT_1:def 3;
rng f c= P by A25,Def14;
hence thesis by A53,A56,A57,Lm3;
end;
thus rng g c= the carrier' of S1;
thus the carrier' of S1 c= rng g
proof
let s1 be object;
assume s1 in the carrier' of S1;
then consider o being OperSymbol of A, p being Element of P* such that
A58: s1 = [o,p] and
A59: product p meets dom Den(o,A) by A6;
consider a being object such that
A60: a in product p and a in dom Den(o,A) by A59,XBOOLE_0:3;
consider h being Function such that
A61: a = h and
A62: dom h = dom p and
A63: for x being object st x in dom p holds h.x in p.x by A60,CARD_3:def 5;
reconsider h as FinSequence by A62,Lm1;
product p c= Funcs(dom p, Union p) by FUNCT_6:1;
then
A64: ex f being Function st h = f & dom f = dom p & rng f c= Union p by A60,A61
,FUNCT_2:def 2;
A65: Union p = union rng p by CARD_3:def 4;
A66: union rng p c= union P by ZFMISC_1:77;
union P = the carrier of A by EQREL_1:def 4;
then rng h c= the carrier of A by A64,A65,A66;
then h is FinSequence of the carrier of A by FINSEQ_1:def 4;
then consider r being FinSequence of rng R such that
A67: h in product r by Th6;
A68: dom h = dom r by A67,CARD_3:9;
A69: Den(o,A) is_exactly_partitable_wrt P by Def10;
now
let x be object;
assume
A70: x in dom r;
then
A71: h.x in p.x by A62,A63,A68;
A72: h.x in r.x by A67,A70,CARD_3:9;
A73: r.x in rng r by A70,FUNCT_1:def 3;
A74: p.x in rng p by A62,A68,A70,FUNCT_1:def 3;
ex c being set st ( c in P)&( r.x c= c) by A8,A73;
hence r.x c= p.x by A71,A72,A74,Lm3;
end;
then
A75: product r c= product p by A62,A68,CARD_3:27;
product p c= dom Den(o,A) by A59,A69;
then consider s2 being OperSymbol of S2 such that
A76: (the Sorts of G)*the_arity_of s2 = r and
A77: s2 in Q.o by A2,A75,Th31,XBOOLE_1:1;
consider p9 being FinSequence of P, o9 being OperSymbol of S2 such that
A78: g.s2 = [Q-index_of s2, p9] and
A79: s2 = o9 and
A80: Args(o9,G) c= product p9 by A24;
dom the Arity of S2 = the carrier' of S2 by FUNCT_2:def 1;
then Args(s2,G) = (the Sorts of G)# .((the Arity of S2).s2) by FUNCT_1:13
.= product r by A76,FINSEQ_2:def 5;
then
A81: p9 = em*r by A13,A79,A80,Th4;
A82: p = em*r by A13,A75,Th4;
Q-index_of s2 = o by A4,A77,Def3;
hence thesis by A24,A58,A78,A81,A82,FUNCT_1:def 3;
end;
end;