:: On Multiset Ordering :: by Grzegorz Bancerek :: :: Received December 31, 2015 :: Copyright (c) 2015-2019 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, RELAT_2, FINSET_1, ARYTM_1, ARYTM_3, FUNCT_1, PARTFUN1, BINOP_1, XXREAL_0, VALUED_0, NUMBERS, CARD_1, MESFUNC1, STRUCT_0, ALGSTR_0, MONOID_1, ORDERS_2, PRE_POLY, BAGORD_2, ZFMISC_1, NAT_1, FUNCOP_1, ORDERS_1, REWRITE1, FINSEQ_1, ORDINAL4, GROEB_1, CARD_3, INTERVA1, MIDSP_1, GRAPH_2, MCART_1, BAGORDER; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, DOMAIN_1, RELAT_1, RELAT_2, RELSET_1, NECKLACE, FUNCT_1, PARTFUN1, BINOP_1, CARD_1, FINSEQ_1, FINSEQ_2, FINSET_1, VALUED_0, NUMBERS, FUNCT_2, XXREAL_0, XCMPLX_0, NAT_1, NAT_D, REWRITE1, GRAPH_2, STRUCT_0, ALGSTR_0, MONOID_1, ORDERS_2, WAYBEL_4, PRE_POLY, FINSEQ_6; constructors DOMAIN_1, RELSET_1, NECKLACE, BINOP_2, WAYBEL_4, REWRITE1, GRAPH_2, NAT_D, MONOID_1, FINSEQ_6, PRE_POLY; registrations XBOOLE_0, SUBSET_1, RELSET_1, ORDINAL1, XREAL_0, VALUED_0, STRUCT_0, ORDERS_2, MONOID_0, CARD_1, PRE_POLY, FINSEQ_1, FINSET_1, REWRITE1, NAT_1, RELAT_1, XTUPLE_0, FINSEQ_6; requirements BOOLE, SUBSET, NUMERALS, ARITHM, REAL; definitions TARSKI, XBOOLE_0, RELAT_1, RELAT_2, FUNCT_1, RELSET_1, OPOSET_1, ORDERS_2, PBOOLE, PRE_POLY; equalities FINSEQ_1, STRUCT_0, PBOOLE; theorems TARSKI, XBOOLE_0, ZFMISC_1, NAT_1, NAT_2, NAT_D, GRAPH_2, FUNCT_1, PARTFUN1, FUNCT_2, ORDINAL1, XREAL_0, XREAL_1, XXREAL_0, VALUED_0, ORDERS_2, MONOID_0, MONOID_1, PRE_POLY, PBOOLE, FUNCOP_1, TREES_2, WAYBEL_4, NECKLACE, PREFER_1, YELLOW_0, FINSEQ_1, RELAT_2, RELSET_1, REWRITE1, FINSEQ_2, FINSEQ_3, FINSEQ_5, RELAT_1, XBOOLE_1, RFUNCT_1, BAGORDER, CARD_2, XTUPLE_0, FOMODEL0, TREES_1, FINSEQ_6; schemes RELSET_1, PARTFUN1, FINSEQ_1, FUNCT_2, NAT_1; begin theorem Th6: for m,n being Nat holds n = (m-'(m-'n))+(n-'m) proof let m,n be Nat; per cases; suppose m <= n; then A1: m-'n = 0 & n-'m = n-m by NAT_2:8,XREAL_1:233; then m-'(m-'n) = m by NAT_D:40; hence thesis by A1; end; suppose m > n; then n-'m = 0 & m-'(m-'n) = n & n+0 = n by NAT_D:58,NAT_2:8; hence thesis; end; end; theorem Lem1: for n,m being Nat holds m-'n >= m-n proof let n,m be Nat; thus thesis by XREAL_0:def 2; end; theorem Th5: for m,n,x,y being Nat st n = (m-'x)+y holds m-'n <= x & n-'m <= y proof let m,n,x,y be Nat such that A0: n = (m-'x)+y; per cases; suppose m <= n; then A1: m-'n = 0 & n-'m = n-m by NAT_2:8,XREAL_1:233; n <= m+y by A0,XREAL_1:6,NAT_D:35; hence thesis by A1,XREAL_1:20; end; suppose m > n; then A2: n-'m = 0 & m-'(m-'n) = n >= m-'x by A0,NAT_D:58,NAT_1:11,NAT_2:8; m-'(m-'n) = m-(m-'n) & m-'x >= m-x by Lem1,XREAL_1:233,NAT_D:35; then m-(m-'n) >= m-x by A2,XXREAL_0:2; hence thesis by XREAL_1:10,A2; end; end; theorem Th5A: for m,n,x,y being Nat st x <= m & n = (m-'x)+y holds x-'(m-'n) = y-'(n-'m) proof let m,n,x,y be Nat; assume Z0: x <= m; assume Z1: n = (m-'x)+y; then m-'n <= x & n-'m <= y by Th5; then A2: x-'(m-'n) = x-(m-'n) & y-'(n-'m) = y-(n-'m) by XREAL_1:233; A3: n-y = m-x by Z0,Z1,XREAL_1:233; per cases; suppose m <= n; then A4: m-'n = 0 & n-'m = n-m by NAT_2:8,XREAL_1:233; hence x-'(m-'n) = x by A2 .= y-n+m by A3 .= y-'(n-'m) by A2,A4; end; suppose m > n; then A5: n-'m = 0 & m-'n = m-n by NAT_2:8,XREAL_1:233; hence x-'(m-'n) = x-m+n by A2 .= y by A3 .= y-'(n-'m) by A2,A5; end; end; theorem Th14: for k,x1,x2,y1,y2 being Nat st x2 <= k & x1 <= (k-'x2)+y2 holds x2+(x1-'y2) <= k & (((k-'x2)+y2)-'x1)+y1 = (k-'(x2+(x1-'y2)))+((y2-'x1)+y1) proof let k,x1,x2,y1,y2 be Nat; assume Z0: x2 <= k; then A1: k-'x2 = k-x2 by XREAL_1:233; assume Z1: x1 <= (k-'x2)+y2; thus x2+(x1-'y2) <= k proof per cases; suppose x1 < y2; then x1-'y2 = 0 by NAT_2:8; hence thesis by Z0; end; suppose x1 >= y2; then x1-'y2 = x1-y2 by XREAL_1:233; then x1-'y2 <= (k-x2)+y2-y2 = k-x2 by A1,Z1,XREAL_1:9; then x2+(x1-'y2) <= k-x2+x2 by XREAL_1:6; hence thesis; end; end; then A2: k-'(x2+(x1-'y2)) = k-(x2+(x1-'y2)) & ((k-'x2)+y2)-'x1 = ((k-x2)+y2)-x1 by Z1,A1,XREAL_1:233; per cases; suppose x1 <= y2; then x1-'y2 = 0 & y2-'x1 = y2-x1 by XREAL_1:233,NAT_2:8; hence (((k-'x2)+y2)-'x1)+y1 = (k-'(x2+(x1-'y2)))+((y2-'x1)+y1) by A2; end; suppose x1 > y2; then y2-'x1 = 0 & x1-'y2 = x1-y2 by XREAL_1:233,NAT_2:8; hence (((k-'x2)+y2)-'x1)+y1 = (k-'(x2+(x1-'y2)))+((y2-'x1)+y1) by A2; end; end; theorem for x,y being Nat st x+y > 0 holds x > 0 or y > 0; reserve a,b for object, I,J for set; registration let I; let J be non empty set; cluster -> total for Function of I,J; coherence proof let f be Function of I,J; dom f = I by FUNCT_2:def 1; hence thesis by PARTFUN1:def 2; end; end; registration cluster asymmetric transitive non empty for RelStr; existence proof set X = {0}; set r = {}[:X,X:]; take R = RelStr(#X,r#); thus R is asymmetric proof let a,b; assume a in the carrier of R & b in the carrier of R; thus thesis; end; thus R is transitive proof let a; thus thesis; end; thus thesis; end; end; registration let I; cluster asymmetric transitive for Relation of I; existence proof set X = I; take r = {}[:X,X:]; thus r is asymmetric proof let a,b; thus thesis; end; thus r is transitive proof let a; thus thesis; end; end; end; registration let R be transitive RelStr; cluster the InternalRel of R -> transitive; coherence proof let a,b,c be object; assume A1: a in field the InternalRel of R & b in field the InternalRel of R & c in field the InternalRel of R; field the InternalRel of R c= (the carrier of R)\/the carrier of R by RELSET_1:8; hence thesis by A1,RELAT_2:def 8,ORDERS_2:def 3; end; end; registration let R be asymmetric RelStr; cluster the InternalRel of R -> asymmetric; coherence by NECKLACE:def 4; end; registration let I; let p,q be I-valued FinSequence; cluster p^q -> I-valued; coherence proof rng p c= I & rng q c= I by RELAT_1:def 19; then rng (p^q) = rng p \/ rng q c= I by FINSEQ_1:31,XBOOLE_1:8; hence rng (p^q) c= I; end; end; theorem Lem8: for p,q being FinSequence st p^q is I-valued holds p is I-valued & q is I-valued proof let p,q be FinSequence; assume Z1: rng (p^q) c= I; A1: rng (p^q) = rng p \/ rng q by FINSEQ_1:31; rng p c= rng p \/ rng q by XBOOLE_1:7; hence rng p c= I by Z1,A1,XBOOLE_1:1; rng q c= rng p \/ rng q by XBOOLE_1:7; hence rng q c= I by Z1,A1,XBOOLE_1:1; end; registration let I; let f be I-valued FinSequence; let n be Nat; cluster f|n -> I-valued; coherence; end; theorem Lem9: for p being FinSequence st a in rng p ex q,r being FinSequence st p = q^<*a*>^r proof let p be FinSequence; assume a in rng p; then consider i being object such that A1: i in dom p & a = p.i by FUNCT_1:def 3; reconsider i as Nat by A1; A3: 1 <= i <= len p by A1,FINSEQ_3:25; consider k being Nat such that A2: i = 1+k by NAT_1:10,A1,FINSEQ_3:25; set q = (1,k)-cut p; set r = (i+1,len p)-cut p; take q,r; k <= i & (i,i)-cut p = <*a*> by A1,A3,A2,NAT_1:11, FINSEQ_6:132; hence p = q^<*a*>^r by A3,A2,FINSEQ_6:136; end; theorem Lem12: for p,q being FinSequence holds p c< q iff len p < len q & for i being Nat st i in dom p holds p.i = q.i proof let p,q be FinSequence; hereby assume Z0: p c< q; hence len p < len q by TREES_1:6; p c= q by Z0,XBOOLE_0:def 8; hence for i being Nat st i in dom p holds p.i = q.i by FOMODEL0:51; end; assume Z2: len p < len q; then dom p c< dom q by FINSEQ_3:118; then A1: dom p c= dom q by XBOOLE_0:def 8; assume for i being Nat st i in dom p holds p.i = q.i; then for i being set st i in dom p holds i in dom q & p.i = q.i by A1; hence p c< q by Z2,XBOOLE_0:def 8,FOMODEL0:51; end; theorem Lem13: for p,q,r being FinSequence holds r^p c< r^q iff p c< q proof let p,q,r be FinSequence; thus r^p c< r^q implies p c< q proof assume A0: r^p c< r^q; len(r^p) = len r+len p & len(r^q) = len r+len q by FINSEQ_1:22; then A2: len p < len q by A0,Lem12,XREAL_1:6; then A3: dom p c= dom q by FINSEQ_3:30; for i being Nat st i in dom p holds p.i = q.i proof let i be Nat; assume i in dom p; then p.i = (r^p).(len r+i) & q.i = (r^q).(len r+i) & len r+i in dom(r^p) by A3,FINSEQ_1:def 7,28; hence thesis by A0,Lem12; end; hence thesis by A2,Lem12; end; assume p c< q; then r^p c= r^q & r^p <> r^q by FINSEQ_6:13,FINSEQ_1:33,XBOOLE_0:def 8; hence thesis by XBOOLE_0:def 8; end; definition let R be asymmetric non empty RelStr; let x,y be Element of R; redefine pred x <= y; asymmetry proof let a,b be Element of R; assume [a,b] in the InternalRel of R; hence not [b,a] in the InternalRel of R by PREFER_1:22; end; end; theorem Lem2: for R being asymmetric non empty RelStr for x,y being Element of R holds x <= y iff x < y proof let R be asymmetric non empty RelStr; let x,y be Element of R; hereby assume Z0: x <= y; then x <> y; hence x < y by Z0,ORDERS_2:def 6; end; assume x < y; hence x <= y by ORDERS_2:def 6; end; begin definition let I; mode multiset of I is Element of finite-MultiSet_over I; end; registration let I; cluster -> I-defined natural-valued for multiset of I; coherence proof let m be multiset of I; m in the carrier of finite-MultiSet_over I c= the carrier of MultiSet_over I by MONOID_0:23; then m is Multiset of I; hence thesis by MONOID_1:27; end; end; registration let I; cluster -> total for multiset of I; coherence proof let m be multiset of I; m in the carrier of finite-MultiSet_over I c= the carrier of MultiSet_over I by MONOID_0:23; then m is Multiset of I; then m is Function of I,NAT by MONOID_1:27; hence thesis; end; end; definition let m be natural-valued Function; redefine func support m equals m"(NAT\{0}); compatibility proof let I; support m = m"(NAT\{0}) proof thus support m c= m"(NAT\{0}) proof let a; assume a in support m; then A1: m.a <> 0 by PRE_POLY:def 7; then A2: a in dom m by FUNCT_1:def 2; m.a in NAT & not m.a in {0} by A1,TARSKI:def 1,ORDINAL1:def 12; then m.a in NAT\{0} by XBOOLE_0:def 5; hence thesis by A2,FUNCT_1:def 7; end; let a; assume a in m"(NAT\{0}); then m.a in NAT\{0} by FUNCT_1:def 7; then not m.a in {0} by XBOOLE_0:def 5; then m.a <> 0 by TARSKI:def 1; hence thesis by PRE_POLY:def 7; end; hence I = support m iff I = m"(NAT\{0}); end; end; registration let I; cluster -> finite-support for multiset of I; coherence proof let m be multiset of I; m in the carrier of finite-MultiSet_over I c= the carrier of MultiSet_over I by MONOID_0:23; then support m is finite by MONOID_1:def 6; hence thesis by PRE_POLY:def 8; end; end; theorem Th1: a is multiset of I iff a is bag of I proof thus a is multiset of I implies a is bag of I; assume a is bag of I; then reconsider b = a as bag of I; dom b = I & rng b c= NAT by PARTFUN1:def 2,VALUED_0:def 6; then b is Function of I,NAT by FUNCT_2:2; then b is Multiset of I & support b is finite by MONOID_1:27; hence thesis by MONOID_1:def 6; end; theorem Th11: 1.finite-MultiSet_over I = EmptyBag I proof 1.MultiSet_over I = I --> 0 = EmptyBag I by MONOID_1:26; hence thesis by MONOID_0:def 24; end; definition let R be RelStr; let x,y be Element of R; pred x ## y means not x <= y & not y <= x; symmetry; end; definition struct(multMagma,RelStr) RelMultMagma (# carrier -> set, multF -> BinOp of the carrier, InternalRel -> Relation of the carrier #); end; definition struct(multLoopStr,RelStr) RelMonoid (# carrier -> set, multF -> BinOp of the carrier, OneF -> Element of the carrier, InternalRel -> Relation of the carrier #); end; definition let M be multLoopStr; mode RelExtension of M -> RelMonoid means :RE: the multLoopStr of it = the multLoopStr of M; existence proof set r = the Relation of the carrier of M; take R = RelMonoid(#the carrier of M, the multF of M, the OneF of M,r#); thus thesis; end; end; registration let M be non empty multLoopStr; cluster -> non empty for RelExtension of M; coherence proof let R be RelExtension of M; the multLoopStr of R = the multLoopStr of M by RE; hence thesis; end; end; registration let M be multLoopStr; cluster strict for RelExtension of M; existence proof set r = the Relation of the carrier of M; set R = RelMonoid(#the carrier of M, the multF of M, the OneF of M,r#); the multLoopStr of R = the multLoopStr of M; then R is RelExtension of M by RE; hence thesis; end; end; theorem Th2: for N being multLoopStr, M being RelExtension of N holds a is Element of M iff a is Element of N proof let N be multLoopStr; let M be RelExtension of N; the multLoopStr of N = the multLoopStr of M by RE; hence thesis; end; theorem Th3: for N being multLoopStr, M being RelExtension of N holds 1.N = 1.M proof let N be multLoopStr; let M be RelExtension of N; the multLoopStr of N = the multLoopStr of M by RE; hence thesis; end; registration let I; let M be RelExtension of finite-MultiSet_over I; cluster -> Function-like Relation-like for Element of M; coherence proof let m be Element of M; m is multiset of I by Th2; hence thesis; end; end; registration let I; let M be RelExtension of finite-MultiSet_over I; cluster -> I-defined natural-valued finite-support for Element of M; coherence proof let m be Element of M; m is multiset of I by Th2; hence thesis; end; end; registration let I; let M be RelExtension of finite-MultiSet_over I; cluster -> total for Element of M; coherence proof let m be Element of M; m is multiset of I by Th2; hence thesis; end; end; theorem for M being RelExtension of finite-MultiSet_over I holds the carrier of M = Bags I proof set N = finite-MultiSet_over I; let M be RelExtension of finite-MultiSet_over I; thus the carrier of M c= Bags I proof let a; assume a in the carrier of M; hence a in Bags I by PRE_POLY:def 12; end; let a; assume a in Bags I; then a is bag of I by PRE_POLY:def 12; then a is Element of N by Th1; then a is Element of M by Th2; hence thesis; end; scheme RelEx{M() -> non empty multLoopStr, R[object,object]}: ex N being strict RelExtension of M() st for x,y being Element of N holds x <= y iff R[x,y]; consider R being Relation of the carrier of M() such that A1: for x,y being Element of M() holds [x,y] in R iff R[x,y] from RELSET_1:sch 2; set N = RelMonoid(#the carrier of M(),the multF of M(),the OneF of M(),R#); the multLoopStr of N = the multLoopStr of M(); then reconsider N as strict RelExtension of M() by RE; take N; let x,y be Element of N; [x,y] in R iff R[x,y] by A1; hence thesis by ORDERS_2:def 5; end; theorem Th4: for N being multLoopStr, M1,M2 being strict RelExtension of N st for m,n being Element of M1 for x,y being Element of M2 st m = x & n = y holds m <= n iff x <= y holds M1 = M2 proof let N be multLoopStr; let M1,M2 be strict RelExtension of N; assume Z4: for m,n being Element of M1 for x,y being Element of M2 st m = x & n = y holds m <= n iff x <= y; A2: the multLoopStr of M1 = the multLoopStr of N & the multLoopStr of M2 = the multLoopStr of N by RE; the InternalRel of M1 = the InternalRel of M2 proof let a,b; hereby assume A3: [a,b] in the InternalRel of M1; then reconsider m = a, n = b as Element of M1 by ZFMISC_1:87; reconsider x = m, y = n as Element of M2 by A2; m <= n by A3,ORDERS_2:def 5; then x <= y by Z4; hence [a,b] in the InternalRel of M2 by ORDERS_2:def 5; end; assume A3: [a,b] in the InternalRel of M2; then reconsider m = a, n = b as Element of M2 by ZFMISC_1:87; reconsider x = m, y = n as Element of M1 by A2; m <= n by A3,ORDERS_2:def 5; then x <= y by Z4; hence [a,b] in the InternalRel of M1 by ORDERS_2:def 5; end; hence M1 = M2 by A2; end; begin definition let R be non empty RelStr; func DershowitzMannaOrder R -> strict RelExtension of finite-MultiSet_over the carrier of R means :DM: for m,n being Element of it holds m <= n iff ex x,y being Element of it st 1.it <> x divides n & m = (n -' x) + y & for b being Element of R st y.b > 0 ex a being Element of R st x.a > 0 & b <= a; existence proof set M = finite-MultiSet_over the carrier of R; defpred R[bag of the carrier of R,bag of the carrier of R] means ex x,y being Element of M st 1.M <> x divides \$2 & \$1 = (\$2 -' x) + y & for b being Element of R st y.b > 0 ex a being Element of R st x.a > 0 & b <= a; consider N being strict RelExtension of M such that A1: for m,n being Element of N holds m <= n iff R[m,n] from RelEx; take N; let m,n be Element of N; hereby assume m <= n; then consider x,y being Element of M such that A2: 1.M <> x divides n & m = (n -' x) + y & for b being Element of R st y.b > 0 ex a being Element of R st x.a > 0 & b <= a by A1; reconsider x,y as Element of N by Th2; take x,y; thus 1.N <> x divides n & m = (n -' x) + y & for b being Element of R st y.b > 0 ex a being Element of R st x.a > 0 & b <= a by A2,Th3; end; given x,y being Element of N such that A3: 1.N <> x divides n & m = (n -' x) + y & for b being Element of R st y.b > 0 ex a being Element of R st x.a > 0 & b <= a; reconsider x,y as Element of M by Th2; 1.M <> x divides n & m = (n -' x) + y & for b being Element of R st y.b > 0 ex a being Element of R st x.a > 0 & b <= a by A3,Th3; hence thesis by A1; end; uniqueness proof set M = finite-MultiSet_over the carrier of R; let N1,N2 be strict RelExtension of finite-MultiSet_over the carrier of R; assume that A1: for m,n being Element of N1 holds m <= n iff ex x,y being Element of N1 st 1.N1 <> x divides n & m = (n -' x) + y & for b being Element of R st y.b > 0 ex a being Element of R st x.a > 0 & b <= a and A2: for m,n being Element of N2 holds m <= n iff ex x,y being Element of N2 st 1.N2 <> x divides n & m = (n -' x) + y & for b being Element of R st y.b > 0 ex a being Element of R st x.a > 0 & b <= a; for m,n being Element of N1 for x,y being Element of N2 st m = x & n = y holds m <= n iff x <= y proof let m,n be Element of N1; let k,l be Element of N2; assume Z0: m = k; assume Z1: n = l; A5: 1.N1 = 1.M = 1.N2 by Th3; hereby assume m <= n; then consider x,y being Element of N1 such that A3: 1.N1 <> x divides n & m = (n -' x) + y & for b being Element of R st y.b > 0 ex a being Element of R st x.a > 0 & b <= a by A1; reconsider x,y as Element of M by Th2; reconsider x,y as Element of N2 by Th2; 1.N2 <> x divides l & k = (l -' x) + y & for b being Element of R st y.b > 0 ex a being Element of R st x.a > 0 & b <= a by Z0,Z1,A3,A5; hence k <= l by A2; end; assume k <= l; then consider x,y being Element of N2 such that A4: 1.N2 <> x divides l & k = (l -' x) + y & for b being Element of R st y.b > 0 ex a being Element of R st x.a > 0 & b <= a by A2; reconsider x,y as Element of M by Th2; reconsider x,y as Element of N1 by Th2; 1.N1 <> x divides n & m = (n -' x) + y & for b being Element of R st y.b > 0 ex a being Element of R st x.a > 0 & b <= a by Z0,Z1,A4,A5; hence m <= n by A1; end; hence thesis by Th4; end; end; theorem Th7: for m,n being bag of I holds n = (m-'(m-'n))+(n-'m) proof let m,n be bag of I; let a; assume a in I; thus n.a = (m.a-'(m.a-'n.a))+(n.a-'m.a) by Th6 .= (m.a-'(m-'n).a)+(n.a-'m.a) by PRE_POLY:def 6 .= (m-'(m-'n)).a+(n.a-'m.a) by PRE_POLY:def 6 .= (m-'(m-'n)).a+(n-'m).a by PRE_POLY:def 6 .= ((m-'(m-'n))+(n-'m)).a by PRE_POLY:def 5; end; theorem Th8: for m,n,x,y being bag of I st n = (m-'x)+y holds m-'n divides x & n-'m divides y proof let m,n,x,y be bag of I; assume Z0: n = (m-'x)+y; thus m-'n divides x proof let a; n.a = (m-'x).a+y.a by Z0,PRE_POLY:def 5 .= (m.a-'x.a)+y.a by PRE_POLY:def 6; then m.a-'n.a <= x.a by Th5; hence (m-'n).a <= x.a by PRE_POLY:def 6; end; let a; n.a = (m-'x).a+y.a by Z0,PRE_POLY:def 5 .= (m.a-'x.a)+y.a by PRE_POLY:def 6; then n.a-'m.a <= y.a by Th5; hence thesis by PRE_POLY:def 6; end; theorem Th8A: for m,n,x,y being bag of I st x divides m & n = (m-'x)+y holds x-'(m-'n) = y-'(n-'m) proof let m,n,x,y be bag of I; assume Z0: x divides m; assume Z1: n = (m-'x)+y; let a; assume a in I; A1: n.a = (m-'x).a+y.a = (m.a-'x.a)+y.a & x.a <= m.a by Z0,Z1,PRE_POLY:def 5,def 6,def 11; thus (x-'(m-'n)).a = x.a-'(m-'n).a by PRE_POLY:def 6 .= x.a-'(m.a-'n.a) by PRE_POLY:def 6 .= y.a-'(n.a-'m.a) by A1,Th5A .= y.a-'(n-'m).a by PRE_POLY:def 6 .= (y-'(n-'m)).a by PRE_POLY:def 6; end; theorem Th9: for m,x,y being bag of I st x divides m & x <> y holds m <> (m-'x)+y proof let m,x,y be bag of I; assume Z0: for a holds x.a <= m.a; given a such that Z1: a in I & x.a <> y.a; take a; thus a in I by Z1; A1: ((m-'x)+y).a = (m-'x).a+y.a = (m.a-'x.a)+y.a by PRE_POLY:def 5,def 6; m.a-'x.a = m.a-x.a by Z0,XREAL_1:233; hence thesis by A1,Z1; end; theorem Lem5: for I being non empty set, R being Relation of I for r being RedSequence of R st len r > 1 holds r.len r in I proof let I be non empty set; let R be Relation of I; let r be RedSequence of R; assume Z0: len r > 1; then consider i being Nat such that A1: len r = 1+i by NAT_1:10; len r >= i >= 1 by Z0,A1,NAT_1:13; then i in dom r & i+1 in dom r by A1,FINSEQ_3:25,FINSEQ_5:6; then [r.i,r.len r] in R by A1,REWRITE1:def 2; hence r.len r in I by ZFMISC_1:87; end; theorem Th13: for R being asymmetric transitive Relation of I for r being RedSequence of R holds r is one-to-one proof let R be asymmetric transitive Relation of I; let r be RedSequence of R; let a,b; assume Z0: a in dom r & b in dom r; then reconsider i = a, j = b as Nat; assume Z1: r.a = r.b & a <> b; A1: for i,j being Nat st i > j & i in dom r & j in dom r holds r.i <> r.j proof let i,j be Nat; assume i > j; then A1: i >= j+1 by NAT_1:13; assume Z3: i in dom r; assume Z4: j in dom r; defpred P[Nat] means \$1 in dom r implies [r.j,r.\$1] in R & r.\$1 <> r.j; A2: P[j+1] proof assume j+1 in dom r; hence [r.j,r.(j+1)] in R by Z4,REWRITE1:def 2; hence thesis by PREFER_1:22; end; A3: for i being Nat st i >= j+1 & P[i] holds P[i+1] proof let i be Nat; assume Z5: i >= j+1 & P[i] & i+1 in dom r; then 1 <= j+1 & i < i+1 <= len r by NAT_1:11,13,FINSEQ_3:25; then 1 <= i <= len r by Z5,XXREAL_0:2; then i in dom r by FINSEQ_3:25; then [r.j,r.i] in R & [r.i,r.(i+1)] in R by Z5,REWRITE1:def 2; hence [r.j,r.(i+1)] in R by RELAT_2:31; hence thesis by PREFER_1:22; end; for i being Nat st i >= j+1 holds P[i] from NAT_1:sch 8(A2,A3); hence r.i <> r.j by A1,Z3; end; i < j or j < i by Z1,XXREAL_0:1; hence thesis by Z0,Z1,A1; end; theorem Th12: for R being asymmetric transitive non empty RelStr for X being set st X is finite & ex x being Element of R st x in X ex x being Element of R st x is_maximal_in X proof let R be asymmetric transitive non empty RelStr; let X be set; assume X is finite; then reconsider X1 = X as finite set; given x being Element of R such that Z1: x in X; set Y = {r where r is Element of X1*: r is RedSequence of the InternalRel of R}; defpred P[Nat] means ex r being RedSequence of the InternalRel of R st r in Y & len r = \$1; A1: for k being Nat st P[k] holds k <= card X1 proof let k be Nat; given r being RedSequence of the InternalRel of R such that A2: r in Y & len r = k; consider q being Element of X1* such that A3: r = q & q is RedSequence of the InternalRel of R by A2; rng r c= X1 & r is one-to-one by A3,Th13,FINSEQ_1:def 4; then len r = card rng r <= card X1 by PRE_POLY:19,NAT_1:43; hence thesis by A2; end; B1: P[1] proof set k = 1; reconsider r = <*x*> as RedSequence of the InternalRel of R by REWRITE1:6; take r; <*x*> is FinSequence of X1 by Z1,FINSEQ_1:74; then <*x*> in X1* by FINSEQ_1:def 11; hence r in Y; thus len r = k by FINSEQ_1:39; end; then A4: ex k being Nat st P[k]; consider k being Nat such that A5: P[k] & for n being Nat st P[n] holds n <= k from NAT_1:sch 6(A1,A4); consider r being RedSequence of the InternalRel of R such that A6: r in Y & len r = k by A5; consider q being Element of X1* such that A7: r = q & q is RedSequence of the InternalRel of R by A6; 1 <= k by B1,A5; then per cases by XXREAL_0:1; suppose C1: k = 1; take x; not ex y being Element of R st y in X & x < y proof given y being Element of R such that A8: y in X & x < y; [x,y] in the InternalRel of R by A8,ORDERS_2:def 5,def 6; then reconsider r = <*x,y*> as RedSequence of the InternalRel of R by REWRITE1:7; <*x,y*> is FinSequence of X1 by Z1,A8,FINSEQ_2:13; then r in X1* by FINSEQ_1:def 11; then r in Y & len r = 2 by FINSEQ_1:44; hence contradiction by A5,C1; end; hence x is_maximal_in X by Z1,WAYBEL_4:55; end; suppose A8: k > 1; then reconsider x = r.k as Element of R by A6,Lem5; take x; A9: k in dom r & r is FinSequence of X1 by A6,A7,FINSEQ_5:6; not ex y being Element of R st y in X & x < y proof given y being Element of R such that B1: y in X & x < y; [x,y] in the InternalRel of R by B1,ORDERS_2:def 5,def 6; then reconsider p = <*x,y*> as RedSequence of the InternalRel of R by REWRITE1:7; p.1 = x by FINSEQ_1:44; then reconsider rp = r\$^p as RedSequence of the InternalRel of R by A6,REWRITE1:8; ex i being Nat st k = 1+i by A8,NAT_1:10; then consider t being FinSequence, a such that B2: r = t^<*a*> by A6,FINSEQ_2:18; k = len t + 1 by A6,B2,FINSEQ_2:16; then x = a by B2,FINSEQ_1:42; then B3: rp = r^<*y*> by B2,REWRITE1:3; reconsider yy = <*y*>, r1 = r as FinSequence of X1 by A7,B1,FINSEQ_1:74; r1^yy is FinSequence of X1; then rp in X1* by B3,FINSEQ_1:def 11; then rp in Y & len rp = k+1 by A6,B3,FINSEQ_2:16; then k+1 <= k by A5; hence contradiction by NAT_1:13; end; hence x is_maximal_in X by A9,FUNCT_1:102,WAYBEL_4:55; end; end; theorem Lem3: for m,n being bag of I holds m-'n divides m proof let m,n be bag of I; let a; m.a-'n.a <= m.a by NAT_D:35; hence (m-'n).a <= m.a by PRE_POLY:def 6; end; registration let I; cluster -> Function-like Relation-like for Element of Bags I; coherence by PRE_POLY:def 12; end; theorem Lem4: for m,n being bag of I holds m-'n <> EmptyBag I or m = n or n-'m <> EmptyBag I proof let m,n be bag of I; assume Z0: m-'n = EmptyBag I; assume m <> n; then consider a such that A1: a in I & m.a <> n.a by PBOOLE:def 10; per cases by A1,XXREAL_0:1; suppose m.a > n.a; then m.a-n.a > 0 by XREAL_1:50; then m.a-'n.a > 0 by XREAL_0:def 2; then 0 < (m-'n).a = 0 by A1,Z0,FUNCOP_1:7,PRE_POLY:def 6; hence thesis; end; suppose A3: n.a > m.a; take a; thus a in I by A1; n.a-m.a > 0 by A3,XREAL_1:50; then n.a-'m.a > 0 by XREAL_0:def 2; then (n-'m).a > 0 by PRE_POLY:def 6; hence (n-'m).a <> (EmptyBag I).a by A1,FUNCOP_1:7; end; end; definition let R being asymmetric transitive non empty RelStr; redefine func DershowitzMannaOrder R means :HO: for m,n being Element of it holds m <= n iff m <> n & for a being Element of R st m.a > n.a ex b being Element of R st a <= b & m.b < n.b; compatibility proof let M be strict RelExtension of finite-MultiSet_over the carrier of R; hereby assume A1: M = DershowitzMannaOrder R; let m,n be Element of M; hereby assume m <= n; then consider x,y being Element of M such that A2: 1.M <> x divides n & m = (n -' x) + y & for b being Element of R st y.b > 0 ex a being Element of R st x.a > 0 & b <= a by A1,DM; set X = {a where a is Element of R: x.a > 0 & ex b being Element of R st y.b > 0 & b <= a}; B1: X c= support x proof let a; assume a in X; then consider c being Element of R such that A3: a = c & x.c > 0 & ex b being Element of R st y.b > 0 & b <= c; thus thesis by A3,PRE_POLY:def 7; end; x <> y proof per cases by Th3; suppose y = 1.M; hence thesis by A2; end; suppose y <> 1.finite-MultiSet_over the carrier of R; then y <> EmptyBag the carrier of R by Th11; then consider b such that A5: b in the carrier of R & y.b <> ((the carrier of R)-->0).b by PBOOLE:def 10; reconsider b as Element of R by A5; A6: 0 <= y.b <> 0 by A5,FUNCOP_1:7; then consider a being Element of R such that A7: x.a > 0 & b <= a by A2; a in X by A6,A7; then consider c being Element of R such that A8: c is_maximal_in X by B1,Th12; A9: c in X & not ex a being Element of R st a in X & c < a by A8,WAYBEL_4:55; not c in support y proof assume c in support y; then A11: 0 <= y.c <> 0 by PRE_POLY:def 7; then consider a being Element of R such that A12: x.a > 0 & c <= a by A2; a in X & c < a by A11,A12,Lem2; hence contradiction by A8,WAYBEL_4:55; end; hence thesis by B1,A9; end; end; hence m <> n by A2,Th9; let a be Element of R; assume m.a > n.a; then m.a-n.a>0 by XREAL_1:50; then m.a-'n.a>0 by XREAL_0:def 2; then A3: (m-'n).a>0 by PRE_POLY:def 6; m-'n divides y by A2,Th8; then y.a > 0 by A3,PRE_POLY:def 11; then consider b being Element of R such that A4: x.b > 0 & a <= b by A2; set X = {c where c is Element of R: x.c > 0 & a <= c}; X c= support x proof let b; assume b in X; then consider c being Element of R such that B2: b = c & x.c > 0 & a <= c; thus thesis by B2,PRE_POLY:def 7; end; then X is finite & b in X by A4; then consider c being Element of R such that B3: c is_maximal_in X by Th12; c in X & not ex a being Element of R st a in X & c < a by B3,WAYBEL_4:55; then consider d being Element of R such that B5: c = d & x.d > 0 & a <= d; take c; thus a <= c by B5; assume m.c >= n.c; then per cases by XXREAL_0:1; suppose m.c > n.c; then m.c-n.c > 0 by XREAL_1:50; then m.c-'n.c > 0 & m-'n divides y by A2,Th8,XREAL_0:def 2; then y.c >= (m-'n).c > 0 by PRE_POLY:def 6,def 11; then consider e being Element of R such that B6: x.e > 0 & c <= e by A2; a <= e by B5,B6,YELLOW_0:def 2; then e in X & c < e by B6,Lem2; hence contradiction by B3,WAYBEL_4:55; end; suppose m.c = n.c; then x.c = x.c-'0 = x.c-'(n.c-'m.c) = x.c-'(n-'m).c = (x-'(n-'m)).c = (y-'(m-'n)).c = y.c-'(m-'n).c = y.c-'(m.c-'n.c) = y.c-'0 = y.c by A2,Th8A,XREAL_1:232,NAT_D:40,PRE_POLY:def 6; then consider e being Element of R such that B6: x.e > 0 & c <= e by A2,B5; a <= e by B5,B6,YELLOW_0:def 2; then e in X & c < e by B6,Lem2; hence contradiction by B3,WAYBEL_4:55; end; end; assume A5: m <> n & for a being Element of R st m.a > n.a ex b being Element of R st a <= b & m.b < n.b; reconsider x = n-'m, y = m-'n as multiset of the carrier of R by Th1; reconsider x,y as Element of M by Th2; A6: m = (n-'x)+y by Th7; A8: x divides n by Lem3; A9: now let b be Element of R; assume y.b > 0; then m.b-'n.b>0 by PRE_POLY:def 6; then m.b-n.b > 0 by XREAL_0:def 2; then consider a being Element of R such that A7: b <= a & m.a < n.a by A5,XREAL_1:47; take a; n.a-m.a > 0 by A7,XREAL_1:50; then n.a-'m.a > 0 by XREAL_0:def 2; hence x.a > 0 & b <= a by A7,PRE_POLY:def 6; end; 1.M <> x proof per cases by A5,Lem4; suppose EmptyBag the carrier of R <> x; then 1.finite-MultiSet_over the carrier of R <> x by Th11; hence thesis by Th3; end; suppose EmptyBag the carrier of R <> y; then consider b such that A10: b in the carrier of R & (EmptyBag the carrier of R).b <> y.b by PBOOLE:def 10; reconsider b as Element of R by A10; 0 <> y.b >= 0 by A10,FUNCOP_1:7; then consider a being Element of R such that A11: x.a > 0 & b <= a by A9; take a; EmptyBag the carrier of R = 1.finite-MultiSet_over the carrier of R = 1.M by Th11,Th3; hence thesis by A11,FUNCOP_1:7; end; end; hence m <= n by A1,A6,A8,A9,DM; end; assume B1: for m,n being Element of M holds m <= n iff m <> n & for a being Element of R st m.a > n.a ex b being Element of R st a <= b & m.b < n.b; for m,n being Element of M holds m <= n iff ex x,y being Element of M st 1.M <> x & x divides n & m = (n -' x) + y & for b being Element of R st y.b > 0 ex a being Element of R st x.a > 0 & b <= a proof let m,n be Element of M; hereby assume Z0: m <= n; reconsider x = n-'m, y = m-'n as multiset of the carrier of R by Th1; reconsider x,y as Element of M by Th2; take x,y; A9: now let b be Element of R; assume y.b > 0; then m.b-'n.b>0 by PRE_POLY:def 6; then m.b-n.b > 0 by XREAL_0:def 2; then consider a being Element of R such that A7: b <= a & m.a < n.a by Z0,B1,XREAL_1:47; take a; n.a-m.a > 0 by A7,XREAL_1:50; then n.a-'m.a > 0 by XREAL_0:def 2; hence x.a > 0 & b <= a by A7,PRE_POLY:def 6; end; thus 1.M <> x proof per cases by Z0,B1,Lem4; suppose EmptyBag the carrier of R <> x; then 1.finite-MultiSet_over the carrier of R <> x by Th11; hence thesis by Th3; end; suppose EmptyBag the carrier of R <> y; then consider b such that A10: b in the carrier of R & (EmptyBag the carrier of R).b <> y.b by PBOOLE:def 10; reconsider b as Element of R by A10; 0 <> y.b >= 0 by A10,FUNCOP_1:7; then consider a being Element of R such that A11: x.a > 0 & b <= a by A9; take a; EmptyBag the carrier of R = 1.finite-MultiSet_over the carrier of R = 1.M by Th11,Th3; hence thesis by A11,FUNCOP_1:7; end; end; thus x divides n by Lem3; thus m = (n -' x) + y by Th7; let b be Element of R; assume y.b > 0; hence ex a being Element of R st x.a > 0 & b <= a by A9; end; given x,y being Element of M such that A2: 1.M <> x & x divides n & m = (n -' x) + y & for b being Element of R st y.b > 0 ex a being Element of R st x.a > 0 & b <= a; now set X = {a where a is Element of R: x.a > 0 & ex b being Element of R st y.b > 0 & b <= a}; B1: X c= support x proof let a; assume a in X; then consider c being Element of R such that A3: a = c & x.c > 0 & ex b being Element of R st y.b > 0 & b <= c; thus thesis by A3,PRE_POLY:def 7; end; x <> y proof per cases by Th3; suppose y = 1.M; hence thesis by A2; end; suppose y <> 1.finite-MultiSet_over the carrier of R; then y <> EmptyBag the carrier of R by Th11; then consider b such that A5: b in the carrier of R & y.b <> ((the carrier of R)-->0).b by PBOOLE:def 10; reconsider b as Element of R by A5; A6: 0 <= y.b <> 0 by A5,FUNCOP_1:7; then consider a being Element of R such that A7: x.a > 0 & b <= a by A2; a in X by A6,A7; then consider c being Element of R such that A8: c is_maximal_in X by B1,Th12; A9: c in X & not ex a being Element of R st a in X & c < a by A8,WAYBEL_4:55; not c in support y proof assume c in support y; then A11: 0 <= y.c <> 0 by PRE_POLY:def 7; then consider a being Element of R such that A12: x.a > 0 & c <= a by A2; a in X & c < a by A11,A12,Lem2; hence contradiction by A8,WAYBEL_4:55; end; hence thesis by B1,A9; end; end; hence m <> n by A2,Th9; let a be Element of R; assume m.a > n.a; then m.a-n.a>0 by XREAL_1:50; then m.a-'n.a>0 by XREAL_0:def 2; then A3: (m-'n).a>0 by PRE_POLY:def 6; m-'n divides y by A2,Th8; then (m-'n).a <= y.a by PRE_POLY:def 11; then consider b being Element of R such that A4: x.b > 0 & a <= b by A2,A3; set X = {c where c is Element of R: x.c > 0 & a <= c}; X c= support x proof let b; assume b in X; then consider c being Element of R such that B2: b = c & x.c > 0 & a <= c; thus thesis by B2,PRE_POLY:def 7; end; then X is finite & b in X by A4; then consider c being Element of R such that B3: c is_maximal_in X by Th12; c in X & not ex a being Element of R st a in X & c < a by B3,WAYBEL_4:55; then consider d being Element of R such that B5: c = d & x.d > 0 & a <= d; take c; thus a <= c by B5; assume m.c >= n.c; then per cases by XXREAL_0:1; suppose m.c > n.c; then m.c-n.c > 0 by XREAL_1:50; then m.c-'n.c > 0 & m-'n divides y by A2,Th8,XREAL_0:def 2; then y.c >= (m-'n).c > 0 by PRE_POLY:def 6,def 11; then consider e being Element of R such that B6: x.e > 0 & c <= e by A2; a <= e by B5,B6,YELLOW_0:def 2; then e in X & c < e by B6,Lem2; hence contradiction by B3,WAYBEL_4:55; end; suppose m.c = n.c; then x.c = x.c-'0 = x.c-'(n.c-'m.c) = x.c-'(n-'m).c = (x-'(n-'m)).c = (y-'(m-'n)).c = y.c-'(m-'n).c = y.c-'(m.c-'n.c) = y.c-'0 = y.c by A2,Th8A,XREAL_1:232,NAT_D:40,PRE_POLY:def 6; then consider e being Element of R such that B6: x.e > 0 & c <= e by A2,B5; a <= e by B5,B6,YELLOW_0:def 2; then e in X & c < e by B6,Lem2; hence contradiction by B3,WAYBEL_4:55; end; end; hence m <= n by B1; end; hence M = DershowitzMannaOrder R by DM; end; end; theorem Th15: for k,x1,x2,y1,y2 being bag of I st x2 divides k & x1 divides (k-'x2)+y2 holds x2+(x1-'y2) divides k & (((k-'x2)+y2)-'x1)+y1 = (k-'(x2+(x1-'y2)))+((y2-'x1)+y1) proof let k,x1,x2,y1,y2 be bag of I; assume A1: for a holds x2.a <= k.a; assume A2: for a holds x1.a <= ((k-'x2)+y2).a; hereby let a; x2.a <= k.a & x1.a <= ((k-'x2)+y2).a = (k-'x2).a+y2.a = (k.a-'x2.a)+y2.a by A1,A2,PRE_POLY:def 5,def 6; then x2.a+(x1.a-'y2.a) <= k.a by Th14; then x2.a+(x1-'y2).a <= k.a by PRE_POLY:def 6; hence (x2+(x1-'y2)).a <= k.a by PRE_POLY:def 5; end; let a such that a in I; x2.a <= k.a & x1.a <= ((k-'x2)+y2).a = (k-'x2).a+y2.a = (k.a-'x2.a)+y2.a by A1,A2,PRE_POLY:def 5,def 6; then A3: (((k.a-'x2.a)+y2.a)-'x1.a)+y1.a = (k.a-'(x2.a+(x1.a-'y2.a)))+((y2.a-'x1.a)+y1.a) by Th14; A4: (((k.a-'x2.a)+y2.a)-'x1.a)+y1.a = (((k-'x2).a+y2.a)-'x1.a)+y1.a by PRE_POLY:def 6 .= (((k-'x2)+y2).a-'x1.a)+y1.a by PRE_POLY:def 5 .= (((k-'x2)+y2)-'x1).a+y1.a by PRE_POLY:def 6 .= ((((k-'x2)+y2)-'x1)+y1).a by PRE_POLY:def 5; (k.a-'(x2.a+(x1.a-'y2.a)))+((y2.a-'x1.a)+y1.a) = (k.a-'(x2.a+(x1.a-'y2.a)))+((y2-'x1).a+y1.a) by PRE_POLY:def 6 .= (k.a-'(x2.a+(x1-'y2).a))+((y2-'x1).a+y1.a) by PRE_POLY:def 6 .= (k.a-'(x2+(x1-'y2)).a)+((y2-'x1).a+y1.a) by PRE_POLY:def 5 .= (k.a-'(x2+(x1-'y2)).a)+((y2-'x1)+y1).a by PRE_POLY:def 5 .= (k-'(x2+(x1-'y2))).a+((y2-'x1)+y1).a by PRE_POLY:def 6; hence thesis by A3,A4,PRE_POLY:def 5; end; registration let R be asymmetric transitive non empty RelStr; cluster DershowitzMannaOrder R -> asymmetric transitive; coherence proof set DM = DershowitzMannaOrder R; thus DM is asymmetric proof let a,b; assume a in the carrier of DM & b in the carrier of DM; then reconsider m = a, n = b as Element of DM; assume [a,b] in the InternalRel of DM & [b,a] in the InternalRel of DM; then A0: m <= n & n <= m by ORDERS_2:def 5; then m <> n & (for a being Element of R st m.a > n.a ex b being Element of R st a <= b & m.b < n.b) & for a being Element of R st n.a > m.a ex b being Element of R st a <= b & n.b < m.b by HO; then consider c being object such that A2: c in the carrier of R & m.c <> n.c by PBOOLE:def 10; reconsider c as Element of R by A2; set X = {d where d is Element of R: c <= d & m.d > n.d}; BC: X c= support m proof let a; assume a in X; then consider d being Element of R such that A3: a = d & c <= d & m.d > n.d; thus thesis by A3,PRE_POLY:def 7; end; ex b being Element of R st b in X proof per cases by A2,XXREAL_0:1; suppose m.c < n.c; then consider d being Element of R such that A5: c <= d & n.d < m.d by A0,HO; take d; thus d in X by A5; end; suppose m.c > n.c; then consider d being Element of R such that A5: c <= d & n.d > m.d by A0,HO; consider e being Element of R such that A6: d <= e & n.e < m.e by A0,HO,A5; take e; c <= e by A5,A6,ORDERS_2:3; hence e in X by A6; end; end; then consider d being Element of R such that A7: d is_maximal_in X by BC,Th12; d in X & not ex a being Element of R st a in X & d < a by A7,WAYBEL_4:55; then consider e being Element of R such that A8: d = e & c <= e & n.e < m.e; consider f being Element of R such that A9: e <= f & n.f > m.f by A0,HO,A8; consider g being Element of R such that A10: f <= g & n.g < m.g by A0,HO,A9; c <= f by A8,A9,ORDERS_2:3; then c <= g & d <= g by A8,A9,A10,ORDERS_2:3; then g in X & d < g by A10,Lem2; hence contradiction by A7,WAYBEL_4:55; end; thus DM is transitive proof let a,b,c be object; assume a in the carrier of DM & b in the carrier of DM & c in the carrier of DM; then reconsider m=a, n=b, k=c as Element of DM; assume [a,b] in the InternalRel of DM & [b,c] in the InternalRel of DM; then A0: m <= n & n <= k by ORDERS_2:def 5; consider x1,y1 being Element of DM such that A2: 1.DM <> x1 divides n & m = (n -' x1) + y1 & for b being Element of R st y1.b > 0 ex a being Element of R st x1.a > 0 & b <= a by A0,DM; consider x2,y2 being Element of DM such that A3: 1.DM <> x2 divides k & n = (k -' x2) + y2 & for b being Element of R st y2.b > 0 ex a being Element of R st x2.a > 0 & b <= a by A0,DM; reconsider x = x2+(x1-'y2), y = (y2-'x1)+y1 as multiset of the carrier of R by Th1; reconsider x, y as Element of DM by Th2; A4: m = (((k-'x2)+y2)-'x1)+y1 = (k -' x) + y by A2,A3,Th15; A5: 1.DM <> x proof consider a such that A7: a in the carrier of R & (1.DM).a <> x2.a by A3,PBOOLE:def 10; reconsider a as Element of R by A7; 1.DM = 1.finite-MultiSet_over the carrier of R = EmptyBag the carrier of R by Th3,Th11; then A8: (1.DM).a = 0 by FUNCOP_1:7; take a; 0 < x2.a <= x2.a+(x1-'y2).a by A7,A8,NAT_1:11; hence thesis by A8,PRE_POLY:def 5; end; A6: x divides k by A2,A3,Th15; for b being Element of R st y.b > 0 ex a being Element of R st x.a > 0 & b <= a proof let b be Element of R; assume y.b > 0; then (y2-'x1).b+y1.b > 0 by PRE_POLY:def 5; then per cases; suppose (y2-'x1).b > 0; then y2.b-'x1.b > 0 by PRE_POLY:def 6; then y2.b-x1.b > 0 by XREAL_0:def 2; then y2.b > x1.b >= 0 by XREAL_1:47; then consider a being Element of R such that B4: x2.a > 0 & b <= a by A3; take a; x.a = x2.a+(x1-'y2).a >= x2.a by NAT_1:11,PRE_POLY:def 5; hence thesis by B4; end; suppose y1.b > 0; then consider a being Element of R such that B1: x1.a > 0 & b <= a by A2; per cases; suppose B2: (x1-'y2).a > 0; take a; (x2+(x1-'y2)).a = x2.a+(x1-'y2).a by PRE_POLY:def 5; hence x.a > 0 by B2; thus b <= a by B1; end; suppose (x1-'y2).a = 0; then x1.a-'y2.a = 0 by PRE_POLY:def 6; then x1.a <= y2.a by NAT_D:36; then consider c being Element of R such that B3: x2.c > 0 & a <= c by A3,B1; take c; x.c = x2.c+(x1-'y2).c by PRE_POLY:def 5; hence thesis by B1,B3,ORDERS_2:3; end; end; end; then m <= k by A4,A5,A6,DM; hence thesis by ORDERS_2:def 5; end; end; end; definition let I; func DivOrder I -> Relation of Bags I means :DO: for b1,b2 being bag of I holds [b1,b2] in it iff b1 <> b2 & b1 divides b2; existence proof defpred R[bag of I, bag of I] means \$1 <> \$2 & \$1 divides \$2; consider R being Relation of Bags I such that A1: for b1,b2 being Element of Bags I holds [b1,b2] in R iff R[b1,b2] from RELSET_1:sch 2; take R; let b1,b2 be bag of I; b1 in Bags I & b2 in Bags I by PRE_POLY:def 12; hence thesis by A1; end; uniqueness proof let R1,R2 be Relation of Bags I such that A1: for b1,b2 being bag of I holds [b1,b2] in R1 iff b1 <> b2 & b1 divides b2 and A2: for b1,b2 being bag of I holds [b1,b2] in R2 iff b1 <> b2 & b1 divides b2; let b1,b2 be Element of Bags I; [b1,b2] in R1 iff b1 <> b2 & b1 divides b2 by A1; hence thesis by A2; end; end; theorem Lem7: for a,b,c being bag of I st a divides b divides c holds a divides c proof let a,b,c be bag of I; assume that A1: for x being object holds a.x <= b.x and A2: for x being object holds b.x <= c.x; let x be object; a.x <= b.x <= c.x by A1,A2; hence thesis by XXREAL_0:2; end; registration let I; cluster DivOrder I -> asymmetric transitive; coherence proof set R = DivOrder I; now let x, y be object; assume A1: [x,y] in R; then reconsider a = x, b = y as Element of Bags I by ZFMISC_1:87; A2: a <> b & a divides b by DO,A1; then consider o being object such that A3: o in I & a.o <> b.o by PBOOLE:def 10; a.o <= b.o by A2,PRE_POLY:def 11; then a.o < b.o by A3,XXREAL_0:1; then not b divides a by PRE_POLY:def 11; hence not [y,x] in R by DO; end; hence R is asymmetric by PREFER_1:22; let a,b,c be object; assume a in field R & b in field R & c in field R; assume A4: [a,b] in R & [b,c] in R; then reconsider a,b,c as Element of Bags I by ZFMISC_1:87; A5: a <> b & a divides b & b divides c by A4,DO; then consider x being object such that A6: x in I & a.x <> b.x by PBOOLE:def 10; a.x <= b.x by A5,PRE_POLY:def 11; then a.x < b.x <= c.x by A5,A6,XXREAL_0:1,PRE_POLY:def 11; then a <> c & a divides c by A5,Lem7; hence thesis by DO; end; end; theorem Th16: for R being asymmetric transitive non empty RelStr holds DivOrder the carrier of R c= the InternalRel of DershowitzMannaOrder R proof let R be asymmetric transitive non empty RelStr; set DM = DershowitzMannaOrder R; let a,b be Element of Bags the carrier of R; assume A1: [a,b] in DivOrder the carrier of R; reconsider a,b as multiset of the carrier of R by Th1; reconsider a,b as Element of DM by Th2; A2: a <> b & a divides b by A1,DO; then for x being Element of R st a.x > b.x ex y being Element of R st x <= y & a.y < b.y by PRE_POLY:def 11; then a <= b by A2,HO; hence thesis by ORDERS_2:def 5; end; theorem for R being asymmetric transitive non empty RelStr st the InternalRel of R is empty holds the InternalRel of DershowitzMannaOrder R = DivOrder the carrier of R proof let R be asymmetric transitive non empty RelStr; assume Z0: the InternalRel of R is empty; let a,b; hereby assume A1: [a,b] in the InternalRel of DershowitzMannaOrder R; then reconsider m = a, n = b as Element of DershowitzMannaOrder R by ZFMISC_1:87; A5: m <= n by A1,ORDERS_2:def 5; then A3: m <> n & for a being Element of R st m.a > n.a ex b being Element of R st a <= b & m.b < n.b by HO; m divides n proof let a; assume A4: m.a > n.a; a in dom m by A4,FUNCT_1:def 2; then reconsider a as Element of R; consider b being Element of R such that A2: a <= b & m.b < n.b by A5,HO,A4; thus thesis by Z0,A2,ORDERS_2:def 5; end; hence [a,b] in DivOrder the carrier of R by A3,DO; end; DivOrder the carrier of R c= the InternalRel of DershowitzMannaOrder R by Th16; hence thesis; end; theorem for R1,R2 being asymmetric transitive non empty RelStr st the carrier of R1 = the carrier of R2 & the InternalRel of R1 c= the InternalRel of R2 holds the InternalRel of DershowitzMannaOrder R1 c= the InternalRel of DershowitzMannaOrder R2 proof let R1,R2 be asymmetric transitive non empty RelStr; assume Z0: the carrier of R1 = the carrier of R2 & the InternalRel of R1 c= the InternalRel of R2; let a,b be Element of DershowitzMannaOrder R1; assume [a,b] in the InternalRel of DershowitzMannaOrder R1; then A3: a <= b by ORDERS_2:def 5; then A1: a <> b & for x being Element of R1 st a.x > b.x ex y being Element of R1 st x <= y & a.y < b.y by HO; reconsider b1 = b, a1 = a as multiset of the carrier of R1 by Th1; reconsider b1, a1 as Element of DershowitzMannaOrder R2 by Z0,Th2; now let x be Element of R2; reconsider x1 = x as Element of R1 by Z0; assume a1.x > b1.x; then consider y being Element of R1 such that A2: x1 <= y & a.y < b.y by A3,HO; reconsider y1 = y as Element of R2 by Z0; take y1; [x1,y] in the InternalRel of R1 by A2,ORDERS_2:def 5; hence x <= y1 & a1.y1 < b1.y1 by Z0,A2,ORDERS_2:def 5; end; then a1 <= b1 by A1,HO; hence thesis by ORDERS_2:def 5; end; begin definition let I; let f be (Bags I)-valued FinSequence; func Sum f -> bag of I means :SUM: ex F being Function of NAT, Bags I st it = F.len f & F.0 = EmptyBag I & for i being Nat for b being bag of I st i < len f & b = f.(i + 1) holds F.(i + 1) = F.i + b; existence proof defpred P[set] means for F being (Bags I)-valued FinSequence st len F = \$1 ex u being bag of I st ex f being Function of NAT, Bags I st u = f.(len F) & f.0 = EmptyBag I & for j being Nat, v being bag of I st j < len F & v = F.(j + 1) holds f.(j + 1) = f.j + v; set V = Bags I; A1: for n be Nat st P[n] holds P[n+1] proof let n be Nat; assume A2: P[n]; let F be (Bags I)-valued FinSequence; A3: rng F c= Bags I by RELAT_1:def 19; then reconsider F1 = F as FinSequence of V by FINSEQ_1:def 4; reconsider G = F1 | Seg(n) as FinSequence of V by FINSEQ_1:18; assume A4: len F = n + 1; then dom F = Seg(n + 1) by FINSEQ_1:def 3; then n + 1 in dom F by FINSEQ_1:4; then F.(n + 1) in rng F by FUNCT_1:def 3; then reconsider u1 = F.(n + 1) as Element of V by A3; A5: n < n + 1 by NAT_1:13; then consider u being bag of I, f being Function of NAT,V such that u = f.(len G) and A6: f.0 = EmptyBag I and A7: for j being Nat, v being bag of I st j < len G & v = G.(j + 1) holds f.(j + 1) = f.j + v by A2,A4,FINSEQ_1:17; defpred P[set,set] means for j being Nat st \$1 = j holds (j < n + 1 implies \$2 = f.\$1) & (n + 1 <= j implies for u being bag of I st u = F.(n + 1) holds \$2 = f.(len G) + u); A8: for k being Element of NAT ex v being Element of V st P[k,v] proof let k be Element of NAT; reconsider i = k as Element of NAT; A9: now assume A10: n + 1 <= i; take v = f.(len G) + u1; let j be Nat; assume k = j; hence j < n + 1 implies v = f.k by A10; assume n + 1 <= j; let u2 be bag of I; assume u2 = F.(n + 1); hence v = f.(len G) + u2; end; now assume A11: i < n + 1; take v = f.k; let j be Nat such that A12: k = j; thus j < n + 1 implies v = f.k; thus n + 1 <= j implies for u being bag of I st u = F.(n + 1) holds v = f.(len G) + u by A11,A12; end; then consider v being bag of I such that B13: P[k,v] by A9; v in V by PRE_POLY:def 12; hence thesis by B13; end; consider f9 being sequence of Bags I such that A13: for k being Element of NAT holds P[k,f9.k] from FUNCT_2:sch 3(A8); A14: for k being Nat holds P[k,f9.k] proof let k be Nat; k in NAT by ORDINAL1:def 12; hence thesis by A13; end; take z = f9.(n + 1); take f99 = f9; thus z = f99.(len F) by A4; thus f99.0 = EmptyBag I by A6,A14; let j be Nat, v be bag of I; assume that A15: j < len F and A16: v = F.(j + 1); A17: len G = n by A4,A5,FINSEQ_1:17; A18: now assume A19: j = n; then f99.(j + 1) = f.j + v by A17,A14,A16; hence f99.(j + 1) = f99.j + v by A5,A14,A19; end; A20: now assume A21: j < n; then A22: j + 1 < n + 1 by XREAL_1:6; 1 <= 1 + j & j + 1 <= n by A21,NAT_1:11,13; then j + 1 in Seg n; then A23: v = G.(j + 1) by A16,FUNCT_1:49; j < len G by A4,A5,A21,FINSEQ_1:17; then A24: f.(j + 1) = f.j + v by A7,A23; j < n + 1 by A21,NAT_1:13; then f.(j + 1) = f9.j + v by A14,A24; hence f99.(j + 1) = f99.j + v by A14,A22; end; j <= n by A4,A15,NAT_1:13; hence f99.(j + 1) = f99.j + v by A20,A18,XXREAL_0:1; end; A25: P[0] proof reconsider f = NAT --> EmptyBag I as sequence of Bags I; let F be (Bags I)-valued FinSequence; assume A26: len F = 0; take u = f.(len F); take f9 = f; thus u = f9.(len F) & f9.0 = EmptyBag I by FUNCOP_1:7; let j be Nat; let v be bag of I; thus j < len F & v = F.(j + 1) implies f9.(j + 1) = f9.j + v by A26; end; for n being Nat holds P[n] from NAT_1:sch 2(A25,A1); hence thesis; end; uniqueness proof let v1,v2 be bag of I; given F being Function of NAT, Bags I such that A27: v1 = F.(len f) and A28: F.0 = EmptyBag I and A29: for j being Nat, v being bag of I st j < len f & v = f.(j + 1) holds F.(j + 1) = F.j + v; given f9 being Function of NAT, Bags I such that A30: v2 = f9.(len f) and A31: f9.0 = EmptyBag I and A32: for j being Nat, v being bag of I st j < len f & v = f.(j + 1) holds f9.(j + 1) = f9.j + v; defpred P[Nat] means \$1 <= len f implies F.\$1 = f9.\$1; now A33: rng f c= Bags I by RELAT_1:def 19; let k be Nat; assume A34: P[k]; assume A35: k + 1 <= len f; 1 <= k + 1 & dom f = Seg(len f) by FINSEQ_1:def 3,NAT_1:11; then k + 1 in dom f by A35; then f.(k + 1) in rng f by FUNCT_1:def 3; then reconsider u1 = f.(k + 1) as Element of Bags I by A33; F.(k + 1) = F.k + u1 by A29,A35,NAT_1:13; hence F.(k + 1) = f9.(k + 1) by A32,A34,A35,NAT_1:13; end; then A37: for k being Nat st P[k] holds P[k+1]; A38: P[0] by A28,A31; for k being Nat holds P[k] from NAT_1:sch 2(A38,A37); hence thesis by A27,A30; end; end; theorem Th21: Sum (<*>Bags I) = EmptyBag I proof set f = <*>Bags I; consider F being Function of NAT, Bags I such that A1: Sum f = F.len f and A2: F.0 = EmptyBag I and for i being Nat for b being bag of I st i < len f & b = f.(i + 1) holds F.(i + 1) = F.i + b by SUM; thus thesis by A1,A2; end; registration let I; let b be bag of I; cluster <*b*> -> Bags I-valued for FinSequence; coherence proof rng <*b*> = {b} & b in Bags I by PRE_POLY:def 12,FINSEQ_1:39; hence thesis by RELAT_1:def 19,ZFMISC_1:31; end; end; theorem Th22: for p being Bags I-valued FinSequence, b being bag of I holds Sum (p^<*b*>) = Sum p + b proof let p be Bags I-valued FinSequence; let b be bag of I; set f = p^<*b*>; consider F being Function of NAT, Bags I such that A1: Sum f = F.len f and A2: F.0 = EmptyBag I and A3: for i being Nat for b being bag of I st i < len f & b = f.(i + 1) holds F.(i + 1) = F.i + b by SUM; consider F1 being Function of NAT, Bags I such that A4: Sum p = F1.len p and A5: F1.0 = EmptyBag I and A6: for i being Nat for b being bag of I st i < len p & b = p.(i + 1) holds F1.(i + 1) = F1.i + b by SUM; defpred P[Nat] means \$1 <= len p implies F.\$1 = F1.\$1; A7: P[0] by A2,A5; A8: for i being Nat st P[i] holds P[i+1] proof let i be Nat; assume A9: P[i] & i+1 <= len p; then i < len p < len p+1 = len f by FINSEQ_2:16,NAT_1:13; then A11: i < len f by XXREAL_0:2; A12: i+1 in dom p by A9,NAT_1:11,FINSEQ_3:25; then reconsider b = p.(i+1) as Element of Bags I by FUNCT_1:102; f.(i+1) = b by A12,FINSEQ_1:def 7; hence F.(i+1) = F.i + b by A3,A11 .= F1.i + b by A9,NAT_1:13 .= F1.(i+1) by A6,A9,NAT_1:13; end; for i being Nat holds P[i] from NAT_1:sch 2(A7,A8); then Sum p = F.len p & len p < len p+1 = len f & f.(len p+1) = b by A4,NAT_1:13,FINSEQ_2:16,FINSEQ_1:42; hence Sum (p^<*b*>) = Sum p + b by A1,A3; end; reserve b for bag of I; theorem Th23: Sum <*b*> = b proof thus Sum <*b*> = Sum ((<*>Bags I)^<*b*>) by FINSEQ_1:34 .= Sum <*>Bags I + b by Th22 .= EmptyBag I + b by Th21 .= b by PRE_POLY:53; end; theorem Th24: for p,q being Bags I-valued FinSequence holds Sum (p^q) = Sum p + Sum q proof let p,q be Bags I-valued FinSequence; set f = p^q; consider F being Function of NAT, Bags I such that A1: Sum f = F.len f and A2: F.0 = EmptyBag I and A3: for i being Nat for b being bag of I st i < len f & b = f.(i + 1) holds F.(i + 1) = F.i + b by SUM; consider F1 being Function of NAT, Bags I such that A4: Sum p = F1.len p and A5: F1.0 = EmptyBag I and A6: for i being Nat for b being bag of I st i < len p & b = p.(i + 1) holds F1.(i + 1) = F1.i + b by SUM; consider F2 being Function of NAT, Bags I such that B1: Sum q = F2.len q and B2: F2.0 = EmptyBag I and B3: for i being Nat for b being bag of I st i < len q & b = q.(i + 1) holds F2.(i + 1) = F2.i + b by SUM; defpred P[Nat] means \$1 <= len p implies F.\$1 = F1.\$1; A7: P[0] by A2,A5; A8: for i being Nat st P[i] holds P[i+1] proof let i be Nat; assume A9: P[i] & i+1 <= len p; then i < len p <= len p+len q = len f by FINSEQ_1:22,NAT_1:11,13; then A11: i < len f by XXREAL_0:2; A12: i+1 in dom p by A9,NAT_1:11,FINSEQ_3:25; then reconsider b = p.(i+1) as Element of Bags I by FUNCT_1:102; f.(i+1) = b by A12,FINSEQ_1:def 7; hence F.(i+1) = F.i + b by A3,A11 .= F1.i + b by A9,NAT_1:13 .= F1.(i+1) by A6,A9,NAT_1:13; end; for i being Nat holds P[i] from NAT_1:sch 2(A7,A8); then A13:Sum p = F.len p by A4; defpred Q[Nat] means \$1 <= len q implies F.(len p+\$1) = Sum p+F2.\$1; A14:Q[0] by A13,B2,PRE_POLY:53; A15:for i being Nat st Q[i] holds Q[i+1] proof let i be Nat; assume A9: Q[i] & i+1 <= len q; then A10: i < len q & len p+len q = len f by FINSEQ_1:22,NAT_1:13; A12: i+1 in dom q by A9,NAT_1:11,FINSEQ_3:25; then reconsider b = q.(i+1) as Element of Bags I by FUNCT_1:102; reconsider lp = len p as Nat; reconsider lpi = (lp)+i as Nat; f.(len p+(i+1)) = b & len p+(i+1) = len p+i+1 by A12,FINSEQ_1:def 7; hence F.(len p+(i+1)) = F.(lpi) + b by A3,A10,XREAL_1:6 .= Sum p+F2.i + b by A9,NAT_1:13 .= Sum p+(F2.i + b) by RFUNCT_1:8 .= Sum p+F2.(i+1) by B3,A9,NAT_1:13; end; for i being Nat holds Q[i] from NAT_1:sch 2(A14,A15); then F.(len p+len q) = Sum p+Sum q by B1; hence Sum (p^q) = Sum p + Sum q by A1,FINSEQ_1:22; end; theorem Th25: for p being Bags I-valued FinSequence holds Sum (<*b*>^p) = b + Sum p proof let p be Bags I-valued FinSequence; thus Sum (<*b*>^p) = Sum <*b*> + Sum p by Th24 .= b + Sum p by Th23; end; theorem Th26: for p being Bags I-valued FinSequence st b in rng p holds b divides Sum p proof let p be Bags I-valued FinSequence; assume b in rng p; then consider q,r being FinSequence such that A1: p = q^<*b*>^r by Lem9; reconsider qb = q^<*b*>, r as Bags I-valued FinSequence by A1,Lem8; qb = qb; then reconsider q as Bags I-valued FinSequence by Lem8; Sum p = Sum(q^<*b*>)+Sum r = Sum q + b + Sum r = Sum r+Sum q+b by A1,Th22,Th24,RFUNCT_1:8; hence b divides Sum p by PRE_POLY:50; end; theorem Th27: for p being Bags I-valued FinSequence, i being object st i in support Sum p ex b st b in rng p & i in support b proof defpred P[Nat] means for p being Bags I-valued FinSequence st len p = \$1 for i being object st i in support Sum p ex b st b in rng p & i in support b; A1: P[0] proof let p be Bags I-valued FinSequence such that A2: len p = 0; let i be object; assume Z0: i in support Sum p; p = {} = <*>Bags I by A2; then i in support EmptyBag I by Z0,Th21; hence thesis; end; A3: for j being Nat st P[j] holds P[j+1] proof let j be Nat; assume A4: P[j]; let p be Bags I-valued FinSequence such that A2: len p = j+1; consider w being FinSequence, x being set such that A5: p = w^<*x*> & len w = j by A2,TREES_2:3; reconsider w, xx = <*x*> as Bags I-valued FinSequence by A5,Lem8; len xx = 1 by FINSEQ_1:40; then 1 in dom xx by FINSEQ_3:25; then x = xx.1 in Bags I by FUNCT_1:102,FINSEQ_1:40; then reconsider x as Element of Bags I; Sum p = Sum w+x by A5,Th22; then A6: support Sum p = (support Sum w)\/support x by PRE_POLY:38; let i be object; assume i in support Sum p; then per cases by A6,XBOOLE_0:def 3; suppose i in support Sum w; then consider b such that A7: b in rng w & i in support b by A4,A5; take b; rng p = rng w \/ rng xx by A5,FINSEQ_1:31; hence thesis by A7,XBOOLE_0:def 3; end; suppose A8: i in support x; take b = x; rng p = rng w \/ rng xx & x in {x} = rng xx by A5,FINSEQ_1:31,39,TARSKI:def 1; hence thesis by A8,XBOOLE_0:def 3; end; end; let p be Bags I-valued FinSequence; for j being Nat holds P[j] from NAT_1:sch 2(A1,A3); then P[len p]; hence thesis; end; definition let I,b; mode partition of b -> Bags I-valued FinSequence means :PART: b = Sum it; existence proof take <*b*>; thus thesis by Th23; end; end; definition let I,b; redefine func <*b*> -> partition of b; coherence proof thus b = Sum <*b*> by Th23; end; end; definition let R be RelStr; let M be RelExtension of finite-MultiSet_over the carrier of R; let b be Element of M; let p be partition of b; attr p is co-ordered means for i being Nat st i in dom p & i+1 in dom p for b1,b2 being Element of M st b1 = p.i & b2 = p.(i+1) holds b2 <= b1; end; definition let R be non empty RelStr; let b be bag of the carrier of R; let p be partition of b; attr p is ordered means (for m being bag of the carrier of R st m in rng p for x being Element of R st m.x > 0 holds m.x = b.x) & (for m being bag of the carrier of R st m in rng p for x,y being Element of R st m.x > 0 & m.y > 0 & x <> y holds x ## y) & (for m being bag of the carrier of R st m in rng p holds m <> EmptyBag the carrier of R) & (for i being Nat st i in dom p & i+1 in dom p for x being Element of R st (p/.(i+1)).x > 0 ex y being Element of R st (p/.i).y > 0 & x <= y); end; reserve R for asymmetric transitive non empty RelStr, a,b,c for bag of the carrier of R, x,y,z for Element of R; theorem <*a*> is ordered iff a <> EmptyBag the carrier of R & for x,y st a.x > 0 & a.y > 0 & x <> y holds x ## y proof hereby assume Z0: <*a*> is ordered; a in {a} = rng <*a*> by TARSKI:def 1,FINSEQ_1:39; hence a <> EmptyBag the carrier of R & for x,y st a.x > 0 & a.y > 0 & x <> y holds x ## y by Z0; end; assume Z3: a <> EmptyBag the carrier of R; assume Z4: for x,y st a.x > 0 & a.y > 0 & x <> y holds x ## y; set p = <*a*>; hereby let m be bag of the carrier of R; assume m in rng p; then m in {a} by FINSEQ_1:39; hence for x being Element of R st m.x > 0 holds m.x = a.x by TARSKI:def 1; end; hereby let m be bag of the carrier of R; assume m in rng p; then m in {a} by FINSEQ_1:39; then m = a by TARSKI:def 1; hence for x,y being Element of R st m.x > 0 & m.y > 0 & x <> y holds x ## y by Z4; end; hereby let m be bag of the carrier of R; assume m in rng p; then m in {a} by FINSEQ_1:39; hence m <> EmptyBag the carrier of R by Z3,TARSKI:def 1; end; let i be Nat; assume i in dom p & i+1 in dom p; then 1 <= i < i+1 <= len p = 1 by FINSEQ_1:40,FINSEQ_3:25,NAT_1:13; hence thesis by XXREAL_0:2; end; theorem Th28: for p being Bags I-valued FinSequence for a,b being bag of I holds <*a*>^p is partition of b iff a divides b & p is partition of b-'a proof let p be Bags I-valued FinSequence; let a,b be bag of I; thus <*a*>^p is partition of b implies a divides b & p is partition of b-'a proof assume b = Sum(<*a*>^p); then A1: b = a+Sum p by Th25; hence a divides b by PRE_POLY:50; thus b-'a = Sum p by A1,PRE_POLY:48; end; assume Z1: a divides b; assume b-'a = Sum p; then Sum p+a = b-'a+a = b by Z1,PRE_POLY:47; hence b = Sum(<*a*>^p) by Th25; end; reserve p for partition of b-'a, q for partition of b; theorem Th30: q = <*a*>^p & q is ordered implies p is ordered proof assume Z1: q = <*a*>^p; assume Z2: q is ordered; hereby let m be bag of the carrier of R; assume A0: m in rng p; then A1: m in rng<*a*>\/rng p = rng q by Z1,XBOOLE_0:def 3,FINSEQ_1:31; let x be Element of R; assume A2: m.x > 0; m divides Sum p = b-'a divides b by A0,Th26,PART,Lem3; then b.x = m.x <= (b-'a).x <= b.x by A1,A2,Z2,PRE_POLY:def 11; hence m.x = (b-'a).x by XXREAL_0:1; end; hereby let m be bag of the carrier of R; assume m in rng p; then m in rng<*a*>\/rng p = rng q by Z1,FINSEQ_1:31,XBOOLE_0:def 3; hence for x,y being Element of R st m.x > 0 & m.y > 0 & x <> y holds x ## y by Z2; end; hereby let m be bag of the carrier of R; assume m in rng p; then m in rng<*a*>\/rng p = rng q by Z1,FINSEQ_1:31,XBOOLE_0:def 3; hence m <> EmptyBag the carrier of R by Z2; end; let i be Nat; assume A1: i in dom p & i+1 in dom p; A2: len <*a*> = 1 by FINSEQ_1:40; then A3: q.(1+i) = p.i & q.(1+(i+1)) = p.(i+1) by Z1,A1,FINSEQ_1:def 7; A4: 1+i in dom q & 1+i+1 = 1+(i+1) in dom q by Z1,A1,A2,FINSEQ_1:28; then q.(1+i) = q/.(1+i) & p/.i = p.i & q.(1+(i+1)) = q/.(1+i+1) & p.(i+1) = p/.(i+1) by A1,PARTFUN1:def 6; hence thesis by Z2,A3,A4; end; definition let I; let m be bag of I; let J be set; func m|J -> bag of I means :BAR: for i being object st i in I holds (i in J implies it.i = m.i) & (not i in J implies it.i = 0); existence proof defpred C[object] means \$1 in J; deffunc F(object) = m.\$1; deffunc G(object) = 0; consider f being Function such that A1: dom f = I & for x being object st x in I holds (C[x] implies f.x = F(x)) & (not C[x] implies f.x = G(x)) from PARTFUN1:sch 1; rng f c= NAT proof let x be object; assume x in rng f; then consider i being object such that A2: i in dom f & x = f.i by FUNCT_1:def 3; x = F(i) or x = G(i) by A1,A2; hence thesis by ORDINAL1:def 12; end; then reconsider f as Function of I,NAT by A1,FUNCT_2:2; f is finite-support proof support f c= support m proof let x be object; assume x in support f; then A3: f.x <> 0 by PRE_POLY:def 7; then x in dom f by FUNCT_1:def 2; then f.x = m.x by A1,A3; hence thesis by A3,PRE_POLY:def 7; end; hence support f is finite; end; then reconsider f as bag of I; take f; thus thesis by A1; end; uniqueness proof let b1,b2 be bag of I such that A1: for i being object st i in I holds (i in J implies b1.i = m.i) & (not i in J implies b1.i = 0) and A2: for i being object st i in I holds (i in J implies b2.i = m.i) & (not i in J implies b2.i = 0); let i be object; assume A3: i in I; per cases; suppose i in J; then b1.i = m.i = b2.i by A1,A2,A3; hence thesis; end; suppose not i in J; then b1.i = 0 = b2.i by A1,A2,A3; hence thesis; end; end; end; reserve J for set, m for bag of I; theorem Th44: support (m|J) = J /\ support m proof set f = m|J; thus support f c= J /\ support m proof let x be object; assume x in support f; then A3: f.x <> 0 by PRE_POLY:def 7; then A4: x in dom f = I by PARTFUN1:def 2,FUNCT_1:def 2; then A5: x in J by BAR,A3; then f.x = m.x by BAR,A4; then x in support m by A3,PRE_POLY:def 7; hence thesis by A5,XBOOLE_0:def 4; end; let x be object; assume x in J /\ support m; then A1: x in J & x in support m by XBOOLE_0:def 4; then A2: m.x <> 0 by PRE_POLY:def 7; then x in dom m = I by PARTFUN1:def 2,FUNCT_1:def 2; then f.x = m.x by A1,BAR; hence thesis by A2,PRE_POLY:def 7; end; theorem (m|J)+(m|(I\J)) = m proof let i be object; assume A1: i in I; A3: ((m|J)+(m|(I\J))).i = (m|J).i+(m|(I\J)).i by PRE_POLY:def 5; per cases; suppose A2: i in J; then not i in I\J by XBOOLE_0:def 5; then (m|J).i = m.i & (m|(I\J)).i = 0 by A1,A2,BAR; hence thesis by A3; end; suppose A2: not i in J; then i in I\J by A1,XBOOLE_0:def 5; then (m|J).i = 0 & (m|(I\J)).i = m.i by A2,BAR; hence thesis by A3; end; end; theorem Th43: m|J divides m proof let i be object; per cases; suppose A1: not i in I; dom (m|J) = I & dom m = I by PARTFUN1:def 2; hence thesis by A1,FUNCT_1:def 2; end; suppose A2: i in I; per cases; suppose i in J; hence thesis by A2,BAR; end; suppose not i in J; hence thesis by A2,BAR; end; end; end; theorem support m c= J implies m|J = m proof assume A1: support m c= J; let i be object; assume A2: i in I; per cases; suppose i in J; hence thesis by A2,BAR; end; suppose not i in J; then (m|J).i = 0 & not i in support m by A1,A2,BAR; hence thesis by PRE_POLY:def 7; end; end; theorem Th27A: support(m-'(m|J)) = (support m)\J proof thus support(m-'(m|J)) c= (support m)\J proof let x be object; assume x in support(m-'(m|J)); then (m-'(m|J)).x <> 0 by PRE_POLY:def 7; then m.x-'(m|J).x <> 0 by PRE_POLY:def 6; then m.x-'(m|J).x > 0; then m.x-(m|J).x > 0 by XREAL_0:def 2; then m.x > (m|J).x by XREAL_1:47; then m.x <> (m|J).x & x in dom m = I & m.x > 0 by PARTFUN1:def 2,FUNCT_1:def 2; then not x in J & x in support m by BAR,PRE_POLY:def 7; hence x in (support m)\J by XBOOLE_0:def 5; end; let x be object; assume x in (support m)\J; then A1: x in (support m) & not x in J by XBOOLE_0:def 5; then A2: m.x <> 0 by PRE_POLY:def 7; then x in dom m = I by PARTFUN1:def 2,FUNCT_1:def 2; then (m|J).x = 0 by A1,BAR; then (m-'(m|J)).x = m.x-'(m|J).x <> 0 by A2,NAT_D:40,PRE_POLY:def 6; hence thesis by PRE_POLY:def 7; end; theorem Th31: q is ordered & q = <*a*>^p & a.x > 0 implies a.x = b.x proof assume Z0: q is ordered; assume Z1: q = <*a*>^p; assume Z2: a.x > 0; a in {a} = rng <*a*> by TARSKI:def 1,FINSEQ_1:39; then a in rng <*a*> \/ rng p = rng q by Z1,XBOOLE_0:def 3,FINSEQ_1:31; hence thesis by Z0,Z2; end; theorem Th32: q is ordered & q = <*a*>^p & a.x > 0 & a.y > 0 & x <> y implies x ## y proof assume Z0: q is ordered; assume Z1: q = <*a*>^p; assume Z2: a.x > 0 & a.y > 0; a in {a} = rng <*a*> by TARSKI:def 1,FINSEQ_1:39; then a in rng <*a*> \/ rng p = rng q by Z1,XBOOLE_0:def 3,FINSEQ_1:31; hence thesis by Z0,Z2; end; theorem Th32A: q is ordered & q = <*a*>^p implies a <> EmptyBag the carrier of R proof assume Z0: q is ordered; assume Z1: q = <*a*>^p; a in {a} = rng <*a*> by TARSKI:def 1,FINSEQ_1:39; then a in rng <*a*> \/ rng p = rng q by Z1,XBOOLE_0:def 3,FINSEQ_1:31; hence thesis by Z0; end; theorem for c being bag of the carrier of R, r being Bags the carrier of R-valued FinSequence st q is ordered & q = <*a,c*>^r & c.y > 0 ex x st a.x > 0 & y <= x proof let c be bag of the carrier of R; let r be Bags the carrier of R-valued FinSequence; assume Z0: q is ordered; assume Z1: q = <*a,c*>^r; assume Z2: c.y > 0; len <*a,c*> = 2 by FINSEQ_1:44; then A1: 1 in dom <*a,c*> & 2 in dom <*a,c*> & dom <*a,c*> c= dom q by Z1,FINSEQ_1:26,FINSEQ_3:25; q/.1 = q.1 = <*a,c*>.1 = a & q/.(1+1) = q.2 = <*a,c*>.2 = c by Z1,A1,PARTFUN1:def 6,FINSEQ_1:def 7,44; hence thesis by Z0,Z2,A1; end; theorem x in I & (for y st y in I & y <> x holds x ## y) implies x is_maximal_in I proof assume Z0: x in I; assume Z1: for y st y in I & y <> x holds x ## y; not ex y st y in I & x < y proof let y; assume y in I & x <= y & x <> y; then x ## y & x <= y by Z1; hence contradiction; end; hence x is_maximal_in I by Z0,WAYBEL_4:55; end; theorem Th36: q is ordered & q = <*a*>^p & c in rng p & c.x > 0 implies ex y st a.y > 0 & x <= y proof assume Z0: q is ordered; assume Z1: q = <*a*>^p; assume c in rng p; then consider i being object such that A1: i in dom p & c = p.i by FUNCT_1:def 3; reconsider i as Nat by A1; A2: 1 <= i & p.i = p/.i by A1,FINSEQ_3:25,PARTFUN1:def 6; defpred P[Nat] means \$1 in dom p implies for x st (p/.\$1).x > 0 ex y st a.y > 0 & x <= y; A5: len <*a*> = 1 & dom <*a*> c= dom q by Z1,FINSEQ_1:26,40; A3: P[1] proof assume A4: 1 in dom p; then A6: 1+1 in dom q by Z1,A5,FINSEQ_1:28; B0: 1 in dom <*a*> by A5,FINSEQ_3:25; then 1 in dom q & q.1 = <*a*>.1 = a by Z1,A5,FINSEQ_1:def 7,40; then q/.1 = a & q/.2 = q.2 = p.1 = p/.1 by Z1,A4,A5,A6,FINSEQ_1:def 7,PARTFUN1:def 6; hence thesis by Z0,A6,A5,B0; end; A8: for i being Nat st i >= 1 & P[i] holds P[i+1] proof let i be Nat; assume B1: i >= 1 & P[i] & i+1 in dom p; then i < i+1 <= len p by NAT_1:13,FINSEQ_3:25; then BB: i <= len p by XXREAL_0:2; then B3: i in dom p by B1,FINSEQ_3:25; B4: 1+i in dom q & 1+i+1 in dom q by Z1,A5,B1,BB,FINSEQ_3:25,FINSEQ_1:28; B5: q/.(1+i) = q.(1+i) = p.i = p/.i & q/.(1+i+1) = q.(1+i+1) = p.(i+1) = p/.(i+1) by Z1,A5,B1,B3,FINSEQ_1:28,def 7,PARTFUN1:def 6; let x; assume (p/.(i+1)).x > 0; then consider y such that B6: (p/.i).y > 0 & x <= y by Z0,B4,B5; consider z such that B7: a.z > 0 & y <= z by BB,B1,FINSEQ_3:25,B6; take z; thus a.z > 0 & x <= z by B6,B7,ORDERS_2:3; end; for i being Nat st i >= 1 holds P[i] from NAT_1:sch 8(A3,A8); hence thesis by A1,A2; end; theorem Th34: q is ordered & q = <*a*>^p implies (x is_maximal_in support b iff a.x > 0) proof assume Z0: q is ordered; assume Z1: q = <*a*>^p; rng p c= Bags the carrier of R by RELAT_1:def 19; then reconsider p as FinSequence of Bags the carrier of R by FINSEQ_1:def 4; set I = the carrier of R; hereby assume x is_maximal_in support b; then A7: x in support b & not ex y st y in support b & x < y by WAYBEL_4:55; then x in support Sum q by PART; then consider d being bag of the carrier of R such that A8: d in rng q & x in support d by Th27; consider i being object such that A9: i in dom q & d = q.i by A8,FUNCT_1:def 3; reconsider i as Nat by A9; 1 <= i by A9,FINSEQ_3:25; then per cases by XXREAL_0:1; suppose i = 1; then d = a by Z1,A9,FINSEQ_1:41; then a.x <> 0 by A8,PRE_POLY:def 7; hence a.x > 0; end; suppose i > 1; then i >= 1+1 by NAT_1:13; then consider k being Nat such that A10: i = 1+1+k by NAT_1:10; 1 <= 1+k <= 1+k+1 = i <= len q by A9,A10,NAT_1:11,FINSEQ_3:25; then 1 <= 1+k <= len q by XXREAL_0:2; then A11: 1+k in dom q by FINSEQ_3:25; then A12: q/.i = q.i & q/.(1+k) = q.(1+k) by A9,PARTFUN1:def 6; d.x <> 0 by A8,PRE_POLY:def 7; then d.x > 0 & i = 1+k+1 by A10; then consider y such that A13: (q/.(1+k)).y > 0 & x <= y by Z0,A9,A11,A12; q.(1+k) in rng q by A11,FUNCT_1:def 3; then y in support (q/.(1+k)) c= support Sum q = support b by A13,A12,Th26,PART,BAGORDER:21,PRE_POLY:def 7; hence a.x > 0 by A7,A13,Lem2; end; end; assume B0: a.x > 0; then B1: x in support a by PRE_POLY:def 7; a in {a} = rng <*a*> c= rng q by Z1,TARSKI:def 1,FINSEQ_1:39,29; then B4: a divides Sum q = b by Th26,PART; then AA: support a c= support b by BAGORDER:21; not ex y st y in support b & x < y proof let y; assume B3: y in support b & x <= y & x <> y; per cases; suppose a.y > 0; then x ## y by Z0,Z1,B0,B3,Th32; hence contradiction by B3; end; suppose B5: a.y = 0; consider d being bag of the carrier of R such that B6: d in rng q & y in support d by B4,B3,Th27; B7: d.y <> 0 by B6,PRE_POLY:def 7; then not d in {a} & {a} = rng <*a*> & rng q = rng <*a*> \/ rng p by Z1,B5,TARSKI:def 1,FINSEQ_1:31,39; then d.y > 0 & d in rng p by B6,B7,XBOOLE_0:def 3; then consider z such that B8: a.z > 0 & y <= z by Z0,Z1,Th36; x <= z & x ## z by Z0,Z1,B0,B3,B8,ORDERS_2:3,Th32; hence contradiction; end; end; hence x is_maximal_in support b by B1,AA,WAYBEL_4:55; end; theorem Th40: q is ordered & q = <*a*>^p implies a = b|{x:x is_maximal_in support b} proof assume Z0: q is ordered; assume Z1: q = <*a*>^p; let y; set J = {x:x is_maximal_in support b}; per cases; suppose A0: y in J; then consider x such that A1: y = x & x is_maximal_in support b; a.y > 0 by Z0,Z1,A1,Th34; hence a.y = b.y by Z0,Z1,Th31 .= (b|J).y by A0,BAR; end; suppose A2: not y in J; then not y is_maximal_in support b; then a.y <= 0 by Z0,Z1,Th34; hence a.y = 0 .= (b|J).y by A2,BAR; end; end; theorem Lem10: for p being Bags I-valued FinSequence st Sum p = EmptyBag I & for a being bag of I st a in rng p holds a <> EmptyBag I holds p = {} proof let p be Bags I-valued FinSequence; assume Z0: Sum p = EmptyBag I; assume Z1: for a being bag of I st a in rng p holds a <> EmptyBag I; assume p <> {}; then consider a being object such that A1: a in rng p by XBOOLE_0:7; rng p c= Bags I by RELAT_1:def 19; then reconsider a as Element of Bags I by A1; consider x being object such that A2: x in I & a.x <> (EmptyBag I).x by A1,Z1,PBOOLE:def 10; A4: (EmptyBag I).x = 0 by A2,FUNCOP_1:7; then A3: a.x > 0 by A2; thus thesis by A4,A3,Z0,A1,Th26,PRE_POLY:def 11; end; theorem Lem11: for a,b being bag of I st a <> EmptyBag I holds a+b <> EmptyBag I proof let a,b be bag of I; given i being object such that A1: i in I & a.i <> (EmptyBag I).i; take i; thus i in I by A1; (EmptyBag I).i = 0 by A1,FUNCOP_1:7; then a.i+b.i <> (EmptyBag I).i by A1; hence thesis by PRE_POLY:def 5; end; theorem for p,q being partition of b st p is ordered & q is ordered holds p = q proof let p,q be partition of b; defpred P[Nat] means for b,q st len q = \$1 & q is ordered for p being partition of b st p is ordered holds q = p; A1: P[0] proof let b,q; assume len q = 0 & q is ordered; then A3: b = Sum q & Sum <*>Bags the carrier of R = EmptyBag the carrier of R & q = {} by PART,Th21; let p be partition of b; assume A4: p is ordered; Sum p = b by PART; hence q = p by A3,A4,Lem10; end; A5: for i being Nat st P[i] holds P[i+1] proof let i be Nat; assume A6: P[i]; let b,q; assume A7: len q = i+1 & q is ordered; then q <> {} & q is FinSequence of Bags the carrier of R by RELAT_1:def 19,FINSEQ_1:def 4; then consider w being FinSequence of Bags the carrier of R, n being Element of Bags the carrier of R such that A8: q = <*n*>^w by FINSEQ_2:130; reconsider w as partition of b-'n by A8,Th28; A9: b = Sum q = n+Sum w <> EmptyBag the carrier of R by A8,A7,Th32A,Th25,Lem11,PART; let p be partition of b; assume A10: p is ordered; Sum p = b & rng p c= Bags the carrier of R by PART,RELAT_1:def 19; then p <> <*>Bags the carrier of R & p is FinSequence of Bags the carrier of R by A9,Th21,FINSEQ_1:def 4; then consider u being FinSequence of Bags the carrier of R, m being Element of Bags the carrier of R such that A11: p = <*m*>^u by FINSEQ_2:130; reconsider u as partition of b-'m by A11,Th28; u = u & w = w; then A12: m = b|{x: x is_maximal_in support b} = n by A10,A11,A7,A8,Th40; A13: w is ordered & u is ordered by A10,A11,A7,A8,Th30; len q = len <*n*> + len w = 1+len w by A8,FINSEQ_1:22,40; hence thesis by A6,A7,A8,A11,A12,A13; end; for i being Nat holds P[i] from NAT_1:sch 2(A1,A5); then P[len p]; hence thesis; end; definition let I; let a,b be bag of I; redefine func [a,b] -> Element of [:Bags I,Bags I:]; coherence proof a in Bags I & b in Bags I by PRE_POLY:def 12; hence thesis by ZFMISC_1:87; end; end; theorem Th42: a <> EmptyBag the carrier of R implies {x:x is_maximal_in support a} <> {} proof set I = the carrier of R; given x such that A1: a.x <> (EmptyBag I).x; (EmptyBag I).x = 0 by FUNCOP_1:7; then x in support a by A1,PRE_POLY:def 7; then consider x such that A2: x is_maximal_in support a by Th12; x in {y:y is_maximal_in support a} by A2; hence thesis; end; definition let R,b; func OrderedPartition b -> Bags the carrier of R-valued FinSequence means :OP: ex F,G being Function of NAT, Bags the carrier of R st F.0 = b & G.0 = EmptyBag the carrier of R & (for i being Nat holds G.(i+1) = (F.i)|{x:x is_maximal_in support (F.i)} & F.(i+1) = (F.i)-'(G.(i+1))) & ex i being Nat st F.i = EmptyBag the carrier of R & it = G|Seg i & for j being Nat st j < i holds F.j <> EmptyBag the carrier of R; existence proof set I = the carrier of R; deffunc S(bag of I) = {x:x is_maximal_in support \$1}; deffunc h(Nat,Element of [:Bags I,Bags I:]) = [\$2`1-'(\$2`1|S(\$2`1)),\$2`1|S(\$2`1)]; consider f being Function of NAT,[:Bags I,Bags I:] such that A1: f.0 = [b,EmptyBag I] & for i being Nat holds f.(i+1) = h(i,f.i) from NAT_1:sch 12; defpred P[Nat] means ex i being Nat st card support (f.i)`1 = \$1; defpred Q[Nat] means card support (f.\$1)`1 = 0; A2: ex k being Nat st P[k] proof take k = card support (f.0)`1; take i = 0; thus thesis; end; A3: for k being Nat st k <> 0 & P[k] ex n being Nat st n < k & P[n] proof let k be Nat; assume Z0: k <> 0; given i being Nat such that Z1: card support (f.i)`1 = k; (f.i)`1 <> EmptyBag I by Z0,Z1; then B1: S((f.i)`1) <> {} by Th42; f.(i+1) = h(i,f.i) by A1; then B2: support (f.(i+1))`1 = (support (f.i)`1)\S((f.i)`1) by Th27A; S((f.i)`1) c= support (f.i)`1 proof let x be object; assume x in S((f.i)`1); then ex y st x = y & y is_maximal_in support (f.i)`1; hence thesis by WAYBEL_4:55; end; then reconsider S = S((f.i)`1) as finite Subset of support (f.i)`1; take n = card support (f.(i+1))`1; card S <> 0 by B1; then n = k - card S & card S > 0 by Z1,B2,CARD_2:44; hence n < k by XREAL_1:44; thus P[n]; end; P[0] from NAT_1:sch 7(A2,A3); then A4: ex i being Nat st Q[i]; consider i being Nat such that A5: Q[i] & for n being Nat st Q[n] holds i <= n from NAT_1:sch 5(A4); Seg i c= NAT = dom pr2 f by FUNCT_2:def 1; then dom ((pr2 f)|Seg i) = Seg i by RELAT_1:62; then reconsider p = (pr2 f)|Seg i as Bags the carrier of R-valued FinSequence by FINSEQ_1:def 2; take p; take F = pr1 f; take G = pr2 f; thus F.0 = (f.0)`1 by FUNCT_2:def 5 .= b by A1; thus G.0 = (f.0)`2 by FUNCT_2:def 6 .= EmptyBag I by A1; hereby let i be Nat; reconsider j = i as Element of NAT by ORDINAL1:def 12; A6: G.(i+1) = (f.(i+1))`2 by FUNCT_2:def 6 .= (h(i,f.i))`2 by A1 .= (f.j)`1|S((f.j)`1); (f.j)`1 = F.i by FUNCT_2:def 5; hence G.(i+1) = (F.i)|S(F.i) by A6; thus F.(i+1) = (f.(i+1))`1 by FUNCT_2:def 5 .= (h(i,f.i))`1 by A1 .= (f.j)`1-'(G.(i+1)) by A6 .= (F.i)-'(G.(i+1)) by FUNCT_2:def 5; end; take i; reconsider j = i as Element of NAT by ORDINAL1:def 12; support (f.i)`1 = {} by A5; then (f.j)`1 = EmptyBag I by PRE_POLY:81; hence F.i = EmptyBag I by FUNCT_2:def 5; thus p = G|Seg i; let k be Nat; reconsider j = k as Element of NAT by ORDINAL1:def 12; assume k < i; then not Q[k] by A5; then (f.j)`1 <> EmptyBag I; hence F.k <> EmptyBag I by FUNCT_2:def 5; end; uniqueness proof let p1,p2 be Bags the carrier of R-valued FinSequence; given F1,G1 being Function of NAT, Bags the carrier of R such that A1: F1.0 = b & G1.0 = EmptyBag the carrier of R & (for i being Nat holds G1.(i+1) = (F1.i)|{x:x is_maximal_in support (F1.i)} & F1.(i+1) = (F1.i)-'(G1.(i+1))) & ex i being Nat st F1.i = EmptyBag the carrier of R & p1 = G1|Seg i & for j being Nat st j < i holds F1.j <> EmptyBag the carrier of R; given F2,G2 being Function of NAT, Bags the carrier of R such that A2: F2.0 = b & G2.0 = EmptyBag the carrier of R & (for i being Nat holds G2.(i+1) = (F2.i)|{x:x is_maximal_in support (F2.i)} & F2.(i+1) = (F2.i)-'(G2.(i+1))) & ex i being Nat st F2.i = EmptyBag the carrier of R & p2 = G2|Seg i & for j being Nat st j < i holds F2.j <> EmptyBag the carrier of R; defpred P[Nat] means G1.\$1 = G2.\$1 & F1.\$1 = F2.\$1; A3: P[0] by A1,A2; A4: for i being Nat st P[i] holds P[i+1] proof let i be Nat; assume A5: P[i]; hence G1.(i+1) = (F2.i)|{x:x is_maximal_in support (F2.i)} by A1 .= G2.(i+1) by A2; hence F1.(i+1) = (F2.i)-'(G2.(i+1)) by A1,A5 .= F2.(i+1) by A2; end; A6: for i being Nat holds P[i] from NAT_1:sch 2(A3,A4); A7: F1 = F2 proof let i be Element of NAT; thus F1.i = F2.i by A6; end; A8: G1 = G2 proof let i be Element of NAT; thus G1.i = G2.i by A6; end; consider i1 being Nat such that A9: F1.i1 = EmptyBag the carrier of R & p1 = G1|Seg i1 & for j being Nat st j < i1 holds F1.j <> EmptyBag the carrier of R by A1; consider i2 being Nat such that AA: F1.i2 = EmptyBag the carrier of R & p2 = G1|Seg i2 & for j being Nat st j < i2 holds F1.j <> EmptyBag the carrier of R by A2,A7,A8; i1 <= i2 <= i1 by A9,AA; hence p1 = p2 by A9,AA,XXREAL_0:1; end; end; definition let R,b; redefine func OrderedPartition b -> partition of b; coherence proof set p = OrderedPartition b; consider F,G being Function of NAT, Bags the carrier of R such that A1: F.0 = b & G.0 = EmptyBag the carrier of R & (for i being Nat holds G.(i+1) = (F.i)|{x:x is_maximal_in support (F.i)} & F.(i+1) = (F.i)-'(G.(i+1))) & ex i being Nat st F.i = EmptyBag the carrier of R & p = G|Seg i & for j being Nat st j < i holds F.j <> EmptyBag the carrier of R by OP; consider i being Nat such that A2: F.i = EmptyBag the carrier of R & p = G|Seg i & for j being Nat st j < i holds F.j <> EmptyBag the carrier of R by A1; defpred P[Nat] means \$1 <= i implies b = F.\$1 + Sum (p|\$1); set I = the carrier of R; A3: P[0] proof p|0 = <*>Bags I; then Sum (p|0) = EmptyBag I by Th21; hence 0 <= i implies b = F.0 + Sum(p|0) by A1,PRE_POLY:53; end; dom G = NAT by FUNCT_2:def 1; then dom p = Seg i & i in NAT by A2,RELAT_1:62,ORDINAL1:def 12; then A5: len p = i by FINSEQ_1:def 3; A4: for j being Nat st P[j] holds P[j+1] proof let j be Nat; assume B1: P[j] & j+1 <= i; rng p c= Bags I by RELAT_1:def 19; then reconsider q = p as FinSequence of Bags I by FINSEQ_1:def 4; B2: q|(j+1) = q|j^<*q/.(j+1)*> by B1,A5,FINSEQ_5:82; j+1 in dom p by A5,B1,NAT_1:11,FINSEQ_3:25; then B4: q/.(j+1) = p.(j+1) = G.(j+1) by A2,PARTFUN1:def 6,FUNCT_1:47; G.(j+1) = (F.j)|{x:x is_maximal_in support (F.j)} by A1; then F.(j+1) = F.j-'(G.(j+1)) & G.(j+1) divides F.j by A1,Th43; then F.(j+1)+G.(j+1) = F.j by PRE_POLY:47; hence b = F.(j+1)+(G.(j+1)+Sum(p|j)) by B1,NAT_1:13,RFUNCT_1:8 .= F.(j+1)+Sum(p|(j+1)) by B2,B4,Th22; end; for j being Nat holds P[j] from NAT_1:sch 2(A3,A4); then P[len p] & p|len p = p by FINSEQ_1:58; hence b = Sum p by A2,A5,PRE_POLY:53; end; end; registration let R,b; cluster OrderedPartition b -> ordered for partition of b; coherence proof let p be partition of b such that A0: p = OrderedPartition b; consider F,G being Function of NAT, Bags the carrier of R such that A1: F.0 = b & G.0 = EmptyBag the carrier of R & (for i being Nat holds G.(i+1) = (F.i)|{x:x is_maximal_in support (F.i)} & F.(i+1) = (F.i)-'(G.(i+1))) & ex i being Nat st F.i = EmptyBag the carrier of R & p = G|Seg i & for j being Nat st j < i holds F.j <> EmptyBag the carrier of R by OP,A0; consider i being Nat such that A2: F.i = EmptyBag the carrier of R & p = G|Seg i & for j being Nat st j < i holds F.j <> EmptyBag the carrier of R by A1; set I = the carrier of R; dom G = NAT by FUNCT_2:def 1; then dom p = Seg i & i in NAT by A2,RELAT_1:62,ORDINAL1:def 12; then A3: len p = i by FINSEQ_1:def 3; defpred P[Nat] means for x st F.\$1.x > 0 holds F.\$1.x = b.x; A4: P[0] by A1; A5: for j being Nat st P[j] holds P[j+1] proof let j be Nat; assume A6: P[j]; let x; assume A7: F.(j+1).x > 0; set S = {y:y is_maximal_in support (F.j)}; F.(j+1) = F.j-'G.(j+1) & G.(j+1) = F.j|S by A1; then A8: F.(j+1).x = F.j.x-'(F.j|S).x by PRE_POLY:def 6; per cases; suppose x in S; then (F.j|S).x = F.j.x by BAR; hence thesis by A7,A8,XREAL_1:232; end; suppose not x in S; then (F.j|S).x = 0 by BAR; then F.(j+1).x = F.j.x by A8,NAT_D:40; hence thesis by A6,A7; end; end; A9: for j being Nat holds P[j] from NAT_1:sch 2(A4,A5); hereby let a; assume a in rng p; then consider j being object such that B1: j in dom p & a = p.j by FUNCT_1:def 3; reconsider j as Nat by B1; consider k being Nat such that B2: j = 1+k by B1,FINSEQ_3:25,NAT_1:10; set S = {x:x is_maximal_in support (F.k)}; B3: a = G.j = (F.k)|S by A1,B2,B1,FUNCT_1:47; let x; assume B4: a.x > 0; then x in S by B3,BAR; then a.x = F.k.x by B3,BAR; hence a.x = b.x by A9,B4; end; hereby let a; assume a in rng p; then consider j being object such that B1: j in dom p & a = p.j by FUNCT_1:def 3; reconsider j as Nat by B1; consider k being Nat such that B2: j = 1+k by B1,FINSEQ_3:25,NAT_1:10; B3: a = G.j = (F.k)|{x:x is_maximal_in support (F.k)} by A1,B2,B1,FUNCT_1:47; {x:x is_maximal_in support (F.k)} c= support (F.k) proof let z be object; assume z in {x:x is_maximal_in support (F.k)}; then ex x st z = x & x is_maximal_in support (F.k); hence thesis by WAYBEL_4:55; end; then (support (F.k))/\{x:x is_maximal_in support (F.k)} = {y:y is_maximal_in support (F.k)} by XBOOLE_1:28; then B4: support a = {x:x is_maximal_in support (F.k)} by B3,Th44; let x,y; assume B5: a.x > 0 & a.y > 0 & x <> y; then x in support a by PRE_POLY:def 7; then consider z such that B6: x = z & z is_maximal_in support (F.k) by B4; y in support a by B5,PRE_POLY:def 7; then consider u being Element of R such that B7: y = u & u is_maximal_in support (F.k) by B4; x in support (F.k) & y in support (F.k) by B6,B7,WAYBEL_4:55; then not x < y & not y < x by B6,B7,WAYBEL_4:55; hence x ## y by Lem2; end; hereby let a; assume a in rng p; then consider j being object such that B1: j in dom p & a = p.j by FUNCT_1:def 3; reconsider j as Nat by B1; consider k being Nat such that B2: j = 1+k by B1,FINSEQ_3:25,NAT_1:10; B3: a = G.j = (F.k)|{x:x is_maximal_in support (F.k)} by A1,B2,B1,FUNCT_1:47; k < j <= i by A3,B2,B1,NAT_1:13,FINSEQ_3:25; then k < i by XXREAL_0:2; then B4: {x:x is_maximal_in support (F.k)} <> {} by A2,Th42; {x:x is_maximal_in support (F.k)} c= support (F.k) proof let z be object; assume z in {x:x is_maximal_in support (F.k)}; then ex x st z = x & x is_maximal_in support (F.k); hence thesis by WAYBEL_4:55; end; then (support (F.k))/\{x:x is_maximal_in support (F.k)} = {y:y is_maximal_in support (F.k)} by XBOOLE_1:28; then support a = {x:x is_maximal_in support (F.k)} by B3,Th44; hence a <> EmptyBag the carrier of R by B4; end; let j be Nat; assume C1: j in dom p & j+1 in dom p; then consider k being Nat such that B2: j = 1+k by NAT_1:10,FINSEQ_3:25; let x; assume C2: (p/.(j+1)).x > 0; set S = {y:y is_maximal_in support (F.j)}; set T = {y:y is_maximal_in support (F.k)}; C4: p/.(j+1) = p.(j+1) = G.(j+1) = F.j|S & p/.j = p.j = G.j = F.k|T & F.j = F.k-'G.j by C1,B2,A1,FUNCT_1:47,PARTFUN1:def 6; then x in S by C2,BAR; then consider y such that C5: x = y & y is_maximal_in support F.j; C6: x in support F.j c= support F.k by C4,C5,WAYBEL_4:55,PRE_POLY:39; T c= support F.k proof let u being object; assume u in T; then ex z st u = z & z is_maximal_in support F.k; hence thesis by WAYBEL_4:55; end; then (support F.k)/\T = T by XBOOLE_1:28; then D2: support(p/.j) = T by C4,Th44; support F.j = (support F.k) \ T by C4,Th27A; then not x in T by C6,XBOOLE_0:def 5; then not x is_maximal_in support F.k; then consider z such that C7: z in support F.k & x < z by C6,WAYBEL_4:55; take z; not z in support F.j & support F.j = (support F.k) \ T by C4,C5,C7,Th27A,WAYBEL_4:55; then z in T by C7,XBOOLE_0:def 5; then (p/.j).z <> 0 by D2,PRE_POLY:def 7; hence (p/.j).z > 0; thus x <= z by C7,Lem2; end; end; theorem b = EmptyBag the carrier of R iff OrderedPartition b = {} proof set I = the carrier of R; set E = EmptyBag I; set p = OrderedPartition b; consider F,G being Function of NAT, Bags the carrier of R such that A1: F.0 = b & G.0 = E & (for i being Nat holds G.(i+1) = (F.i)|{x:x is_maximal_in support (F.i)} & F.(i+1) = (F.i)-'(G.(i+1))) & ex i being Nat st F.i = E & p = G|Seg i & for j being Nat st j < i holds F.j <> E by OP; consider i being Nat such that A2: F.i = E & p = G|Seg i & for j being Nat st j < i holds F.j <> E by A1; hereby assume b = E; then i <= 0 by A1,A2; then i = 0; hence p = {} by A2; end; assume p = {}; then p = <*>Bags I; then Sum p = E by Th21; hence thesis by PART; end; definition let R; func PrecM R -> strict RelExtension of finite-MultiSet_over the carrier of R means :PM: for m,n being Element of it holds m <= n iff m <> n & for x st m.x > 0 holds m.x < n.x or ex y st n.y > 0 & x <= y; existence proof set I = the carrier of R; set M = finite-MultiSet_over I; defpred R[bag of I,bag of I] means \$1 <> \$2 & for x st \$1.x > 0 holds \$1.x < \$2.x or ex y st \$2.y > 0 & x <= y; consider N being strict RelExtension of M such that A1: for m,n being Element of N holds m <= n iff R[m,n] from RelEx; take N; thus thesis by A1; end; uniqueness proof let N1,N2 be strict RelExtension of finite-MultiSet_over the carrier of R such that A1: for m,n being Element of N1 holds m <= n iff m <> n & for x st m.x > 0 holds m.x < n.x or ex y st n.y > 0 & x <= y and A2: for m,n being Element of N2 holds m <= n iff m <> n & for x st m.x > 0 holds m.x < n.x or ex y st n.y > 0 & x <= y; for m,n being Element of N1 for x,y being Element of N2 st m = x & n = y holds m <= n iff x <= y proof let m,n be Element of N1; let k,l be Element of N2; assume Z0: m = k; assume Z1: n = l; m <= n iff m <> n & for x st m.x > 0 holds m.x < n.x or ex y st n.y > 0 & x <= y by A1; hence thesis by A2,Z0,Z1; end; hence thesis by Th4; end; end; registration let R; cluster PrecM R -> asymmetric transitive; coherence proof set RR = the InternalRel of PrecM R; thus A0: PrecM R is asymmetric proof let a,b be object; assume a in the carrier of PrecM R & b in the carrier of PrecM R; then reconsider m = a, n = b as Element of PrecM R; assume [a,b] in RR & [b,a] in RR; then A0: m <= n & n <= m by ORDERS_2:def 5; then m <> n & (for x st m.x > 0 holds m.x < n.x or ex y st n.y > 0 & x <= y) & (for x st n.x > 0 holds n.x < m.x or ex y st m.y > 0 & x <= y) by PM; then consider x such that A2: m.x <> n.x by PBOOLE:def 21; set X = {y: m.y > 0 & x <= y}; ex y st m.y > 0 & x <= y proof per cases by A2,XXREAL_0:1; suppose m.x < n.x; hence ex y st m.y > 0 & x <= y by A0,PM; end; suppose n.x < m.x; then consider y such that A5: n.y > 0 & x <= y by A0,PM; per cases by A0,PM; suppose n.y <= m.y; hence ex y st m.y > 0 & x <= y by A5; end; suppose ex z st m.z > 0 & y <= z; hence ex y st m.y > 0 & x <= y by A5,ORDERS_2:3; end; end; end; then consider y such that A6: m.y > 0 & x <= y; A7: y in X by A6; X c= support m proof let z be object; assume z in X; then ex y st z = y & m.y > 0 & x <= y; hence thesis by PRE_POLY:def 7; end; then consider y such that A8: y is_maximal_in X by A7,Th12; y in X by A8,WAYBEL_4:55; then consider z such that A9: y = z & m.z > 0 & x <= z; per cases by A0,PM,A9; suppose m.z < n.z; then consider u being Element of R such that A10: m.u > 0 & z <= u by A0,PM; x <= u by A9,A10,ORDERS_2:3; then u in X & y < u by A9,A10,Lem2; hence contradiction by A8,WAYBEL_4:55; end; suppose ex u being Element of R st n.u > 0 & z <= u; then consider u being Element of R such that A11: n.u > 0 & z <= u; per cases by A0,PM; suppose n.u <= m.u; then m.u > 0 & x <= u by A9,A11,ORDERS_2:3; then u in X & y < u by A9,A11,Lem2; hence contradiction by A8,WAYBEL_4:55; end; suppose ex v being Element of R st m.v > 0 & u <= v; then consider v being Element of R such that A12: m.v > 0 & u <= v; A13: z <= v by A11,A12,ORDERS_2:3; then x <= v by A9,ORDERS_2:3; then v in X & y < v by A9,A12,A13,Lem2; hence contradiction by A8,WAYBEL_4:55; end; end; end; thus PrecM R is transitive proof let a,b,c be object; assume a in the carrier of PrecM R & b in the carrier of PrecM R & c in the carrier of PrecM R; assume A4: [a,b] in RR & [b,c] in RR; then reconsider a,b,c as Element of PrecM R by ZFMISC_1:87; A6: a <= b <= c by A4,ORDERS_2:def 5; A5: now let x; assume a.x > 0; then per cases by A6,PM; suppose A4: a.x < b.x; then b.x < c.x or ex y st c.y > 0 & x <= y by A6,PM; hence a.x < c.x or ex y st c.y > 0 & x <= y by A4,XXREAL_0:2; end; suppose ex y st b.y > 0 & x <= y; then consider y such that B1: b.y > 0 & x <= y; per cases by A6,PM; suppose b.y <= c.y; hence a.x < c.x or ex y st c.y > 0 & x <= y by B1; end; suppose ex z st c.z > 0 & y <= z; then consider z such that B2: c.z > 0 & y <= z; thus a.x < c.x or ex y st c.y > 0 & x <= y by B2,B1,ORDERS_2:3; end; end; end; a <> c by A4,A0,PREFER_1:22; then a <= c by A5,PM; hence thesis by ORDERS_2:def 5; end; end; end; definition let I; let R be Relation of I,I; func LexOrder(I,R) -> Relation of I* means :LO: for p,q being I-valued FinSequence holds [p,q] in it iff p c< q or ex k being Nat st k in dom p & k in dom q & [p.k,q.k] in R & for n being Nat st 1 <= n < k holds p.n = q.n; existence proof defpred R[Element of I*, Element of I*] means \$1 c< \$2 or ex k being Nat st k in dom \$1 & k in dom \$2 & [\$1.k,\$2.k] in R & for n being Nat st 1 <= n < k holds \$1.n = \$2.n; consider R being Relation of I* such that A1: for b1,b2 being Element of I* holds [b1,b2] in R iff R[b1,b2] from RELSET_1:sch 2; take R; let b1,b2 be I-valued FinSequence; rng b1 c= I & rng b2 c= I by RELAT_1:def 19; then b1 is FinSequence of I & b2 is FinSequence of I by FINSEQ_1:def 4; then b1 in I* & b2 in I* by FINSEQ_1:def 11; hence thesis by A1; end; uniqueness proof let R1,R2 be Relation of I* such that A1: for p,q being I-valued FinSequence holds [p,q] in R1 iff p c< q or ex k being Nat st k in dom p & k in dom q & [p.k,q.k] in R & for n being Nat st 1 <= n < k holds p.n = q.n and A2: for p,q being I-valued FinSequence holds [p,q] in R2 iff p c< q or ex k being Nat st k in dom p & k in dom q & [p.k,q.k] in R & for n being Nat st 1 <= n < k holds p.n = q.n; let p,q be Element of I*; [p,q] in R1 iff p c< q or ex k being Nat st k in dom p & k in dom q & [p.k,q.k] in R & for n being Nat st 1 <= n < k holds p.n = q.n by A1; hence thesis by A2; end; end; registration let I; let R be transitive Relation of I; cluster LexOrder(I,R) -> transitive; coherence proof set Q = LexOrder(I,R); let a,b,c be object; assume a in field Q & b in field Q & c in field Q; assume A1: [a,b] in Q & [b,c] in Q; then reconsider a,b,c as Element of I* by ZFMISC_1:87; per cases by A1,LO; suppose a c< b & b c< c; then a c< c by XBOOLE_1:56; hence thesis by LO; end; suppose A2: a c< b & ex k being Nat st k in dom b & k in dom c & [b.k,c.k] in R & for n being Nat st 1 <= n < k holds b.n = c.n; then consider k being Nat such that A3: k in dom b & k in dom c & [b.k,c.k] in R & for n being Nat st 1 <= n < k holds b.n = c.n; per cases; suppose A4: len a < k; k <= len c by A3,FINSEQ_3:25; then A5: len a < len c by A4,XXREAL_0:2; for n being Nat st n in dom a holds a.n = c.n proof let n be Nat; assume A6: n in dom a; then n <= len a by FINSEQ_3:25; then 1 <= n < k by A4,A6,XXREAL_0:2,FINSEQ_3:25; then b.n = c.n by A3; hence thesis by A2,A6,Lem12; end; then a c< c by A5,Lem12; hence thesis by LO; end; suppose A7: len a >= k; 1 <= k by A3,FINSEQ_3:25; then A8: k in dom a by A7,FINSEQ_3:25; then A9: [a.k,c.k] in R by A2,A3,Lem12; for n being Nat st 1 <= n < k holds a.n = c.n proof let n be Nat; assume A10: 1 <= n < k; then n < len a by A7,XXREAL_0:2; then n in dom a by A10,FINSEQ_3:25; then a.n = b.n by A2,Lem12; hence thesis by A10,A3; end; hence thesis by A3,A8,A9,LO; end; end; suppose A12: b c< c & ex k being Nat st k in dom a & k in dom b & [a.k,b.k] in R & for n being Nat st 1 <= n < k holds a.n = b.n; then consider k being Nat such that A11: k in dom a & k in dom b & [a.k,b.k] in R & for n being Nat st 1 <= n < k holds a.n = b.n; dom b c= dom c by A12,XBOOLE_0:def 8,XTUPLE_0:8; then A13: k in dom c & [a.k,c.k] in R by A12,A11,Lem12; for n being Nat st 1 <= n < k holds a.n = c.n proof let n be Nat; assume A14: 1 <= n < k; k <= len b by A11,FINSEQ_3:25; then n < len b by A14,XXREAL_0:2; then b.n = c.n by A12,Lem12,A14,FINSEQ_3:25; hence thesis by A11,A14; end; hence thesis by A11,A13,LO; end; suppose A15: (ex k being Nat st k in dom a & k in dom b & [a.k,b.k] in R & for n being Nat st 1 <= n < k holds a.n = b.n) & ex k being Nat st k in dom b & k in dom c & [b.k,c.k] in R & for n being Nat st 1 <= n < k holds b.n = c.n; then consider k1 being Nat such that A16: k1 in dom a & k1 in dom b & [a.k1,b.k1] in R & for n being Nat st 1 <= n < k1 holds a.n = b.n; consider k2 being Nat such that A17: k2 in dom b & k2 in dom c & [b.k2,c.k2] in R & for n being Nat st 1 <= n < k2 holds b.n = c.n by A15; per cases by XXREAL_0:1; suppose A18: k1 < k2; k2 <= len c by A17,FINSEQ_3:25; then 1 <= k1 < len c by A16,A18,FINSEQ_3:25,XXREAL_0:2; then A19: k1 in dom c & [a.k1,c.k1] in R by A16,A17,A18,FINSEQ_3:25; for n being Nat st 1 <= n < k1 holds a.n = c.n proof let n be Nat; assume 1 <= n < k1; then a.n = b.n & 1 <= n < k2 by A16,A18,XXREAL_0:2; hence thesis by A17; end; hence thesis by A16,A19,LO; end; suppose A20: k1 = k2; then A21: [a.k1,c.k1] in R by A16,A17,RELAT_2:31; for n being Nat st 1 <= n < k1 holds a.n = c.n proof let n be Nat; assume 1 <= n < k1; then a.n = b.n & b.n = c.n by A16,A17,A20; hence thesis; end; hence thesis by A20,A16,A17,A21,LO; end; suppose A22: k1 > k2; k1 <= len a by A16,FINSEQ_3:25; then 1 <= k2 < len a by A17,A22,FINSEQ_3:25,XXREAL_0:2; then A19: k2 in dom a & [a.k2,c.k2] in R by A16,A17,A22,FINSEQ_3:25; for n being Nat st 1 <= n < k2 holds a.n = c.n proof let n be Nat; assume 1 <= n < k2; then c.n = b.n & 1 <= n < k1 by A17,A22,XXREAL_0:2; hence thesis by A16; end; hence thesis by A17,A19,LO; end; end; end; end; registration let I; let R be asymmetric Relation of I; cluster LexOrder(I,R) -> asymmetric; coherence proof set Q = LexOrder(I,R); let a,b be object; assume a in field Q & b in field Q; assume A1: [a,b] in Q & [b,a] in Q; then reconsider a,b as Element of I* by ZFMISC_1:87; set c = a; per cases by A1,LO; suppose a c< b & b c< c; hence thesis; end; suppose A2: a c< b & ex k being Nat st k in dom b & k in dom c & [b.k,c.k] in R & for n being Nat st 1 <= n < k holds b.n = c.n; then consider k being Nat such that A3: k in dom b & k in dom c & [b.k,c.k] in R & for n being Nat st 1 <= n < k holds b.n = c.n; [a.k,c.k] in R by A2,A3,Lem12; hence thesis by PREFER_1:22; end; suppose A12: b c< c & ex k being Nat st k in dom a & k in dom b & [a.k,b.k] in R & for n being Nat st 1 <= n < k holds a.n = b.n; then consider k being Nat such that A11: k in dom a & k in dom b & [a.k,b.k] in R & for n being Nat st 1 <= n < k holds a.n = b.n; k in dom c & [a.k,c.k] in R by A12,A11,Lem12; hence thesis by PREFER_1:22; end; suppose A15: (ex k being Nat st k in dom a & k in dom b & [a.k,b.k] in R & for n being Nat st 1 <= n < k holds a.n = b.n) & ex k being Nat st k in dom b & k in dom c & [b.k,c.k] in R & for n being Nat st 1 <= n < k holds b.n = c.n; then consider k1 being Nat such that A16: k1 in dom a & k1 in dom b & [a.k1,b.k1] in R & for n being Nat st 1 <= n < k1 holds a.n = b.n; consider k2 being Nat such that A17: k2 in dom b & k2 in dom c & [b.k2,c.k2] in R & for n being Nat st 1 <= n < k2 holds b.n = c.n by A15; per cases by XXREAL_0:1; suppose A18: k1 < k2; k2 <= len c by A17,FINSEQ_3:25; then 1 <= k1 < len c by A16,A18,FINSEQ_3:25,XXREAL_0:2; then k1 in dom c & [a.k1,c.k1] in R by A16,A17,A18; hence thesis by PREFER_1:22; end; suppose k1 = k2; hence thesis by A16,A17,PREFER_1:22; end; suppose A22: k1 > k2; k1 <= len a by A16,FINSEQ_3:25; then 1 <= k2 < len a by A17,A22,FINSEQ_3:25,XXREAL_0:2; then k2 in dom a & [a.k2,c.k2] in R by A16,A17,A22; hence thesis by PREFER_1:22; end; end; end; end; theorem for R being asymmetric Relation of I for p,q,r being I-valued FinSequence holds [p,q] in LexOrder(I,R) iff [r^p,r^q] in LexOrder(I,R) proof let R be asymmetric Relation of I; let p,q,r be I-valued FinSequence; hereby assume [p,q] in LexOrder(I,R); then per cases by LO; suppose p c< q; then r^p c= r^q & r^p <> r^q by FINSEQ_6:13,FINSEQ_1:33,XBOOLE_0:def 8; then r^p c< r^q by XBOOLE_0:def 8; hence [r^p,r^q] in LexOrder(I,R) by LO; end; suppose ex k being Nat st k in dom p & k in dom q & [p.k,q.k] in R & for n being Nat st 1 <= n < k holds p.n = q.n; then consider k being Nat such that A1: k in dom p & k in dom q & [p.k,q.k] in R & for n being Nat st 1 <= n < k holds p.n = q.n; set i = len r; set j = i+k; A2: j in dom(r^p) & j in dom(r^q) by A1,FINSEQ_1:28; A3: (r^p).j = p.k & (r^q).j = q.k by A1,FINSEQ_1:def 7; for n being Nat st 1 <= n < j holds (r^p).n = (r^q).n proof let n be Nat; assume A4: 1 <= n < j; per cases by NAT_1:13; suppose n <= i; then n in dom r by A4,FINSEQ_3:25; then (r^p).n = r.n = (r^q).n by FINSEQ_1:def 7; hence thesis; end; suppose i+1 <= n; then consider m being Nat such that A5: n = i+1+m by NAT_1:10; A5A: n = i+(1+m) by A5; then A6: 1 <= 1+m < k by A4,NAT_1:11,XREAL_1:6; k <= len p & k <= len q by A1,FINSEQ_3:25; then 1 <= 1+m <= len p & 1+m <= len q by A6,XXREAL_0:2; then 1+m in dom p & 1+m in dom q by FINSEQ_3:25; then (r^p).n = p.(1+m) & (r^q).n = q.(1+m) by A5A,FINSEQ_1:def 7; hence thesis by A1,A6; end; end; hence [r^p,r^q] in LexOrder(I,R) by LO,A1,A2,A3; end; end; assume [r^p,r^q] in LexOrder(I,R); then per cases by LO; suppose r^p c< r^q; then p c< q by Lem13; hence [p,q] in LexOrder(I,R) by LO; end; suppose ex k being Nat st k in dom(r^p) & k in dom(r^q) & [(r^p).k,(r^q).k] in R & for n being Nat st 1 <= n < k holds (r^p).n = (r^q).n; then consider k being Nat such that A1: k in dom(r^p) & k in dom(r^q) & [(r^p).k,(r^q).k] in R & for n being Nat st 1 <= n < k holds (r^p).n = (r^q).n; set i = len r; A3: 1 <= k by A1,FINSEQ_3:25; now assume k <= i; then k in dom r by A3,FINSEQ_3:25; then (r^p).k = r.k = (r^q).k by FINSEQ_1:def 7; hence contradiction by A1,PREFER_1:22; end; then k >= i+1 by NAT_1:13; then consider j being Nat such that A4: k = i+1+j by NAT_1:10; A5: k = i+(1+j) by A4; k <= len(r^p) = i+len p & k <= len(r^q) = i+len q by A1,FINSEQ_3:25,FINSEQ_1:22; then A9: 1 <= 1+j <= len p & 1+j <= len q by A5,NAT_1:11,XREAL_1:6; then A6: 1+j in dom p & 1+j in dom q by FINSEQ_3:25; then A7: (r^p).k = p.(1+j) & (r^q).k = q.(1+j) by A5,FINSEQ_1:def 7; for n being Nat st 1 <= n < 1+j holds p.n = q.n proof let n be Nat; assume A8: 1 <= n < 1+j; then n < len p & n < len q by A9,XXREAL_0:2; then n in dom p & n in dom q by A8,FINSEQ_3:25; then p.n = (r^p).(i+n) & q.n = (r^q).(i+n) & 1 <= i+n < k by FINSEQ_1:def 7,NAT_1:12,XREAL_1:6,A5,A8; hence thesis by A1; end; hence thesis by LO,A1,A6,A7; end; end; definition let R; func PrecPrecM R -> strict RelExtension of finite-MultiSet_over the carrier of R means :PPM: for m,n being Element of it holds m <= n iff [OrderedPartition m, OrderedPartition n] in LexOrder(the carrier of PrecM R, the InternalRel of PrecM R); existence proof set I = the carrier of R; set M = finite-MultiSet_over I; defpred R[bag of I,bag of I] means [OrderedPartition \$1, OrderedPartition \$2] in LexOrder(the carrier of PrecM R, the InternalRel of PrecM R); consider N being strict RelExtension of M such that A1: for m,n being Element of N holds m <= n iff R[m,n] from RelEx; take N; thus thesis by A1; end; uniqueness proof let N1,N2 be strict RelExtension of finite-MultiSet_over the carrier of R such that A1: for m,n being Element of N1 holds m <= n iff [OrderedPartition m, OrderedPartition n] in LexOrder(the carrier of PrecM R, the InternalRel of PrecM R) and A2: for m,n being Element of N2 holds m <= n iff [OrderedPartition m, OrderedPartition n] in LexOrder(the carrier of PrecM R, the InternalRel of PrecM R); for m,n being Element of N1 for x,y being Element of N2 st m = x & n = y holds m <= n iff x <= y proof let m,n be Element of N1; let k,l be Element of N2; assume Z0: m = k; assume Z1: n = l; m <= n iff [OrderedPartition m, OrderedPartition n] in LexOrder(the carrier of PrecM R, the InternalRel of PrecM R) by A1; hence thesis by A2,Z0,Z1; end; hence thesis by Th4; end; end; registration let R; cluster PrecPrecM R -> asymmetric transitive; coherence proof set Q = the InternalRel of PrecPrecM R; thus PrecPrecM R is asymmetric proof let a,b be object; assume a in the carrier of PrecPrecM R & b in the carrier of PrecPrecM R; then reconsider m = a, n = b as Element of PrecPrecM R; assume [a,b] in Q & [b,a] in Q; then m <= n <= m by ORDERS_2:def 5; then [OrderedPartition m, OrderedPartition n] in LexOrder(the carrier of PrecM R, the InternalRel of PrecM R) & [OrderedPartition n, OrderedPartition m] in LexOrder(the carrier of PrecM R, the InternalRel of PrecM R) by PPM; hence thesis by PREFER_1:22; end; let a,b,c be object; assume a in the carrier of PrecPrecM R & b in the carrier of PrecPrecM R & c in the carrier of PrecPrecM R; then reconsider m = a, n = b, o = c as Element of PrecPrecM R; assume [a,b] in Q & [b,c] in Q; then m <= n <= o by ORDERS_2:def 5; then [OrderedPartition m, OrderedPartition n] in LexOrder(the carrier of PrecM R, the InternalRel of PrecM R) & [OrderedPartition n, OrderedPartition o] in LexOrder(the carrier of PrecM R, the InternalRel of PrecM R) by PPM; then [OrderedPartition m, OrderedPartition o] in LexOrder(the carrier of PrecM R, the InternalRel of PrecM R) by RELAT_2:31; then m <= o by PPM; hence thesis by ORDERS_2:def 5; end; end; theorem for a,b being Element of DershowitzMannaOrder R st a <= b holds b <> EmptyBag the carrier of R proof set DM = DershowitzMannaOrder R; set I = the carrier of R; set E = EmptyBag I; let a,b be Element of DM; assume Z0: a <= b; per cases; suppose a = E; hence b <> E by Z0; end; suppose A1: a <> E; E divides a by PRE_POLY:59; then [E,a] in DivOrder I c= the InternalRel of DM by A1,DO,Th16; hence thesis by Z0,ORDERS_2:def 5; end; end; theorem for a,b,c,d being Element of DershowitzMannaOrder R for e being bag of the carrier of R st a <= b & e divides a & e divides b holds c = a-'e & d = b-'e implies c <= d proof let a,b,c,d be Element of DershowitzMannaOrder R; let e be bag of the carrier of R; assume Z1: a <= b; assume Z2: e divides a; assume Z3: e divides b; assume Z4: c = a-'e; assume d = b-'e; then A0: a = c+e & b = d+e & a <> b by Z1,Z2,Z3,Z4,PRE_POLY:47; for x st c.x > d.x ex y st x <= y & c.y < d.y proof let x; assume c.x > d.x; then a.x = c.x+e.x > d.x+e.x = b.x by A0,PRE_POLY:def 5,XREAL_1:6; then consider y such that A2: x <= y & a.y < b.y by Z1,HO; take y; a.y = c.y+e.y & b.y = d.y+e.y by A0,PRE_POLY:def 5; hence thesis by A2,XREAL_1:6; end; hence c <= d by A0,HO; end; theorem Lem14: for p being Bags I-valued FinSequence, x being object st x in I & (Sum p).x > 0 ex i being Nat st i in dom p & (p/.i).x > 0 proof let p be Bags I-valued FinSequence; let x be object; assume Z0: x in I; assume Z1: (Sum p).x > 0; defpred P[object] means for p being Bags I-valued FinSequence st p = \$1 & (Sum p).x > 0 ex i being Nat st i in dom p & (p/.i).x > 0; A1: P[ {} ] proof let p be Bags I-valued FinSequence; assume p = {}; then p = <*>Bags I; then Sum p = EmptyBag I by Th21; hence thesis by Z0,FUNCOP_1:7; end; A2: for p being FinSequence, a being object st P[p] holds P[p^<*a*>] proof let p be FinSequence; let a be object; assume Z0: P[p]; let q be Bags I-valued FinSequence; assume A3: q = p^<*a*>; then reconsider p, aa = <*a*> as Bags I-valued FinSequence by Lem8; len aa = 1 by FINSEQ_1:40; then 1 in dom aa by FINSEQ_3:25; then aa.1 in Bags I by FUNCT_1:102; then reconsider a as Element of Bags I by FINSEQ_1:40; assume (Sum q).x > 0; then (Sum p).x+a.x = ((Sum p)+a).x > 0 by Th22,A3,PRE_POLY:def 5; then per cases; suppose A4: a.x > 0; take i = len p+1; len q = len p+1 >= 1 by A3,NAT_1:11,FINSEQ_2:16; hence i in dom q by FINSEQ_3:25; then q/.i = q.i by PARTFUN1:def 6; hence thesis by A4,A3,FINSEQ_1:42; end; suppose (Sum p).x > 0; then consider i being Nat such that A5: i in dom p & (p/.i).x > 0 by Z0; take i; A6: dom p c= dom q by A3,FINSEQ_1:26; hence i in dom q by A5; q/.i = q.i = p.i by A3,A5,A6,FINSEQ_1:def 7,PARTFUN1:def 6; hence (q/.i).x > 0 by PARTFUN1:def 6,A5; end; end; for p being FinSequence holds P[p] from FINSEQ_1:sch 3(A1,A2); hence thesis by Z1; end; theorem q is ordered & (q/.1).x = 0 & b.x > 0 implies ex y st (q/.1).y > 0 & x <= y proof assume Z0: q is ordered; assume Z2: (q/.1).x = 0; assume Z3: b.x > 0; defpred P[Nat] means \$1 in dom q implies for x st (q/.\$1).x > 0 ex y st (q/.1).y > 0 & x <= y; A1: P[2] proof assume A2: 2 in dom q; then 2 <= len q by FINSEQ_3:25; then 1 <= len q by XXREAL_0:2; then 1 in dom q & 2 = 1+1 by FINSEQ_3:25; hence thesis by A2,Z0; end; A3: for i being Nat st 2 <= i & P[i] holds P[i+1] proof let i be Nat; assume A4: 2 <= i & P[i] & i+1 in dom q; then i <= i+1 <= len q by NAT_1:11,FINSEQ_3:25; then A0: 1 <= i <= len q by A4,XXREAL_0:2; then A5: i in dom q by FINSEQ_3:25; let x; assume (q/.(i+1)).x > 0; then consider y such that A6: (q/.i).y > 0 & x <= y by Z0,A4,A5; consider z such that A7: (q/.1).z > 0 & y <= z by A4,A0,A6,FINSEQ_3:25; take z; thus (q/.1).z > 0 by A7; thus x <= z by A6,A7,ORDERS_2:3; end; A8: for i being Nat st i >= 2 holds P[i] from NAT_1:sch 8(A1,A3); b = Sum q by PART; then consider i being Nat such that A9: i in dom q & (q/.i).x > 0 by Z3,Lem14; 1 <= i & i <> 1 by A9,Z2,FINSEQ_3:25; then 1 < i by XXREAL_0:1; then 1+1 <= i by NAT_1:13; hence thesis by A8,A9; end;