Copyright (c) 2002 Association of Mizar Users
environ
vocabulary AMI_1, MSUALG_1, FUNCT_1, RELAT_1, PBOOLE, BOOLE, EQREL_1,
ZF_REFLE, QC_LANG1, PRALG_1, FINSEQ_1, TDGROUP, CARD_3, GROUP_6, ALG_1,
FINSEQ_4, SEQM_3, PRALG_2, MSUALG_3, WELLORD1, MSUALG_4, OSALG_1,
ORDERS_1, NATTRA_1, RELAT_2, FINSEQ_5, ARYTM_1, TARSKI, YELLOW18,
YELLOW15, SETFAM_1, COH_SP, QUANTAL1, OSALG_4;
notation ZFMISC_1, TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, RELAT_2, FUNCT_1,
RELSET_1, PARTFUN1, EQREL_1, SETFAM_1, STRUCT_0, XCMPLX_0, XREAL_0,
ORDERS_1, ORDERS_3, NAT_1, FUNCT_2, FINSEQ_1, CARD_3, FINSEQ_4, FINSEQ_5,
PBOOLE, WAYBEL_0, PRALG_1, MSUALG_1, MSUALG_3, PRALG_2, OSALG_1, OSALG_3,
MSUALG_4, YELLOW18;
constructors ORDERS_3, INT_1, NAT_1, FINSEQ_5, FINSEQ_4, MSUALG_3, WAYBEL_0,
OSALG_3, MSUALG_4, EQREL_1, YELLOW18;
clusters MSUALG_1, PRALG_1, MSUALG_3, PRALG_2, RELSET_1, SETFAM_1, STRUCT_0,
FINSEQ_5, INT_1, RELAT_1, ORDERS_3, FILTER_1, SUBSET_1, OSALG_1,
MSUALG_4, MSAFREE, PARTFUN1;
requirements BOOLE, SUBSET, NUMERALS, REAL, ARITHM;
definitions TARSKI, MSUALG_3, XBOOLE_0, OSALG_1, OSALG_3;
theorems XBOOLE_0, XBOOLE_1, FUNCT_1, FUNCT_2, PBOOLE, CARD_3, MSUALG_1,
PRALG_1, FINSEQ_4, MSUALG_5, SQUARE_1, OSALG_1, OSALG_3, RELAT_2,
PRALG_2, ZFMISC_1, RELAT_1, RELSET_1, EQREL_1, MSUALG_3, MSUALG_6,
MSAFREE, TARSKI, SYSREL, ORDERS_1, FINSEQ_1, AXIOMS, FINSEQ_3, ENUMSET1,
FINSEQ_5, REAL_1, INT_1, ORDERS_3, PARTFUN1, WAYBEL_0, TOLER_1, GRFUNC_1,
MSUALG_9, MSUALG_4, XCMPLX_1, FINSEQ_2;
schemes FUNCT_1, ZFREFLE1, MSUALG_2, COMPTS_1, NAT_1, FUNCT_2;
begin
definition
let R be non empty Poset;
cluster Relation-yielding OrderSortedSet of R;
existence
proof
set I = the carrier of R;
consider R1 be Relation;
deffunc F(set) = R1;
consider f be Function such that
A1: dom f = I & for x be set st x in I holds f.x = F(x)
from Lambda;
reconsider f as ManySortedSet of I by A1,PBOOLE:def 3;
f is order-sorted
proof let s1,s2 be Element of R such that s1 <= s2;
f.s1 = R1 & f.s2 = R1 by A1;
hence f.s1 c= f.s2;
end;
then reconsider f as OrderSortedSet of R;
take f;
for x be set st x in dom f holds f.x is Relation by A1;
hence thesis by MSUALG_4:def 1;
end;
end;
:: this is a stronger condition for relation than just being order-sorted
definition
let R be non empty Poset;
let A,B be ManySortedSet of the carrier of R;
let IT be ManySortedRelation of A,B;
attr IT is os-compatible means :Def1:
for s1,s2 being Element of R st s1 <= s2
for x,y being set st x in A.s1 & y in B.s1 holds
[x,y] in IT.s1 iff [x,y] in IT.s2;
end;
definition
let R be non empty Poset;
let A,B be ManySortedSet of the carrier of R;
cluster os-compatible ManySortedRelation of A,B;
existence
proof
set I = the carrier of R;
consider R1 be Relation such that A1: R1 = {};
deffunc F(set) = R1;
consider f be Function such that
A2: dom f = I & for x be set st x in I holds f.x = F(x)
from Lambda;
reconsider f as ManySortedSet of R by A2,PBOOLE:def 3;
take f;
set f1 = f;
A3: for s1,s2 being Element of R st s1 <= s2
for x,y being set st x in A.s1 & y in B.s1 holds
[x,y] in f1.s1 iff [x,y] in f1.s2
proof
let s1,s2 be Element of R such that s1 <= s2;
A4: f1.s1 = R1 by A2 .= f1.s2 by A2;
let x,y be set such that x in A.s1 & y in B.s1;
thus [x,y] in f1.s1 iff [x,y] in f1.s2 by A4;
end;
for i be set st i in I holds f.i is Relation of A.i,B.i
proof
let i be set;
assume i in I;
then f.i = {} by A1,A2;
hence thesis by RELSET_1:25;
end;
then reconsider f2 = f1 as ManySortedRelation of A,B by MSUALG_4:def 2;
f2 is os-compatible by A3,Def1;
hence thesis;
end;
end;
definition
let R be non empty Poset;
let A,B be ManySortedSet of the carrier of R;
mode OrderSortedRelation of A,B is os-compatible ManySortedRelation of A,B;
canceled;
end;
theorem Bze:
for R being non empty Poset,
A,B being ManySortedSet of the carrier of R,
OR being ManySortedRelation of A,B holds
OR is os-compatible implies OR is OrderSortedSet of R
proof
let R be non empty Poset,
A,B be ManySortedSet of the carrier of R,
OR be ManySortedRelation of A,B;
assume A1: OR is os-compatible;
set OR1 = OR;
OR1 is order-sorted
proof
let s1,s2 be Element of R such that A2: s1 <= s2;
for x,y being set holds [x,y] in OR.s1 implies [x,y] in OR.s2
proof let x,y be set such that A3: [x,y] in OR.s1;
x in A.s1 & y in B.s1 by A3,ZFMISC_1:106;
hence [x,y] in OR.s2 by A1,A2,A3,Def1;
end;
hence thesis by RELAT_1:def 3;
end;
hence thesis;
end;
definition
let R be non empty Poset;
let A,B be ManySortedSet of R;
cluster os-compatible -> order-sorted ManySortedRelation of A,B;
coherence by Bze;
end;
definition
let R be non empty Poset;
let A be ManySortedSet of the carrier of R;
mode OrderSortedRelation of A is OrderSortedRelation of A,A;
end;
definition
let S be OrderSortedSign,
U1 be OSAlgebra of S;
mode OrderSortedRelation of U1 -> ManySortedRelation of U1 means
:Def3: it is os-compatible;
existence
proof
reconsider Y = the Sorts of U1 as OrderSortedSet of S by OSALG_1:17;
consider X being OrderSortedRelation of Y;
reconsider X1=X as ManySortedRelation of U1;
take X1;
thus thesis;
end;
end;
:: REVISE: the definition of ManySorted diagonal from MSUALG_6
:: should be moved to MSUALG_4; the "compatible" attr from MSUALG_6
:: should replace the MSCongruence-like
definition
let S be OrderSortedSign,
U1 be OSAlgebra of S;
cluster MSEquivalence-like OrderSortedRelation of U1;
existence
proof
deffunc F(Element of S) =
id ((the Sorts of U1).$1);
consider f be Function such that A1: dom f = the carrier of S &
for d be Element of S holds
f.d = F(d) from LambdaB;
reconsider f as ManySortedSet of the carrier of S
by A1,PBOOLE:def 3;
for x be set st x in dom f holds f.x is Relation
proof
let x be set;
assume x in dom f;
then f.x = id ((the Sorts of U1).x) by A1;
hence thesis;
end;
then reconsider f as ManySortedRelation of the carrier of S
by MSUALG_4:def 1;
for i be set st i in the carrier of S holds f.i is
Relation of (the Sorts of U1).i,(the Sorts of U1).i
proof
let i be set;
assume i in the carrier of S;
then f.i = id ((the Sorts of U1).i) by A1;
hence thesis;
end;
then reconsider f as
ManySortedRelation of the Sorts of U1,the Sorts of U1
by MSUALG_4:def 2;
reconsider f as ManySortedRelation of U1;
for i be set, R be Relation of (the Sorts of U1).i st
i in the carrier of S & f.i = R holds
R is Equivalence_Relation of (the Sorts of U1).i
proof
let i be set,
R be Relation of (the Sorts of U1).i;
assume i in the carrier of S & f.i = R;
then R = id ((the Sorts of U1).i) by A1;
hence thesis;
end;
then A2: f is MSEquivalence_Relation-like by MSUALG_4:def 3;
take f;
set f1 = f;
f1 is os-compatible
proof let s1,s2 be Element of S such that
A3: s1 <= s2;
reconsider s3 = s1, s4 = s2 as Element of S;
reconsider X = the Sorts of U1 as OrderSortedSet of S by OSALG_1:17;
X.s3 c= X.s4 by A3,OSALG_1:def 18;
then A4: id(X.s1) c= id(X.s2) by SYSREL:33;
A5: f1.s1 = id(X.s1) & f1.s2 = id(X.s2) by A1;
let x,y be set such that A6: x in (the Sorts of U1).s1
& y in (the Sorts of U1).s1;
thus [x,y] in f1.s1 implies [x,y] in f1.s2 by A4,A5;
assume [x,y] in f1.s2;
then x = y by A5,RELAT_1:def 10;
hence [x,y] in f1.s1 by A5,A6,RELAT_1:def 10;
end;
hence thesis by A2,Def3,MSUALG_4:def 5;
end;
end;
:: REVISE: we need the fact that id has the type,
:: the original prf can be simplified
definition
let S be OrderSortedSign,
U1 be non-empty OSAlgebra of S;
cluster MSCongruence-like (MSEquivalence-like OrderSortedRelation of U1);
existence
proof
deffunc F(Element of S) = id ((the Sorts of U1).$1);
consider f be Function such that A1: dom f = the carrier of S &
for d be Element of S holds
f.d = F(d) from LambdaB;
reconsider f as ManySortedSet of the carrier of S
by A1,PBOOLE:def 3;
for x be set st x in dom f holds f.x is Relation
proof
let x be set;
assume x in dom f;
then f.x = id ((the Sorts of U1).x) by A1;
hence thesis;
end;
then reconsider f as ManySortedRelation of the carrier of S
by MSUALG_4:def 1;
for i be set st i in the carrier of S holds f.i is
Relation of (the Sorts of U1).i,(the Sorts of U1).i
proof
let i be set;
assume i in the carrier of S;
then f.i = id ((the Sorts of U1).i) by A1;
hence thesis;
end;
then reconsider f as
ManySortedRelation of the Sorts of U1,the Sorts of U1
by MSUALG_4:def 2;
reconsider f as ManySortedRelation of U1;
for i be set, R be Relation of (the Sorts of U1).i st
i in the carrier of S & f.i = R holds
R is Equivalence_Relation of (the Sorts of U1).i
proof
let i be set,
R be Relation of (the Sorts of U1).i;
assume i in the carrier of S & f.i = R;
then R = id ((the Sorts of U1).i) by A1;
hence thesis;
end;
then f is MSEquivalence_Relation-like by MSUALG_4:def 3;
then reconsider f as MSEquivalence-like ManySortedRelation of U1
by MSUALG_4:def 5;
set f1 = f;
f1 is os-compatible
proof let s1,s2 be Element of S such that
A2: s1 <= s2;
reconsider s3 = s1, s4 = s2 as Element of S;
reconsider X = the Sorts of U1 as OrderSortedSet of S by OSALG_1:17;
X.s3 c= X.s4 by A2,OSALG_1:def 18;
then A3: id(X.s1) c= id(X.s2) by SYSREL:33;
A4: f1.s1 = id(X.s1) & f1.s2 = id(X.s2) by A1;
let x,y be set such that A5: x in (the Sorts of U1).s1
& y in (the Sorts of U1).s1;
thus [x,y] in f1.s1 implies [x,y] in f1.s2 by A3,A4;
assume [x,y] in f1.s2;
then x = y by A4,RELAT_1:def 10;
hence [x,y] in f1.s1 by A4,A5,RELAT_1:def 10;
end;
then reconsider f = f1 as MSEquivalence-like OrderSortedRelation of U1
by Def3;
take f;
for o be Element of the OperSymbols of S
for x,y be Element of Args(o,U1) st
(for n be Nat st n in dom x holds
[x.n,y.n] in f.((the_arity_of o)/.n))
holds [Den(o,U1).x,Den(o,U1).y] in f.(the_result_sort_of o)
proof
let o be Element of the OperSymbols of S;
let x,y be Element of Args(o,U1);
assume A6: for n be Nat st n in dom x holds
[x.n,y.n] in f.((the_arity_of o)/.n);
A7: dom x = dom (the_arity_of o) &
dom y = dom (the_arity_of o) by MSUALG_3:6;
for a be set st a in dom (the_arity_of o) holds x.a = y.a
proof
let a be set;
assume A8: a in dom (the_arity_of o);
then reconsider n = a as Nat;
A9: (the_arity_of o)/.n = (the_arity_of o).n
by A8,FINSEQ_4:def 4;
set ao = the_arity_of o;
ao.n in rng ao by A8,FUNCT_1:def 5;
then A10: f.(ao.n) = id ((the Sorts of U1).(ao.n)) by A1;
[x.n,y.n] in f.(ao.n) by A6,A7,A8,A9; hence thesis by A10,RELAT_1:def
10;
end;
then A11: Den(o,U1).x = Den(o,U1).y by A7,FUNCT_1:9;
set r = the_result_sort_of o;
A12: f.r = id ((the Sorts of U1).r) by A1;
A13: dom (the ResultSort of S) = the OperSymbols of S &
rng (the ResultSort of S) c= the carrier of S
by FUNCT_2:def 1;
then A14: dom ((the Sorts of U1)*(the ResultSort of S))
= dom (the ResultSort of S) by PBOOLE:def 3;
Result(o,U1) = ((the Sorts of U1) * the ResultSort of S).o
by MSUALG_1:def 10
.= (the Sorts of U1).((the ResultSort of S).o)
by A13,A14,FUNCT_1:22
.= (the Sorts of U1).r by MSUALG_1:def 7;
hence thesis by A11,A12,RELAT_1:def 10;
end;
hence thesis by MSUALG_4:def 6;
end;
end;
definition
let S be OrderSortedSign,
U1 be non-empty OSAlgebra of S;
mode OSCongruence of U1 is
MSCongruence-like (MSEquivalence-like OrderSortedRelation of U1);
end;
:: TODO: a smooth transition between Relations and Graphs would
:: be useful here, the FinSequence approach seemed to me faster than
:: transitive closure of R \/ R" .. maybe not, can be later a theorem
:: all could be done generally for reflexive (or with small
:: modification even non reflexive) Relations
:: I found ex post that attributes disconnected and connected defined
:: in ORDERS_3 have st. in common here, but the theory there is not developed
:: suggested improvements: f connects x,y; x is_connected_with y;
:: connected iff for x,y holds x is_connected_with y
:: finally I found this is the EqCl from MSUALG_5 - should be merged
definition
let R be non empty Poset;
func Path_Rel R -> Equivalence_Relation of the carrier of R means
:Def4: for x,y being set holds [x,y] in it iff
x in the carrier of R & y in the carrier of R &
ex p being FinSequence of the carrier of R
st 1 < len p & p.1 = x & p.(len p) = y &
for n being Nat st 2 <= n & n <= len p
holds [p.n,p.(n-1)] in the InternalRel of R or
[p.(n-1),p.n] in the InternalRel of R;
existence
proof
A1: the InternalRel of R is_reflexive_in the carrier of R
by ORDERS_1:def 4;
defpred PC[set,set] means
ex p being FinSequence of the carrier of R
st 1 < len p & p.1 = $1 & p.(len p) = $2 &
for n being Nat st 2 <= n & n <= len p
holds [p.n,p.(n-1)] in the InternalRel of R or
[p.(n-1),p.n] in the InternalRel of R;
set P = { [x,y] where x,y is Element of R:
x in the carrier of R & y in the carrier of R & PC[x,y]};
A2: for x,y being set holds [x,y] in P iff
x in the carrier of R & y in the carrier of R & PC[x,y]
proof
let x,y be set;
hereby assume [x,y] in P;
then consider x1,y1 being Element of R such that
A3: [x,y] = [x1,y1] and
A4: x1 in the carrier of R & y1 in the carrier of R & PC[x1,y1];
x = x1 & y = y1 by A3,ZFMISC_1:33;
hence x in the carrier of R & y in the carrier of R & PC[x,y] by A4;
end;
thus thesis;
end;
P c= [:the carrier of R, the carrier of R:]
proof let z be set such that A6: z in P;
consider x,y being Element of R such that A7: z = [x,y] &
x in the carrier of R & y in the carrier of R & PC[x,y] by A6;
thus thesis by A7,ZFMISC_1:106;
end;
then reconsider P1 = P as Relation of the carrier of R by RELSET_1:def 1;
now let x be set;
assume A8: x in the carrier of R;
PC[x,x]
proof
set F = <*x,x*>;
A9: F.1 = x & F.2 = x by FINSEQ_1:61;
A10: len F = 2 by FINSEQ_1:61;
rng F = {x,x} by FINSEQ_2:147 .= {x} by ENUMSET1:69;
then rng F c= the carrier of R by A8,ZFMISC_1:37;
then reconsider F1 = F as FinSequence of the carrier of R
by FINSEQ_1:def 4;
take F1;
thus 1 < len F1 by A10;
thus F1.1 = x & F1.(len F1) = x by A10,FINSEQ_1:61;
let n1 be Nat such that A11: 2 <= n1 & n1 <= len F1;
n1 = 2 by A10,A11,AXIOMS:21;
hence thesis by A1,A8,A9,RELAT_2:def 1;
end;
hence [x,x] in P1 by A8;
end;
then P1 is_reflexive_in the carrier of R by RELAT_2:def 1;
then
A12: dom P1 = the carrier of R & field P1 = the carrier of R by ORDERS_1:98;
now let x,y be set;
assume A14: x in the carrier of R & y in the carrier of R
& [x,y] in P1;
then consider p being FinSequence of the carrier of R
such that A15: 1 < len p & p.1 = x & p.(len p) = y &
for n being Nat st 2 <= n & n <= len p
holds [p.n,p.(n-1)] in the InternalRel of R or
[p.(n-1),p.n] in the InternalRel of R by A2;
PC[y,x]
proof :: just counting, more builtin arithmetics would be nice
take F = Rev p;
A16: len F = len p by FINSEQ_5:def 3;
thus 1 < len F by A15,FINSEQ_5:def 3;
thus F.1 = y & F.(len F) = x by A15,A16,FINSEQ_5:65;
let n1 be Nat such that A17: 2 <= n1 & n1 <= len F;
A18: 1 <= n1 by A17,AXIOMS:22;
A19: 2 - 1 <= n1 - 1 by A17,REAL_1:49;
then 0 <= n1 - 1 by AXIOMS:22;
then reconsider n1_1 = n1 - 1 as Nat by INT_1:16;
n1 - 1 <= len F - 0 by A17,REAL_1:92;
then A20: n1_1 in dom p by A16,A19,FINSEQ_3:27;
then A21: n1 in dom p & (n1 - 1) in dom p
by A16,A17,A18,FINSEQ_3:27;
A22: F.(n1 - 1) = p.(len p - (n1 - 1) + 1) by A20,FINSEQ_5:61
.= p.((len p - n1) + 1 + 1) by XCMPLX_1:37 .=
p.((len p - n1) + (1 + 1)) by XCMPLX_1:1 .= p.((len p - n1) + 2);
set n2 = (len p - n1) + 2;
0 <= len p - n1 by A16,A17,SQUARE_1:12;
then A23: 2 + 0 <= n2 by AXIOMS:24;
len p - n1 <= len p - 2 by A17,REAL_1:92;
then (len p - n1) + 2 <= len p - 2 + 2 by AXIOMS:24;
then A24: (len p - n1) + 2 <= len p + ( 2 - 2) by XCMPLX_1:30;
0 <= n2 by A23,AXIOMS:22;
then reconsider n2 = (len p - n1) + 2 as Nat by INT_1:16;
p.(n2-1) =
p.((len p - n1) + (2 - 1)) by XCMPLX_1:31 .= F.n1 by A21,FINSEQ_5:61;
hence [F.n1,F.(n1-1)] in the InternalRel of R or
[F.(n1-1),F.n1] in the InternalRel of R by A15,A22,A23,A24;
end;
hence [y,x] in P1 by A14;
end;
then A25: P1 is_symmetric_in the carrier of R by RELAT_2:def 3;
now let x,y,z be set;
assume A26: x in the carrier of R & y in the carrier of R &
z in the carrier of R & [x,y] in P1 & [y,z] in P1;
then PC[x,y] & PC[y,z] by A2;
then consider p1,p2 being FinSequence of the carrier of R
such that A27: 1 < len p1 & p1.1 = x & p1.(len p1) = y &
for n being Nat st 2 <= n & n <= len p1
holds [p1.n,p1.(n-1)] in the InternalRel of R or
[p1.(n-1),p1.n] in the InternalRel of R
and A28: 1 < len p2 & p2.1 = y & p2.(len p2) = z &
for n being Nat st 2 <= n & n <= len p2
holds [p2.n,p2.(n-1)] in the InternalRel of R or
[p2.(n-1),p2.n] in the InternalRel of R;
PC[x,z]
proof
take F = p1^p2;
A29: len F = len p1 + len p2 by FINSEQ_1:35;
1 + 1 < len p1 + len p2 by A27,A28,REAL_1:67;
hence 1 < len F by A29,AXIOMS:22;
1 in dom p1 by A27,FINSEQ_3:27;
hence F.1 = x by A27,FINSEQ_1:def 7;
len p2 in dom p2 by A28,FINSEQ_3:27;
hence F.(len F) = z by A28,A29,FINSEQ_1:def 7;
let n1 be Nat such that A30: 2 <= n1 & n1 <= len F;
A31: 1 <= n1 by A30,AXIOMS:22;
A32: 2 - 1 <= n1 - 1 by A30,REAL_1:49;
then 0 <= n1 - 1 by AXIOMS:22;
then reconsider n1_1 = n1 - 1 as Nat by INT_1:16;
A33: n1 - 1 <= len F - 0 by A30,REAL_1:92;
A34: len p1 + 1 <= n1 implies len p1 + 1 = n1 or len p1 + 1 < n1
by REAL_1:def 5;
per cases by A34,INT_1:20;
suppose A35: n1 <= len p1;
then A36: n1 in dom p1 by A31,FINSEQ_3:27;
n1 - 1 <= len p1 - 0 by A35,REAL_1:92;
then n1_1 in dom p1 by A32,FINSEQ_3:27;
then F.n1 = p1.n1 & F.(n1 -1) = p1.(n1 - 1) by A36,FINSEQ_1:def 7;
hence [F.n1,F.(n1-1)] in the InternalRel of R or
[F.(n1-1),F.n1] in the InternalRel of R by A27,A30,A35;
suppose A37: len p1 + 1 < n1;
len p1 < len p1 + 1 by REAL_1:69;
then A38: len p1 < n1 by A37,AXIOMS:22;
(len p1 + 1) - 1 < n1 - 1 by A37,REAL_1:54;
then len p1 < n1 - 1 by XCMPLX_1:26;
then A39: F.n1_1 = p2.(n1_1 - len p1) by A33,FINSEQ_1:37;
0 <= n1 - len p1 by A38,SQUARE_1:12;
then reconsider k = n1 - len p1 as Nat by INT_1:16;
A40: F.n1 = p2.k & F.(n1 - 1) = p2.(k - 1) by A30,A38,A39,FINSEQ_1:37,
XCMPLX_1:21;
1 < n1 - len p1 by A37,REAL_1:86;
then A41: 1 + 1 <= n1 - len p1 by INT_1:20;
n1 <= len p1 + len p2 by A30,FINSEQ_1:35;
then 2 <= k & k <= len p2 by A41,REAL_1:86;
hence thesis by A28,A40;
suppose A42: len p1 + 1 = n1;
:: we misuse reflexivity here
then A43: len p1 = n1 - 1 by XCMPLX_1:26;
A44: len p1 in dom p1 by A27,FINSEQ_3:27;
A45: len p1 + 1 <= len p1 + len p2 by A28,REAL_1:67;
A46: F.(n1 - 1) = y by A27,A43,A44,FINSEQ_1:def 7;
(len p1 + 1) - len p1 = 1 by XCMPLX_1:26;
then F.n1 = y by A28,A42,A45,FINSEQ_1:36;
hence thesis by A1,A26,A46,RELAT_2:def 1;
end;
hence [x,z] in P1 by A26;
end;
then P1 is_transitive_in the carrier of R by RELAT_2:def 8;
then reconsider P1 = P as Equivalence_Relation of the carrier of R
by A12,PARTFUN1:def 4,A25,RELAT_2:def 11,def 16;
take P1;
thus thesis by A2;
end;
uniqueness
proof
defpred PC1[set,set] means
$1 in the carrier of R & $2 in the carrier of R &
ex p being FinSequence of the carrier of R
st 1 < len p & p.1 = $1 & p.(len p) = $2 &
for n being Nat st 2 <= n & n <= len p
holds [p.n,p.(n-1)] in the InternalRel of R or
[p.(n-1),p.n] in the InternalRel of R;
let X,Y be Equivalence_Relation of the carrier of R;
assume A47: for x,y being set holds [x,y] in X iff PC1[x,y];
assume A48: for x,y being set holds [x,y] in Y iff PC1[x,y];
for x,y being set holds [x,y] in X iff [x,y] in Y
proof let x,y be set;
hereby assume [x,y] in X;
then PC1[x,y] by A47;
hence [x,y] in Y by A48;
end;
assume [x,y] in Y;
then PC1[x,y] by A48;
hence thesis by A47;
end;
hence thesis by RELAT_1:def 2;
end;
end;
theorem Th2:
for R being non empty Poset, s1,s2 being Element of R
st s1 <= s2 holds [s1,s2] in Path_Rel R
proof
let R be non empty Poset, s1,s2 be Element of R such that
A1: s1 <= s2;
set p = <* s1, s2 *>;
A2: len p = 2 by FINSEQ_1:61;
then A3: 1 < len p & p.1 = s1 & p.(len p) = s2 by FINSEQ_1:61;
for n being Nat st 2 <= n & n <= len p
holds [p.n,p.(n-1)] in the InternalRel of R or
[p.(n-1),p.n] in the InternalRel of R
proof let n1 be Nat such that A4: 2 <= n1 & n1 <= len p;
A5: n1 = 2 by A2,A4,AXIOMS:21;
[s1,s2] in the InternalRel of R by A1,ORDERS_1:def 9;
hence thesis by A3,A5,FINSEQ_1:61;
end;
hence [s1,s2] in Path_Rel R by A3,Def4;
end;
:: again, should be defined for Relations probably
definition
let R be non empty Poset;
let s1,s2 be Element of R;
pred s1 ~= s2 means :Def5:
[s1,s2] in Path_Rel R;
reflexivity
proof
set PR = Path_Rel R;
field PR = the carrier of R by ORDERS_1:97;
then PR is_reflexive_in the carrier of R by RELAT_2:def 9;
hence thesis by RELAT_2:def 1;
end;
symmetry
proof
set PR = Path_Rel R;
field PR = the carrier of R by ORDERS_1:97;
then PR is_symmetric_in the carrier of R by RELAT_2:def 11;
hence thesis by RELAT_2:def 3;
end;
end;
theorem
for R being non empty Poset,
s1,s2,s3 being Element of R holds
s1 ~= s2 & s2 ~= s3 implies s1 ~= s3
proof
let R be non empty Poset;
let s1,s2,s3 be Element of R;
assume A1: s1 ~= s2 & s2 ~= s3;
set PR = Path_Rel R;
A2: [s1,s2] in PR & [s2,s3] in PR by A1,Def5;
field PR = the carrier of R by ORDERS_1:97;
then PR is_transitive_in the carrier of R by RELAT_2:def 16;
then [s1,s3] in PR by A2,RELAT_2:def 8;
hence thesis by Def5;
end;
:: do for Relations
definition
let R be non empty Poset;
func Components R -> non empty (Subset-Family of R) equals :Def6:
Class Path_Rel R;
coherence;
end;
definition
let R be non empty Poset;
cluster -> non empty Element of Components R;
coherence
proof let X be Element of Components R;
X in Components R;
then X in Class Path_Rel R by Def6;
then consider x being set such that
A1: x in the carrier of R &
X = Class(Path_Rel R,x) by EQREL_1:def 5;
thus thesis by A1,EQREL_1:28;
end;
end;
definition
let R be non empty Poset;
mode Component of R is Element of Components R;
canceled;
end;
definition
let R be non empty Poset;
let s1 be Element of R;
func CComp s1 -> Component of R equals :Def8:
Class(Path_Rel R,s1);
correctness
proof
set C = Class(Path_Rel R,s1);
C in Class(Path_Rel R) by EQREL_1:def 5;
hence thesis by Def6;
end;
end;
theorem Th4:
for R being non empty Poset,
s1 be Element of R holds
s1 in CComp(s1)
proof
let R be non empty Poset;
let s1 be Element of R;
s1 in Class(Path_Rel R,s1) by EQREL_1:28;
hence thesis by Def8;
end;
theorem Th5:
for R being non empty Poset,
s1,s2 being Element of R st s1 <= s2 holds
CComp(s1) = CComp(s2)
proof
let R be non empty Poset,
s1,s2 be Element of R
such that A1: s1 <= s2;
[s1,s2] in Path_Rel R by A1,Th2;
then Class(Path_Rel R,s1) = Class(Path_Rel R,s2) by EQREL_1:44;
hence CComp(s1) =
Class(Path_Rel R,s2) by Def8 .= CComp(s2) by Def8;
end;
definition
let R be non empty Poset;
let A be ManySortedSet of the carrier of R;
let C be Component of R;
func A-carrier_of C equals :Def9:
union {A.s where s is Element of R: s in C};
correctness;
end;
theorem Th6:
for R being non empty Poset,
A being ManySortedSet of the carrier of R,
s being (Element of R),
x being set st x in A.s holds
x in A-carrier_of CComp(s)
proof
let R be non empty Poset;
let A be ManySortedSet of the carrier of R,
s be (Element of R),
x be set such that A1: x in A.s;
s in CComp(s) by Th4;
then A.s in {A.s1 where s1 is Element of R: s1 in CComp(s)};
then x in union {A.s1 where s1 is Element of R:
s1 in CComp(s)} by A1,TARSKI:def 4;
hence thesis by Def9;
end;
definition
let R be non empty Poset;
attr R is locally_directed means
:Def10: for C being Component of R holds C is directed;
end;
theorem Th7:
for R being discrete non empty Poset holds
for x,y being Element of R st
[x,y] in Path_Rel R holds x = y
proof
let R be discrete non empty Poset;
let x,y be Element of R;
assume [x,y] in Path_Rel R;
then consider p being FinSequence of the carrier of R such that
A1: 1 < len p & p.1 = x & p.(len p) = y &
for n being Nat st 2 <= n & n <= len p
holds [p.n,p.(n-1)] in the InternalRel of R or
[p.(n-1),p.n] in the InternalRel of R by Def4;
for n1 being Nat st 1 <= n1 & n1 <= len p holds p.n1 = x
proof let n1 be Nat such that A2: 1 <= n1 & n1 <= len p;
defpred P[Nat] means p.$1 <> x & 1 <= $1;
assume A3: p.n1 <> x;
then A4: ex k being Nat st P[k] by A2;
consider k being Nat such that
A5: P[k] & for n being Nat st P[n] holds k <= n from Min(A4);
1 < k by A1,A5,REAL_1:def 5;
then A6: 1 + 1 <= k by INT_1:20;
then A7: 1 + 1 - 1 <= k - 1 by REAL_1:49;
then 0 <= k - 1 by AXIOMS:22;
then reconsider k1 = k - 1 as Nat by INT_1:16;
k <= n1 by A2,A3,A5;
then A8: k <= len p by A2,AXIOMS:22;
then k in dom p by A5,FINSEQ_3:27;
then reconsider pk = p.k as Element of R by PARTFUN1:27;
k1 < k by INT_1:26;
then A9: p.k1 = x by A5,A7;
per cases by A1,A6,A8,A9;
suppose [pk,x] in the InternalRel of R;
then pk <= x by ORDERS_1:def 9;
hence contradiction by A5,ORDERS_3:1;
suppose [x,pk] in the InternalRel of R;
then x <= pk by ORDERS_1:def 9;
hence contradiction by A5,ORDERS_3:1;
end;
hence thesis by A1;
end;
theorem Th8:
for R being discrete non empty Poset,
C being Component of R
ex x being Element of R st
C = {x}
proof
let R be discrete non empty Poset,
C be Component of R;
C in Components R;
then C in Class Path_Rel R by Def6;
then consider x being set such that
A1: x in the carrier of R and
A2: C = Class(Path_Rel R,x) by EQREL_1:def 5;
reconsider x1 = x as Element of R by A1;
take x1;
for y being set holds y in C iff y = x1
proof let y be set;
hereby assume A3: y in C;
then A4: [y,x] in Path_Rel R by A2,EQREL_1:27;
reconsider y1 = y as Element of R by A3;
y1 = x1 by A4,Th7;
hence y = x1;
end;
assume y = x1;
hence y in C by A2,EQREL_1:28;
end;
hence thesis by TARSKI:def 1;
end;
theorem Th9:
for R being discrete non empty Poset holds R is locally_directed
proof
let R be discrete non empty Poset;
let C be Component of R;
consider x being Element of R such that
A1: C = {x} by Th8;
for x,y being Element of R st x in C & y in C
ex z being Element of R st z in C & x <= z & y <= z
proof let x1,y1 be Element of R such that
A2: x1 in C & y1 in C;
A3: x1 = x & x = y1 by A1,A2,TARSKI:def 1;
take x1;
thus thesis by A2,A3;
end;
hence C is directed by WAYBEL_0:def 1;
end;
:: the system could generate this one from the following
definition
cluster locally_directed (non empty Poset);
existence
proof consider R being discrete non empty Poset;
take R;
thus thesis by Th9;
end;
end;
definition
cluster locally_directed OrderSortedSign;
existence
proof consider R being discrete OrderSortedSign;
take R;
thus thesis by Th9;
end;
end;
definition
cluster discrete -> locally_directed (non empty Poset);
coherence by Th9;
end;
definition
let S be locally_directed (non empty Poset);
cluster -> directed Component of S;
coherence by Def10;
end;
theorem Th10:
{} is Equivalence_Relation of {}
proof
reconsider R = {} as Relation of {} by RELSET_1:25;
R is_reflexive_in {} by RELAT_2:def 9,TOLER_1:1,2;
then dom R = {} & field R = {} by ORDERS_1:98;
hence thesis by TOLER_1:3,9,PARTFUN1:def 4;
end;
:: Much of what follows can be done generally for OrderSortedRelations
:: of OrderSortedSets (and not just OrderSortedRelations of OSAlgebras),
:: unfortunately, multiple inheritence would be needed to widen the
:: latter to the former
:: Classes on connected components
definition
let S be locally_directed OrderSortedSign;
let A be OSAlgebra of S;
let E be MSEquivalence-like OrderSortedRelation of A;
let C be Component of S;
func CompClass(E,C) -> Equivalence_Relation of
(the Sorts of A)-carrier_of C means
:Def11: for x,y being set holds
[x,y] in it iff ex s1 being Element of S
st s1 in C & [x,y] in E.s1;
existence
proof
defpred CC1[set,set] means
ex s1 being Element of S
st s1 in C & [$1,$2] in E.s1;
A1: E is os-compatible by Def3;
per cases;
suppose A2: (the Sorts of A)-carrier_of C is empty;
for x,y being set holds [x,y] in {} iff
ex s1 being Element of S
st s1 in C & [x,y] in E.s1
proof let x,y be set;
thus [x,y] in {} implies
ex s1 being Element of S
st s1 in C & [x,y] in E.s1;
assume ex s1 being Element of S
st s1 in C & [x,y] in E.s1;
then consider s1 being Element of S
such that A3: s1 in C & [x,y] in E.s1;
A4: x in (the Sorts of A).s1 by A3,ZFMISC_1:106;
(the Sorts of A).s1 in {(the Sorts of A).s
where s is Element of S: s in C} by A3;
then x in union {(the Sorts of A).s where
s is Element of S: s in C} by A4,TARSKI:def 4;
hence thesis by A2,Def9;
end;
hence thesis by A2,Th10;
suppose (the Sorts of A)-carrier_of C is non empty;
then reconsider SAC = (the Sorts of A)-carrier_of C as non empty set;
set CC = {[x,y] where x,y is Element of SAC: CC1[x,y]};
A5: for x,y being set holds [x,y] in CC iff CC1[x,y]
proof
let x,y be set;
hereby assume [x,y] in CC;
then consider x1,y1 being Element of SAC such that
A6: [x,y] = [x1,y1] and
A7: CC1[x1,y1];
thus CC1[x,y] by A6,A7;
end;
assume A8: CC1[x,y];
then consider s1 being Element of S
such that A9: s1 in C & [x,y] in E.s1;
A10: (the Sorts of A).s1 in {(the Sorts of A).s
where s is Element of S: s in C} by A9;
x in (the Sorts of A).s1 & y in (the Sorts of A).s1 by A9,ZFMISC_1:106;
then x in
union {(the Sorts of A).s where s is Element of S:
s in C} & y in
union {(the Sorts of A).s where s is Element of S:
s in C} by A10,TARSKI:def 4;
then reconsider x1 = x, y1 =y as Element of SAC by Def9;
[x1,y1] in CC by A8;
hence thesis;
end;
CC c= [:SAC, SAC:]
proof let z be set such that A11: z in CC;
consider x,y being Element of SAC such that
A12: z = [x,y] & CC1[x,y] by A11;
thus thesis by A12,ZFMISC_1:106;
end;
then reconsider P1 = CC as Relation of SAC by RELSET_1:def 1;
now let x be set such that A13: x in SAC;
reconsider x1 = x as Element of SAC by A13;
x in union {(the Sorts of A).s
where s is Element of S: s in C} by A13,Def9;
then consider X being set such that
A14: x in X and
A15: X in {(the Sorts of A).s
where s is Element of S: s in C} by TARSKI:def 4;
consider s being Element of S such that
A16: X = (the Sorts of A).s & s in C by A15;
field(E.s) = (the Sorts of A).s by ORDERS_1:97;
then
E.s is_reflexive_in (the Sorts of A).s by RELAT_2:def 9;
then [x,x] in E.s by A14,A16,RELAT_2:def 1;
then [x1,x1] in CC by A16;
hence [x,x] in P1;
end;
then P1 is_reflexive_in SAC by RELAT_2:def 1;
then
A17: dom P1 = SAC & field P1 = SAC by ORDERS_1:98;
now let x,y be set such that A19:
x in SAC & y in SAC & [x,y] in P1;
reconsider x1 = x, y1 = y as Element of SAC by A19;
consider x2,y2 being Element of SAC such that
A20: [x,y] = [x2,y2] & CC1[x2,y2] by A19;
A21: x = x2 & y = y2 by A20,ZFMISC_1:33;
consider s5 being Element of S
such that A22: s5 in C & [x2,y2] in E.s5 by A20;
A23: x2 in (the Sorts of A).s5 & y2 in (the Sorts of A).s5
by A22,ZFMISC_1:106;
field(E.s5) = (the Sorts of A).s5 by ORDERS_1:97;
then E.s5 is_symmetric_in (the Sorts of A).s5 by RELAT_2:def 11;
then [y,x] in E.s5 by A21,A22,A23,RELAT_2:def 3;
then [y1,x1] in CC by A22;
hence [y,x] in P1;
end;
then A24: P1 is_symmetric_in SAC by RELAT_2:def 3;
now let x,y,z be set such that A25: x in SAC & y in SAC & z in SAC
& [x,y] in P1 & [y,z] in P1;
consider x2,y2 being Element of SAC such that
A26: [x,y] = [x2,y2] & CC1[x2,y2] by A25;
A27: x = x2 & y = y2 by A26,ZFMISC_1:33;
consider y3,z3 being Element of SAC such that
A28: [y,z] = [y3,z3] & CC1[y3,z3] by A25;
A29: y = y3 & z = z3 by A28,ZFMISC_1:33;
consider s5 being Element of S
such that A30: s5 in C & [x2,y2] in E.s5 by A26;
A31: x2 in (the Sorts of A).s5 & y2 in (the Sorts of A).s5
by A30,ZFMISC_1:106;
consider s6 being Element of S
such that A32: s6 in C & [y3,z3] in E.s6 by A28;
A33: y3 in (the Sorts of A).s6 & z3 in (the Sorts of A).s6
by A32,ZFMISC_1:106;
reconsider s5_1 = s5, s6_1 = s6 as Element of S;
consider su being Element of S such that
A34: su in C & s5_1 <= su & s6_1 <= su by A30,A32,WAYBEL_0:def 1;
A35: [x2,y2] in E.su & [y3,z3] in E.su
by A1,A30,A31,A32,A33,A34,Def1;
then A36: x2 in (the Sorts of A).su & y2 in (the Sorts of A).su &
z3 in (the Sorts of A).su by ZFMISC_1:106;
field(E.su) = (the Sorts of A).su by ORDERS_1:97;
then E.su is_transitive_in (the Sorts of A).su by RELAT_2:def 16;
then [x2,z3] in E.su by A27,A29,A35,A36,RELAT_2:def 8;
hence [x,z] in P1 by A27,A29,A34;
end;
then P1 is_transitive_in SAC by RELAT_2:def 8;
then reconsider P1 as Equivalence_Relation of (the Sorts of A)-carrier_of C
by A17,PARTFUN1:def 4,A24,RELAT_2:def 11,def 16;
take P1;
thus thesis by A5;
end;
uniqueness
proof
defpred CC1[set,set] means
ex s1 being Element of S
st s1 in C & [$1,$2] in E.s1;
let X,Y be Equivalence_Relation of
(the Sorts of A)-carrier_of C;
assume A37: for x,y being set holds [x,y] in X iff CC1[x,y];
assume A38: for x,y being set holds [x,y] in Y iff CC1[x,y];
for x,y being set holds [x,y] in X iff [x,y] in Y
proof let x,y be set;
hereby assume [x,y] in X;
then CC1[x,y] by A37;
hence [x,y] in Y by A38;
end;
assume [x,y] in Y;
then CC1[x,y] by A38;
hence thesis by A37;
end;
hence thesis by RELAT_1:def 2;
end;
end;
:: we could give a name to Class CompClass(E,C)
:: restriction of Class CompClass(E,C) to A.s1
definition
let S be locally_directed OrderSortedSign;
let A be OSAlgebra of S;
let E be MSEquivalence-like OrderSortedRelation of A;
let s1 be Element of S;
func OSClass(E,s1) -> Subset of Class(CompClass(E,CComp(s1))) means
:Def12:
for z being set holds z in it iff
ex x being set st x in (the Sorts of A).s1 &
z = Class( CompClass(E,CComp(s1)), x);
existence
proof
defpred CC1[set] means
ex x being set st x in (the Sorts of A).s1 &
$1 = Class( CompClass(E,CComp(s1)), x);
set CS = Class(CompClass(E,CComp(s1)));
set SAC = (the Sorts of A)-carrier_of CComp(s1);
per cases;
suppose A1: CS is empty;
reconsider CS1 = {} as Subset of CS by XBOOLE_1:2;
take CS1;
let z be set;
thus z in CS1 implies CC1[z];
assume CC1[z];
then consider x being set such that A2: x in (the Sorts of A).s1 &
z = Class( CompClass(E,CComp(s1)), x);
x in SAC by A2,Th6;
hence thesis by A1,A2,EQREL_1:def 5;
suppose CS is non empty;
then reconsider CS1 = CS as non empty Subset-Family of SAC;
set CC = {x where x is Element of CS1: CC1[x]};
now let x be set;
assume x in CC;
then consider y being Element of CS1 such that
A3: x = y & CC1[y];
thus x in CS1 by A3;
end;
then reconsider CC2 = CC as Subset of CS by TARSKI:def 3;
take CC2;
for x being set holds x in CC iff CC1[x]
proof
let x be set;
hereby assume x in CC;
then consider x1 being Element of CS1 such that
A4: x = x1 & CC1[x1];
thus CC1[x] by A4;
end;
assume A5: CC1[x];
then consider y being set such that
A6: y in (the Sorts of A).s1 and
A7: x = Class( CompClass(E,CComp(s1)), y);
s1 in CComp(s1) by Th4;
then (the Sorts of A).s1 in {(the Sorts of A).s where s is Element of
the carrier of S: s in CComp(s1)};
then y in union {(the Sorts of A).s where s is Element of
the carrier of S: s in CComp(s1)} by A6,TARSKI:def 4;
then y in SAC by Def9;
then x in Class( CompClass(E,CComp(s1))) by A7,EQREL_1:def 5;
hence x in CC by A5;
end;
hence thesis;
end;
uniqueness
proof
defpred CC1[set] means
ex x being set st x in (the Sorts of A).s1 &
$1 = Class( CompClass(E,CComp(s1)), x);
let X,Y be Subset of Class(CompClass(E,CComp(s1)));
assume A8: for x being set holds x in X iff CC1[x];
assume A9: for x being set holds x in Y iff CC1[x];
for x being set holds x in X iff x in Y
proof let x be set;
hereby assume x in X;
then CC1[x] by A8;
hence x in Y by A9;
end;
assume x in Y;
then CC1[x] by A9;
hence thesis by A8;
end;
hence thesis by TARSKI:2;
end;
end;
definition
let S be locally_directed OrderSortedSign;
let A be non-empty OSAlgebra of S;
let E be MSEquivalence-like OrderSortedRelation of A;
let s1 be Element of S;
cluster OSClass(E,s1) -> non empty;
coherence
proof
consider x being set such that A1: x in (the Sorts of A).s1
by XBOOLE_0:def 1;
Class( CompClass(E,CComp(s1)), x) in OSClass(E,s1) by A1,Def12;
hence thesis;
end;
end;
theorem Th11:
for S being locally_directed OrderSortedSign,
A being OSAlgebra of S,
E being (MSEquivalence-like OrderSortedRelation of A),
s1,s2 being Element of S st s1 <= s2
holds OSClass(E,s1) c= OSClass(E,s2)
proof
let S be locally_directed OrderSortedSign;
let A be OSAlgebra of S;
let E be MSEquivalence-like OrderSortedRelation of A;
let s1,s2 be Element of S;
reconsider s3 = s1, s4 = s2 as Element of S;
assume A1: s1 <= s2;
then A2: CComp(s1) = CComp(s2) by Th5;
thus OSClass(E,s1) c= OSClass(E,s2)
proof let z be set such that A3: z in OSClass(E,s1);
consider x being set such that A4: x in (the Sorts of A).s1 &
z = Class( CompClass(E,CComp(s1)), x) by A3,Def12;
reconsider SO = the Sorts of A as OrderSortedSet of S by OSALG_1:17;
SO.s3 c= SO.s4 by A1,OSALG_1:def 18;
hence thesis by A2,A4,Def12;
end;
end;
:: finally, this is analogy of the Many-Sorted Class E for order-sorted E
:: this definition should work for order-sorted MSCongruence too
:: if non-empty not needed, prove the following cluster
definition
let S be locally_directed OrderSortedSign;
let A be OSAlgebra of S;
let E be MSEquivalence-like OrderSortedRelation of A;
func OSClass E -> OrderSortedSet of S means
:Def13: for s1 being Element of S holds
it.s1 = OSClass(E,s1);
existence
proof
deffunc F(Element of S) = OSClass(E,$1);
consider f being Function such that A1: dom f = the carrier of S and
A2: for i being Element of S
holds f.i = F(i) from LambdaB;
reconsider f1 = f as ManySortedSet of the carrier of S
by A1,PBOOLE:def 3;
set f2 = f1;
f2 is order-sorted
proof let s1,s2 be Element of S such that A3: s1 <= s2;
f2.s1 = OSClass(E,s1) & f2.s2 = OSClass(E,s2) by A2;
hence f2.s1 c= f2.s2 by A3,Th11;
end;
hence thesis by A2;
end;
uniqueness
proof let X,Y be OrderSortedSet of S;
assume A4: for s1 being Element of S holds
X.s1 = OSClass(E,s1);
assume A5: for s1 being Element of S holds
Y.s1 = OSClass(E,s1);
now let s1 be set;
assume s1 in the carrier of S;
then reconsider s2 = s1 as Element of S;
thus X.s1 = OSClass(E,s2) by A4 .= Y.s1 by A5;
end;
hence X = Y by PBOOLE:3;
end;
end;
definition
let S be locally_directed OrderSortedSign;
let A be non-empty OSAlgebra of S;
let E be MSEquivalence-like OrderSortedRelation of A;
cluster OSClass E -> non-empty;
coherence
proof
for i being set st i in the carrier of S
holds (OSClass E).i is non empty
proof let i be set such that A1: i in the carrier of S;
reconsider s = i as Element of S by A1;
(OSClass E).s = OSClass( E,s) by Def13;
hence (OSClass E).i is non empty;
end;
hence thesis by PBOOLE:def 16;
end;
end;
:: order-sorted equiv of Class(R,x)
definition
let S be locally_directed OrderSortedSign;
let U1 be non-empty OSAlgebra of S;
let E be MSEquivalence-like OrderSortedRelation of U1;
let s be Element of S;
let x be Element of (the Sorts of U1).s;
func OSClass(E,x) -> Element of OSClass(E,s) equals
:Def14: Class( CompClass(E, CComp(s)), x);
correctness by Def12;
end;
theorem
for R being locally_directed (non empty Poset),
x,y being Element of R
st (ex z being Element of R st z <= x & z <= y)
holds ex u being Element of R st x <= u & y <= u
proof
let R be locally_directed (non empty Poset),
x,y be Element of R such that
A1: (ex z being Element of R st z <= x & z <= y);
reconsider x1 = x,y1 = y as Element of R;
consider z being Element of R such that
A2: z <= x & z <= y by A1;
CComp z = CComp(x) & CComp(z) = CComp(y) by A2,Th5;
then x in CComp(z) & y in CComp(z) by Th4;
then ex u being Element of R st u in CComp(z) & x1 <= u & y1 <= u
by WAYBEL_0:def 1;
hence thesis;
end;
theorem Th13:
for S be locally_directed OrderSortedSign,
U1 be non-empty OSAlgebra of S,
E be (MSEquivalence-like OrderSortedRelation of U1),
s be (Element of S),
x,y be Element of (the Sorts of U1).s holds
OSClass(E,x) = OSClass(E,y) iff [x,y] in E.s
proof
let S be locally_directed OrderSortedSign;
let U1 be non-empty OSAlgebra of S;
let E be MSEquivalence-like OrderSortedRelation of U1;
let s be Element of S;
let x,y be Element of (the Sorts of U1).s;
reconsider SU = the Sorts of U1 as OrderSortedSet of S by OSALG_1:17;
A1: x in (the Sorts of U1)-carrier_of CComp(s) by Th6;
A2: s in CComp(s) by Th4;
A3: E is os-compatible by Def3;
hereby
assume OSClass(E,x) = OSClass(E,y);
then Class( CompClass(E, CComp(s)), x) = OSClass(E,y) by Def14 .= Class(
CompClass(E, CComp(s)), y) by Def14;
then [x,y] in CompClass(E, CComp(s)) by A1,EQREL_1:44;
then consider s1 being Element of S such that
A4: s1 in CComp(s) & [x,y] in E.s1 by Def11;
reconsider sn1 = s, s1_1 = s1 as Element of S;
A5: x in SU.s1_1 & y in SU.s1_1
by A4,ZFMISC_1:106;
consider s2 being Element of S such that
A6: s2 in CComp(s) & s1_1 <= s2 & sn1 <= s2 by A2,A4,WAYBEL_0:def 1;
[x,y] in E.s2 by A3,A4,A5,A6,Def1;
hence [x,y] in E.s by A3,A6,Def1;
end;
assume A7: [x,y] in E.s;
A8: x in (the Sorts of U1)-carrier_of CComp(s) by Th6;
s in CComp(s) by Th4;
then [x,y] in CompClass(E, CComp(s)) by A7,Def11;
then Class( CompClass(E, CComp(s)), x) = Class( CompClass(E, CComp(s)), y)
by A8,EQREL_1:44;
hence OSClass(E,x) = Class( CompClass(E, CComp(s)), y) by Def14 .= OSClass(E
,y) by Def14;
end;
theorem Th14:
for S be locally_directed OrderSortedSign,
U1 be non-empty OSAlgebra of S,
E be (MSEquivalence-like OrderSortedRelation of U1),
s1,s2 be (Element of S),
x be Element of (the Sorts of U1).s1 st
s1 <= s2 holds
for y being Element of (the Sorts of U1).s2
st y = x holds OSClass(E,x) = OSClass(E,y)
proof
let S be locally_directed OrderSortedSign,
U1 be non-empty OSAlgebra of S,
E be (MSEquivalence-like OrderSortedRelation of U1),
s1,s2 be (Element of S),
x be Element of (the Sorts of U1).s1;
assume s1 <= s2;
then A1: CComp(s1) = CComp(s2) by Th5;
let y be Element of (the Sorts of U1).s2 such that
A2: y = x;
thus OSClass(E,x) = Class( CompClass(E, CComp(s2)), y) by A1,A2,Def14
.= OSClass(E,y) by Def14;
end;
begin
::::::::::::::::::::::::::::::::::::::
:: Order Sorted Quotient Algebra ::
::::::::::::::::::::::::::::::::::::::
:: take care (or even prove counterexample) - order-sorted
:: ManySortedFunction generaly doesnot exist
reserve S for locally_directed OrderSortedSign;
reserve o for Element of the OperSymbols of S;
:: multiclasses
definition let S,o;
let A be non-empty OSAlgebra of S;
let R be OSCongruence of A;
let x be Element of Args(o,A);
func R #_os x -> Element of product ((OSClass R) * (the_arity_of o)) means
:Def15:
for n be Nat st n in dom (the_arity_of o)
ex y being Element of (the Sorts of A).((the_arity_of o)/.n)
st y = x.n & it.n = OSClass(R, y);
existence
proof
set ar = the_arity_of o,
da = dom ar;
defpred P[set,set] means
for n be Nat st n = $1 holds
ex y being Element of (the Sorts of A).((the_arity_of o)/.n)
st y = x.n & $2 = OSClass(R, y);
A1: for k be set st k in da ex u be set st P[k,u]
proof
let k be set;
assume A2: k in da;
then reconsider n = k as Nat;
reconsider y = x.n as
Element of (the Sorts of A).((the_arity_of o)/.n) by A2,MSUALG_6:2;
take OSClass(R,y);
thus thesis;
end;
consider f be Function such that
A3: dom f = da & for x be set st x in da holds P[x,f.x]
from NonUniqFuncEx(A1);
A4: dom ((OSClass R) * ar) = da by PBOOLE:def 3;
for y be set st y in dom ((OSClass R) * ar) holds
f.y in ((OSClass R) * ar).y
proof
let y be set;
assume A5: y in dom ((OSClass R) * ar);
then A6: ((OSClass R) * ar).y = (OSClass R).(ar.y) by FUNCT_1:22;
ar.y in rng ar by A4,A5,FUNCT_1:def 5;
then reconsider s = ar.y as Element of S;
reconsider n = y as Nat by A5;
consider z being Element of (the Sorts of A).((the_arity_of o)/.n)
such that A7: z = x.n & f.n = OSClass(R, z) by A3,A4,A5;
((ar)/.n) = ar.n by A4,A5,FINSEQ_4:def 4;
then f.y in OSClass (R,s) by A7;
hence thesis by A6,Def13;
end;
then reconsider f as Element of product ((OSClass R) * ar)
by A3,A4,CARD_3:18;
take f;
let n be Nat;
assume n in da;
hence thesis by A3;
end;
uniqueness
proof
let F,G be Element of product ((OSClass R) * (the_arity_of o));
assume that
A8: for n be Nat st n in dom (the_arity_of o) holds
ex y being Element of (the Sorts of A).((the_arity_of o)/.n)
st y = x.n & F.n = OSClass(R, y) and
A9: for n be Nat st n in dom (the_arity_of o) holds
ex y being Element of (the Sorts of A).((the_arity_of o)/.n)
st y = x.n & G.n = OSClass(R, y);
dom F = dom ((OSClass R) * (the_arity_of o)) &
dom G = dom ((OSClass R) * (the_arity_of o)) by CARD_3:18;
then A10: dom F = dom (the_arity_of o) &
dom G = dom (the_arity_of o) by PBOOLE:def 3;
for y be set st y in dom (the_arity_of o) holds F.y = G.y
proof
let y be set;
assume A11: y in dom (the_arity_of o);
then reconsider n = y as Nat;
consider z being Element of (the Sorts of A).((the_arity_of o)/.n)
such that A12: z = x.n & F.n = OSClass(R, z) by A8,A11;
consider z1 being Element of (the Sorts of A).((the_arity_of o)/.n)
such that A13: z1 = x.n & G.n = OSClass(R, z1) by A9,A11;
thus thesis by A12,A13;
end;
hence thesis by A10,FUNCT_1:9;
end;
end;
:: the quotient will be different for order-sorted;
:: this def seems ok for order-sorted
definition let S,o;
let A be non-empty OSAlgebra of S;
let R be OSCongruence of A;
func OSQuotRes(R,o) ->
Function of ((the Sorts of A) * the ResultSort of S).o,
((OSClass R) * the ResultSort of S).o means :Def16:
for x being Element of (the Sorts of A).(the_result_sort_of o)
holds it.x = OSClass(R,x);
existence
proof
set rs = (the_result_sort_of o),
D = (the Sorts of A).rs;
deffunc F(Element of D) = OSClass(R,$1);
consider f be Function such that
A1: dom f = D & for d be Element of D holds f.d = F(d)
from LambdaB;
A2: o in the OperSymbols of S;
A3: dom (the ResultSort of S) = the OperSymbols of S &
rng (the ResultSort of S) c= the carrier of S
by FUNCT_2:def 1;
o in dom ((the Sorts of A)*(the ResultSort of S))
by A2,PBOOLE:def 3;
then A4: ((the Sorts of A) * the ResultSort of S).o =
(the Sorts of A).((the ResultSort of S).o) by FUNCT_1:22
.= D by MSUALG_1:def 7;
dom ((OSClass R) * the ResultSort of S) =
dom (the ResultSort of S) by A3,PBOOLE:def 3;
then A5: ((OSClass R) * the ResultSort of S).o =
(OSClass R).((the ResultSort of S).o) by A3,FUNCT_1:22
.= (OSClass R).rs by MSUALG_1:def 7;
for x be set st x in D holds f.x in (OSClass R).rs
proof
let x be set;
assume x in D;
then reconsider x1 = x as Element of D;
f.x1 = OSClass(R,x1) by A1;
then f.x1 in OSClass (R,rs);
hence thesis by Def13;
end; then reconsider f as
Function of ((the Sorts of A) * the ResultSort of S).o,
((OSClass R) * the ResultSort of S).o
by A1,A4,A5,FUNCT_2:5;
take f;
thus thesis by A1;
end;
uniqueness
proof
let f,g be Function of
((the Sorts of A) * the ResultSort of S).o,
((OSClass R) * the ResultSort of S).o;
set SA = the Sorts of A,
RS = the ResultSort of S,
rs = the_result_sort_of o;
assume that
A6: for x being Element of SA.rs holds f.x = OSClass(R,x) and
A7: for x being Element of SA.rs holds g.x = OSClass(R,x);
A8: o in the OperSymbols of S;
A9: dom RS = the OperSymbols of S &
rng RS c= the carrier of S by FUNCT_2:def 1;
o in dom (SA*RS) by A8,PBOOLE:def 3;
then A10: (SA * RS).o = SA.(RS.o) by FUNCT_1:22
.= SA.rs by MSUALG_1:def 7;
dom ((OSClass R) * RS) = dom RS by A9,PBOOLE:def 3;
then ((OSClass R) * RS).o = (OSClass R).(RS.o) by A9,FUNCT_1:22
.= (OSClass R).rs by MSUALG_1:def 7;
then A11: dom f = SA.rs & rng f c= (OSClass R).rs &
dom g = SA.rs & rng g c= (OSClass R).rs by A10,FUNCT_2:def 1;
now
let x be set;
assume x in SA.rs;
then reconsider x1 = x as Element of SA.rs;
f.x1 = OSClass(R,x1) & g.x1 = OSClass(R,x1) by A6,A7;
hence f.x = g.x;
end;
hence thesis by A11,FUNCT_1:9;
end;
func OSQuotArgs(R,o) ->
Function of ((the Sorts of A)# * the Arity of S).o,
((OSClass R)# * the Arity of S).o means
for x be Element of Args(o,A) holds it.x = R #_os x;
existence
proof
set D = Args(o,A);
deffunc F(Element of D) = R #_os $1;
consider f be Function such that
A12: dom f = D & for d be Element of D holds f.d = F(d)
from LambdaB;
A13: D = ((the Sorts of A)# * the Arity of S).o
by MSUALG_1:def 9;
A14: o in the OperSymbols of S;
then o in dom ((the Sorts of A)# * the Arity of S) by PBOOLE:def 3;
then A15: ((the Sorts of A)# * the Arity of S).o =
(the Sorts of A)#.((the Arity of S).o) by FUNCT_1:22
.= ((the Sorts of A)#.(the_arity_of o)) by MSUALG_1:def 6;
set ao = the_arity_of o;
o in dom ((OSClass R)# * the Arity of S) by A14,PBOOLE:def 3;
then A16: ((OSClass R)# * the Arity of S).o =
(OSClass R)#.((the Arity of S).o) by FUNCT_1:22
.= (OSClass R)#.ao by MSUALG_1:def 6;
for x be set st x in (the Sorts of A)#.ao holds
f.x in (OSClass R)#.ao
proof
let x be set;
assume x in (the Sorts of A)#.ao;
then reconsider x1 = x as Element of D by A15,MSUALG_1:def 9;
A17: f.x1 = R #_os x1 by A12;
(OSClass R)#.ao = product((OSClass R)*ao) by MSUALG_1:def 3;
hence thesis by A17;
end;
then reconsider f as Function of
((the Sorts of A)# * the Arity of S).o,
((OSClass R)# * the Arity of S).o by A12,A13,A15,A16,FUNCT_2:5;
take f;
thus thesis by A12;
end;
uniqueness
proof
let f,g be Function of
((the Sorts of A)# * the Arity of S).o,
((OSClass R)# * the Arity of S).o;
assume that
A18: for x be Element of Args(o,A) holds f.x = R #_os x and
A19: for x be Element of Args(o,A) holds g.x = R #_os x;
o in the OperSymbols of S;
then o in dom ((the Sorts of A)# * the Arity of S) by PBOOLE:def 3;
then A20: ((the Sorts of A)# * the Arity of S).o =
(the Sorts of A)#.((the Arity of S).o) by FUNCT_1:22
.= ((the Sorts of A)#.(the_arity_of o)) by MSUALG_1:def 6;
set ao = the_arity_of o;
A21: dom f = (the Sorts of A)#.ao &
dom g = (the Sorts of A)#.ao by A20,FUNCT_2:def 1;
now
let x be set;
assume x in (the Sorts of A)#.ao;
then reconsider x1 = x as Element of Args(o,A) by A20,MSUALG_1:def 9;
f.x1 = R #_os x1 & g.x1 = R #_os x1 by A18,A19; hence f.x = g.x;
end;
hence thesis by A21,FUNCT_1:9;
end;
end;
definition let S;
let A be non-empty OSAlgebra of S;
let R be OSCongruence of A;
func OSQuotRes R ->
ManySortedFunction of ((the Sorts of A) * the ResultSort of S),
((OSClass R) * the ResultSort of S) means
for o being OperSymbol of S holds it.o = OSQuotRes(R,o);
existence
proof
set O = the OperSymbols of S;
defpred P[set,set] means
for o be OperSymbol of S st o = $1 holds $2 = OSQuotRes(R,o);
A1: for x be set st x in O ex y be set st P[x,y]
proof
let x be set;
assume x in O;
then reconsider x1 = x as OperSymbol of S;
take OSQuotRes(R,x1);
thus thesis;
end;
consider f be Function such that
A2: dom f = O & for x be set st x in O holds P[x,f.x]
from NonUniqFuncEx(A1);
reconsider f as ManySortedSet of O by A2,PBOOLE:def 3;
for x be set st x in dom f holds f.x is Function
proof
let x be set;
assume x in dom f;
then reconsider x1 = x as OperSymbol of S by A2;
f.x1 = OSQuotRes(R,x1) by A2;
hence thesis;
end;
then reconsider f as ManySortedFunction of O by PRALG_1:def 15;
for i be set st i in O holds f.i is
Function of ((the Sorts of A) * the ResultSort of S).i,
((OSClass R) * the ResultSort of S).i
proof
let i be set;
assume i in O;
then reconsider i1 = i as OperSymbol of S;
f.i1 = OSQuotRes(R,i1) by A2;
hence thesis;
end;
then reconsider f as ManySortedFunction of
((the Sorts of A) * the ResultSort of S),
((OSClass R) * the ResultSort of S) by MSUALG_1:def 2;
take f;
thus thesis by A2;
end;
uniqueness
proof
let f,g be ManySortedFunction of
((the Sorts of A) * the ResultSort of S),
((OSClass R) * the ResultSort of S);
assume that
A3: for o being OperSymbol of S holds f.o = OSQuotRes(R,o) and
A4: for o being OperSymbol of S holds g.o = OSQuotRes(R,o);
now
let i be set;
assume i in the OperSymbols of S;
then reconsider i1 = i as OperSymbol of S;
f.i1 = OSQuotRes(R,i1) & g.i1 = OSQuotRes(R,i1) by A3,A4;
hence f.i = g.i;
end;
hence thesis by PBOOLE:3;
end;
func OSQuotArgs R ->
ManySortedFunction of (the Sorts of A)# * the Arity of S,
(OSClass R)# * the Arity of S means
for o be OperSymbol of S holds it.o = OSQuotArgs(R,o);
existence
proof
set O = the OperSymbols of S;
defpred P[set,set] means
for o be OperSymbol of S st o = $1 holds $2 = OSQuotArgs(R,o);
A5: for x be set st x in O ex y be set st P[x,y]
proof
let x be set;
assume x in O;
then reconsider x1 = x as OperSymbol of S;
take OSQuotArgs(R,x1);
thus thesis;
end;
consider f be Function such that
A6: dom f = O & for x be set st x in O holds P[x,f.x]
from NonUniqFuncEx(A5);
reconsider f as ManySortedSet of O by A6,PBOOLE:def 3;
for x be set st x in dom f holds f.x is Function
proof
let x be set;
assume x in dom f;
then reconsider x1 = x as OperSymbol of S by A6;
f.x1 = OSQuotArgs(R,x1) by A6;
hence thesis;
end;
then reconsider f as ManySortedFunction of O by PRALG_1:def 15;
for i be set st i in O holds f.i is
Function of ((the Sorts of A)# * the Arity of S).i,
((OSClass R)# * the Arity of S).i
proof
let i be set;
assume i in O;
then reconsider i1 = i as OperSymbol of S;
f.i1 = OSQuotArgs(R,i1) by A6;
hence thesis;
end;
then reconsider f as ManySortedFunction of
((the Sorts of A)# * the Arity of S),
((OSClass R)# * the Arity of S) by MSUALG_1:def 2;
take f;
thus thesis by A6;
end;
uniqueness
proof
let f,g be ManySortedFunction of
((the Sorts of A)# * the Arity of S),
((OSClass R)# * the Arity of S);
assume that
A7: for o being OperSymbol of S holds f.o = OSQuotArgs(R,o) and
A8: for o being OperSymbol of S holds g.o = OSQuotArgs(R,o);
now
let i be set;
assume i in the OperSymbols of S;
then reconsider i1 = i as OperSymbol of S;
f.i1 = OSQuotArgs(R,i1) & g.i1 = OSQuotArgs(R,i1) by A7,A8;
hence f.i = g.i;
end;
hence thesis by PBOOLE:3;
end;
end;
theorem Th15:
for A be non-empty OSAlgebra of S,
R be OSCongruence of A, x be set
st x in ((OSClass R)# * the Arity of S).o
ex a be Element of Args(o,A) st x = R #_os a
proof
let A be non-empty OSAlgebra of S,
R be OSCongruence of A,
x be set;
assume A1: x in ((OSClass R)# * the Arity of S).o;
set ar = the_arity_of o;
A2: ar = (the Arity of S).o by MSUALG_1:def 6;
then ((OSClass R)# * the Arity of S).o = product ((OSClass R) * ar)
by MSAFREE:1;
then consider f be Function such that
A3: f = x & dom f = dom ((OSClass R) * ar) &
for y be set st y in dom ((OSClass R) * ar) holds
f.y in ((OSClass R) * ar).y by A1,CARD_3:def 5;
A4: dom ((OSClass R) * ar) = dom ar by PBOOLE:def 3;
A5: for n be Nat st n in dom f holds f.n in OSClass (R,((ar)/.n))
proof
let n be Nat;
assume A6: n in dom f;
then A7: ar.n = ((ar)/.n) by A3,A4,FINSEQ_4:def 4;
reconsider s = ((ar)/.n) as Element of S;
((OSClass R) * ar).n = (OSClass R).s by A3,A6,A7,FUNCT_1:22
.= OSClass (R,s) by Def13;
hence thesis by A3,A6;
end;
defpred P[set,set] means $2 in (the Sorts of A).((ar)/.$1) & $2 in f.$1;
A8: for a be set st a in dom f ex b be set st P[a,b]
proof
let a be set;
assume A9: a in dom f; then reconsider n = a as Nat by A3;
reconsider s = ((ar)/.a) as Element of S;
f.n in OSClass (R,s) by A5,A9;
then consider x being set such that A10: x in (the Sorts of A).s &
f.n = Class( CompClass(R,CComp(s)), x) by Def12;
take x;
x in (the Sorts of A)-carrier_of CComp(s) by A10,Th6;
hence thesis by A10,EQREL_1:28;
end;
consider g be Function such that
A11: dom g = dom f & for a be set st a in dom f holds P[a,g.a]
from NonUniqFuncEx(A8);
A12: Args(o,A) = ((the Sorts of A)# * (the Arity of S)).o
by MSUALG_1:def 9
.= product ((the Sorts of A) * ar) by A2,MSAFREE:1;
dom (the Sorts of A) = the carrier of S by PBOOLE:def 3;
then rng ar c= dom (the Sorts of A);
then A13: dom g = dom ((the Sorts of A) * ar) by A3,A4,A11,RELAT_1:46;
for y be set st y in dom ((the Sorts of A) * ar) holds
g.y in ((the Sorts of A) * ar).y
proof
let y be set;
assume A14: y in dom ((the Sorts of A) * ar);
then reconsider n = y as Nat;
A15: ar.n = ((ar)/.n) by A3,A4,A11,A13,A14,FINSEQ_4:def 4;
reconsider s = ((ar)/.n) as Element of S;
g.n in (the Sorts of A).s by A11,A13,A14;
hence thesis by A14,A15,FUNCT_1:22;
end;
then reconsider g as Element of Args(o,A) by A12,A13,CARD_3:18;
take g;
A16: dom (R #_os g) = dom ((OSClass R) * ar) by CARD_3:18;
for x being set st x in dom ar holds f.x = (R #_os g).x
proof
let x be set;
assume A17: x in dom ar;
then reconsider n = x as Nat;
reconsider s = ((ar)/.n) as Element of S;
consider z being Element of (the Sorts of A).((the_arity_of o)/.n)
such that A18: z = g.n & (R #_os g).n = OSClass(R, z) by A17,Def15;
A19: g.n in (the Sorts of A).((ar)/.n) & g.n in f.n by A3,A4,A11,A17;
f.n in OSClass (R,s) by A3,A4,A5,A17;
then consider u being set such that A20: u in (the Sorts of A).s &
f.n = Class( CompClass(R,CComp(s)), u) by Def12;
u in (the Sorts of A)-carrier_of CComp(s) by A20,Th6;
then f.n = Class( CompClass(R,CComp(s)), g.n) by A19,A20,EQREL_1:31;
hence thesis by A18,Def14;
end;
hence thesis by A3,A4,A16,FUNCT_1:9;
end;
definition let S,o;
let A be non-empty OSAlgebra of S;
let R be OSCongruence of A;
func OSQuotCharact(R,o) ->
Function of ((OSClass R)# * the Arity of S).o,
((OSClass R) * the ResultSort of S).o means :Def20:
for a be Element of Args(o,A) st
R #_os a in ((OSClass R)# * the Arity of S).o
holds it.(R #_os a) = ((OSQuotRes(R,o)) * (Den(o,A))).a;
existence
proof
set Ca = ((OSClass R)# * the Arity of S).o,
Cr = ((OSClass R) * the ResultSort of S).o;
defpred P[set,set] means
for a be Element of Args(o,A) st $1 = R #_os a holds
$2 = ((OSQuotRes(R,o)) * (Den(o,A))).a;
A1: for x be set st x in Ca ex y be set st y in Cr & P[x,y]
proof
let x be set;
assume x in Ca;
then consider a be Element of Args(o,A) such that A2: x = R #_os a by Th15
;
take y = ((OSQuotRes(R,o)) * (Den(o,A))).a;
A3: dom Den(o,A) = Args(o,A) & rng Den(o,A) c= Result(o,A)
by FUNCT_2:def 1;
A4: o in the OperSymbols of S;
set ro = the_result_sort_of o,
ar = the_arity_of o;
A5: ro in CComp(ro) by Th4;
o in dom ((the Sorts of A) * the ResultSort of S)
by A4,PBOOLE:def 3;
then A6: ((the Sorts of A) * the ResultSort of S).o =
(the Sorts of A).((the ResultSort of S).o) by FUNCT_1:22
.= (the Sorts of A).ro by MSUALG_1:def 7;
o in dom ((OSClass R) * the ResultSort of S) by A4,PBOOLE:def 3;
then A7: ((OSClass R) * the ResultSort of S).o =
(OSClass R).((the ResultSort of S).o) by FUNCT_1:22
.= (OSClass R).ro by MSUALG_1:def 7;
then A8: dom (OSQuotRes(R,o)) = (the Sorts of A).ro &
rng (OSQuotRes(R,o)) c= (OSClass R).ro by A6,FUNCT_2:def 1;
A9: Result(o,A) = (the Sorts of A).ro
by A6,MSUALG_1:def 10;
then OSQuotRes(R,o).(Den(o,A).a) in rng (OSQuotRes(R,o))
by A8,FUNCT_1:def 5;
then A10: OSQuotRes(R,o).(Den(o,A).a) in (OSClass R).ro by A7;
A11: dom (OSQuotRes(R,o) * Den(o,A)) = dom Den(o,A)
by A3,A8,A9,RELAT_1:46;
hence y in Cr by A3,A7,A10,FUNCT_1:22;
let b be Element of Args(o,A); assume
A12: x = R #_os b;
reconsider da = (Den(o,A)).a, db = (Den(o,A)).b as
Element of (the Sorts of A).ro by A6,MSUALG_1:def 10;
A13: da in (the Sorts of A)-carrier_of CComp(ro) by Th6;
A14: y = (OSQuotRes(R,o)).((Den(o,A)).a) by A3,A11,FUNCT_1:22
.= OSClass(R, da) by Def16
.= Class( CompClass(R, CComp(ro)), da) by Def14;
A15: ((OSQuotRes(R,o)) * (Den(o,A))).b = (OSQuotRes(R,o)).db
by A3,A11,FUNCT_1:22
.= OSClass(R,db) by Def16
.= Class( CompClass(R, CComp(ro)), db) by Def14;
for n be Nat st n in dom a holds [a.n,b.n] in R.((ar)/.n)
proof
let n be Nat;
assume A16: n in dom a;
A17: dom a = dom ar & dom b = dom ar by MSUALG_3:6;
then consider ya being Element of (the Sorts of A).((ar)/.n) such that
A18: ya = a.n & (R #_os a).n = OSClass(R, ya) by A16,Def15;
consider yb being Element of (the Sorts of A).((ar)/.n) such that
A19: yb = b.n & (R #_os b).n = OSClass(R, yb) by A16,A17,Def15;
thus thesis by A2,A12,A18,A19,Th13;
end;
then [da,db] in R.ro by MSUALG_4:def 6;
then [da,db] in CompClass(R, CComp(ro)) by A5,Def11;
hence y = ((OSQuotRes(R,o)) * (Den(o,A))).b by A13,A14,A15,EQREL_1:44;
end;
consider f be Function such that
A20: dom f = Ca & rng f c= Cr & for x be set st x in Ca holds
P[x,f.x] from NonUniqBoundFuncEx(A1);
reconsider f as Function of
((OSClass R)# * the Arity of S).o,
((OSClass R) * the ResultSort of S).o by A20,FUNCT_2:4;
take f;
thus thesis by A20;
end;
uniqueness
proof
let F,G be Function of ((OSClass R)# * the Arity of S).o,
((OSClass R) * the ResultSort of S).o;
assume that
A21: for a be Element of Args(o,A) st
R #_os a in ((OSClass R)# * the Arity of S).o
holds F.(R #_os a) = ((OSQuotRes(R,o)) * (Den(o,A))).a and
A22: for a be Element of Args(o,A) st
R #_os a in ((OSClass R)# * the Arity of S).o
holds G.(R #_os a) = ((OSQuotRes(R,o)) * (Den(o,A))).a;
set ao = the_arity_of o;
A23: dom (the Arity of S) = the OperSymbols of S &
rng (the Arity of S) c= (the carrier of S)* by FUNCT_2:def 1;
then dom ((OSClass R)# * the Arity of S) = dom (the Arity of S)
by PBOOLE:def 3;
then A24: ((OSClass R)# * the Arity of S).o =
(OSClass R)#.((the Arity of S).o) by A23,FUNCT_1:22
.= (OSClass R)#.ao by MSUALG_1:def 6;
then A25: dom F = (OSClass R)#.ao & dom G = (OSClass R)#.ao
by FUNCT_2:def 1;
now
let x be set;
assume A26: x in (OSClass R)#.ao;
then consider a be Element of Args(o,A) such that
A27: x = R #_os a by A24,Th15;
F.x = (OSQuotRes(R,o) * Den(o,A)).a &
G.x = ((OSQuotRes(R,o)) * Den(o,A)).a by A21,A22,A24,A26,A27;
hence F.x = G.x;
end;
hence thesis by A25,FUNCT_1:9;
end;
end;
definition let S;
let A be non-empty OSAlgebra of S;
let R be OSCongruence of A;
func OSQuotCharact R -> ManySortedFunction of
(OSClass R)# * the Arity of S, (OSClass R) * the ResultSort of S
means :Def21:
for o be OperSymbol of S holds it.o = OSQuotCharact(R,o);
existence
proof
set O = the OperSymbols of S;
defpred P[set,set] means
for o be OperSymbol of S st o = $1 holds $2 = OSQuotCharact(R,o);
A1: for x be set st x in O ex y be set st P[x,y]
proof
let x be set;
assume x in O;
then reconsider x1 = x as OperSymbol of S;
take OSQuotCharact(R,x1);
thus thesis;
end;
consider f be Function such that
A2: dom f = O & for x be set st x in O holds P[x,f.x]
from NonUniqFuncEx(A1);
reconsider f as ManySortedSet of O by A2,PBOOLE:def 3;
for x be set st x in dom f holds f.x is Function
proof
let x be set;
assume x in dom f;
then reconsider x1 = x as OperSymbol of S by A2;
f.x1 = OSQuotCharact(R,x1) by A2;
hence thesis;
end;
then reconsider f as ManySortedFunction of O by PRALG_1:def 15;
for i be set st i in O holds f.i is
Function of ((OSClass R)# * the Arity of S).i,
((OSClass R) * the ResultSort of S).i
proof
let i be set;
assume i in O;
then reconsider i1 = i as OperSymbol of S;
f.i1 = OSQuotCharact(R,i1) by A2;
hence thesis;
end;
then reconsider f as ManySortedFunction of
((OSClass R)# * the Arity of S),
((OSClass R) * the ResultSort of S) by MSUALG_1:def 2;
take f;
thus thesis by A2;
end;
uniqueness
proof
let f,g be ManySortedFunction of
((OSClass R)# * the Arity of S),
((OSClass R) * the ResultSort of S);
assume that
A3: for o being OperSymbol of S holds
f.o = OSQuotCharact(R,o) and
A4: for o being OperSymbol of S holds
g.o = OSQuotCharact(R,o);
now
let i be set;
assume i in the OperSymbols of S;
then reconsider i1 = i as OperSymbol of S;
f.i1 = OSQuotCharact(R,i1) & g.i1 = OSQuotCharact(R,i1)
by A3,A4; hence f.i = g.i;
end;
hence thesis by PBOOLE:3;
end;
end;
definition let S;
let U1 be non-empty OSAlgebra of S;
let R be OSCongruence of U1;
func QuotOSAlg(U1,R) -> OSAlgebra of S equals :Def22:
MSAlgebra(# OSClass R, OSQuotCharact R #);
coherence by OSALG_1:17;
end;
:: we could note that for discrete the QuotOSAlg and QuotMsAlg are equal
definition let S; let U1 be non-empty OSAlgebra of S;
let R be OSCongruence of U1;
cluster QuotOSAlg (U1,R) -> strict non-empty;
coherence
proof
QuotOSAlg (U1,R) = MSAlgebra(# OSClass R, OSQuotCharact R #) by Def22;
hence thesis by MSUALG_1:def 8;
end;
end;
definition let S; let U1 be non-empty OSAlgebra of S;
let R be OSCongruence of U1;
let s be Element of S;
func OSNat_Hom(U1,R,s) ->
Function of (the Sorts of U1).s,OSClass(R,s) means :Def23:
for x being Element of (the Sorts of U1).s holds
it.x = OSClass(R,x);
existence
proof
deffunc F(Element of (the Sorts of U1).s) = OSClass(R,$1);
thus ex F being Function of (the Sorts of U1).s,OSClass(R,s) st
for x being Element of (the Sorts of U1).s holds
F.x = F(x) from LambdaD;
end;
uniqueness
proof
let f,g be Function of (the Sorts of U1).s,OSClass (R,s);
assume that
A1: for x being Element of (the Sorts of U1).s holds
f.x = OSClass(R,x) and
A2: for x being Element of (the Sorts of U1).s holds
g.x = OSClass(R,x);
A3: dom f = (the Sorts of U1).s & dom g = (the Sorts of U1).s
by FUNCT_2:def 1;
now
let x be set;
assume x in (the Sorts of U1).s;
then reconsider x1 = x as Element of (the Sorts of U1).s;
f.x = OSClass(R,x1) & g.x = OSClass(R,x1) by A1,A2;
hence f.x = g.x;
end;
hence thesis by A3,FUNCT_1:9;
end;
end;
definition let S; let U1 be non-empty OSAlgebra of S;
let R be OSCongruence of U1;
func OSNat_Hom(U1,R) ->
ManySortedFunction of U1, QuotOSAlg (U1,R) means :Def24:
for s be Element of S holds it.s = OSNat_Hom(U1,R,s);
existence
proof
deffunc F(Element of S) = OSNat_Hom(U1,R,$1);
consider f be Function such that A1: dom f = the carrier of S &
for d be Element of S holds
f.d = F(d) from LambdaB;
reconsider f as ManySortedSet of the carrier of S
by A1,PBOOLE:def 3;
for x be set st x in dom f holds f.x is Function
proof
let x be set;
assume x in dom f;
then reconsider y = x as Element of S by A1;
f.y = OSNat_Hom(U1,R,y) by A1;
hence thesis;
end;
then reconsider f as ManySortedFunction of the carrier of S
by PRALG_1:def 15;
for i be set st i in the carrier of S holds
f.i is Function of (the Sorts of U1).i, (OSClass R).i
proof
let i be set;
assume i in the carrier of S;
then reconsider s = i as Element of S;
A2: OSClass(R,s) = (OSClass R).i by Def13;
f.s = OSNat_Hom(U1,R,s) by A1;
hence thesis by A2;
end;
then reconsider f as ManySortedFunction of the Sorts of U1,OSClass R
by MSUALG_1:def 2;
QuotOSAlg (U1,R) = MSAlgebra(#OSClass R, OSQuotCharact R#) by Def22;
then reconsider f as ManySortedFunction of U1,QuotOSAlg (U1,R);
take f;
thus thesis by A1;
end;
uniqueness
proof
let F,G be ManySortedFunction of U1, QuotOSAlg (U1,R);
assume that
A3: for s be Element of S holds F.s = OSNat_Hom(U1,R,s) and
A4: for s be Element of S holds G.s = OSNat_Hom(U1,R,s);
now
let i be set;
assume i in the carrier of S;
then reconsider s = i as SortSymbol of S;
F.s = OSNat_Hom(U1,R,s) & G.s = OSNat_Hom(U1,R,s)
by A3,A4; hence F.i = G.i;
end;
hence thesis by PBOOLE:3;
end;
end;
theorem
for U1 be non-empty OSAlgebra of S,
R be OSCongruence of U1 holds
OSNat_Hom(U1,R) is_epimorphism U1, QuotOSAlg (U1,R) &
OSNat_Hom(U1,R) is order-sorted
proof
let U1 be non-empty OSAlgebra of S,
R be OSCongruence of U1;
set F = OSNat_Hom(U1,R),
QA = QuotOSAlg (U1,R),
S1 = the Sorts of U1;
A1: QA = MSAlgebra (# OSClass R, OSQuotCharact R #) by Def22;
for o be Element of the OperSymbols of S st Args (o,U1) <> {}
for x be Element of Args(o,U1) holds
(F.(the_result_sort_of o)).(Den(o,U1).x) = Den(o,QA).(F#x)
proof
let o be Element of the OperSymbols of S such that Args (o,U1) <> {};
let x be Element of Args(o,U1);
set ro = the_result_sort_of o,
ar = the_arity_of o;
A2: Den(o,QA) = (OSQuotCharact R).o by A1,MSUALG_1:def 11
.= OSQuotCharact(R,o) by Def21;
A3: dom (F#x) = dom ar & dom x = dom ar by MSUALG_3:6;
A4: dom (R #_os x) = dom ((OSClass R) * (the_arity_of o))
by CARD_3:18;
dom (OSClass R) = the carrier of S by PBOOLE:def 3;
then rng ar c= dom (OSClass R);
then A5: dom (R #_os x) = dom ar by A4,RELAT_1:46;
(the Arity of S).o = ar by MSUALG_1:def 6;
then A6: ((OSClass R)# * the Arity of S).o = product ((OSClass R) * ar)
by MSAFREE:1;
for a be set st a in dom ar holds (F#x).a = (R #_os x).a
proof
let a be set;
assume A7: a in dom ar;
then reconsider n = a as Nat;
set Fo = OSNat_Hom(U1,R,((ar)/.n)),
s = ((ar)/.n);
A8: n in dom ((the Sorts of U1) * ar) by A7,PBOOLE:def 3;
then ((the Sorts of U1) * ar).n = (the Sorts of U1).(ar.n)
by FUNCT_1:22
.= S1.s by A7,FINSEQ_4:def 4;
then reconsider xn = x.n as Element of S1.s by A8,MSUALG_3:6;
consider z being Element of S1.s such that
A9: z = x.n & (R #_os x).n = OSClass(R,z) by A7,Def15;
thus (F#x).a = (F.((ar)/.n)).(x.n) by A3,A7,MSUALG_3:def 8
.= Fo.xn by Def24
.= (R #_os x).a by A9,Def23;
end;
then A10: F # x = R #_os x by A3,A5,FUNCT_1:9;
A11: dom Den(o,U1) = Args(o,U1) & rng Den(o,U1) c= Result(o,U1)
by FUNCT_2:def 1;
A12: dom (the Sorts of U1) = the carrier of S by PBOOLE:def 3;
A13: dom (the ResultSort of S) = the OperSymbols of S &
rng (the ResultSort of S) c= the carrier of S
by FUNCT_2:def 1;
rng (the ResultSort of S) c= dom (the Sorts of U1) by A12;
then dom ((the Sorts of U1) * the ResultSort of S) =
dom (the ResultSort of S) by RELAT_1:46;
then A14: ((the Sorts of U1) * the ResultSort of S).o
= (the Sorts of U1).((the ResultSort of S).o)
by A13,FUNCT_1:22
.= (the Sorts of U1).ro by MSUALG_1:def 7;
then A15: Result(o,U1) = S1.ro by MSUALG_1:def 10;
reconsider dx = (Den(o,U1)).x as Element of S1.ro by A14,MSUALG_1:def 10;
rng Den(o,U1) c= dom OSQuotRes(R,o)
by A11,A14,A15,FUNCT_2:def 1;
then A16: dom ((OSQuotRes(R,o)) * Den(o,U1)) = dom Den(o,U1)
by RELAT_1:46;
Den(o,QA).(F#x) = ((OSQuotRes(R,o)) * (Den(o,U1))).x by A2,A6,A10,Def20
.= (OSQuotRes(R,o)) . dx by A11,A16,FUNCT_1:22
.= OSClass (R, dx) by Def16
.= (OSNat_Hom(U1,R,ro)).dx by Def23
.= (F.ro).((Den(o,U1)).x) by Def24;
hence thesis;
end;
hence F is_homomorphism U1,QA by MSUALG_3:def 9;
for i be set st i in the carrier of S holds
rng (F.i) = (the Sorts of QA).i
proof
let i be set;
assume i in the carrier of S;
then reconsider s = i as Element of S;
reconsider f = F.i as Function of S1.s, (the Sorts of QA).s
by MSUALG_1:def 2;
QA = MSAlgebra (# OSClass R,OSQuotCharact R #) by Def22;
then A17: (the Sorts of QA).s = OSClass (R,s) by Def13;
A18: dom f = S1.s & rng f c= (the Sorts of QA).s
by FUNCT_2:def 1;
for x be set st x in (the Sorts of QA).i holds x in rng f
proof
let x be set;
assume x in (the Sorts of QA).i;
then consider a1 being set such that
A19: a1 in S1.s & x = Class(CompClass(R,CComp(s)),a1) by A17,Def12;
reconsider a2 = a1 as Element of S1.s by A19;
A20: OSClass(R,a2) = x by A19,Def14;
A21: f.a1 in rng f by A18,A19,FUNCT_1:def 5;
f = OSNat_Hom(U1,R,s) by Def24;
hence thesis by A20,A21,Def23;
end;
then (the Sorts of QA).i c= rng f by TARSKI:def 3;
hence thesis by XBOOLE_0:def 10;
end;
hence F is "onto" by MSUALG_3:def 3;
thus F is order-sorted
proof
let s1,s2 be Element of S such that A22: s1 <= s2;
let a1 be set such that A23: a1 in dom (F.s1);
reconsider S2 = S1 as OrderSortedSet of S by OSALG_1:17;
A24: S2.s1 c= S2.s2 by A22,OSALG_1:def 18;
A25: dom (F.s2) = S1.s2 by FUNCT_2:def 1;
A26: a1 in S1.s1 by A23;
hence a1 in dom (F.s2) by A24,A25;
reconsider b1 = a1 as Element of S1.s1 by A23;
reconsider b2 = a1 as Element of S1.s2 by A24,A26;
thus (F.s1).a1 = OSNat_Hom(U1,R,s1).b1 by Def24
.= OSClass(R,b1) by Def23 .= OSClass(R,b2) by A22,Th14
.= OSNat_Hom(U1,R,s2).b2 by Def23 .= (F.s2).a1 by Def24;
end;
end;
theorem Th17:
for U1,U2 being non-empty OSAlgebra of S,
F being ManySortedFunction of U1,U2 st
F is_homomorphism U1,U2 & F is order-sorted holds
MSCng(F) is OSCongruence of U1
proof
let U1,U2 be non-empty OSAlgebra of S,
F be ManySortedFunction of U1,U2 such that
A1: F is_homomorphism U1,U2 & F is order-sorted;
reconsider S1 = the Sorts of U1
as OrderSortedSet of S by OSALG_1:17;
MSCng(F) is os-compatible
proof
let s1,s2 be Element of S such that
A2: s1 <= s2;
reconsider s3 = s1, s4 = s2 as SortSymbol of S;
let x,y be set such that
A3: x in (the Sorts of U1).s1 & y in (the Sorts of U1).s1;
A4: S1.s3 c= S1.s4 by A2,OSALG_1:def 18;
A5: dom (F.s3) = S1.s3 & dom (F.s4) = S1.s4 by FUNCT_2:def 1;
reconsider x1 = x, y1 = y as Element of (the Sorts of U1).s1 by A3;
reconsider x2 = x, y2 = y as Element of (the Sorts of U1).s2 by A3,A4;
A6: [x2,y2] in MSCng(F,s2) iff (F.s2).x2 = (F.s2).y2 by MSUALG_4:def 19;
A7: x1 in dom (F.s4) & (F.s3).x1 = (F.s4).x1 &
y1 in dom (F.s4) & (F.s3).y1 = (F.s4).y1 by A1,A2,A5,OSALG_3:def 1;
(MSCng(F)).s1 = MSCng(F,s1) &
(MSCng(F)).s2 = MSCng(F,s2) by A1,MSUALG_4:def 20;
hence [x,y] in (MSCng(F)).s1 iff [x,y] in (MSCng(F)).s2 by A6,A7,MSUALG_4:
def 19;
end;
hence MSCng(F) is OSCongruence of U1 by Def3;
end;
:: just a casting func, currently no other way how to employ the type system
definition let S; let U1,U2 be non-empty OSAlgebra of S;
let F be ManySortedFunction of U1,U2;
assume A1: F is_homomorphism U1,U2 & F is order-sorted;
func OSCng(F) -> OSCongruence of U1 equals
:Def25: MSCng(F);
correctness by A1,Th17;
end;
definition let S; let U1,U2 be non-empty OSAlgebra of S;
let F be ManySortedFunction of U1,U2;
let s be Element of S;
assume A1: F is_homomorphism U1,U2 & F is order-sorted;
func OSHomQuot(F,s) -> Function of
(the Sorts of (QuotOSAlg (U1,OSCng F))).s,(the Sorts of U2).s means:Def26:
for x be Element of (the Sorts of U1).s holds
it.(OSClass(OSCng(F),x)) = (F.s).x;
existence
proof
set qa = QuotOSAlg (U1,OSCng F),
cqa = the Sorts of qa,
S1 = the Sorts of U1,
S2 = the Sorts of U2;
qa = MSAlgebra (# OSClass OSCng(F),OSQuotCharact OSCng(F) #)
by Def22;
then A2: cqa.s = OSClass (OSCng(F),s) by Def13;
defpred P[set,set] means
for a be Element of S1.s st $1 = OSClass(OSCng(F),a) holds
$2 = (F.s).a;
A3: for x be set st x in cqa.s ex y be set st y in S2.s & P[x,y]
proof
let x be set;
assume x in cqa.s;
then consider a being set such that
A4: a in (the Sorts of U1).s &
x = Class( CompClass(OSCng(F),CComp(s)), a) by A2,Def12;
reconsider a as Element of S1.s by A4;
take y = (F.s).a;
thus y in S2.s;
A5: x = OSClass(OSCng(F),a) by A4,Def14;
let b be Element of S1.s; assume
x = OSClass(OSCng(F),b);
then [b,a] in (OSCng(F)).s by A5,Th13;
then [b,a] in (MSCng(F)).s by A1,Def25;
then [b,a] in MSCng(F,s) by A1,MSUALG_4:def 20;
hence thesis by MSUALG_4:def 19;
end;
consider G being Function such that
A6: dom G = cqa.s & rng G c= S2.s & for x be set st x in cqa.s
holds P[x,G.x] from NonUniqBoundFuncEx(A3);
reconsider G as Function of cqa.s,S2.s by A6,FUNCT_2:def 1,RELSET_1:11;
take G;
let a be Element of S1.s;
thus G.(OSClass(OSCng(F),a)) = (F.s).a by A2,A6;
end;
uniqueness
proof
set qa = QuotOSAlg (U1, OSCng F),
cqa = the Sorts of qa,
u1 = the Sorts of U1,
u2 = the Sorts of U2;
qa = MSAlgebra (# OSClass OSCng(F),OSQuotCharact OSCng(F) #)
by Def22;
then A7: cqa.s = OSClass (OSCng(F),s) by Def13;
let H,G be Function of cqa.s,u2.s;
assume that
A8: for a be Element of u1.s holds
H.(OSClass(OSCng(F),a)) = (F.s).a and
A9: for a be Element of u1.s holds
G.(OSClass(OSCng(F),a)) = (F.s).a;
for x be set st x in cqa.s holds H.x = G.x
proof
let x be set;
assume x in cqa.s;
then consider y being set such that
A10: y in (the Sorts of U1).s &
x = Class( CompClass(OSCng(F),CComp(s)), y) by A7,Def12;
reconsider y1 = y as Element of u1.s by A10;
A11: OSClass(OSCng(F),y1) = x by A10,Def14;
hence H.x = (F.s).y1 by A8 .= G.x by A9,A11;
end;
hence thesis by FUNCT_2:18;
end;
end;
:: this seems a bit too permissive, but same as the original
:: we should assume F order-sorted probably
definition let S; let U1,U2 be non-empty OSAlgebra of S;
let F be ManySortedFunction of U1,U2;
func OSHomQuot(F) ->
ManySortedFunction of (QuotOSAlg (U1, OSCng F)),U2 means :Def27:
for s be Element of S holds it.s = OSHomQuot(F,s);
existence
proof
deffunc F(Element of S) = OSHomQuot(F,$1);
consider f be Function such that A1: dom f = the carrier of S &
for d be Element of S holds f.d = F(d)
from LambdaB;
reconsider f as ManySortedSet of the carrier of S
by A1,PBOOLE:def 3;
for x be set st x in dom f holds f.x is Function
proof
let x be set;
assume x in dom f;
then reconsider y = x as Element of S by A1;
f.y = OSHomQuot(F,y) by A1;
hence thesis;
end;
then reconsider f as ManySortedFunction of the carrier of S
by PRALG_1:def 15;
for i be set st i in the carrier of S holds
f.i is Function of
(the Sorts of QuotOSAlg (U1, OSCng F)).i, (the Sorts of U2).i
proof
let i be set;
assume i in the carrier of S;
then reconsider s = i as Element of S;
f.s = OSHomQuot(F,s) by A1;
hence thesis;
end;
then reconsider f as ManySortedFunction of
the Sorts of QuotOSAlg (U1,OSCng F),the Sorts of U2
by MSUALG_1:def 2;
reconsider f as ManySortedFunction of QuotOSAlg (U1,OSCng F),U2;
take f;
thus thesis by A1;
end;
uniqueness
proof
let H,G be ManySortedFunction of QuotOSAlg (U1,OSCng F),U2;
assume that
A2: for s be Element of S holds H.s = OSHomQuot(F,s) and
A3: for s be Element of S holds G.s = OSHomQuot(F,s);
now
let i be set;
assume i in the carrier of S;
then reconsider s = i as SortSymbol of S;
H.s = OSHomQuot(F,s) & G.s = OSHomQuot(F,s) by A2,A3; hence H.i = G.i;
end;
hence thesis by PBOOLE:3;
end;
end;
theorem Th18:
for U1,U2 be non-empty OSAlgebra of S,
F be ManySortedFunction of U1,U2 st
F is_homomorphism U1,U2 & F is order-sorted holds
OSHomQuot(F) is_monomorphism QuotOSAlg (U1,OSCng F),U2 &
OSHomQuot(F) is order-sorted
proof
let U1,U2 be non-empty OSAlgebra of S,
F be ManySortedFunction of U1,U2;
set mc = OSCng(F),
qa = QuotOSAlg (U1,mc),
qh = OSHomQuot(F),
S1 = the Sorts of U1;
assume A1: F is_homomorphism U1,U2 & F is order-sorted;
A2: qa = MSAlgebra (# OSClass mc, OSQuotCharact mc #) by Def22;
for o be Element of the OperSymbols of S st Args (o,qa) <> {}
for x be Element of Args(o,qa) holds
(qh.(the_result_sort_of o)).(Den(o,qa).x) = Den(o,U2).(qh#x)
proof
let o be Element of the OperSymbols of S such that Args (o,qa) <> {};
let x be Element of Args(o,qa);
reconsider o1 = o as OperSymbol of S;
set ro = the_result_sort_of o,
ar = the_arity_of o;
A3: Den(o,qa) = (OSQuotCharact mc).o by A2,MSUALG_1:def 11
.= OSQuotCharact(mc,o1) by Def21;
Args(o,qa) = ((OSClass mc)# * (the Arity of S)).o
by A2,MSUALG_1:def 9;
then consider a be Element of Args(o,U1) such that
A4: x = mc #_os a by Th15;
A5: dom Den(o,U1) = Args(o,U1) & rng Den(o,U1) c= Result(o,U1)
by FUNCT_2:def 1;
o in the OperSymbols of S;
then o in dom (S1 * the ResultSort of S) by PBOOLE:def 3;
then A6: ((the Sorts of U1) * the ResultSort of S).o
= (the Sorts of U1).((the ResultSort of S).o)
by FUNCT_1:22
.= (the Sorts of U1).ro by MSUALG_1:def 7;
then A7: Result(o,U1) = S1.ro by MSUALG_1:def 10;
reconsider da = (Den(o,U1)).a as Element of S1.ro by A6,MSUALG_1:def 10;
A8: qh.ro = OSHomQuot(F,ro) by Def27;
rng Den(o,U1) c= dom OSQuotRes(mc,o)
by A5,A6,A7,FUNCT_2:def 1;
then A9: dom ((OSQuotRes(mc,o)) * Den(o,U1)) = dom Den(o,U1)
by RELAT_1:46;
A10: dom (qh # x) = dom ar & dom (F # a) = dom ar &
dom x = dom ar & dom a = dom ar by MSUALG_3:6;
A11: now
let y be set;
assume A12: y in dom ar;
then reconsider n = y as Nat;
A13: ar/.n = ar.n by A12,FINSEQ_4:def 4;
ar.n in rng ar by A12,FUNCT_1:def 5;
then reconsider s = ar.n as SortSymbol of S;
consider an being Element of S1.s such that
A14: an = a.n & x.n = OSClass(mc,an) by A4,A12,A13,Def15;
(qh # x).n = (qh.s).(x.n) by A10,A12,A13,MSUALG_3:def 8
.= OSHomQuot(F,s).OSClass(mc,an) by A14,Def27
.= (F.s).an by A1,Def26
.= (F # a).n by A10,A12,A13,A14,MSUALG_3:def 8;
hence (qh # x).y = (F # a).y;
end;
ar = (the Arity of S).o by MSUALG_1:def 6;
then product((OSClass mc) * ar) =
((OSClass mc)# * the Arity of S).o by MSAFREE:1;
then Den(o,qa).x = (OSQuotRes(mc,o) * Den(o,U1)).a by A3,A4,Def20
.= (OSQuotRes(mc,o)) . da by A5,A9,FUNCT_1:22
.= OSClass (OSCng(F),da) by Def16;
then (qh.ro).(Den(o,qa).x) = (F.ro).((Den(o,U1)).a) by A1,A8,Def26
.= Den(o,U2).(F#a) by A1,MSUALG_3:def 9;
hence thesis by A10,A11,FUNCT_1:9;
end;
hence qh is_homomorphism qa,U2 by MSUALG_3:def 9;
for i be set st i in the carrier of S
holds (qh.i) is one-to-one
proof
let i be set;
set f = qh.i;
assume i in the carrier of S;
then reconsider s = i as SortSymbol of S;
A15: f = OSHomQuot(F,s) by Def27;
for x1,x2 be set st x1 in dom f & x2 in dom f & f.x1 = f.x2
holds x1 = x2
proof
let x1,x2 be set;
assume A16: x1 in dom f & x2 in dom f & f.x1 = f.x2;
then x1 in (OSClass mc).s & x2 in
(OSClass mc).s by A2,A15,FUNCT_2:def 1;
then A17: x1 in OSClass (mc,s) & x2 in OSClass (mc,s) by Def13;
then consider a1 being set such that
A18: a1 in S1.s &
x1 = Class( CompClass(OSCng(F),CComp(s)), a1) by Def12;
consider a2 being set such that
A19: a2 in S1.s &
x2 = Class( CompClass(OSCng(F),CComp(s)), a2) by A17,Def12;
reconsider a1 as Element of S1.s by A18;
reconsider a2 as Element of S1.s by A19;
A20: x1 = OSClass(OSCng(F),a1) & x2 = OSClass(OSCng(F),a2)
by A18,A19,Def14;
(F.s).a1 = f.(OSClass(OSCng(F),a1)) &
(F.s).a2 = f.(OSClass(OSCng(F),a2)) by A1,A15,Def26;
then [a1,a2] in MSCng(F,s) by A16,A20,MSUALG_4:def 19;
then [a1,a2] in (MSCng(F)).s by A1,MSUALG_4:def 20;
then [a1,a2] in (OSCng(F)).s by A1,Def25;
hence thesis by A20,Th13;
end;
hence thesis by FUNCT_1:def 8;
end;
hence qh is "1-1" by MSUALG_3:1;
thus OSHomQuot(F) is order-sorted
proof
let s1,s2 being Element of S such that A21: s1 <= s2;
let a1 be set such that A22: a1 in dom (qh.s1);
reconsider sqa = the Sorts of qa as OrderSortedSet of S by OSALG_1:17;
reconsider S1O = S1 as OrderSortedSet of S by OSALG_1:17;
A23: S1O.s1 c= S1O.s2 by A21,OSALG_1:def 18;
A24: dom (qh.s1) = (the Sorts of qa).s1 &
dom (qh.s2) = (the Sorts of qa).s2 by FUNCT_2:def 1;
sqa.s1 c= sqa.s2 by A21,OSALG_1:def 18;
hence a1 in dom (qh.s2) by A22,A24;
qa = MSAlgebra(# OSClass mc, OSQuotCharact mc #) by Def22;
then a1 in (OSClass OSCng(F)).s1 by A22;
then a1 in OSClass (OSCng(F),s1) by Def13;
then consider x being set such that
A25: x in S1.s1 and
A26: a1 = Class( CompClass(OSCng(F),CComp(s1)), x) by Def12;
reconsider x1 = x as Element of S1.s1 by A25;
reconsider x2 = x as Element of S1.s2 by A23,A25;
reconsider s3 = s1, s4 = s2 as Element of S;
x1 in dom (F.s3) by A25,FUNCT_2:def 1;
then A27: x1 in dom (F.s4) &
(F.s3).x1 = (F.s4).x1 by A1,A21,OSALG_3:def 1;
A28: a1 = OSClass(OSCng(F),x1) by A26,Def14;
then A29: a1 = OSClass(OSCng(F),x2) by A21,Th14;
thus (qh.s1).a1 = OSHomQuot(F,s1).(OSClass(OSCng(F),x1)) by A28,Def27
.= (F.s2).x1 by A1,A27,Def26 .=
OSHomQuot(F,s2).(OSClass(OSCng(F),x2)) by A1,Def26
.= (qh.s2).a1 by A29,Def27;
end;
end;
theorem Th19:
for U1,U2 be non-empty OSAlgebra of S,
F be ManySortedFunction of U1,U2 st
F is_epimorphism U1,U2 & F is order-sorted holds
OSHomQuot(F) is_isomorphism QuotOSAlg (U1,OSCng F),U2
proof
let U1,U2 be non-empty OSAlgebra of S,
F be ManySortedFunction of U1,U2;
set mc = OSCng(F),
qa = QuotOSAlg (U1,mc),
qh = OSHomQuot(F);
assume A1: F is_epimorphism U1,U2 & F is order-sorted;
then A2: F is_homomorphism U1,U2 & F is "onto"
by MSUALG_3:def 10;
then qh is_monomorphism qa,U2 by A1,Th18;
then A3: qh is_homomorphism qa,U2 & qh is "1-1" by MSUALG_3:def 11;
set Sq = the Sorts of qa,
S1 = the Sorts of U1,
S2 = the Sorts of U2;
for i be set st i in the carrier of S holds rng (qh.i) = S2.i
proof
let i be set;
set f = qh.i;
assume i in the carrier of S;
then reconsider s = i as SortSymbol of S;
A4: qh.i = OSHomQuot(F,s) by Def27;
then A5: dom f = Sq.s & rng f c= S2.s by FUNCT_2:def 1,RELSET_1:12;
thus rng f c= S2.i by A4,RELSET_1:12;
A6: rng (F.s) = S2.s by A2,MSUALG_3:def 3;
let x be set;
assume x in S2.i;
then consider a be set such that
A7: a in dom (F.s) & (F.s).a = x by A6,FUNCT_1:def 5;
reconsider a as Element of S1.s by A7;
A8: f.(OSClass(OSCng(F),a)) = x by A1,A2,A4,A7,Def26;
qa = MSAlgebra(#OSClass OSCng(F),OSQuotCharact OSCng(F)#)
by Def22;
then Sq.s = OSClass (OSCng(F),s) by Def13;
hence thesis by A5,A8,FUNCT_1:def 5;
end;
then qh is "onto" by MSUALG_3:def 3;
hence thesis by A3,MSUALG_3:13;
end;
theorem
for U1,U2 be non-empty OSAlgebra of S,
F be ManySortedFunction of U1,U2 st
F is_epimorphism U1,U2 & F is order-sorted holds
QuotOSAlg (U1,OSCng F),U2 are_isomorphic
proof
let U1,U2 be non-empty OSAlgebra of S,
F be ManySortedFunction of U1,U2;
assume F is_epimorphism U1,U2 & F is order-sorted;
then OSHomQuot(F) is_isomorphism QuotOSAlg (U1,OSCng F),U2 by Th19;
hence thesis by MSUALG_3:def 13;
end;
:: monotone OSCongruence ... monotonicity is properly stronger
:: than MSCongruence, so we define it more broadly and prove the
:: ccluster then, however if used for other things than OSCongruences
:: the name of the attribute should be changed
:: this condition is nontrivial only for nonmonotone osas (see further),
:: where Den(o1,U1).x1 can differ from Den(o2,U2).x1
:: is OK for constants ... their Args is always {{}}, so o1 <= o2
:: implies for them [Den(o1,U1).{},Den(o2,U1).{}] in R
definition
let S be OrderSortedSign,
U1 be non-empty OSAlgebra of S,
R be MSEquivalence-like OrderSortedRelation of U1;
attr R is monotone means :Def28:
for o1,o2 being OperSymbol of S st o1 <= o2
for x1 being Element of Args(o1,U1)
for x2 being Element of Args(o2,U1) st
( for y being Nat st y in dom x1 holds
[x1.y,x2.y] in R.((the_arity_of o2)/.y)
)
holds [Den(o1,U1).x1,Den(o2,U1).x2] in R.(the_result_sort_of o2);
end;
theorem Th21:
for S being OrderSortedSign,
U1 being non-empty OSAlgebra of S holds
[| the Sorts of U1, the Sorts of U1 |] is OSCongruence of U1
proof
let S be OrderSortedSign,
U1 be non-empty OSAlgebra of S;
reconsider C = [| the Sorts of U1, the Sorts of U1 |] as
MSCongruence of U1 by MSUALG_5:20;
C is os-compatible
proof
let s1,s2 be Element of S such that A1: s1 <= s2;
reconsider s3 = s1, s4 = s2 as Element of S;
let x,y be set such that A2: x in (the Sorts of U1).s1 &
y in (the Sorts of U1).s1;
reconsider O1 = (the Sorts of U1) as OrderSortedSet of S by OSALG_1:17;
A3: O1.s3 c= O1.s4 by A1,OSALG_1:def 18;
C.s1 = [:(the Sorts of U1).s1,(the Sorts of U1).s1:] &
C.s2 = [:(the Sorts of U1).s2,(the Sorts of U1).s2:] by PRALG_2:def 9;
hence [x,y] in C.s1 iff [x,y] in C.s2 by A2,A3,ZFMISC_1:106;
end;
hence [| the Sorts of U1, the Sorts of U1 |] is OSCongruence of U1
by Def3;
end;
theorem Th22:
for S being OrderSortedSign,
U1 being non-empty OSAlgebra of S,
R being OSCongruence of U1 st
R = [| (the Sorts of U1), (the Sorts of U1) |] holds
R is monotone
proof
let S be OrderSortedSign,
U1 be non-empty OSAlgebra of S,
R be OSCongruence of U1 such that
A1: R = [| (the Sorts of U1), (the Sorts of U1) |];
let o1,o2 be OperSymbol of S such that A2: o1 <= o2;
let x1 be Element of Args(o1,U1);
let x2 be Element of Args(o2,U1) such that
for y being Nat st y in dom x1 holds
[x1.y,x2.y] in R.((the_arity_of o2)/.y);
set s2 = the_result_sort_of o2, s1 = the_result_sort_of o1;
A3: s1 <= s2 by A2,OSALG_1:def 22;
reconsider O1 = the Sorts of U1 as OrderSortedSet of S by OSALG_1:17;
A4: O1.s1 c= O1.s2 by A3,OSALG_1:def 18;
Den(o1,U1).x1 in (the Sorts of U1).s1 by MSUALG_9:19;
then A5: Den(o1,U1).x1 in (the Sorts of U1).s2 &
Den(o2,U1).x2 in (the Sorts of U1).s2 by A4,MSUALG_9:19;
R.s2 = [:(the Sorts of U1).s2,(the Sorts of U1).s2:] by A1,PRALG_2:def 9;
hence [Den(o1,U1).x1,Den(o2,U1).x2] in R.(the_result_sort_of o2)
by A5,ZFMISC_1:106;
end;
definition
let S be OrderSortedSign,
U1 be non-empty OSAlgebra of S;
cluster monotone OSCongruence of U1;
existence
proof reconsider R = [| the Sorts of U1, the Sorts of U1 |] as
OSCongruence of U1 by Th21;
take R;
thus thesis by Th22;
end;
end;
definition
let S be OrderSortedSign,
U1 be non-empty OSAlgebra of S;
cluster monotone (MSEquivalence-like OrderSortedRelation of U1);
existence
proof consider R being monotone OSCongruence of U1;
take R;
thus thesis;
end;
end;
theorem Th23:
for S being OrderSortedSign,
U1 being non-empty OSAlgebra of S,
R being monotone (MSEquivalence-like OrderSortedRelation of U1)
holds R is MSCongruence-like
proof
let S be OrderSortedSign,
U1 be non-empty OSAlgebra of S,
R be monotone (MSEquivalence-like OrderSortedRelation of U1);
for o be (Element of the OperSymbols of S),
x,y be Element of Args(o,U1) st
(for n be Nat st n in dom x holds
[x.n,y.n] in R.((the_arity_of o)/.n))
holds [Den(o,U1).x,Den(o,U1).y] in R.(the_result_sort_of o) by Def28;
hence R is MSCongruence-like by MSUALG_4:def 6;
end;
definition
let S be OrderSortedSign,
U1 be non-empty OSAlgebra of S;
cluster monotone -> MSCongruence-like
(MSEquivalence-like OrderSortedRelation of U1);
coherence by Th23;
end;
theorem Th24:
for S being OrderSortedSign,
U1 being monotone non-empty OSAlgebra of S,
R being OSCongruence of U1 holds
R is monotone
proof
let S be OrderSortedSign,
U1 be monotone non-empty OSAlgebra of S,
R be OSCongruence of U1;
let o1,o2 be OperSymbol of S such that A1: o1 <= o2;
let x1 be Element of Args(o1,U1);
let x2 be Element of Args(o2,U1) such that
A2: for y being Nat st y in dom x1 holds
[x1.y,x2.y] in R.((the_arity_of o2)/.y);
A3: Den(o1,U1) c= Den(o2,U1) by A1,OSALG_1:27;
Args(o1,U1) c= Args(o2,U1) by A1,OSALG_1:26;
then reconsider x3 = x1 as Element of Args(o2,U1) by TARSKI:def 3;
A4: [Den(o2,U1).x3,Den(o2,U1).x2] in R.(the_result_sort_of o2)
by A2,MSUALG_4:def 6;
x1 in Args(o1,U1);
then x1 in dom Den(o1,U1) by FUNCT_2:def 1;
hence [Den(o1,U1).x1,Den(o2,U1).x2] in R.(the_result_sort_of o2) by A3,A4,
GRFUNC_1:8;
end;
definition
let S be OrderSortedSign,
U1 be monotone non-empty OSAlgebra of S;
cluster -> monotone OSCongruence of U1;
coherence by Th24;
end;
:: monotonicity of quotient by monotone oscongruence
definition let S;
let U1 be non-empty OSAlgebra of S;
let R be monotone OSCongruence of U1;
cluster QuotOSAlg(U1,R) -> monotone;
coherence
proof
set A = QuotOSAlg(U1,R);
A1: A = MSAlgebra(# OSClass R, OSQuotCharact R #) by Def22;
reconsider O1 = the Sorts of U1 as OrderSortedSet of S by OSALG_1:17;
let o1,o2 be OperSymbol of S such that A2: o1 <= o2;
A3: o1 ~= o2 & (the_arity_of o1) <= (the_arity_of o2) &
the_result_sort_of o1 <= the_result_sort_of o2 by A2,OSALG_1:def 22;
A4: dom Den(o2,A) = Args(o2,A) &
dom Den(o1,A) = Args(o1,A) by FUNCT_2:def 1;
A5: Args(o1,A) c= Args(o2,A) &
Result(o1,A) c= Result(o2,A) by A2,OSALG_1:26;
then A6: dom Den(o1,A) = (dom Den(o2,A)) /\ Args(o1,A) by A4,XBOOLE_1:28;
Den(o1,A) = (OSQuotCharact R).o1 &
Den(o2,A) = (OSQuotCharact R).o2 by A1,MSUALG_1:def 11;
then A7: Den(o1,A) = OSQuotCharact( R,o1) &
Den(o2,A) = OSQuotCharact( R,o2) by Def21;
A8: O1.(the_result_sort_of o1) c= O1.(the_result_sort_of o2)
by A3,OSALG_1:def 19;
o1 in the OperSymbols of S &
o2 in the OperSymbols of S;
then A9: o1 in dom (the ResultSort of S) &
o2 in dom (the ResultSort of S) by FUNCT_2:def 1;
len (the_arity_of o1) = len (the_arity_of o2) by A3,OSALG_1:def 7;
then A10: dom (the_arity_of o1) = dom (the_arity_of o2) by FINSEQ_3:31;
for x being set st x in dom Den(o1,A) holds Den(o1,A).x = Den(o2,A).x
proof
let x be set such that A11: x in dom Den(o1,A);
A12: x in Args(o1,A) by A11;
then x in Args(o2,A) by A5;
then A13: x in ((OSClass R)# * the Arity of S).o1 &
x in ((OSClass R)# * the Arity of S).o2 by A1,A12,MSUALG_1:def 9;
then consider a1 being Element of Args(o1,U1) such that
A14: x = R #_os a1 by Th15;
consider a2 being Element of Args(o2,U1) such that
A15: x = R #_os a2 by A13,Th15;
for y being Nat st y in dom a1 holds
[a1.y,a2.y] in R.((the_arity_of o2)/.y)
proof
let y be Nat such that A16: y in dom a1;
A17: y in dom (the_arity_of o1) &
y in dom (the_arity_of o2) by A10,A16,MSUALG_6:2;
then consider z1 being Element of (the Sorts of U1).((the_arity_of o1)/.y
)
such that A18: z1 = a1.y & (R #_os a1).y = OSClass(R, z1) by Def15;
consider z2 being
Element of (the Sorts of U1).((the_arity_of o2)/.y) such that
A19: z2 = a2.y & (R #_os a2).y = OSClass(R, z2) by A17,Def15;
A20: (the_arity_of o1)/.y = (the_arity_of o1).y &
(the_arity_of o2)/.y = (the_arity_of o2).y by A17,FINSEQ_4:def 4;
reconsider s1 = (the_arity_of o1).y,
s2 = (the_arity_of o2).y as SortSymbol of S by A17,PARTFUN1:27;
A21: s1 <= s2 by A3,A17,OSALG_1:def 7;
then (the Sorts of U1).((the_arity_of o1)/.y) c=
(the Sorts of U1).((the_arity_of o2)/.y) by A20,OSALG_1:def 19;
then reconsider z12 = z1 as
Element of (the Sorts of U1).((the_arity_of o2)/.y) by TARSKI:def 3;
OSClass(R, z2) = OSClass(R, z12) by A14,A15,A18,A19,A20,A21,Th14;
hence [a1.y,a2.y] in R.((the_arity_of o2)/.y) by A18,A19,Th13;
end;
then A22: [Den(o1,U1).a1,Den(o2,U1).a2] in R.(the_result_sort_of o2)
by A2,Def28;
A23: OSQuotCharact(R,o1).(R #_os a1) =
((OSQuotRes(R,o1)) * (Den(o1,U1))).a1 &
OSQuotCharact(R,o2).(R #_os a2) =
((OSQuotRes(R,o2)) * (Den(o2,U1))).a2 by A13,A14,A15,Def20;
Result(o1,U1) =
((the Sorts of U1) * the ResultSort of S).o1 by MSUALG_1:def 10
.= (the Sorts of U1).((the ResultSort of S).o1) by A9,FUNCT_1:23
.= (the Sorts of U1).(the_result_sort_of o1) by MSUALG_1:def 7;
then reconsider da1 = Den(o1,U1).a1 as
Element of (the Sorts of U1).(the_result_sort_of o1);
a1 in Args(o1,U1);
then a1 in dom Den(o1,U1) by FUNCT_2:def 1;
then A24: ((OSQuotRes(R,o1)) * (Den(o1,U1))).a1 = OSQuotRes(R,o1).da1 by
FUNCT_1:23
.= OSClass(R,da1) by Def16;
Result(o2,U1) =
((the Sorts of U1) * the ResultSort of S).o2 by MSUALG_1:def 10
.= (the Sorts of U1).((the ResultSort of S).o2) by A9,FUNCT_1:23
.= (the Sorts of U1).(the_result_sort_of o2) by MSUALG_1:def 7;
then reconsider da2 = Den(o2,U1).a2 as
Element of (the Sorts of U1).(the_result_sort_of o2);
a2 in Args(o2,U1);
then a2 in dom Den(o2,U1) by FUNCT_2:def 1;
then A25: ((OSQuotRes(R,o2)) * (Den(o2,U1))).a2 = OSQuotRes(R,o2).da2 by
FUNCT_1:23
.= OSClass(R,da2) by Def16;
reconsider da12 = da1 as
Element of (the Sorts of U1).(the_result_sort_of o2) by A8,TARSKI:def 3;
OSClass(R,da1) = OSClass(R,da12) by A3,Th14
.= OSClass(R,da2) by A22,Th13;
hence Den(o1,A).x = Den(o2,A).x by A7,A14,A15,A23,A24,A25;
end;
hence Den(o2,A)|Args(o1,A) = Den(o1,A) by A6,FUNCT_1:68;
end;
end;
theorem
for S ::being locally_directed OrderSortedSign,
for U1 be non-empty OSAlgebra of S,
R be monotone OSCongruence of U1 holds
QuotOSAlg(U1,R) is monotone OSAlgebra of S;
theorem
for U1 being non-empty OSAlgebra of S,
U2 being monotone non-empty OSAlgebra of S,
F being ManySortedFunction of U1,U2 st
F is_homomorphism U1,U2 & F is order-sorted holds
OSCng(F) is monotone
proof
let U1 be non-empty OSAlgebra of S,
U2 be monotone non-empty OSAlgebra of S,
F be ManySortedFunction of U1,U2 such that
A1: F is_homomorphism U1,U2 & F is order-sorted;
set O1 = the Sorts of U1;
reconsider S1 = the Sorts of U1 as OrderSortedSet of S by OSALG_1:17;
let o1,o2 being OperSymbol of S such that A2: o1 <= o2;
set R = OSCng(F), w1 = the_arity_of o1, w2 = the_arity_of o2,
rs1 = the_result_sort_of o1, rs2 = the_result_sort_of o2;
let x1 being (Element of Args(o1,U1)),
x2 being Element of Args(o2,U1) such that
A3: for y being Nat st y in dom x1 holds
[x1.y,x2.y] in R.((the_arity_of o2)/.y);
set D1 = Den(o1,U1).x1, D2 = Den(o2,U1).x2, M = MSCng(F);
A4: M.rs1 = MSCng(F,rs1) & M.rs2 = MSCng(F,rs2)
& M = R by A1,Def25,MSUALG_4:def 20;
A5: Args(o1,U1) c= Args(o2,U1)
& Result(o1,U1) c= Result(o2,U1) by A2,OSALG_1:26;
A6: w1 <= w2 & rs1 <= rs2 by A2,OSALG_1:def 22;
then A7: S1.rs1 c= S1.rs2 by OSALG_1:def 18;
reconsider x12=x1 as Element of Args(o2,U1) by A5,TARSKI:def 3;
A8: [Den(o2,U1).x12,Den(o2,U1).x2] in R.rs2 by A3,MSUALG_4:def 6;
A9: D2 in O1.rs2 & Den(o2,U1).x12 in O1.rs2
& D1 in S1.rs1 by MSUALG_9:19;
then A10: D1 in S1.rs2
& D1 in dom (F.rs1) by A7,FUNCT_2:def 1;
reconsider D11=D1,D12=Den(o2,U1).x12 as Element of O1.rs2 by A7,A9;
F#x1 in Args(o1,U2);
then A11: F#x1 in dom Den(o1,U2) by FUNCT_2:def 1;
A12: Den(o2,U2)|Args(o1,U2) = Den(o1,U2) by A2,OSALG_1:def 23;
(F.rs2).(Den(o1,U1).x1)
= (F.rs1).(Den(o1,U1).x1) by A1,A6,A10,OSALG_3:def 1
.= Den(o1,U2).(F#x1) by A1,MSUALG_3:def 9
.= Den(o2,U2).(F#x1) by A11,A12,FUNCT_1:68
.= Den(o2,U2).(F#x12) by A1,A2,OSALG_3:13
.= (F.rs2).(Den(o2,U1).x12) by A1,MSUALG_3:def 9;
then A13: [D11,D12] in MSCng(F,rs2) by MSUALG_4:def 19;
field(R.rs2) = (O1.rs2) by ORDERS_1:97;
then (R.rs2) is_transitive_in (O1.rs2) by RELAT_2:def 16;
hence [Den(o1,U1).x1,Den(o2,U1).x2] in R.rs2
by A4,A8,A9,A13,RELAT_2:def 8;
end;
:: these are a bit more general versions of OSHomQuot, that
:: I need for OSAFREE; more proper way how to do this is restating
:: the MSUALG_9 quotient theorems for OSAs, but that's more work
definition let S; let U1,U2 be non-empty OSAlgebra of S;
let F be ManySortedFunction of U1,U2;
let R be OSCongruence of U1;
let s be Element of S;
assume A1: F is_homomorphism U1,U2 & F is order-sorted
& R c= OSCng F;
func OSHomQuot(F,R,s) -> Function of
(the Sorts of (QuotOSAlg (U1,R))).s,(the Sorts of U2).s means :Def29:
for x be Element of (the Sorts of U1).s holds
it.(OSClass(R,x)) = (F.s).x;
existence
proof
set qa = QuotOSAlg (U1,R),
cqa = the Sorts of qa,
S1 = the Sorts of U1,
S2 = the Sorts of U2;
qa = MSAlgebra (# OSClass R,OSQuotCharact R #)
by Def22;
then A2: cqa.s = OSClass (R,s) by Def13;
defpred P[set,set] means
for a be Element of S1.s st $1 = OSClass(R,a) holds
$2 = (F.s).a;
A3: for x be set st x in cqa.s ex y be set st y in S2.s & P[x,y]
proof
let x be set;
assume x in cqa.s;
then consider a being set such that
A4: a in (the Sorts of U1).s &
x = Class( CompClass(R,CComp(s)), a) by A2,Def12;
reconsider a as Element of S1.s by A4;
take y = (F.s).a;
A5: R.s c= (OSCng F).s by A1,PBOOLE:def 5;
thus y in S2.s;
A6: x = OSClass(R,a) by A4,Def14;
let b be Element of S1.s; assume
x = OSClass(R,b);
then [b,a] in R.s by A6,Th13;
then [b,a] in (OSCng(F)).s by A5;
then [b,a] in (MSCng(F)).s by A1,Def25;
then [b,a] in MSCng(F,s) by A1,MSUALG_4:def 20;
hence thesis by MSUALG_4:def 19;
end;
consider G being Function such that
A7: dom G = cqa.s & rng G c= S2.s & for x be set st x in cqa.s
holds P[x,G.x] from NonUniqBoundFuncEx(A3);
reconsider G as Function of cqa.s,S2.s by A7,FUNCT_2:def 1,RELSET_1:11;
take G;
let a be Element of S1.s;
thus G.(OSClass(R,a)) = (F.s).a by A2,A7;
end;
uniqueness
proof
set qa = QuotOSAlg (U1, R),
cqa = the Sorts of qa,
u1 = the Sorts of U1,
u2 = the Sorts of U2;
qa = MSAlgebra (# OSClass R,OSQuotCharact R #)
by Def22;
then A8: cqa.s = OSClass (R,s) by Def13;
let H,G be Function of cqa.s,u2.s;
assume that
A9: for a be Element of u1.s holds
H.(OSClass(R,a)) = (F.s).a and
A10: for a be Element of u1.s holds
G.(OSClass(R,a)) = (F.s).a;
for x be set st x in cqa.s holds H.x = G.x
proof
let x be set;
assume x in cqa.s;
then consider y being set such that
A11: y in (the Sorts of U1).s &
x = Class( CompClass(R,CComp(s)), y) by A8,Def12;
reconsider y1 = y as Element of u1.s by A11;
A12: OSClass(R,y1) = x by A11,Def14;
hence H.x = (F.s).y1 by A9 .= G.x by A10,A12;
end;
hence thesis by FUNCT_2:18;
end;
end;
:: this seems a bit too permissive, but same as the original
:: we should assume F order-sorted probably
definition let S; let U1,U2 be non-empty OSAlgebra of S;
let F be ManySortedFunction of U1,U2;
let R be OSCongruence of U1;
func OSHomQuot(F,R) ->
ManySortedFunction of (QuotOSAlg (U1, R)),U2 means :Def30:
for s be Element of S holds it.s = OSHomQuot(F,R,s);
existence
proof
deffunc F(Element of S) = OSHomQuot(F,R,$1);
consider f be Function such that A1: dom f = the carrier of S &
for d be Element of S holds f.d = F(d)
from LambdaB;
reconsider f as ManySortedSet of the carrier of S
by A1,PBOOLE:def 3;
for x be set st x in dom f holds f.x is Function
proof
let x be set;
assume x in dom f;
then reconsider y = x as Element of S by A1;
f.y = OSHomQuot(F,R,y) by A1;
hence thesis;
end;
then reconsider f as ManySortedFunction of the carrier of S
by PRALG_1:def 15;
for i be set st i in the carrier of S holds
f.i is Function of
(the Sorts of QuotOSAlg (U1, R)).i, (the Sorts of U2).i
proof
let i be set;
assume i in the carrier of S;
then reconsider s = i as Element of S;
f.s = OSHomQuot(F,R,s) by A1;
hence thesis;
end;
then reconsider f as ManySortedFunction of
the Sorts of QuotOSAlg (U1,R),the Sorts of U2 by MSUALG_1:def 2;
reconsider f as ManySortedFunction of QuotOSAlg (U1,R),U2;
take f;
thus thesis by A1;
end;
uniqueness
proof
let H,G be ManySortedFunction of QuotOSAlg (U1,R),U2;
assume that
A2: for s be Element of S holds H.s = OSHomQuot(F,R,s) and
A3: for s be Element of S holds G.s = OSHomQuot(F,R,s);
now
let i be set;
assume i in the carrier of S;
then reconsider s = i as SortSymbol of S;
H.s = OSHomQuot(F,R,s) & G.s = OSHomQuot(F,R,s) by A2,A3; hence H.i = G.
i;
end;
hence thesis by PBOOLE:3;
end;
end;
theorem
for U1,U2 be non-empty OSAlgebra of S,
F be ManySortedFunction of U1,U2,
R be OSCongruence of U1 st
F is_homomorphism U1,U2 & F is order-sorted & R c= OSCng F
holds
OSHomQuot(F,R) is_homomorphism QuotOSAlg (U1,R),U2 &
OSHomQuot(F,R) is order-sorted
proof
let U1,U2 be non-empty OSAlgebra of S,
F be ManySortedFunction of U1,U2,
R be OSCongruence of U1;
set mc = R,
qa = QuotOSAlg (U1,mc),
qh = OSHomQuot(F,R),
S1 = the Sorts of U1;
assume A1: F is_homomorphism U1,U2 & F is order-sorted & R c= OSCng F;
A2: qa = MSAlgebra (# OSClass mc, OSQuotCharact mc #) by Def22;
for o be Element of the OperSymbols of S st Args (o,qa) <> {}
for x be Element of Args(o,qa) holds
(qh.(the_result_sort_of o)).(Den(o,qa).x) = Den(o,U2).(qh#x)
proof
let o be Element of the OperSymbols of S such that Args (o,qa) <> {};
let x be Element of Args(o,qa);
reconsider o1 = o as OperSymbol of S;
set ro = the_result_sort_of o,
ar = the_arity_of o;
A3: Den(o,qa) = (OSQuotCharact mc).o by A2,MSUALG_1:def 11
.= OSQuotCharact(mc,o1) by Def21;
Args(o,qa) = ((OSClass mc)# * (the Arity of S)).o
by A2,MSUALG_1:def 9;
then consider a be Element of Args(o,U1) such that
A4: x = mc #_os a by Th15;
A5: dom Den(o,U1) = Args(o,U1) & rng Den(o,U1) c= Result(o,U1)
by FUNCT_2:def 1;
o in the OperSymbols of S;
then o in dom (S1 * the ResultSort of S) by PBOOLE:def 3;
then A6: ((the Sorts of U1) * the ResultSort of S).o
= (the Sorts of U1).((the ResultSort of S).o)
by FUNCT_1:22
.= (the Sorts of U1).ro by MSUALG_1:def 7;
then A7: Result(o,U1) = S1.ro by MSUALG_1:def 10;
reconsider da = (Den(o,U1)).a as Element of S1.ro by A6,MSUALG_1:def 10;
A8: qh.ro = OSHomQuot(F,R,ro) by Def30;
rng Den(o,U1) c= dom OSQuotRes(mc,o)
by A5,A6,A7,FUNCT_2:def 1;
then A9: dom ((OSQuotRes(mc,o)) * Den(o,U1)) = dom Den(o,U1)
by RELAT_1:46;
A10: dom (qh # x) = dom ar & dom (F # a) = dom ar &
dom x = dom ar & dom a = dom ar by MSUALG_3:6;
A11: now
let y be set;
assume A12: y in dom ar;
then reconsider n = y as Nat;
A13: ar/.n = ar.n by A12,FINSEQ_4:def 4;
ar.n in rng ar by A12,FUNCT_1:def 5;
then reconsider s = ar.n as SortSymbol of S;
consider an being Element of S1.s such that
A14: an = a.n & x.n = OSClass(mc,an) by A4,A12,A13,Def15;
(qh # x).n = (qh.s).(x.n) by A10,A12,A13,MSUALG_3:def 8
.= OSHomQuot(F,R,s).OSClass(mc,an) by A14,Def30
.= (F.s).an by A1,Def29
.= (F # a).n by A10,A12,A13,A14,MSUALG_3:def 8;
hence (qh # x).y = (F # a).y;
end;
ar = (the Arity of S).o by MSUALG_1:def 6;
then product((OSClass mc) * ar) =
((OSClass mc)# * the Arity of S).o by MSAFREE:1;
then Den(o,qa).x = (OSQuotRes(mc,o) * Den(o,U1)).a by A3,A4,Def20
.= (OSQuotRes(mc,o)) . da by A5,A9,FUNCT_1:22
.= OSClass (R,da) by Def16;
then (qh.ro).(Den(o,qa).x) = (F.ro).((Den(o,U1)).a) by A1,A8,Def29
.= Den(o,U2).(F#a) by A1,MSUALG_3:def 9;
hence thesis by A10,A11,FUNCT_1:9;
end;
hence qh is_homomorphism qa,U2 by MSUALG_3:def 9;
thus OSHomQuot(F,R) is order-sorted
proof
let s1,s2 being Element of S such that A15: s1 <= s2;
let a1 be set such that A16: a1 in dom (qh.s1);
reconsider sqa = the Sorts of qa as OrderSortedSet of S by OSALG_1:17;
reconsider S1O = S1 as OrderSortedSet of S by OSALG_1:17;
A17: S1O.s1 c= S1O.s2 by A15,OSALG_1:def 18;
A18: dom (qh.s1) = (the Sorts of qa).s1 &
dom (qh.s2) = (the Sorts of qa).s2 by FUNCT_2:def 1;
sqa.s1 c= sqa.s2 by A15,OSALG_1:def 18;
hence a1 in dom (qh.s2) by A16,A18;
qa = MSAlgebra(# OSClass mc, OSQuotCharact mc #) by Def22;
then a1 in (OSClass R).s1 by A16;
then a1 in OSClass (R,s1) by Def13;
then consider x being set such that
A19: x in S1.s1 and
A20: a1 = Class( CompClass(R,CComp(s1)), x) by Def12;
reconsider x1 = x as Element of S1.s1 by A19;
reconsider x2 = x as Element of S1.s2 by A17,A19;
reconsider s3 = s1, s4 = s2 as Element of S;
x1 in dom (F.s3) by A19,FUNCT_2:def 1;
then A21: x1 in dom (F.s4) &
(F.s3).x1 = (F.s4).x1 by A1,A15,OSALG_3:def 1;
A22: a1 = OSClass(R,x1) by A20,Def14;
then A23: a1 = OSClass(R,x2) by A15,Th14;
thus (qh.s1).a1 = OSHomQuot(F,R,s1).(OSClass(R,x1)) by A22,Def30
.= (F.s2).x1 by A1,A21,Def29 .=
OSHomQuot(F,R,s2).(OSClass(R,x2)) by A1,Def29
.= (qh.s2).a1 by A23,Def30;
end;
end;