:: BAGORDER semantic presentation

theorem Th1: :: BAGORDER:1

for x, y, z being set st z in x & z in y holds
( x \ {z} = y \ {z} iff x = y )

proof end;

theorem :: BAGORDER:2

for n, k being Element of NAT holds
( k in Seg n iff ( k - 1 is Element of NAT & k - 1 < n ) )

proof end;

registration

let f be finite-support Function;
let X be set ;
cluster f | X -> finite-support ;
coherence

proof end;

end;

theorem Th3: :: BAGORDER:3

for f being Function
for x being set st x in dom f holds
f * <*x*> = <*(f . x)*>

proof end;

theorem Th4: :: BAGORDER:4

for f, g, h being Function st dom f = dom g & rng f c= dom h & rng g c= dom h & f,g are_fiberwise_equipotent holds
h * f,h * g are_fiberwise_equipotent

proof end;

theorem Th5: :: BAGORDER:5

for fs being FinSequence of NAT holds
( Sum fs = 0 iff fs = (len fs) |-> 0 )

proof end;

definition

let n, i, j be Element of NAT ;
let b be ManySortedSet of n;
func i,j -cut b -> ManySortedSet of j -' i means :Def1: :: BAGORDER:def 1
for k being Element of NAT st k in j -' i holds
it . k = b . (i + k);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines -cut BAGORDER:def 1 :

registration

let n, i, j be Element of NAT ;
let b be natural-yielding ManySortedSet of n;
cluster i,j -cut b -> natural-yielding ;
coherence

proof end;

end;

registration

let n, i, j be Element of NAT ;
let b be finite-support ManySortedSet of n;
cluster i,j -cut b -> finite-support ;
coherence ;

end;

theorem Th6: :: BAGORDER:6

for n, i being Element of NAT
for a, b being ManySortedSet of n holds
( a = b iff ( 0 ,(i + 1) -cut a = 0 ,(i + 1) -cut b & (i + 1),n -cut a = (i + 1),n -cut b ) )

proof end;

definition

let x be non empty set ;
let n be non empty Element of NAT ;
func Fin x,n -> set equals :: BAGORDER:def 2
{ y where y is Subset of x : ( y is finite & not y is empty & Card y <=` n ) } ;
coherence ;

end;

:: deftheorem defines Fin BAGORDER:def 2 :

registration

let x be non empty set ;
let n be non empty Element of NAT ;
cluster Fin x,n -> non empty ;
coherence

proof end;

end;

theorem Th7: :: BAGORDER:7

for R being non empty transitive antisymmetric RelStr
for X being finite Subset of R st X <> {} holds
ex x being Element of R st
( x in X & x is_maximal_wrt X,the InternalRel of R )

proof end;

theorem Th8: :: BAGORDER:8

for R being non empty transitive antisymmetric RelStr
for X being finite Subset of R st X <> {} holds
ex x being Element of R st
( x in X & x is_minimal_wrt X,the InternalRel of R )

proof end;

theorem :: BAGORDER:9

for R being non empty transitive antisymmetric RelStr
for f being sequence of R st f is descending holds
for j, i being Element of NAT st i < j holds
( f . i <> f . j & [(f . j),(f . i)] in the InternalRel of R )

proof end;

definition

let R be non empty RelStr ;
let s be sequence of R;
attr s is non-increasing means :Def3: :: BAGORDER:def 3
for i being Element of NAT holds [(s . (i + 1)),(s . i)] in the InternalRel of R;

end;

:: deftheorem Def3 defines non-increasing BAGORDER:def 3 :

theorem Th10: :: BAGORDER:10

for R being non empty transitive RelStr
for f being sequence of R st f is non-increasing holds
for j, i being Element of NAT st i < j holds
[(f . j),(f . i)] in the InternalRel of R

proof end;

theorem Th11: :: BAGORDER:11

for R being non empty transitive RelStr
for s being sequence of R st R is well_founded & s is non-increasing holds
ex p being Element of NAT st
for r being Element of NAT st p <= r holds
s . p = s . r

proof end;

theorem Th12: :: BAGORDER:12

for X being set
for a being Element of X
for A being finite Subset of X
for R being Order of X st A = {a} & R linearly_orders A holds
SgmX R,A = <*a*>

proof end;

definition

let n be Ordinal;
let b be bag of n;
func TotDegree b -> Element of NAT means :Def4: :: BAGORDER:def 4
ex f being FinSequence of NAT st
( it = Sum f & f = b * (SgmX (RelIncl n),(support b)) );
existence

proof end;

uniqueness ;

end;

:: deftheorem Def4 defines TotDegree BAGORDER:def 4 :

theorem Th13: :: BAGORDER:13

for n being Ordinal
for b being bag of n
for s being finite Subset of n
for f, g being FinSequence of NAT st f = b * (SgmX (RelIncl n),(support b)) & g = b * (SgmX (RelIncl n),((support b) \/ s)) holds
Sum f = Sum g

proof end;

theorem Th14: :: BAGORDER:14

for n being Ordinal
for a, b being bag of n holds TotDegree (a + b) = (TotDegree a) + (TotDegree b)

proof end;

theorem :: BAGORDER:15

for n being Ordinal
for a, b being bag of n st b divides a holds
TotDegree (a -' b) = (TotDegree a) - (TotDegree b)

proof end;

theorem Th16: :: BAGORDER:16

for n being Ordinal
for b being bag of n holds
( TotDegree b = 0 iff b = EmptyBag n )

proof end;

theorem Th17: :: BAGORDER:17

for i, j, n being Element of NAT holds i,j -cut (EmptyBag n) = EmptyBag (j -' i)

proof end;

theorem Th18: :: BAGORDER:18

for i, j, n being Element of NAT
for a, b being bag of n holds i,j -cut (a + b) = (i,j -cut a) + (i,j -cut b)

proof end;

theorem :: BAGORDER:19

for X being set holds support (EmptyBag X) = {}

proof end;

theorem Th20: :: BAGORDER:20

for X being set
for b being bag of X st support b = {} holds
b = EmptyBag X

proof end;

theorem Th21: :: BAGORDER:21

for n, m being Ordinal
for b being bag of n st m in n holds
b | m is bag of m

proof end;

theorem :: BAGORDER:22

for n being Ordinal
for a, b being bag of n st b divides a holds
support b c= support a

proof end;

definition

let n be set ;
mode TermOrder of n is Order of Bags n;

end;

notation

let n be Ordinal;
synonym LexOrder n for BagOrder n;

end;

definition

let n be Ordinal;
let T be TermOrder of n;
canceled;
canceled;
attr T is admissible means :Def7: :: BAGORDER:def 7
( T is_strongly_connected_in Bags n & ( for a being bag of n holds [(EmptyBag n),a] in T ) & ( for a, b, c being bag of n st [a,b] in T holds
[(a + c),(b + c)] in T ) );

end;

:: deftheorem BAGORDER:def 5 :

:: deftheorem BAGORDER:def 6 :

:: deftheorem Def7 defines admissible BAGORDER:def 7 :

theorem Th23: :: BAGORDER:23

for n being Ordinal holds LexOrder n is admissible

proof end;

registration

let n be Ordinal;
cluster admissible Relation of Bags n, Bags n;
existence

proof end;

end;

registration

let n be Ordinal;
cluster LexOrder n -> admissible ;
coherence by Th23;

end;

theorem :: BAGORDER:24

for o being infinite Ordinal holds not LexOrder o is well-ordering

proof end;

definition

let n be Ordinal;
func InvLexOrder n -> TermOrder of n means :Def8: :: BAGORDER:def 8
for p, q being bag of n holds
( [p,q] in it iff ( p = q or ex i being Ordinal st
( i in n & p . i < q . i & ( for k being Ordinal st i in k & k in n holds
p . k = q . k ) ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def8 defines InvLexOrder BAGORDER:def 8 :

theorem Th25: :: BAGORDER:25

for n being Ordinal holds InvLexOrder n is admissible

proof end;

registration

let n be Ordinal;
cluster InvLexOrder n -> admissible ;
coherence by Th25;

end;

theorem Th26: :: BAGORDER:26

for o being Ordinal holds InvLexOrder o is well-ordering

proof end;

definition

let n be Ordinal;
let o be TermOrder of n;
assume A1: for a, b, c being bag of n st [a,b] in o holds
[(a + c),(b + c)] in o ;
func Graded o -> TermOrder of n means :Def9: :: BAGORDER:def 9
for a, b being bag of n holds
( [a,b] in it iff ( TotDegree a < TotDegree b or ( TotDegree a = TotDegree b & [a,b] in o ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def9 defines Graded BAGORDER:def 9 :

theorem Th27: :: BAGORDER:27

for n being Ordinal
for o being TermOrder of n st ( for a, b, c being bag of n st [a,b] in o holds
[(a + c),(b + c)] in o ) & o is_strongly_connected_in Bags n holds
Graded o is admissible

proof end;

definition

let n be Ordinal;
func GrLexOrder n -> TermOrder of n equals :: BAGORDER:def 10
Graded (LexOrder n);
coherence ;
func GrInvLexOrder n -> TermOrder of n equals :: BAGORDER:def 11
Graded (InvLexOrder n);
coherence ;

end;

:: deftheorem defines GrLexOrder BAGORDER:def 10 :

:: deftheorem defines GrInvLexOrder BAGORDER:def 11 :

theorem Th28: :: BAGORDER:28

for n being Ordinal holds GrLexOrder n is admissible

proof end;

registration

let n be Ordinal;
cluster GrLexOrder n -> admissible ;
coherence by Th28;

end;

theorem :: BAGORDER:29

for o being infinite Ordinal holds not GrLexOrder o is well-ordering

proof end;

theorem Th30: :: BAGORDER:30

for n being Ordinal holds GrInvLexOrder n is admissible

proof end;

registration

let n be Ordinal;
cluster GrInvLexOrder n -> admissible ;
coherence by Th30;

end;

theorem :: BAGORDER:31

for o being Ordinal holds GrInvLexOrder o is well-ordering

proof end;

definition

let i, n be Element of NAT ;
let o1 be TermOrder of (i + 1);
let o2 be TermOrder of (n -' (i + 1));
func BlockOrder i,n,o1,o2 -> TermOrder of n means :Def12: :: BAGORDER:def 12
for p, q being bag of n holds
( [p,q] in it iff ( ( 0 ,(i + 1) -cut p <> 0 ,(i + 1) -cut q & [(0 ,(i + 1) -cut p),(0 ,(i + 1) -cut q)] in o1 ) or ( 0 ,(i + 1) -cut p = 0 ,(i + 1) -cut q & [((i + 1),n -cut p),((i + 1),n -cut q)] in o2 ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def12 defines BlockOrder BAGORDER:def 12 :