The abstract of the Mizar article:

On Ordering of Bags

by

Gilbert Lee, and

Piotr Rudnicki

Received March 12, 2002

MML identifier: BAGORDER

[ Mizar article, MML identifier index ]

environ

 vocabulary DICKSON, BAGORDER, TARSKI, ARYTM_1, ARYTM_3, RELAT_1, WELLORD1,
      RELAT_2, MCART_1, CAT_1, ORDINAL2, ORDERS_1, FUNCT_1, RLVECT_1, RLVECT_2,
      FUNCOP_1, SEQM_3, ALGSEQ_1, BOOLE, PBOOLE, ORDINAL1, CARD_1, CARD_3,
      FINSET_1, FINSUB_1, NORMSP_1, POLYNOM1, FINSEQ_1, FINSEQ_2, GRAPH_2,
      WAYBEL_4, WELLFND1, FUNCT_4, WELLORD2, TRIANG_1, SQUARE_1, ORDERS_2,
      FINSEQ_4, PROB_1, FUNCT_2, RFINSEQ, PARTFUN1;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, STRUCT_0, RELAT_1, RELAT_2,
      RELSET_1, FINSET_1, FINSUB_1, CQC_LANG, ORDINAL1, MCART_1, WELLORD1,
      ORDERS_1, ORDERS_2, WELLFND1, NUMBERS, XREAL_0, REAL_1, NAT_1, FUNCT_1,
      SEQM_3, WAYBEL_0, CARD_1, NORMSP_1, PBOOLE, PRALG_1, CARD_3, DICKSON,
      BINARITH, FINSEQ_1, WSIERP_1, POLYNOM1, RVSUM_1, PRE_CIRC, YELLOW_1,
      WAYBEL_4, PARTFUN1, FUNCT_2, FUNCT_4, TRIANG_1, POLYNOM2, FINSEQ_4,
      CQC_SIM1, DOMAIN_1, FINSEQOP, RFINSEQ;
 constructors WELLFND1, PRE_CIRC, REAL_1, FINSEQOP, DOMAIN_1, BINARITH,
      DICKSON, WSIERP_1, WAYBEL_4, TRIANG_1, POLYNOM2, ORDERS_2, CQC_SIM1;
 clusters DICKSON, YELLOW_1, ORDERS_1, CARD_1, POLYNOM1, BINARITH, STRUCT_0,
      RELSET_1, SUBSET_1, WAYBEL_0, FINSET_1, FINSUB_1, CARD_5, CQC_LANG,
      ORDINAL1, FUNCT_1, FINSEQ_1, XREAL_0, MEMBERED, RELAT_1, FUNCT_2,
      NUMBERS, ORDINAL2;
 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} iff x = y;

theorem :: BAGORDER:2
  for n, k being Nat holds k in Seg n iff k-1 is Nat & k-1 < n;

definition
  let f be natural-yielding Function, X be set;
  cluster f|X -> natural-yielding;
end;

definition
  let f be finite-support Function, X be set;
  cluster f|X -> finite-support;
end;

theorem :: BAGORDER:3
for f being Function, x being set st x in dom f holds f*<*x*> = <*f.x*>;

theorem :: BAGORDER:4
for f, g, h being Function
 st dom f = dom g & rng f c= dom h & rng g c= dom h &
    f, g are_fiberwise_equipotent
  holds h*f, h*g are_fiberwise_equipotent;

theorem :: BAGORDER:5
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 Nat st k in j-'i holds it.k = b.(i+k);
end;

definition
  let n,i,j be Nat, b be natural-yielding ManySortedSet of n;
  cluster (i,j)-cut b -> natural-yielding;
end;

definition
  let n,i,j be Nat, b be finite-support ManySortedSet of n;
  cluster (i,j)-cut b -> finite-support;
end;

theorem :: BAGORDER:6
  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 empty Nat;
  func Fin (x,n) equals
:: BAGORDER:def 2
    {y where y is Element of bool x : y is finite & y is non empty &
                                      Card y <=` n};
end;

definition
  let x be non empty set, n be non empty Nat;
  cluster Fin (x,n) -> non empty;
end;

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_maximal_wrt X, the InternalRel of R;

theorem :: BAGORDER:8
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:9
  for R being non empty antisymmetric transitive RelStr, f being sequence of R
 st f is descending
  holds for j, i being Nat st i<j
          holds f.i<>f.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:10
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<j holds [f.j,f.i] in the InternalRel of R;

theorem :: BAGORDER:11
for R being non empty transitive RelStr, s being sequence of R
 st R is well_founded & s is non-increasing
  holds ex p being Nat st for r being Nat st p <= r holds s.p = s.r;

theorem :: BAGORDER:12
for X being set, a be Element of X, A being finite Subset of X,
    R being Order of X st A = {a} & R linearly_orders A
  holds SgmX (R, A) = <*a*>;

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:13
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:14
for n being Ordinal, a, b being bag of n
  holds TotDegree (a+b) = TotDegree a + TotDegree b;

theorem :: BAGORDER:15
  for n be Ordinal, a,b being bag of n
 st b divides a holds TotDegree(a-'b) = TotDegree(a) - TotDegree(b);

theorem :: BAGORDER:16
for n being Ordinal, b being bag of n holds TotDegree b = 0 iff b = EmptyBag n;

theorem :: BAGORDER:17
for i,j,n being Nat holds (i,j)-cut EmptyBag n = EmptyBag (j-'i);

theorem :: BAGORDER:18
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);

theorem :: BAGORDER:19
  for X being set holds support EmptyBag X = {};

theorem :: BAGORDER:20
for X being set, b be bag of X st support b = {} holds b = EmptyBag X;

theorem :: BAGORDER:21
for n, m being Ordinal, b being bag of n st m in n holds b|m is bag of m;

theorem :: BAGORDER:22
  for n being Ordinal, 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;
  canceled;
end;

definition
  let n be Ordinal;
  redefine func BagOrder n;
  synonym LexOrder n;
  canceled;
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 7
  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:23  :: 4.61 i) Lexicographical order is admissible
for n being Ordinal holds LexOrder n is admissible;

definition
  let n be Ordinal;
  cluster admissible TermOrder of n;
end;

definition
  let n be Ordinal;
  cluster LexOrder n -> admissible;
end;

theorem :: BAGORDER:24
  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 8
  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:25  :: Ex 4.61 ii
for n being Ordinal holds InvLexOrder n is admissible;

definition
  let n be Ordinal;
  cluster InvLexOrder n -> admissible;
end;

theorem :: BAGORDER:26
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 9
       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:27  :: 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 10
    Graded LexOrder n;
  func GrInvLexOrder n -> TermOrder of n equals
:: BAGORDER:def 11         :: Ex 4.61: iiic
    Graded InvLexOrder n;
end;

theorem :: BAGORDER:28
                                           :: Ex 4.61: iiib
for n being Ordinal holds GrLexOrder n is admissible;

definition
  let n be Ordinal;
  cluster GrLexOrder n -> admissible;
end;

theorem :: BAGORDER:29
  for o being infinite Ordinal holds GrLexOrder o is non well-ordering;

theorem :: BAGORDER:30
for n being Ordinal holds GrInvLexOrder n is admissible;

definition
  let n be Ordinal;
  cluster GrInvLexOrder n -> admissible;
end;

theorem :: BAGORDER:31
  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 12
   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:32 ::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 13
     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:33
for n being Nat holds the carrier of product(n --> OrderedNAT) = Bags n;

theorem :: BAGORDER:34
for n being Nat holds NaivelyOrderedBags n = product (n --> OrderedNAT);

theorem :: BAGORDER:35 ::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 14 :: FPOSMIN :
      it in X & it is_minimal_wrt X, the InternalRel of R;
  func PosetMax X -> Element of R means
:: BAGORDER:def 15
    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 ->
           Function of NAT, bool[: Fin the carrier of R, Fin the carrier of R:]
    means
:: BAGORDER:def 16
  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 Element of 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:36
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:37
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:38
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:39
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 17
       union rng FinOrd-Approx R;
end;

definition
  let R be connected (non empty Poset);
  func FinPoset R -> Poset equals
:: BAGORDER:def 18
     RelStr (# Fin the carrier of R, FinOrd R #);
end;

definition
  let R be connected (non empty Poset);
  cluster FinPoset R -> non empty;
end;

theorem :: BAGORDER:40
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);

definition
  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 19
   it in C & it is_minimal_wrt C, the InternalRel of R;
end;

definition
  let R  be non empty RelStr, s be sequence of R, j  be Nat;
  func SeqShift (s, j) -> sequence of R means
:: BAGORDER:def 20
    for i being Nat holds it.i = s.(i+j);
end;

theorem :: BAGORDER:41
for R being non empty RelStr, s being sequence of R, j being Nat
 st s is descending holds SeqShift(s, j) is descending;

theorem :: BAGORDER:42 :: Theorem 4:69
  for R being connected (non empty Poset)
  st R is well_founded holds FinPoset R is well_founded;