:: by Grzegorz Bancerek

::

:: Received December 31, 2015

:: Copyright (c) 2015-2021 Association of Mizar Users

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) )

( x2 + (x1 -' y2) <= k & (((k -' x2) + y2) -' x1) + y1 = (k -' (x2 + (x1 -' y2))) + ((y2 -' x1) + y1) )

proof end;

registration

existence

ex b_{1} being RelStr st

( b_{1} is asymmetric & b_{1} is transitive & not b_{1} is empty )

end;
ex b

( b

proof end;

registration

let I be set ;

existence

ex b_{1} being Relation of I st

( b_{1} is asymmetric & b_{1} is transitive )

end;
existence

ex b

( b

proof end;

registration
end;

registration
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 )

for p, q being FinSequence st p ^ q is I -valued holds

( p is I -valued & q is I -valued )

proof end;

registration
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

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 ) ) )

( p c< q iff ( len p < len q & ( for i being Nat st i in dom p holds

p . i = q . i ) ) )

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_{1},b_{2}) holds

not R42(R,b_{2},b_{1})

end;
let x, y be Element of R;

:: original: <=

redefine pred x <= y;

asymmetry

for x, y being Element of R st R42(R,b

not R42(R,b

proof end;

registration

let I be set ;

coherence

for b_{1} being multiset of I holds

( b_{1} is I -defined & b_{1} is natural-valued )

end;
coherence

for b

( b

proof end;

registration
end;

definition

let m be natural-valued Function;

compatibility

for b_{1} being set holds

( b_{1} = support m iff b_{1} = m " (NAT \ {0}) )

end;
compatibility

for b

( b

proof end;

:: deftheorem defines support BAGORD_2:def 1 :

for m being natural-valued Function holds support m = m " (NAT \ {0});

for m being natural-valued Function holds support m = m " (NAT \ {0});

registration
end;

definition

let R be RelStr ;

let x, y be Element of R;

symmetry

for x, y being Element of R st not x <= y & not y <= x holds

( not y <= x & not x <= y ) ;

end;
let x, y be Element of R;

symmetry

for x, y being Element of R st not x <= y & not y <= x holds

( not y <= x & not x <= y ) ;

:: 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 ) );

for R being RelStr

for x, y being Element of R holds

( x ## y iff ( not x <= y & not y <= x ) );

definition

attr c_{1} is strict ;

struct RelMultMagma -> multMagma , RelStr ;

aggr RelMultMagma(# carrier, multF, InternalRel #) -> RelMultMagma ;

end;
struct RelMultMagma -> multMagma , RelStr ;

aggr RelMultMagma(# carrier, multF, InternalRel #) -> RelMultMagma ;

definition

attr c_{1} is strict ;

struct RelMonoid -> multLoopStr , RelStr ;

aggr RelMonoid(# carrier, multF, OneF, InternalRel #) -> RelMonoid ;

end;
struct RelMonoid -> multLoopStr , RelStr ;

aggr RelMonoid(# carrier, multF, OneF, InternalRel #) -> RelMonoid ;

definition

let M be multLoopStr ;

ex b_{1} being RelMonoid st multLoopStr(# the carrier of b_{1}, the multF of b_{1}, the OneF of b_{1} #) = multLoopStr(# the carrier of M, the multF of M, the OneF of M #)

end;
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 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 #);

ex b

proof end;

:: deftheorem RE defines RelExtension BAGORD_2:def 3 :

for M being multLoopStr

for b_{2} being RelMonoid holds

( b_{2} is RelExtension of M iff multLoopStr(# the carrier of b_{2}, the multF of b_{2}, the OneF of b_{2} #) = multLoopStr(# the carrier of M, the multF of M, the OneF of M #) );

for M being multLoopStr

for b

( b

registration

let M be non empty multLoopStr ;

coherence

for b_{1} being RelExtension of M holds not b_{1} is empty

end;
coherence

for b

proof end;

registration
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 )

for N being multLoopStr

for M being RelExtension of N holds

( a is Element of M iff a is Element of N )

proof end;

registration

let I be set ;

let M be RelExtension of finite-MultiSet_over I;

coherence

for b_{1} being Element of M holds

( b_{1} is Function-like & b_{1} is Relation-like )

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

coherence

for b

( b

proof end;

registration

let I be set ;

let M be RelExtension of finite-MultiSet_over I;

coherence

for b_{1} being Element of M holds

( b_{1} is I -defined & b_{1} is natural-valued & b_{1} is finite-support )

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

coherence

for b

( b

proof end;

registration

let I be set ;

let M be RelExtension of finite-MultiSet_over I;

coherence

for b_{1} being Element of M holds b_{1} is total

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

coherence

for b

proof end;

scheme :: BAGORD_2:sch 1

RelEx{ F_{1}() -> non empty multLoopStr , P_{1}[ object , object ] } :

RelEx{ F

ex N being strict RelExtension of F_{1}() st

for x, y being Element of N holds

( x <= y iff P_{1}[x,y] )

for x, y being Element of N holds

( x <= y iff P

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

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 ;

ex b_{1} being strict RelExtension of finite-MultiSet_over the carrier of R st

for m, n being Element of b_{1} holds

( m <= n iff ex x, y being Element of b_{1} st

( 1. b_{1} <> 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 b_{1}, b_{2} being strict RelExtension of finite-MultiSet_over the carrier of R st ( for m, n being Element of b_{1} holds

( m <= n iff ex x, y being Element of b_{1} st

( 1. b_{1} <> 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_{2} holds

( m <= n iff ex x, y being Element of b_{2} st

( 1. b_{2} <> 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_{1} = b_{2}

end;
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 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 ) ) ) );

ex b

for m, n being Element of b

( m <= n iff ex x, y being Element of b

( 1. b

ex a being Element of R st

( x . a > 0 & b <= a ) ) ) )

proof end;

uniqueness for b

( m <= n iff ex x, y being Element of b

( 1. b

ex a being Element of R st

( x . a > 0 & b <= a ) ) ) ) ) & ( for m, n being Element of b

( m <= n iff ex x, y being Element of b

( 1. b

ex a being Element of R st

( x . a > 0 & b <= a ) ) ) ) ) holds

b

proof end;

:: deftheorem DM defines DershowitzMannaOrder BAGORD_2:def 4 :

for R being non empty RelStr

for b_{2} being strict RelExtension of finite-MultiSet_over the carrier of R holds

( b_{2} = DershowitzMannaOrder R iff for m, n being Element of b_{2} holds

( m <= n iff ex x, y being Element of b_{2} st

( 1. b_{2} <> 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 R being non empty RelStr

for b

( b

( m <= n iff ex x, y being Element of b

( 1. b

ex a being Element of R st

( x . a > 0 & b <= a ) ) ) ) );

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 )

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)

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 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

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

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

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;

registration

let I be set ;

coherence

for b_{1} being Element of Bags I holds

( b_{1} is Function-like & b_{1} is Relation-like )
by PRE_POLY:def 12;

end;
coherence

for b

( b

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 )

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 ;

for b_{1} being strict RelExtension of finite-MultiSet_over the carrier of R holds

( b_{1} = DershowitzMannaOrder R iff for m, n being Element of b_{1} 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 ) ) ) ) )

end;
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 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 ) ) ) );

for b

( b

( 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;

:: deftheorem HO defines DershowitzMannaOrder BAGORD_2:def 5 :

for R being non empty transitive asymmetric RelStr

for b_{2} being strict RelExtension of finite-MultiSet_over the carrier of R holds

( b_{2} = DershowitzMannaOrder R iff for m, n being Element of b_{2} 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 ) ) ) ) );

for R being non empty transitive asymmetric RelStr

for b

( b

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

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

( DershowitzMannaOrder R is asymmetric & DershowitzMannaOrder R is transitive )

end;
coherence

( DershowitzMannaOrder R is asymmetric & DershowitzMannaOrder R is transitive )

proof end;

definition

let I be set ;

ex b_{1} being Relation of (Bags I) st

for b1, b2 being bag of I holds

( [b1,b2] in b_{1} iff ( b1 <> b2 & b1 divides b2 ) )

for b_{1}, b_{2} being Relation of (Bags I) st ( for b1, b2 being bag of I holds

( [b1,b2] in b_{1} iff ( b1 <> b2 & b1 divides b2 ) ) ) & ( for b1, b2 being bag of I holds

( [b1,b2] in b_{2} iff ( b1 <> b2 & b1 divides b2 ) ) ) holds

b_{1} = b_{2}

end;
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 for b1, b2 being bag of I holds

( [b1,b2] in it iff ( b1 <> b2 & b1 divides b2 ) );

ex b

for b1, b2 being bag of I holds

( [b1,b2] in b

proof end;

uniqueness for b

( [b1,b2] in b

( [b1,b2] in b

b

proof end;

:: deftheorem DO defines DivOrder BAGORD_2:def 6 :

for I being set

for b_{2} being Relation of (Bags I) holds

( b_{2} = DivOrder I iff for b1, b2 being bag of I holds

( [b1,b2] in b_{2} iff ( b1 <> b2 & b1 divides b2 ) ) );

for I being set

for b

( b

( [b1,b2] in b

registration
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

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)

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;

ex b_{1} being bag of I ex F being Function of NAT,(Bags I) st

( b_{1} = 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 ) )

for b_{1}, b_{2} being bag of I st ex F being Function of NAT,(Bags I) st

( b_{1} = 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_{2} = 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_{1} = b_{2}

end;
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 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 ) );

ex b

( b

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

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

for b being bag of I st i < len f & b = f . (i + 1) holds

F . (i + 1) = (F . i) + b ) ) holds

b

proof end;

:: deftheorem SUM defines Sum BAGORD_2:def 7 :

for I being set

for f being Bags b_{1} -valued FinSequence

for b_{3} being bag of I holds

( b_{3} = Sum f iff ex F being Function of NAT,(Bags I) st

( b_{3} = 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 ) ) );

for I being set

for f being Bags b

for b

( b

( b

for b being bag of I st i < len f & b = f . (i + 1) holds

F . (i + 1) = (F . i) + b ) ) );

registration

let I be set ;

let b be bag of I;

coherence

for b_{1} being FinSequence st b_{1} = <*b*> holds

b_{1} is Bags I -valued

end;
let b be bag of I;

coherence

for b

b

proof end;

theorem Th22: :: BAGORD_2:33

for I being set

for p being Bags b_{1} -valued FinSequence

for b being bag of I holds Sum (p ^ <*b*>) = (Sum p) + b

for p being Bags b

for b being bag of I holds Sum (p ^ <*b*>) = (Sum p) + b

proof end;

theorem Th25: :: BAGORD_2:36

for I being set

for b being bag of I

for p being Bags b_{1} -valued FinSequence holds Sum (<*b*> ^ p) = b + (Sum p)

for b being bag of I

for p being Bags b

proof end;

theorem Th26: :: BAGORD_2:37

for I being set

for b being bag of I

for p being Bags b_{1} -valued FinSequence st b in rng p holds

b divides Sum p

for b being bag of I

for p being Bags b

b divides Sum p

proof end;

theorem Th27: :: BAGORD_2:38

for I being set

for p being Bags b_{1} -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 )

for p being Bags b

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;

existence

ex b_{1} being Bags I -valued FinSequence st b = Sum b_{1}

end;
let b be bag of I;

existence

ex b

proof end;

:: deftheorem PART defines partition BAGORD_2:def 8 :

for I being set

for b being bag of I

for b_{3} being Bags b_{1} -valued FinSequence holds

( b_{3} is partition of b iff b = Sum b_{3} );

for I being set

for b being bag of I

for b

( 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

end;
let b be bag of I;

:: original: <*

redefine func <*b*> -> partition of b;

coherence

<*b*> is partition of b

proof 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;

end;
let M be RelExtension of finite-MultiSet_over the carrier of R;

let b be Element of M;

let p be partition of b;

:: 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 );

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;

end;
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 ) ) );

( ( 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 ) ) );

:: 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 ) ) ) );

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 ) ) )

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_{1} -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 ) )

for p being Bags b

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

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 ;

ex b_{1} being bag of I st

for i being object st i in I holds

( ( i in J implies b_{1} . i = m . i ) & ( not i in J implies b_{1} . i = 0 ) )

for b_{1}, b_{2} being bag of I st ( for i being object st i in I holds

( ( i in J implies b_{1} . i = m . i ) & ( not i in J implies b_{1} . i = 0 ) ) ) & ( for i being object st i in I holds

( ( i in J implies b_{2} . i = m . i ) & ( not i in J implies b_{2} . i = 0 ) ) ) holds

b_{1} = b_{2}

end;
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 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 ) );

ex b

for i being object st i in I holds

( ( i in J implies b

proof end;

uniqueness for b

( ( i in J implies b

( ( i in J implies b

b

proof end;

:: deftheorem BAR defines | BAGORD_2:def 11 :

for I being set

for m being bag of I

for J being set

for b_{4} being bag of I holds

( b_{4} = m | J iff for i being object st i in I holds

( ( i in J implies b_{4} . i = m . i ) & ( not i in J implies b_{4} . i = 0 ) ) );

for I being set

for m being bag of I

for J being set

for b

( b

( ( i in J implies b

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

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

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

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_{1} -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 )

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

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

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 )

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 )

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 }

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_{1} -valued FinSequence st Sum p = EmptyBag I & ( for a being bag of I st a in rng p holds

a <> EmptyBag I ) holds

p = {}

for p being Bags b

a <> EmptyBag I ) holds

p = {}

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

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):]

end;
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;

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 } <> {}

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;

ex b_{1} 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_{1} = G | (Seg i) & ( for j being Nat st j < i holds

F . j <> EmptyBag the carrier of R ) ) )

for b_{1}, b_{2} 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_{1} = 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_{2} = G | (Seg i) & ( for j being Nat st j < i holds

F . j <> EmptyBag the carrier of R ) ) ) holds

b_{1} = b_{2}

end;
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 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 ) ) );

ex b

( 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

F . j <> EmptyBag the carrier of R ) ) )

proof end;

uniqueness for b

( 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

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

F . j <> EmptyBag the carrier of R ) ) ) holds

b

proof 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_{3} being Bags the carrier of b_{1} -valued FinSequence holds

( b_{3} = 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_{3} = G | (Seg i) & ( for j being Nat st j < i holds

F . j <> EmptyBag the carrier of R ) ) ) );

for R being non empty transitive asymmetric RelStr

for b being bag of the carrier of R

for b

( b

( 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

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

end;
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;

registration

let R be non empty transitive asymmetric RelStr ;

let b be bag of the carrier of R;

coherence

for b_{1} being partition of b st b_{1} = OrderedPartition b holds

b_{1} is ordered

end;
let b be bag of the carrier of R;

coherence

for b

b

proof 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 = {} )

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 ;

ex b_{1} being strict RelExtension of finite-MultiSet_over the carrier of R st

for m, n being Element of b_{1} 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 b_{1}, b_{2} being strict RelExtension of finite-MultiSet_over the carrier of R st ( for m, n being Element of b_{1} 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_{2} 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_{1} = b_{2}

end;
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 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 ) ) ) ) );

ex b

for m, n being Element of b

( 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

( 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

( 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

proof end;

:: deftheorem PM defines PrecM BAGORD_2:def 13 :

for R being non empty transitive asymmetric RelStr

for b_{2} being strict RelExtension of finite-MultiSet_over the carrier of R holds

( b_{2} = PrecM R iff for m, n being Element of b_{2} 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 R being non empty transitive asymmetric RelStr

for b

( b

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

end;
coherence

( PrecM R is asymmetric & PrecM R is transitive )

proof end;

definition

let I be set ;

let R be Relation of I,I;

ex b_{1} being Relation of (I *) st

for p, q being I -valued FinSequence holds

( [p,q] in b_{1} 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 b_{1}, b_{2} being Relation of (I *) st ( for p, q being I -valued FinSequence holds

( [p,q] in b_{1} 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_{2} 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_{1} = b_{2}

end;
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 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 ) ) ) );

ex b

for p, q being I -valued FinSequence holds

( [p,q] in b

( 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

( [p,q] in b

( 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

( 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

proof end;

:: deftheorem LO defines LexOrder BAGORD_2:def 14 :

for I being set

for R being Relation of I,I

for b_{3} being Relation of (I *) holds

( b_{3} = LexOrder (I,R) iff for p, q being b_{1} -valued FinSequence holds

( [p,q] in b_{3} 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 I being set

for R being Relation of I,I

for b

( b

( [p,q] in b

( 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
end;

registration
end;

theorem :: BAGORD_2:60

for I being set

for R being asymmetric Relation of I

for p, q, r being b_{1} -valued FinSequence holds

( [p,q] in LexOrder (I,R) iff [(r ^ p),(r ^ q)] in LexOrder (I,R) )

for R being asymmetric Relation of I

for p, q, r being b

( [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 ;

ex b_{1} being strict RelExtension of finite-MultiSet_over the carrier of R st

for m, n being Element of b_{1} holds

( m <= n iff [(OrderedPartition m),(OrderedPartition n)] in LexOrder ( the carrier of (PrecM R), the InternalRel of (PrecM R)) )

for b_{1}, b_{2} being strict RelExtension of finite-MultiSet_over the carrier of R st ( for m, n being Element of b_{1} 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_{2} holds

( m <= n iff [(OrderedPartition m),(OrderedPartition n)] in LexOrder ( the carrier of (PrecM R), the InternalRel of (PrecM R)) ) ) holds

b_{1} = b_{2}

end;
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 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)) );

ex b

for m, n being Element of b

( m <= n iff [(OrderedPartition m),(OrderedPartition n)] in LexOrder ( the carrier of (PrecM R), the InternalRel of (PrecM R)) )

proof end;

uniqueness for b

( 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

( m <= n iff [(OrderedPartition m),(OrderedPartition n)] in LexOrder ( the carrier of (PrecM R), the InternalRel of (PrecM R)) ) ) holds

b

proof end;

:: deftheorem PPM defines PrecPrecM BAGORD_2:def 15 :

for R being non empty transitive asymmetric RelStr

for b_{2} being strict RelExtension of finite-MultiSet_over the carrier of R holds

( b_{2} = PrecPrecM R iff for m, n being Element of b_{2} holds

( m <= n iff [(OrderedPartition m),(OrderedPartition n)] in LexOrder ( the carrier of (PrecM R), the InternalRel of (PrecM R)) ) );

for R being non empty transitive asymmetric RelStr

for b

( b

( 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 ;

coherence

( PrecPrecM R is asymmetric & PrecPrecM R is transitive )

end;
coherence

( PrecPrecM R is asymmetric & PrecPrecM R is transitive )

proof 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

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

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_{1} -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 )

for p being Bags b

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 )

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;