:: On Multiset Ordering
:: by Grzegorz Bancerek
::
:: Copyright (c) 2015-2018 Association of Mizar Users

theorem Th6: :: BAGORD_2:1
for m, n being Nat holds n = (m -' (m -' n)) + (n -' m)
proof end;

theorem Lem1: :: BAGORD_2:2
for n, m being Nat holds m -' n >= m - n
proof end;

theorem Th5: :: BAGORD_2:3
for m, n, x, y being Nat st n = (m -' x) + y holds
( m -' n <= x & n -' m <= y )
proof end;

theorem Th5A: :: BAGORD_2:4
for m, n, x, y being Nat st x <= m & n = (m -' x) + y holds
x -' (m -' n) = y -' (n -' m)
proof end;

theorem Th14: :: 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) )
proof end;

theorem :: BAGORD_2:6
for x, y being Nat holds
( not x + y > 0 or x > 0 or y > 0 ) ;

registration
let I be set ;
let J be non empty set ;
cluster Function-like V28(I,J) -> total for Function of ,;
coherence
for b1 being Function of I,J holds b1 is total
proof end;
end;

registration
existence
ex b1 being RelStr st
( b1 is asymmetric & b1 is transitive & not b1 is empty )
proof end;
end;

registration
let I be set ;
existence
ex b1 being Relation of I st
( b1 is asymmetric & b1 is transitive )
proof end;
end;

registration
let R be transitive RelStr ;
cluster the InternalRel of R -> transitive ;
coherence
the InternalRel of R is transitive
proof end;
end;

registration
let R be asymmetric RelStr ;
cluster the InternalRel of R -> asymmetric ;
coherence
the InternalRel of R is asymmetric
by NECKLACE:def 4;
end;

registration
let I be set ;
let p, q be I -valued FinSequence;
cluster p ^ q -> I -valued ;
coherence
p ^ q is I -valued
proof end;
end;

theorem Lem8: :: BAGORD_2:7
for I being set
for p, q being FinSequence st p ^ q is I -valued holds
( p is I -valued & q is I -valued )
proof end;

registration
let I be set ;
let f be I -valued FinSequence;
let n be Nat;
cluster f | n -> I -valued ;
coherence
f | n is I -valued
;
end;

theorem Lem9: :: BAGORD_2:8
for a being object
for p being FinSequence st a in rng p holds
ex q, r being FinSequence st p = (q ^ <*a*>) ^ r
proof end;

theorem Lem12: :: 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 ) ) )
proof end;

theorem Lem13: :: BAGORD_2:10
for p, q, r being FinSequence holds
( r ^ p c< r ^ q iff p c< q )
proof end;

definition
let R be non empty asymmetric RelStr ;
let x, y be Element of R;
:: original: <=
redefine pred x <= y;
asymmetry
for x, y being Element of R st R42(R,b1,b2) holds
not R42(R,b2,b1)
proof end;
end;

theorem Lem2: :: BAGORD_2:11
for R being non empty asymmetric RelStr
for x, y being Element of R holds
( x <= y iff x < y )
proof end;

definition
let I be set ;
mode multiset of I is Element of ;
end;

registration
let I be set ;
cluster -> I -defined natural-valued for multiset of I;
coherence
for b1 being multiset of I holds
( b1 is I -defined & b1 is natural-valued )
proof end;
end;

registration
let I be set ;
cluster -> total for multiset of I;
coherence
for b1 being multiset of I holds b1 is total
proof end;
end;

definition
let m be natural-valued Function;
redefine func support m equals :: BAGORD_2:def 1
m " ();
compatibility
for b1 being set holds
( b1 = support m iff b1 = m " () )
proof end;
end;

:: deftheorem defines support BAGORD_2:def 1 :
for m being natural-valued Function holds support m = m " ();

registration
let I be set ;
cluster -> finite-support for multiset of I;
coherence
for b1 being multiset of I holds b1 is finite-support
proof end;
end;

theorem Th1: :: BAGORD_2:12
for a being object
for I being set holds
( a is multiset of I iff a is bag of I )
proof end;

theorem Th11: :: BAGORD_2:13
for I being set holds 1. = EmptyBag I
proof end;

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
for x, y being Element of R st not x <= y & not y <= x holds
( not y <= x & not x <= y )
;
end;

:: deftheorem defines ## BAGORD_2:def 2 :
for R being RelStr
for x, y being Element of R holds
( x ## y iff ( not x <= y & not y <= x ) );

definition end;

definition end;

definition
let M be multLoopStr ;
mode RelExtension of M -> RelMonoid means :RE: :: BAGORD_2:def 3
multLoopStr(# the carrier of it, the multF of it, the OneF of it #) = multLoopStr(# the carrier of M, the multF of M, the OneF of M #);
existence
ex b1 being RelMonoid st multLoopStr(# the carrier of b1, the multF of b1, the OneF of b1 #) = multLoopStr(# the carrier of M, the multF of M, the OneF of M #)
proof end;
end;

:: deftheorem RE defines RelExtension BAGORD_2:def 3 :
for M being multLoopStr
for b2 being RelMonoid holds
( b2 is RelExtension of M iff multLoopStr(# the carrier of b2, the multF of b2, the OneF of b2 #) = multLoopStr(# the carrier of M, the multF of M, the OneF of M #) );

registration
let M be non empty multLoopStr ;
cluster -> non empty for RelExtension of M;
coherence
for b1 being RelExtension of M holds not b1 is empty
proof end;
end;

registration
let M be multLoopStr ;
cluster strict for RelExtension of M;
existence
ex b1 being RelExtension of M st b1 is strict
proof end;
end;

theorem Th2: :: BAGORD_2:14
for a being object
for N being multLoopStr
for M being RelExtension of N holds
( a is Element of M iff a is Element of N )
proof end;

theorem Th3: :: BAGORD_2:15
for N being multLoopStr
for M being RelExtension of N holds 1. N = 1. M
proof end;

registration
let I be set ;
let M be RelExtension of finite-MultiSet_over I;
coherence
for b1 being Element of M holds
( b1 is Function-like & b1 is Relation-like )
proof end;
end;

registration
let I be set ;
let M be RelExtension of finite-MultiSet_over I;
coherence
for b1 being Element of M holds
( b1 is I -defined & b1 is natural-valued & b1 is finite-support )
proof end;
end;

registration
let I be set ;
let M be RelExtension of finite-MultiSet_over I;
cluster -> total for Element of M;
coherence
for b1 being Element of M holds b1 is total
proof end;
end;

theorem :: BAGORD_2:16
for I being set
for M being RelExtension of finite-MultiSet_over I holds the carrier of M = Bags I
proof end;

scheme :: BAGORD_2:sch 1
RelEx{ F1() -> non empty multLoopStr , P1[ object , object ] } :
ex N being strict RelExtension of F1() st
for x, y being Element of N holds
( x <= y iff P1[x,y] )
proof end;

theorem Th4: :: BAGORD_2:17
for N being multLoopStr
for 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 end;

definition
let R be non empty RelStr ;
func DershowitzMannaOrder R -> strict RelExtension of finite-MultiSet_over the carrier of R means :DM: :: 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 & x divides n & m = (n -' x) + y & ( for b being Element of R st y . b > 0 holds
ex a being Element of R st
( x . a > 0 & b <= a ) ) ) );
existence
ex b1 being strict RelExtension of finite-MultiSet_over the carrier of R st
for m, n being Element of b1 holds
( m <= n iff ex x, y being Element of b1 st
( 1. b1 <> x & x divides n & m = (n -' x) + y & ( for b being Element of R st y . b > 0 holds
ex a being Element of R st
( x . a > 0 & b <= a ) ) ) )
proof end;
uniqueness
for b1, b2 being strict RelExtension of finite-MultiSet_over the carrier of R st ( for m, n being Element of b1 holds
( m <= n iff ex x, y being Element of b1 st
( 1. b1 <> x & x divides n & m = (n -' x) + y & ( for b being Element of R st y . b > 0 holds
ex a being Element of R st
( x . a > 0 & b <= a ) ) ) ) ) & ( for m, n being Element of b2 holds
( m <= n iff ex x, y being Element of b2 st
( 1. b2 <> x & x divides n & m = (n -' x) + y & ( for b being Element of R st y . b > 0 holds
ex a being Element of R st
( x . a > 0 & b <= a ) ) ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem DM defines DershowitzMannaOrder BAGORD_2:def 4 :
for R being non empty RelStr
for b2 being strict RelExtension of finite-MultiSet_over the carrier of R holds
( b2 = DershowitzMannaOrder R iff for m, n being Element of b2 holds
( m <= n iff ex x, y being Element of b2 st
( 1. b2 <> x & x divides n & m = (n -' x) + y & ( for b being Element of R st y . b > 0 holds
ex a being Element of R st
( x . a > 0 & b <= a ) ) ) ) );

theorem Th7: :: BAGORD_2:18
for I being set
for m, n being bag of I holds n = (m -' (m -' n)) + (n -' m)
proof end;

theorem Th8: :: BAGORD_2:19
for I being set
for m, n, x, y being bag of I st n = (m -' x) + y holds
( m -' n divides x & n -' m divides y )
proof end;

theorem Th8A: :: BAGORD_2:20
for I being set
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 end;

theorem Th9: :: BAGORD_2:21
for I being set
for m, x, y being bag of I st x divides m & x <> y holds
m <> (m -' x) + y
proof end;

theorem Lem5: :: BAGORD_2:22
for I being non empty set
for R being Relation of I
for r being RedSequence of R st len r > 1 holds
r . (len r) in I
proof end;

theorem Th13: :: BAGORD_2:23
for I being set
for R being asymmetric transitive Relation of I
for r being RedSequence of R holds r is one-to-one
proof end;

theorem Th12: :: BAGORD_2:24
for R being non empty transitive asymmetric RelStr
for X being set st X is finite & ex x being Element of R st x in X holds
ex x being Element of R st x is_maximal_in X
proof end;

theorem Lem3: :: BAGORD_2:25
for I being set
for m, n being bag of I holds m -' n divides m
proof end;

registration
let I be set ;
cluster -> Relation-like Function-like for of ;
coherence
for b1 being Element of Bags I holds
( b1 is Function-like & b1 is Relation-like )
by PRE_POLY:def 12;
end;

theorem Lem4: :: BAGORD_2:26
for I being set
for m, n being bag of I holds
( m -' n <> EmptyBag I or m = n or n -' m <> EmptyBag I )
proof end;

definition
let R be non empty transitive asymmetric RelStr ;
redefine func DershowitzMannaOrder R means :HO: :: 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 holds
ex b being Element of R st
( a <= b & m . b < n . b ) ) ) );
compatibility
for b1 being strict RelExtension of finite-MultiSet_over the carrier of R holds
( b1 = DershowitzMannaOrder R iff for m, n being Element of b1 holds
( m <= n iff ( m <> n & ( for a being Element of R st m . a > n . a holds
ex b being Element of R st
( a <= b & m . b < n . b ) ) ) ) )
proof end;
end;

:: deftheorem HO defines DershowitzMannaOrder BAGORD_2:def 5 :
for R being non empty transitive asymmetric RelStr
for b2 being strict RelExtension of finite-MultiSet_over the carrier of R holds
( b2 = DershowitzMannaOrder R iff for m, n being Element of b2 holds
( m <= n iff ( m <> n & ( for a being Element of R st m . a > n . a holds
ex b being Element of R st
( a <= b & m . b < n . b ) ) ) ) );

theorem Th15: :: BAGORD_2:27
for I being set
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 end;

registration
let R be non empty transitive asymmetric RelStr ;
coherence
proof end;
end;

definition
let I be set ;
func DivOrder I -> Relation of (Bags I) means :DO: :: BAGORD_2:def 6
for b1, b2 being bag of I holds
( [b1,b2] in it iff ( b1 <> b2 & b1 divides b2 ) );
existence
ex b1 being Relation of (Bags I) st
for b1, b2 being bag of I holds
( [b1,b2] in b1 iff ( b1 <> b2 & b1 divides b2 ) )
proof end;
uniqueness
for b1, b2 being Relation of (Bags I) st ( for b1, b2 being bag of I holds
( [b1,b2] in b1 iff ( b1 <> b2 & b1 divides b2 ) ) ) & ( for b1, b2 being bag of I holds
( [b1,b2] in b2 iff ( b1 <> b2 & b1 divides b2 ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem DO defines DivOrder BAGORD_2:def 6 :
for I being set
for b2 being Relation of (Bags I) holds
( b2 = DivOrder I iff for b1, b2 being bag of I holds
( [b1,b2] in b2 iff ( b1 <> b2 & b1 divides b2 ) ) );

theorem Lem7: :: BAGORD_2:28
for I being set
for a, b, c being bag of I st a divides b & b divides c holds
a divides c
proof end;

registration
let I be set ;
coherence
( DivOrder I is asymmetric & DivOrder I is transitive )
proof end;
end;

theorem Th16: :: BAGORD_2:29
for R being non empty transitive asymmetric RelStr holds DivOrder the carrier of R c= the InternalRel of
proof end;

theorem :: BAGORD_2:30
for R being non empty transitive asymmetric RelStr st the InternalRel of R is empty holds
the InternalRel of = DivOrder the carrier of R
proof end;

theorem :: BAGORD_2:31
for R1, R2 being non empty transitive asymmetric RelStr st the carrier of R1 = the carrier of R2 & the InternalRel of R1 c= the InternalRel of R2 holds
the InternalRel of () c= the InternalRel of ()
proof end;

definition
let I be set ;
let f be Bags I -valued FinSequence;
func Sum f -> bag of I means :SUM: :: 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 ) );
existence
ex b1 being bag of I ex F being Function of NAT,(Bags I) st
( b1 = 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 ) )
proof end;
uniqueness
for b1, b2 being bag of I st ex F being Function of NAT,(Bags I) st
( b1 = 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 ) ) & ex F being Function of NAT,(Bags I) st
( b2 = 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 ) ) holds
b1 = b2
proof end;
end;

:: deftheorem SUM defines Sum BAGORD_2:def 7 :
for I being set
for f being Bags b1 -valued FinSequence
for b3 being bag of I holds
( b3 = Sum f iff ex F being Function of NAT,(Bags I) st
( b3 = 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 ) ) );

theorem Th21: :: BAGORD_2:32
for I being set holds Sum (<*> (Bags I)) = EmptyBag I
proof end;

registration
let I be set ;
let b be bag of I;
cluster K286(b) -> Bags I -valued for FinSequence;
coherence
for b1 being FinSequence st b1 = <*b*> holds
b1 is Bags I -valued
proof end;
end;

theorem Th22: :: BAGORD_2:33
for I being set
for p being Bags b1 -valued FinSequence
for b being bag of I holds Sum (p ^ <*b*>) = (Sum p) + b
proof end;

theorem Th23: :: BAGORD_2:34
for I being set
for b being bag of I holds Sum <*b*> = b
proof end;

theorem Th24: :: BAGORD_2:35
for I being set
for p, q being Bags b1 -valued FinSequence holds Sum (p ^ q) = (Sum p) + (Sum q)
proof end;

theorem Th25: :: BAGORD_2:36
for I being set
for b being bag of I
for p being Bags b1 -valued FinSequence holds Sum (<*b*> ^ p) = b + (Sum p)
proof end;

theorem Th26: :: BAGORD_2:37
for I being set
for b being bag of I
for p being Bags b1 -valued FinSequence st b in rng p holds
b divides Sum p
proof end;

theorem Th27: :: BAGORD_2:38
for I being set
for p being Bags b1 -valued FinSequence
for i being object st i in support (Sum p) holds
ex b being bag of I st
( b in rng p & i in support b )
proof end;

definition
let I be set ;
let b be bag of I;
mode partition of b -> Bags I -valued FinSequence means :PART: :: BAGORD_2:def 8
b = Sum it;
existence
ex b1 being Bags I -valued FinSequence st b = Sum b1
proof end;
end;

:: deftheorem PART defines partition BAGORD_2:def 8 :
for I being set
for b being bag of I
for b3 being Bags b1 -valued FinSequence holds
( b3 is partition of b iff b = Sum b3 );

definition
let I be set ;
let b be bag of I;
:: original: <*
redefine func <*b*> -> partition of b;
coherence
<*b*> is partition of b
proof 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 :: BAGORD_2:def 9
for i being Nat st i in dom p & i + 1 in dom p holds
for b1, b2 being Element of M st b1 = p . i & b2 = p . (i + 1) holds
b2 <= b1;
end;

:: deftheorem defines co-ordered BAGORD_2:def 9 :
for R being RelStr
for M being RelExtension of finite-MultiSet_over the carrier of R
for b being Element of M
for p being partition of b holds
( p is co-ordered iff for i being Nat st i in dom p & i + 1 in dom p holds
for b1, b2 being Element of M st b1 = p . i & b2 = p . (i + 1) holds
b2 <= b1 );

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 holds
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 holds
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 holds
for x being Element of R st (p /. (i + 1)) . x > 0 holds
ex y being Element of R st
( (p /. i) . y > 0 & x <= y ) ) );
end;

:: deftheorem defines ordered BAGORD_2:def 10 :
for R being non empty RelStr
for b being bag of the carrier of R
for p being partition of b holds
( p is ordered iff ( ( for m being bag of the carrier of R st m in rng p holds
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 holds
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 holds
for x being Element of R st (p /. (i + 1)) . x > 0 holds
ex y being Element of R st
( (p /. i) . y > 0 & x <= y ) ) ) );

theorem :: BAGORD_2:39
for R being non empty transitive asymmetric RelStr
for a being bag of the carrier of R holds
( <*a*> is ordered iff ( a <> EmptyBag the carrier of R & ( for x, y being Element of R st a . x > 0 & a . y > 0 & x <> y holds
x ## y ) ) )
proof end;

theorem Th28: :: BAGORD_2:40
for I being set
for p being Bags b1 -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 end;

theorem Th30: :: BAGORD_2:41
for R being non empty transitive asymmetric RelStr
for a, b being bag of the carrier of R
for p being partition of b -' a
for q being partition of b st q = <*a*> ^ p & q is ordered holds
p is ordered
proof end;

definition
let I be set ;
let m be bag of I;
let J be set ;
func m | J -> bag of I means :BAR: :: 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 ) );
existence
ex b1 being bag of I st
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 ) )
proof end;
uniqueness
for b1, b2 being bag of I st ( 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 ) ) ) & ( 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 ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem BAR defines | BAGORD_2:def 11 :
for I being set
for m being bag of I
for J being set
for b4 being bag of I holds
( b4 = m | J iff for i being object st i in I holds
( ( i in J implies b4 . i = m . i ) & ( not i in J implies b4 . i = 0 ) ) );

theorem Th44: :: BAGORD_2:42
for I, J being set
for m being bag of I holds support (m | J) = J /\ ()
proof end;

theorem :: BAGORD_2:43
for I, J being set
for m being bag of I holds (m | J) + (m | (I \ J)) = m
proof end;

theorem Th43: :: BAGORD_2:44
for I, J being set
for m being bag of I holds m | J divides m
proof end;

theorem :: BAGORD_2:45
for I, J being set
for m being bag of I st support m c= J holds
m | J = m
proof end;

theorem Th27A: :: BAGORD_2:46
for I, J being set
for m being bag of I holds support (m -' (m | J)) = () \ J
proof end;

theorem Th31: :: BAGORD_2:47
for R being non empty transitive asymmetric RelStr
for a, b being bag of the carrier of R
for x being Element of R
for p being partition of b -' a
for q being partition of b st q is ordered & q = <*a*> ^ p & a . x > 0 holds
a . x = b . x
proof end;

theorem Th32: :: BAGORD_2:48
for R being non empty transitive asymmetric RelStr
for a, b being bag of the carrier of R
for x, y being Element of R
for p being partition of b -' a
for q being partition of b st q is ordered & q = <*a*> ^ p & a . x > 0 & a . y > 0 & x <> y holds
x ## y
proof end;

theorem Th32A: :: BAGORD_2:49
for R being non empty transitive asymmetric RelStr
for a, b being bag of the carrier of R
for p being partition of b -' a
for q being partition of b st q is ordered & q = <*a*> ^ p holds
a <> EmptyBag the carrier of R
proof end;

theorem :: BAGORD_2:50
for R being non empty transitive asymmetric RelStr
for a, b being bag of the carrier of R
for y being Element of R
for q being partition of b
for c being bag of the carrier of R
for r being Bags the carrier of b1 -valued FinSequence st q is ordered & q = <*a,c*> ^ r & c . y > 0 holds
ex x being Element of R st
( a . x > 0 & y <= x )
proof end;

theorem :: BAGORD_2:51
for I being set
for R being non empty transitive asymmetric RelStr
for x being Element of R st x in I & ( for y being Element of R st y in I & y <> x holds
x ## y ) holds
x is_maximal_in I
proof end;

theorem Th36: :: BAGORD_2:52
for R being non empty transitive asymmetric RelStr
for a, b, c being bag of the carrier of R
for x being Element of R
for p being partition of b -' a
for q being partition of b st q is ordered & q = <*a*> ^ p & c in rng p & c . x > 0 holds
ex y being Element of R st
( a . y > 0 & x <= y )
proof end;

theorem Th34: :: BAGORD_2:53
for R being non empty transitive asymmetric RelStr
for a, b being bag of the carrier of R
for x being Element of R
for p being partition of b -' a
for q being partition of b st q is ordered & q = <*a*> ^ p holds
( x is_maximal_in support b iff a . x > 0 )
proof end;

theorem Th40: :: BAGORD_2:54
for R being non empty transitive asymmetric RelStr
for a, b being bag of the carrier of R
for p being partition of b -' a
for q being partition of b st q is ordered & q = <*a*> ^ p holds
a = b | { x where x is Element of R : x is_maximal_in support b }
proof end;

theorem Lem10: :: BAGORD_2:55
for I being set
for p being Bags b1 -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 end;

theorem Lem11: :: BAGORD_2:56
for I being set
for a, b being bag of I st a <> EmptyBag I holds
a + b <> EmptyBag I
proof end;

theorem :: BAGORD_2:57
for R being non empty transitive asymmetric RelStr
for b being bag of the carrier of R
for p, q being partition of b st p is ordered & q is ordered holds
p = q
proof end;

definition
let I be set ;
let a, b be bag of I;
:: original: [
redefine func [a,b] -> Element of [:(Bags I),(Bags I):];
coherence
[a,b] is Element of [:(Bags I),(Bags I):]
proof end;
end;

theorem Th42: :: BAGORD_2:58
for R being non empty transitive asymmetric RelStr
for a being bag of the carrier of R st a <> EmptyBag the carrier of R holds
{ x where x is Element of R : x is_maximal_in support a } <> {}
proof end;

definition
let R be non empty transitive asymmetric RelStr ;
let b be bag of the carrier of R;
func OrderedPartition b -> Bags the carrier of R -valued FinSequence means :OP: :: 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 where x is Element of R : 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
ex b1 being Bags the carrier of R -valued FinSequence 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 where x is Element of R : 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 & b1 = G | (Seg i) & ( for j being Nat st j < i holds
F . j <> EmptyBag the carrier of R ) ) )
proof end;
uniqueness
for b1, b2 being Bags the carrier of R -valued FinSequence st 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 where x is Element of R : 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 & b1 = G | (Seg i) & ( for j being Nat st j < i holds
F . j <> EmptyBag the carrier of R ) ) ) & 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 where x is Element of R : 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 & b2 = G | (Seg i) & ( for j being Nat st j < i holds
F . j <> EmptyBag the carrier of R ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem OP defines OrderedPartition BAGORD_2:def 12 :
for R being non empty transitive asymmetric RelStr
for b being bag of the carrier of R
for b3 being Bags the carrier of b1 -valued FinSequence holds
( b3 = OrderedPartition b iff 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 where x is Element of R : 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 & b3 = G | (Seg i) & ( for j being Nat st j < i holds
F . j <> EmptyBag the carrier of R ) ) ) );

definition
let R be non empty transitive asymmetric RelStr ;
let b be bag of the carrier of R;
:: original: OrderedPartition
redefine func OrderedPartition b -> partition of b;
coherence
proof end;
end;

registration
let R be non empty transitive asymmetric RelStr ;
let b be bag of the carrier of R;
cluster (R,b) -> ordered for partition of b;
coherence
for b1 being partition of b st b1 = OrderedPartition b holds
b1 is ordered
proof end;
end;

theorem :: BAGORD_2:59
for R being non empty transitive asymmetric RelStr
for b being bag of the carrier of R holds
( b = EmptyBag the carrier of R iff OrderedPartition b = {} )
proof end;

definition
let R be non empty transitive asymmetric RelStr ;
func PrecM R -> strict RelExtension of finite-MultiSet_over the carrier of R means :PM: :: BAGORD_2:def 13
for m, n being Element of it holds
( m <= n iff ( m <> n & ( for x being Element of R holds
( not m . x > 0 or m . x < n . x or ex y being Element of R st
( n . y > 0 & x <= y ) ) ) ) );
existence
ex b1 being strict RelExtension of finite-MultiSet_over the carrier of R st
for m, n being Element of b1 holds
( m <= n iff ( m <> n & ( for x being Element of R holds
( not m . x > 0 or m . x < n . x or ex y being Element of R st
( n . y > 0 & x <= y ) ) ) ) )
proof end;
uniqueness
for b1, b2 being strict RelExtension of finite-MultiSet_over the carrier of R st ( for m, n being Element of b1 holds
( m <= n iff ( m <> n & ( for x being Element of R holds
( not m . x > 0 or m . x < n . x or ex y being Element of R st
( n . y > 0 & x <= y ) ) ) ) ) ) & ( for m, n being Element of b2 holds
( m <= n iff ( m <> n & ( for x being Element of R holds
( not m . x > 0 or m . x < n . x or ex y being Element of R st
( n . y > 0 & x <= y ) ) ) ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem PM defines PrecM BAGORD_2:def 13 :
for R being non empty transitive asymmetric RelStr
for b2 being strict RelExtension of finite-MultiSet_over the carrier of R holds
( b2 = PrecM R iff for m, n being Element of b2 holds
( m <= n iff ( m <> n & ( for x being Element of R holds
( not m . x > 0 or m . x < n . x or ex y being Element of R st
( n . y > 0 & x <= y ) ) ) ) ) );

registration
let R be non empty transitive asymmetric RelStr ;
coherence
( PrecM R is asymmetric & PrecM R is transitive )
proof end;
end;

definition
let I be set ;
let R be Relation of I,I;
func LexOrder (I,R) -> Relation of (I *) means :LO: :: 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 & n < k holds
p . n = q . n ) ) ) );
existence
ex b1 being Relation of (I *) st
for p, q being I -valued FinSequence holds
( [p,q] in b1 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 & n < k holds
p . n = q . n ) ) ) )
proof end;
uniqueness
for b1, b2 being Relation of (I *) st ( for p, q being I -valued FinSequence holds
( [p,q] in b1 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 & n < k holds
p . n = q . n ) ) ) ) ) & ( for p, q being I -valued FinSequence holds
( [p,q] in b2 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 & n < k holds
p . n = q . n ) ) ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem LO defines LexOrder BAGORD_2:def 14 :
for I being set
for R being Relation of I,I
for b3 being Relation of (I *) holds
( b3 = LexOrder (I,R) iff for p, q being b1 -valued FinSequence holds
( [p,q] in b3 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 & n < k holds
p . n = q . n ) ) ) ) );

registration
let I be set ;
let R be transitive Relation of I;
cluster LexOrder (I,R) -> transitive ;
coherence
LexOrder (I,R) is transitive
proof end;
end;

registration
let I be set ;
let R be asymmetric Relation of I;
cluster LexOrder (I,R) -> asymmetric ;
coherence
LexOrder (I,R) is asymmetric
proof end;
end;

theorem :: BAGORD_2:60
for I being set
for R being asymmetric Relation of I
for p, q, r being b1 -valued FinSequence holds
( [p,q] in LexOrder (I,R) iff [(r ^ p),(r ^ q)] in LexOrder (I,R) )
proof end;

definition
let R be non empty transitive asymmetric RelStr ;
func PrecPrecM R -> strict RelExtension of finite-MultiSet_over the carrier of R means :PPM: :: BAGORD_2:def 15
for m, n being Element of it holds
( m <= n iff [(),()] in LexOrder ( the carrier of (), the InternalRel of ()) );
existence
ex b1 being strict RelExtension of finite-MultiSet_over the carrier of R st
for m, n being Element of b1 holds
( m <= n iff [(),()] in LexOrder ( the carrier of (), the InternalRel of ()) )
proof end;
uniqueness
for b1, b2 being strict RelExtension of finite-MultiSet_over the carrier of R st ( for m, n being Element of b1 holds
( m <= n iff [(),()] in LexOrder ( the carrier of (), the InternalRel of ()) ) ) & ( for m, n being Element of b2 holds
( m <= n iff [(),()] in LexOrder ( the carrier of (), the InternalRel of ()) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem PPM defines PrecPrecM BAGORD_2:def 15 :
for R being non empty transitive asymmetric RelStr
for b2 being strict RelExtension of finite-MultiSet_over the carrier of R holds
( b2 = PrecPrecM R iff for m, n being Element of b2 holds
( m <= n iff [(),()] in LexOrder ( the carrier of (), the InternalRel of ()) ) );

registration
let R be non empty transitive asymmetric RelStr ;
coherence
proof end;
end;

theorem :: BAGORD_2:61
for R being non empty transitive asymmetric RelStr
for a, b being Element of st a <= b holds
b <> EmptyBag the carrier of R
proof end;

theorem :: BAGORD_2:62
for R being non empty transitive asymmetric RelStr
for a, b, c, d being Element of
for e being bag of the carrier of R st a <= b & e divides a & e divides b & c = a -' e & d = b -' e holds
c <= d
proof end;

theorem Lem14: :: BAGORD_2:63
for I being set
for p being Bags b1 -valued FinSequence
for x being object st x in I & (Sum p) . x > 0 holds
ex i being Nat st
( i in dom p & (p /. i) . x > 0 )
proof end;

theorem :: BAGORD_2:64
for R being non empty transitive asymmetric RelStr
for b being bag of the carrier of R
for x being Element of R
for q being partition of b st q is ordered & (q /. 1) . x = 0 & b . x > 0 holds
ex y being Element of R st
( (q /. 1) . y > 0 & x <= y )
proof end;