:: On Ordering of Bags :: by Gilbert Lee and Piotr Rudnicki :: :: Received March 12, 2002 :: Copyright (c) 2002-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, XBOOLE_0, SUBSET_1, FINSEQ_1, ARYTM_1, ARYTM_3, XXREAL_0, CARD_1, NAT_1, PRE_POLY, FUNCT_1, RELAT_1, TARSKI, CLASSES1, CARD_3, FINSEQ_2, PBOOLE, GRAPH_2, VALUED_0, FINSUB_1, FINSET_1, RELAT_2, ORDERS_2, WAYBEL_4, STRUCT_0, WELLFND1, WELLORD1, ORDERS_1, ORDINAL1, WELLORD2, ORDINAL4, REAL_1, FUNCOP_1, FUNCT_4, PARTFUN1, DICKSON, RLVECT_2, ZFMISC_1, MCART_1, BAGORDER, XCMPLX_0; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, XCMPLX_0, RELAT_1, PBOOLE, RELAT_2, RELSET_1, PARTFUN1, FINSET_1, FINSUB_1, ORDINAL1, FUNCT_7, XTUPLE_0, MCART_1, WELLORD1, ORDERS_1, WELLFND1, CARD_1, NUMBERS, VALUED_0, XXREAL_0, XREAL_0, FUNCT_1, PRE_POLY, CARD_3, NAT_D, FINSEQ_1, FINSEQ_2, RVSUM_1, WSIERP_1, FUNCOP_1, FUNCT_2, SEQ_4, DOMAIN_1, FINSEQOP, CLASSES1, RECDEF_1, NAT_1, STRUCT_0, WAYBEL_0, YELLOW_1, WAYBEL_4, PRALG_1, ORDERS_2, DICKSON; constructors DOMAIN_1, FINSEQOP, NAT_D, WSIERP_1, PRALG_1, TRIANG_1, WAYBEL_4, WELLFND1, DICKSON, RECDEF_1, BINOP_2, SEQ_4, CLASSES1, RELSET_1, FUNCT_7, REAL_1, XTUPLE_0, WELLORD1, PRE_POLY, NUMBERS; registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, FUNCT_2, FINSET_1, FINSUB_1, NUMBERS, XXREAL_0, XREAL_0, NAT_1, CARD_1, MEMBERED, FINSEQ_1, CARD_5, STRUCT_0, ORDERS_2, WAYBEL_0, YELLOW_1, DICKSON, VALUED_0, XXREAL_2, RELSET_1, PRE_POLY, WELLORD1, WELLORD2, XTUPLE_0; requirements SUBSET, NUMERALS, REAL, BOOLE, ARITHM; begin :: Preliminaries theorem :: BAGORDER:1 for x,y,z being set st z in x & z in y holds x \ {z} = y \ {z} implies x = y; theorem :: BAGORDER:2 for n, k being Element of NAT holds k in Seg n iff k-1 is Element of NAT & k-1 < n; registration let f be finite-support Function, X be set; cluster f|X -> finite-support; end; ::$CT theorem :: BAGORDER:4 for fs being FinSequence of NAT holds Sum fs = 0 iff fs = (len fs) |-> 0; definition let n,i,j be Nat, b be ManySortedSet of n; func (i,j)-cut b -> ManySortedSet of j-'i means :: BAGORDER:def 1 for k being Element of NAT st k in j-'i holds it.k = b.(i+k); end; registration let n,i,j be Nat, b be natural-valued ManySortedSet of n; cluster (i,j)-cut b -> natural-valued; end; registration let n,i,j be Element of NAT, b be finite-support ManySortedSet of n; cluster (i,j)-cut b -> finite-support; end; theorem :: BAGORDER:5 for n,i being Nat, a,b being ManySortedSet of n holds a = b iff (0,i+1)-cut a = (0,i+1)-cut b & (i+1,n)-cut a = (i+1,n)-cut b; definition let x be non empty set, n be non zero Element of NAT; func Fin (x,n) -> set equals :: BAGORDER:def 2 {y where y is Subset of x : y is finite & y is non empty & card y c= n}; end; registration let x be non empty set, n be non zero Element of NAT; cluster Fin (x,n) -> non empty; end; theorem :: BAGORDER:6 for R being antisymmetric transitive non empty RelStr, X being finite Subset of R st X <> {} holds ex x being Element of R st x in X & x is_maximal_wrt X, the InternalRel of R; theorem :: BAGORDER:7 for R being antisymmetric transitive non empty RelStr, X being finite Subset of R st X <> {} holds ex x being Element of R st x in X & x is_minimal_wrt X, the InternalRel of R; theorem :: BAGORDER:8 for R being non empty antisymmetric transitive RelStr, f being sequence of R st f is descending holds for j, i being Nat st if.j & [f.j,f.i] in the InternalRel of R; definition let R be non empty RelStr, s be sequence of R; attr s is non-increasing means :: BAGORDER:def 3 for i being Nat holds [s.(i+1),s.i] in the InternalRel of R; end; theorem :: BAGORDER:9 for R being non empty transitive RelStr, f being sequence of R st f is non-increasing holds for j, i being Nat st i; begin :: More about bags definition let n be Ordinal, b be bag of n; func TotDegree b -> Nat means :: BAGORDER:def 4 ex f being FinSequence of NAT st it = Sum f & f = b*SgmX(RelIncl n, support b); end; theorem :: BAGORDER:12 for n being Ordinal, b being bag of n, s being finite Subset of n, f, g being FinSequence of NAT st f = b*SgmX(RelIncl n, support b) & g = b*SgmX(RelIncl n, support b \/ s) holds Sum f = Sum g; theorem :: BAGORDER:13 for n being Ordinal, a, b being bag of n holds TotDegree (a+b) = TotDegree a + TotDegree b; theorem :: BAGORDER:14 for n be Ordinal, a,b being bag of n st b divides a holds TotDegree(a-'b) = TotDegree(a) - TotDegree(b); theorem :: BAGORDER:15 for n being Ordinal, b being bag of n holds TotDegree b = 0 iff b = EmptyBag n; theorem :: BAGORDER:16 for i,j,n being Nat holds (i,j)-cut EmptyBag n = EmptyBag (j-'i); theorem :: BAGORDER:17 for i,j,n being Nat, a,b being bag of n holds (i,j)-cut (a+b) = (i,j)-cut(a) + (i,j)-cut(b); ::$CT 2 theorem :: BAGORDER:20 for n, m being Ordinal, b being bag of n st m in n holds b|m is bag of m; theorem :: BAGORDER:21 for n being set, a, b being bag of n st b divides a holds support b c= support a; begin :: Some Special Orders (Section 4.4) definition let n be set; mode TermOrder of n is Order of Bags n; end; notation let n be Ordinal; synonym LexOrder n for BagOrder n; end; definition :: Definition 4.59 - admissible (specific for Bags) let n be Ordinal, T be TermOrder of n; attr T is admissible means :: BAGORDER:def 5 T is_strongly_connected_in Bags n & (for a being bag of n holds [EmptyBag n, a] in T) & for a, b, c being bag of n st [a, b] in T holds [a+c, b+c] in T; end; theorem :: BAGORDER:22 :: 4.61 i) Lexicographical order is admissible for n being Ordinal holds LexOrder n is admissible; registration let n be Ordinal; cluster LexOrder n -> admissible; end; registration let n be Ordinal; cluster admissible for TermOrder of n; end; theorem :: BAGORDER:23 for o being infinite Ordinal holds LexOrder o is non well-ordering; definition let n be Ordinal; func InvLexOrder n -> TermOrder of n means :: BAGORDER:def 6 for p,q being bag of n holds [p,q] in it iff p = q or ex i being Ordinal st i in n & p.i < q.i & for k being Ordinal st i in k & k in n holds p.k = q.k; end; theorem :: BAGORDER:24 :: Ex 4.61 ii for n being Ordinal holds InvLexOrder n is admissible; registration let n be Ordinal; cluster InvLexOrder n -> admissible; end; theorem :: BAGORDER:25 for o being Ordinal holds InvLexOrder o is well-ordering; definition let n be Ordinal, o be TermOrder of n such that for a,b,c being bag of n st [a,b] in o holds [a+c, b+c] in o; func Graded o -> TermOrder of n means :: BAGORDER:def 7 for a, b being bag of n holds [a,b] in it iff ( TotDegree a < TotDegree b or TotDegree a = TotDegree b & [a,b] in o ); end; theorem :: BAGORDER:26 :: Exercise 4.61: iiia for n being Ordinal, o being TermOrder of n st (for a,b,c being bag of n st [a,b] in o holds [a+c, b+c] in o) & o is_strongly_connected_in Bags n holds Graded o is admissible; definition let n be Ordinal; func GrLexOrder n -> TermOrder of n equals :: BAGORDER:def 8 Graded LexOrder n; func GrInvLexOrder n -> TermOrder of n equals :: BAGORDER:def 9 :: Ex 4.61: iiic Graded InvLexOrder n; end; theorem :: BAGORDER:27 :: Ex 4.61: iiib for n being Ordinal holds GrLexOrder n is admissible; registration let n be Ordinal; cluster GrLexOrder n -> admissible; end; theorem :: BAGORDER:28 for o being infinite Ordinal holds GrLexOrder o is non well-ordering; theorem :: BAGORDER:29 for n being Ordinal holds GrInvLexOrder n is admissible; registration let n be Ordinal; cluster GrInvLexOrder n -> admissible; end; theorem :: BAGORDER:30 for o being Ordinal holds GrInvLexOrder o is well-ordering; definition let i,n be Nat, o1 be TermOrder of (i+1), o2 be TermOrder of (n-'(i+1)); func BlockOrder(i,n,o1,o2) -> TermOrder of n means :: BAGORDER:def 10 for p,q being bag of n holds [p,q] in it iff (0,i+1)-cut p <> (0,i+1)-cut q & [(0,i+1)-cut p,(0,i+1)-cut q] in o1 or (0,i+1)-cut p = (0,i+1)-cut q & [(i+1,n)-cut p,(i+1,n)-cut q] in o2; end; theorem :: BAGORDER:31 ::E_4_61_iv: :: Exercise 4.61: iv for i,n being Nat, o1 being TermOrder of (i+1), o2 being TermOrder of (n-'(i+1)) st o1 is admissible & o2 is admissible holds BlockOrder(i,n,o1,o2) is admissible; definition let n be Nat; func NaivelyOrderedBags n -> strict RelStr means :: BAGORDER:def 11 the carrier of it = Bags n & for x,y being bag of n holds [x,y] in the InternalRel of it iff x divides y; end; theorem :: BAGORDER:32 for n being Nat holds the carrier of product(n --> OrderedNAT) = Bags n; theorem :: BAGORDER:33 for n being Nat holds NaivelyOrderedBags n = product (n --> OrderedNAT); theorem :: BAGORDER:34 ::T_4_62: :: Theorem 4.62 for n being Nat, o be TermOrder of n st o is admissible holds the InternalRel of NaivelyOrderedBags n c= o & o is well-ordering; begin :: Ordering of finite subsets definition let R be connected non empty Poset, X be Element of Fin the carrier of R such that X is non empty; func PosetMin X -> Element of R means :: BAGORDER:def 12 :: FPOSMIN : it in X & it is_minimal_wrt X, the InternalRel of R; func PosetMax X -> Element of R means :: BAGORDER:def 13 it in X & it is_maximal_wrt X, the InternalRel of R; end; definition let R be connected non empty Poset; func FinOrd-Approx R -> sequence of bool[: Fin the carrier of R, Fin the carrier of R:] means :: BAGORDER:def 14 dom it = NAT & it.0 = {[x,y] where x, y is Element of Fin the carrier of R : x = {} or (x<>{} & y <> {} & PosetMax x <> PosetMax y & [PosetMax x,PosetMax y] in the InternalRel of R)} & for n being Nat holds it.(n+1) = {[x,y] where x,y is Element of Fin the carrier of R : x <> {} & y <> {} & PosetMax x = PosetMax y & [x \{PosetMax x}, y \{PosetMax y}] in it.n}; end; theorem :: BAGORDER:35 for R being connected non empty Poset, x,y being Element of Fin the carrier of R holds [x,y] in union rng FinOrd-Approx R iff x = {} or x<>{} & y<>{} & PosetMax x <> PosetMax y & [PosetMax x,PosetMax y] in the InternalRel of R or x<>{} & y<>{} & PosetMax x = PosetMax y & [x\{PosetMax x},y\{PosetMax y}] in union rng FinOrd-Approx R; theorem :: BAGORDER:36 for R being connected non empty Poset, x being Element of Fin the carrier of R st x <> {} holds not [x,{}] in union rng FinOrd-Approx R; theorem :: BAGORDER:37 for R being connected non empty Poset, a being Element of Fin the carrier of R holds a\{PosetMax a} is Element of Fin the carrier of R; theorem :: BAGORDER:38 for R being connected non empty Poset holds union (rng FinOrd-Approx R) is Order of Fin the carrier of R; definition let R be connected non empty Poset; func FinOrd R -> Order of Fin (the carrier of R) equals :: BAGORDER:def 15 union rng FinOrd-Approx R; end; definition let R be connected non empty Poset; func FinPoset R -> Poset equals :: BAGORDER:def 16 RelStr (# Fin the carrier of R, FinOrd R #); end; registration let R be connected non empty Poset; cluster FinPoset R -> non empty; end; theorem :: BAGORDER:39 for R being connected non empty Poset,a,b being Element of FinPoset R holds [a,b] in the InternalRel of FinPoset R iff ex x,y being Element of Fin the carrier of R st a = x & b = y & (x = {} or x<>{} & y<>{} & PosetMax x <> PosetMax y & [PosetMax x,PosetMax y] in the InternalRel of R or x<>{} & y<>{} & PosetMax x = PosetMax y & [x\{PosetMax x},y\{PosetMax y}] in FinOrd R); registration let R be connected non empty Poset; cluster FinPoset R -> connected; end; definition let R be connected non empty RelStr, C be non empty set such that R is well_founded and C c= the carrier of R; func MinElement (C,R)-> Element of R means :: BAGORDER:def 17 it in C & it is_minimal_wrt C, the InternalRel of R; end; theorem :: BAGORDER:40 for R being non empty RelStr, s being sequence of R, j being Nat st s is descending holds s^\j is descending; theorem :: BAGORDER:41 :: Theorem 4:69 for R being connected non empty Poset st R is well_founded holds FinPoset R is well_founded;