:: On Multiset Ordering :: by Grzegorz Bancerek :: :: Received December 31, 2015 :: Copyright (c) 2015-2018 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; begin theorem :: BAGORD_2:1 for m,n being Nat holds n = (m-'(m-'n))+(n-'m); theorem :: BAGORD_2:2 for n,m being Nat holds m-'n >= m-n; theorem :: BAGORD_2:3 for m,n,x,y being Nat st n = (m-'x)+y holds m-'n <= x & n-'m <= y; theorem :: BAGORD_2:4 for m,n,x,y being Nat st x <= m & n = (m-'x)+y holds x-'(m-'n) = y-'(n-'m); theorem :: BAGORD_2:5 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); theorem :: BAGORD_2:6 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; end; registration cluster asymmetric transitive non empty for RelStr; end; registration let I; cluster asymmetric transitive for Relation of I; end; registration let R be transitive RelStr; cluster the InternalRel of R -> transitive; end; registration let R be asymmetric RelStr; cluster the InternalRel of R -> asymmetric; end; registration let I; let p,q be I-valued FinSequence; cluster p^q -> I-valued; end; theorem :: BAGORD_2:7 for p,q being FinSequence st p^q is I-valued holds p is I-valued & q is I-valued; registration let I; let f be I-valued FinSequence; let n be Nat; cluster f|n -> I-valued; end; theorem :: BAGORD_2:8 for p being FinSequence st a in rng p ex q,r being FinSequence st p = q^<*a*>^r; theorem :: BAGORD_2:9 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; theorem :: BAGORD_2:10 for p,q,r being FinSequence holds r^p c< r^q iff p c< q; definition let R be asymmetric non empty RelStr; let x,y be Element of R; redefine pred x <= y; asymmetry; end; theorem :: BAGORD_2:11 for R being asymmetric non empty RelStr for x,y being Element of R holds x <= y iff x < y; 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; end; registration let I; cluster -> total for multiset of I; end; definition let m be natural-valued Function; redefine func support m equals :: BAGORD_2:def 1 m"(NAT\{0}); end; registration let I; cluster -> finite-support for multiset of I; end; theorem :: BAGORD_2:12 a is multiset of I iff a is bag of I; theorem :: BAGORD_2:13 1.finite-MultiSet_over I = EmptyBag I; definition let R be RelStr; let x,y be Element of R; pred x ## y means :: BAGORD_2:def 2 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 :: BAGORD_2:def 3 the multLoopStr of it = the multLoopStr of M; end; registration let M be non empty multLoopStr; cluster -> non empty for RelExtension of M; end; registration let M be multLoopStr; cluster strict for RelExtension of M; end; theorem :: BAGORD_2:14 for N being multLoopStr, M being RelExtension of N holds a is Element of M iff a is Element of N; theorem :: BAGORD_2:15 for N being multLoopStr, M being RelExtension of N holds 1.N = 1.M; registration let I; let M be RelExtension of finite-MultiSet_over I; cluster -> Function-like Relation-like for Element of M; end; registration let I; let M be RelExtension of finite-MultiSet_over I; cluster -> I-defined natural-valued finite-support for Element of M; end; registration let I; let M be RelExtension of finite-MultiSet_over I; cluster -> total for Element of M; end; theorem :: BAGORD_2:16 for M being RelExtension of finite-MultiSet_over I holds the carrier of M = Bags I; scheme :: BAGORD_2:sch 1 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]; theorem :: BAGORD_2:17 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; begin definition let R be non empty RelStr; func DershowitzMannaOrder R -> strict RelExtension of finite-MultiSet_over the carrier of R means :: BAGORD_2:def 4 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; end; theorem :: BAGORD_2:18 for m,n being bag of I holds n = (m-'(m-'n))+(n-'m); theorem :: BAGORD_2:19 for m,n,x,y being bag of I st n = (m-'x)+y holds m-'n divides x & n-'m divides y; theorem :: BAGORD_2:20 for m,n,x,y being bag of I st x divides m & n = (m-'x)+y holds x-'(m-'n) = y-'(n-'m); theorem :: BAGORD_2:21 for m,x,y being bag of I st x divides m & x <> y holds m <> (m-'x)+y; theorem :: BAGORD_2:22 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; theorem :: BAGORD_2:23 for R being asymmetric transitive Relation of I for r being RedSequence of R holds r is one-to-one; theorem :: BAGORD_2:24 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; theorem :: BAGORD_2:25 for m,n being bag of I holds m-'n divides m; registration let I; cluster -> Function-like Relation-like for Element of Bags I; end; theorem :: BAGORD_2:26 for m,n being bag of I holds m-'n <> EmptyBag I or m = n or n-'m <> EmptyBag I; definition let R being asymmetric transitive non empty RelStr; redefine func DershowitzMannaOrder R means :: BAGORD_2:def 5 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; end; theorem :: BAGORD_2:27 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); registration let R be asymmetric transitive non empty RelStr; cluster DershowitzMannaOrder R -> asymmetric transitive; end; definition let I; func DivOrder I -> Relation of Bags I means :: BAGORD_2:def 6 for b1,b2 being bag of I holds [b1,b2] in it iff b1 <> b2 & b1 divides b2; end; theorem :: BAGORD_2:28 for a,b,c being bag of I st a divides b divides c holds a divides c; registration let I; cluster DivOrder I -> asymmetric transitive; end; theorem :: BAGORD_2:29 for R being asymmetric transitive non empty RelStr holds DivOrder the carrier of R c= the InternalRel of DershowitzMannaOrder R; theorem :: BAGORD_2:30 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; theorem :: BAGORD_2:31 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; begin definition let I; let f be (Bags I)-valued FinSequence; func Sum f -> bag of I means :: BAGORD_2:def 7 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; end; theorem :: BAGORD_2:32 Sum (<*>Bags I) = EmptyBag I; registration let I; let b be bag of I; cluster <*b*> -> Bags I-valued for FinSequence; end; theorem :: BAGORD_2:33 for p being Bags I-valued FinSequence, b being bag of I holds Sum (p^<*b*>) = Sum p + b; reserve b for bag of I; theorem :: BAGORD_2:34 Sum <*b*> = b; theorem :: BAGORD_2:35 for p,q being Bags I-valued FinSequence holds Sum (p^q) = Sum p + Sum q; theorem :: BAGORD_2:36 for p being Bags I-valued FinSequence holds Sum (<*b*>^p) = b + Sum p; theorem :: BAGORD_2:37 for p being Bags I-valued FinSequence st b in rng p holds b divides Sum p; theorem :: BAGORD_2:38 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; definition let I,b; mode partition of b -> Bags I-valued FinSequence means :: BAGORD_2:def 8 b = Sum it; end; definition let I,b; redefine func <*b*> -> partition of b; 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 :: BAGORD_2:def 9 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 :: BAGORD_2:def 10 (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 :: BAGORD_2:39 <*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; theorem :: BAGORD_2:40 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; reserve p for partition of b-'a, q for partition of b; theorem :: BAGORD_2:41 q = <*a*>^p & q is ordered implies p is ordered; definition let I; let m be bag of I; let J be set; func m|J -> bag of I means :: BAGORD_2:def 11 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); end; reserve J for set, m for bag of I; theorem :: BAGORD_2:42 support (m|J) = J /\ support m; theorem :: BAGORD_2:43 (m|J)+(m|(I\J)) = m; theorem :: BAGORD_2:44 m|J divides m; theorem :: BAGORD_2:45 support m c= J implies m|J = m; theorem :: BAGORD_2:46 support(m-'(m|J)) = (support m)\J; theorem :: BAGORD_2:47 q is ordered & q = <*a*>^p & a.x > 0 implies a.x = b.x; theorem :: BAGORD_2:48 q is ordered & q = <*a*>^p & a.x > 0 & a.y > 0 & x <> y implies x ## y; theorem :: BAGORD_2:49 q is ordered & q = <*a*>^p implies a <> EmptyBag the carrier of R; theorem :: BAGORD_2:50 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; theorem :: BAGORD_2:51 x in I & (for y st y in I & y <> x holds x ## y) implies x is_maximal_in I; theorem :: BAGORD_2:52 q is ordered & q = <*a*>^p & c in rng p & c.x > 0 implies ex y st a.y > 0 & x <= y; theorem :: BAGORD_2:53 q is ordered & q = <*a*>^p implies (x is_maximal_in support b iff a.x > 0); theorem :: BAGORD_2:54 q is ordered & q = <*a*>^p implies a = b|{x:x is_maximal_in support b}; theorem :: BAGORD_2:55 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 = {}; theorem :: BAGORD_2:56 for a,b being bag of I st a <> EmptyBag I holds a+b <> EmptyBag I; theorem :: BAGORD_2:57 for p,q being partition of b st p is ordered & q is ordered holds p = q; definition let I; let a,b be bag of I; redefine func [a,b] -> Element of [:Bags I,Bags I:]; end; theorem :: BAGORD_2:58 a <> EmptyBag the carrier of R implies {x:x is_maximal_in support a} <> {}; definition let R,b; func OrderedPartition b -> Bags the carrier of R-valued FinSequence means :: BAGORD_2:def 12 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; end; definition let R,b; redefine func OrderedPartition b -> partition of b; end; registration let R,b; cluster OrderedPartition b -> ordered for partition of b; end; theorem :: BAGORD_2:59 b = EmptyBag the carrier of R iff OrderedPartition b = {}; definition let R; func PrecM R -> strict RelExtension of finite-MultiSet_over the carrier of R means :: BAGORD_2:def 13 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; end; registration let R; cluster PrecM R -> asymmetric transitive; end; definition let I; let R be Relation of I,I; func LexOrder(I,R) -> Relation of I* means :: BAGORD_2:def 14 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; end; registration let I; let R be transitive Relation of I; cluster LexOrder(I,R) -> transitive; end; registration let I; let R be asymmetric Relation of I; cluster LexOrder(I,R) -> asymmetric; end; theorem :: BAGORD_2:60 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); definition let R; func PrecPrecM R -> strict RelExtension of finite-MultiSet_over the carrier of R means :: BAGORD_2:def 15 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); end; registration let R; cluster PrecPrecM R -> asymmetric transitive; end; theorem :: BAGORD_2:61 for a,b being Element of DershowitzMannaOrder R st a <= b holds b <> EmptyBag the carrier of R; theorem :: BAGORD_2:62 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; theorem :: BAGORD_2:63 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; theorem :: BAGORD_2:64 q is ordered & (q/.1).x = 0 & b.x > 0 implies ex y st (q/.1).y > 0 & x <= y;