:: On Multiset Ordering
:: by Grzegorz Bancerek
::
:: Received December 31, 2015
:: Copyright (c) 2015-2021 Association of Mizar Users

theorem Th6: :: BAGORD_2:1

for m, n being Nat holds n = (m -' (m -' n)) + (n -' m)

proof end;

theorem :: BAGORD_2:2

for n, m being Nat holds m -' n >= m - n by XREAL_0:def 2;

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

canceled;

registration

cluster non empty transitive asymmetric for RelStr ;

existence
ex b₁ being RelStr st
( b₁ is asymmetric & b₁ is transitive & not b₁ is empty )

proof end;

end;

registration

let I be set ;

cluster Relation-like I -defined I -valued asymmetric transitive for Element of bool [:I,I:];

existence
ex b₁ being Relation of I st
( b₁ is asymmetric & b₁ 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,b₁,b₂) holds
not R42(R,b₂,b₁)

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 (finite-MultiSet_over I);

end;

registration

let I be set ;

cluster -> I -defined natural-valued for Element of the carrier of (finite-MultiSet_over I);

coherence
for b₁ being multiset of I holds
( b₁ is I -defined & b₁ is natural-valued )

proof end;

end;

registration

let I be set ;

cluster -> total for Element of the carrier of (finite-MultiSet_over I);

coherence
for b₁ being multiset of I holds b₁ is total

proof end;

end;

definition

let m be natural-valued Function;

redefine func support m equals :: BAGORD_2:def 1
m " (NAT \ {0});

compatibility
for b₁ being set holds
( b₁ = support m iff b₁ = m " (NAT \ {0}) )

proof end;

end;

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

registration

let I be set ;

cluster -> finite-support for Element of the carrier of (finite-MultiSet_over I);

coherence
for b₁ being multiset of I holds b₁ 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. (finite-MultiSet_over I) = 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

attr c₁ is strict ;
struct RelMultMagma -> multMagma , RelStr ;
aggr RelMultMagma(# carrier, multF, InternalRel #) -> RelMultMagma ;

end;

definition

attr c₁ is strict ;
struct RelMonoid -> multLoopStr , RelStr ;
aggr RelMonoid(# carrier, multF, OneF, InternalRel #) -> RelMonoid ;

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 b₁ being RelMonoid st multLoopStr(# the carrier of b₁, the multF of b₁, the OneF of b₁ #) = 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 b₂ being RelMonoid holds
( b₂ is RelExtension of M iff multLoopStr(# the carrier of b₂, the multF of b₂, the OneF of b₂ #) = 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 b₁ being RelExtension of M holds not b₁ is empty

proof end;

end;

registration

let M be multLoopStr ;

cluster strict for RelExtension of M;

existence
ex b₁ being RelExtension of M st b₁ 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;

cluster -> Relation-like Function-like for Element of the carrier of M;

coherence
for b₁ being Element of M holds
( b₁ is Function-like & b₁ is Relation-like )

proof end;

end;

registration

let I be set ;
let M be RelExtension of finite-MultiSet_over I;

cluster -> I -defined natural-valued finite-support for Element of the carrier of M;

coherence
for b₁ being Element of M holds
( b₁ is I -defined & b₁ is natural-valued & b₁ 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 the carrier of M;

coherence
for b₁ being Element of M holds b₁ 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{ F₁() -> non empty multLoopStr , P₁[ object , object ] } :

ex N being strict RelExtension of F₁() st
for x, y being Element of N holds
( x <= y iff P₁[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 b₁ being strict RelExtension of finite-MultiSet_over the carrier of R st
for m, n being Element of b₁ holds
( m <= n iff ex x, y being Element of b₁ st
( 1. b₁ <> 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 b₁, b₂ being strict RelExtension of finite-MultiSet_over the carrier of R st ( for m, n being Element of b₁ holds
( m <= n iff ex x, y being Element of b₁ st
( 1. b₁ <> 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 b₂ holds
( m <= n iff ex x, y being Element of b₂ st
( 1. b₂ <> 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
b₁ = b₂

proof end;

end;

:: deftheorem DM defines DershowitzMannaOrder BAGORD_2:def 4 :
for R being non empty RelStr
for b₂ being strict RelExtension of finite-MultiSet_over the carrier of R holds
( b₂ = DershowitzMannaOrder R iff for m, n being Element of b₂ holds
( m <= n iff ex x, y being Element of b₂ st
( 1. b₂ <> 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 Element of Bags I;

coherence
for b₁ being Element of Bags I holds
( b₁ is Function-like & b₁ 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 b₁ being strict RelExtension of finite-MultiSet_over the carrier of R holds
( b₁ = DershowitzMannaOrder R iff for m, n being Element of b₁ 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 b₂ being strict RelExtension of finite-MultiSet_over the carrier of R holds
( b₂ = DershowitzMannaOrder R iff for m, n being Element of b₂ 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 ;

cluster DershowitzMannaOrder R -> transitive asymmetric strict ;

coherence
( DershowitzMannaOrder R is asymmetric & DershowitzMannaOrder R is transitive )

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 b₁ being Relation of (Bags I) st
for b1, b2 being bag of I holds
( [b1,b2] in b₁ iff ( b1 <> b2 & b1 divides b2 ) )

proof end;

uniqueness
for b₁, b₂ being Relation of (Bags I) st ( for b1, b2 being bag of I holds
( [b1,b2] in b₁ iff ( b1 <> b2 & b1 divides b2 ) ) ) & ( for b1, b2 being bag of I holds
( [b1,b2] in b₂ iff ( b1 <> b2 & b1 divides b2 ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem DO defines DivOrder BAGORD_2:def 6 :
for I being set
for b₂ being Relation of (Bags I) holds
( b₂ = DivOrder I iff for b1, b2 being bag of I holds
( [b1,b2] in b₂ 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 ;

cluster DivOrder I -> asymmetric transitive ;

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 (DershowitzMannaOrder R)

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 (DershowitzMannaOrder R) = 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 (DershowitzMannaOrder R1) c= the InternalRel of (DershowitzMannaOrder R2)

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 b₁ being bag of I ex F being Function of NAT,(Bags I) st
( b₁ = 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 b₁, b₂ being bag of I st ex F being Function of NAT,(Bags I) st
( b₁ = 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
( b₂ = 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
b₁ = b₂

proof end;

end;

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

coherence
for b₁ being FinSequence st b₁ = <*b*> holds
b₁ is Bags I -valued

proof end;

end;

theorem Th22: :: BAGORD_2:33

for I being set
for p being Bags b₁ -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 b₁ -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 b₁ -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 b₁ -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 b₁ -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 b₁ being Bags I -valued FinSequence st b = Sum b₁

proof end;

end;

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

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 b₁ -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 b₁ being bag of I st
for i being object st i in I holds
( ( i in J implies b₁ . i = m . i ) & ( not i in J implies b₁ . i = 0 ) )

proof end;

uniqueness
for b₁, b₂ being bag of I st ( for i being object st i in I holds
( ( i in J implies b₁ . i = m . i ) & ( not i in J implies b₁ . i = 0 ) ) ) & ( for i being object st i in I holds
( ( i in J implies b₂ . i = m . i ) & ( not i in J implies b₂ . i = 0 ) ) ) holds
b₁ = b₂

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 b₄ being bag of I holds
( b₄ = m | J iff for i being object st i in I holds
( ( i in J implies b₄ . i = m . i ) & ( not i in J implies b₄ . i = 0 ) ) );

theorem Th44: :: BAGORD_2:42

for I, J being set
for m being bag of I holds support (m | J) = J /\ (support m)

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)) = (support m) \ 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 b₁ -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 b₁ -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 b₁ 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 & b₁ = G | (Seg i) & ( for j being Nat st j < i holds
F . j <> EmptyBag the carrier of R ) ) )

proof end;

uniqueness
for b₁, b₂ 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 & b₁ = 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 & b₂ = G | (Seg i) & ( for j being Nat st j < i holds
F . j <> EmptyBag the carrier of R ) ) ) holds
b₁ = b₂

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 b₃ being Bags the carrier of b₁ -valued FinSequence holds
( b₃ = 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 & b₃ = 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
OrderedPartition b is partition of b

proof end;

end;

registration

let R be non empty transitive asymmetric RelStr ;
let b be bag of the carrier of R;

cluster OrderedPartition b -> ordered for partition of b;

coherence
for b₁ being partition of b st b₁ = OrderedPartition b holds
b₁ 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 b₁ being strict RelExtension of finite-MultiSet_over the carrier of R st
for m, n being Element of b₁ 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 b₁, b₂ being strict RelExtension of finite-MultiSet_over the carrier of R st ( for m, n being Element of b₁ 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 b₂ 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
b₁ = b₂

proof end;

end;

:: deftheorem PM defines PrecM BAGORD_2:def 13 :
for R being non empty transitive asymmetric RelStr
for b₂ being strict RelExtension of finite-MultiSet_over the carrier of R holds
( b₂ = PrecM R iff for m, n being Element of b₂ 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 ;

cluster PrecM R -> transitive asymmetric strict ;

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 b₁ being Relation of (I *) st
for p, q being I -valued FinSequence holds
( [p,q] in b₁ 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 b₁, b₂ being Relation of (I *) st ( for p, q being I -valued FinSequence holds
( [p,q] in b₁ 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 b₂ 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
b₁ = b₂

proof end;

end;

:: deftheorem LO defines LexOrder BAGORD_2:def 14 :
for I being set
for R being Relation of I,I
for b₃ being Relation of (I *) holds
( b₃ = LexOrder (I,R) iff for p, q being b₁ -valued FinSequence holds
( [p,q] in b₃ 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 b₁ -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 [(OrderedPartition m),(OrderedPartition n)] in LexOrder ( the carrier of (PrecM R), the InternalRel of (PrecM R)) );

existence
ex b₁ being strict RelExtension of finite-MultiSet_over the carrier of R st
for m, n being Element of b₁ holds
( m <= n iff [(OrderedPartition m),(OrderedPartition n)] in LexOrder ( the carrier of (PrecM R), the InternalRel of (PrecM R)) )

proof end;

uniqueness
for b₁, b₂ being strict RelExtension of finite-MultiSet_over the carrier of R st ( for m, n being Element of b₁ 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 b₂ holds
( m <= n iff [(OrderedPartition m),(OrderedPartition n)] in LexOrder ( the carrier of (PrecM R), the InternalRel of (PrecM R)) ) ) holds
b₁ = b₂

proof end;

end;

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

registration

let R be non empty transitive asymmetric RelStr ;

cluster PrecPrecM R -> transitive asymmetric strict ;

coherence
( PrecPrecM R is asymmetric & PrecPrecM R is transitive )

proof end;

end;

theorem :: BAGORD_2:61

for R being non empty transitive asymmetric RelStr
for a, b being Element of (DershowitzMannaOrder R) 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 (DershowitzMannaOrder R)
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 b₁ -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;