:: On Ordering of Bags
:: by Gilbert Lee and Piotr Rudnicki
::
:: Received March 12, 2002
:: Copyright (c) 2002-2021 Association of Mizar Users

theorem Th1: :: BAGORDER:1

for x, y, z being set st z in x & z in y & x \ {z} = y \ {z} holds
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
f | X is finite-support

proof end;

end;

theorem :: BAGORDER:3

canceled;

::$CT

theorem Th3: :: BAGORDER:4

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

proof end;

definition

let n, i, j be 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
ex b₁ being ManySortedSet of j -' i st
for k being Element of NAT st k in j -' i holds
b₁ . k = b . (i + k)

proof end;

uniqueness
for b₁, b₂ being ManySortedSet of j -' i st ( for k being Element of NAT st k in j -' i holds
b₁ . k = b . (i + k) ) & ( for k being Element of NAT st k in j -' i holds
b₂ . k = b . (i + k) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def1 defines -cut BAGORDER:def 1 :
for n, i, j being Nat
for b being ManySortedSet of n
for b₅ being ManySortedSet of j -' i holds
( b₅ = (i,j) -cut b iff for k being Element of NAT st k in j -' i holds
b₅ . k = b . (i + k) );

registration

let n, i, j be Nat;
let b be natural-valued ManySortedSet of n;

cluster (i,j) -cut b -> natural-valued ;

coherence
(i,j) -cut b is natural-valued

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
(i,j) -cut b is finite-support ;

end;

theorem Th4: :: BAGORDER:5

for n, i being 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 zero 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 c= n ) } ;

coherence
{ y where y is Subset of x : ( y is finite & not y is empty & card y c= n ) } is set ;

end;

:: deftheorem defines Fin BAGORDER:def 2 :
for x being non empty set
for n being non zero Element of NAT holds Fin (x,n) = { y where y is Subset of x : ( y is finite & not y is empty & card y c= n ) } ;

registration

let x be non empty set ;
let n be non zero Element of NAT ;

cluster Fin (x,n) -> non empty ;

coherence
not Fin (x,n) is empty

proof end;

end;

theorem Th5: :: BAGORDER:6

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 Th6: :: 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_minimal_wrt X, the InternalRel of R )

proof end;

theorem :: BAGORDER:8

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

proof end;

definition

let R be non empty RelStr ;
let s be sequence of R;

attr s is non-increasing means :: BAGORDER:def 3
for i being Nat holds [(s . (i + 1)),(s . i)] in the InternalRel of R;

end;

:: deftheorem defines non-increasing BAGORDER:def 3 :
for R being non empty RelStr
for s being sequence of R holds
( s is non-increasing iff for i being Nat holds [(s . (i + 1)),(s . i)] in the InternalRel of R );

theorem Th8: :: BAGORDER:9

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

proof end;

theorem Th9: :: BAGORDER:10

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 Nat st
for r being Nat st p <= r holds
s . p = s . r

proof end;

theorem Th10: :: BAGORDER:11

for X being set
for R being Order of X
for B being finite Subset of X
for x being object st B = {x} holds
SgmX (R,B) = <*x*>

proof end;

definition

let n be Ordinal;
let b be bag of n;

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

existence
ex b₁ being Nat ex f being FinSequence of NAT st
( b₁ = Sum f & f = b * (SgmX ((RelIncl n),(support b))) )

proof end;

uniqueness
for b₁, b₂ being Nat st ex f being FinSequence of NAT st
( b₁ = Sum f & f = b * (SgmX ((RelIncl n),(support b))) ) & ex f being FinSequence of NAT st
( b₂ = Sum f & f = b * (SgmX ((RelIncl n),(support b))) ) holds
b₁ = b₂ ;

end;

:: deftheorem Def4 defines TotDegree BAGORDER:def 4 :
for n being Ordinal
for b being bag of n
for b₃ being Nat holds
( b₃ = TotDegree b iff ex f being FinSequence of NAT st
( b₃ = Sum f & f = b * (SgmX ((RelIncl n),(support b))) ) );

theorem Th11: :: BAGORDER:12

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 Th12: :: BAGORDER:13

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

proof end;

theorem :: BAGORDER:14

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 Th14: :: BAGORDER:15

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

proof end;

theorem Th15: :: BAGORDER:16

for i, j, n being Nat holds (i,j) -cut (EmptyBag n) = EmptyBag (j -' i)

proof end;

theorem Th16: :: BAGORDER:17

for i, j, n being 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:18

canceled;

theorem :: BAGORDER:19

canceled;

::$CT 2

theorem Th17: :: BAGORDER:20

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

for n being set
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;

attr T is admissible means :Def5: :: BAGORDER:def 5
( 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 Def5 defines admissible BAGORDER:def 5 :
for n being Ordinal
for T being TermOrder of n holds
( T is admissible iff ( 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 ) ) );

theorem Th19: :: BAGORDER:22

for n being Ordinal holds LexOrder n is admissible

proof end;

registration

let n be Ordinal;

cluster LexOrder n -> admissible ;

coherence
LexOrder n is admissible by Th19;

end;

registration

let n be Ordinal;

cluster Relation-like Bags n -defined Bags n -valued total V18( Bags n, Bags n) reflexive antisymmetric transitive admissible for Element of bool [:(Bags n),(Bags n):];

existence
ex b₁ being TermOrder of n st b₁ is admissible

proof end;

end;

theorem :: BAGORDER:23

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 :Def6: :: BAGORDER:def 6
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
ex b₁ being TermOrder of n st
for p, q being bag of n holds
( [p,q] in b₁ 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 ) ) ) )

proof end;

uniqueness
for b₁, b₂ being TermOrder of n st ( for p, q being bag of n holds
( [p,q] in b₁ 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 ) ) ) ) ) & ( for p, q being bag of n holds
( [p,q] in b₂ 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 ) ) ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def6 defines InvLexOrder BAGORDER:def 6 :
for n being Ordinal
for b₂ being TermOrder of n holds
( b₂ = InvLexOrder n iff for p, q being bag of n holds
( [p,q] in b₂ 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 ) ) ) ) );

theorem Th21: :: BAGORDER:24

for n being Ordinal holds InvLexOrder n is admissible

proof end;

registration

let n be Ordinal;

cluster InvLexOrder n -> admissible ;

coherence
InvLexOrder n is admissible by Th21;

end;

theorem Th22: :: BAGORDER:25

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 :Def7: :: BAGORDER:def 7
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
ex b₁ being TermOrder of n st
for a, b being bag of n holds
( [a,b] in b₁ iff ( TotDegree a < TotDegree b or ( TotDegree a = TotDegree b & [a,b] in o ) ) )

proof end;

uniqueness
for b₁, b₂ being TermOrder of n st ( for a, b being bag of n holds
( [a,b] in b₁ iff ( TotDegree a < TotDegree b or ( TotDegree a = TotDegree b & [a,b] in o ) ) ) ) & ( for a, b being bag of n holds
( [a,b] in b₂ iff ( TotDegree a < TotDegree b or ( TotDegree a = TotDegree b & [a,b] in o ) ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def7 defines Graded BAGORDER:def 7 :
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 ) holds
for b₃ being TermOrder of n holds
( b₃ = Graded o iff for a, b being bag of n holds
( [a,b] in b₃ iff ( TotDegree a < TotDegree b or ( TotDegree a = TotDegree b & [a,b] in o ) ) ) );

theorem Th23: :: BAGORDER:26

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 8
Graded (LexOrder n);

coherence
Graded (LexOrder n) is TermOrder of n ;

func GrInvLexOrder n -> TermOrder of n equals :: BAGORDER:def 9
Graded (InvLexOrder n);

coherence
Graded (InvLexOrder n) is TermOrder of n ;

end;

:: deftheorem defines GrLexOrder BAGORDER:def 8 :
for n being Ordinal holds GrLexOrder n = Graded (LexOrder n);

:: deftheorem defines GrInvLexOrder BAGORDER:def 9 :
for n being Ordinal holds GrInvLexOrder n = Graded (InvLexOrder n);

theorem Th24: :: BAGORDER:27

for n being Ordinal holds GrLexOrder n is admissible

proof end;

registration

let n be Ordinal;

cluster GrLexOrder n -> admissible ;

coherence
GrLexOrder n is admissible by Th24;

end;

theorem :: BAGORDER:28

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

proof end;

theorem Th26: :: BAGORDER:29

for n being Ordinal holds GrInvLexOrder n is admissible

proof end;

registration

let n be Ordinal;

cluster GrInvLexOrder n -> admissible ;

coherence
GrInvLexOrder n is admissible by Th26;

end;

theorem :: BAGORDER:30

for o being Ordinal holds GrInvLexOrder o is well-ordering

proof end;

definition

let i, n be 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 :Def10: :: BAGORDER:def 10
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
ex b₁ being TermOrder of n st
for p, q being bag of n holds
( [p,q] in b₁ 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 ) ) )

proof end;

uniqueness
for b₁, b₂ being TermOrder of n st ( for p, q being bag of n holds
( [p,q] in b₁ 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 ) ) ) ) & ( for p, q being bag of n holds
( [p,q] in b₂ 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 ) ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def10 defines BlockOrder BAGORDER:def 10 :
for i, n being Nat
for o1 being TermOrder of (i + 1)
for o2 being TermOrder of (n -' (i + 1))
for b₅ being TermOrder of n holds
( b₅ = BlockOrder (i,n,o1,o2) iff for p, q being bag of n holds
( [p,q] in b₅ 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 ) ) ) );

theorem :: BAGORDER:31

for i, n being Nat
for o1 being TermOrder of (i + 1)
for o2 being TermOrder of (n -' (i + 1)) st o1 is admissible & o2 is admissible holds
BlockOrder (i,n,o1,o2) is admissible

proof end;

definition

let n be Nat;

func NaivelyOrderedBags n -> strict RelStr means :Def11: :: BAGORDER:def 11
( the carrier of it = Bags n & ( for x, y being bag of n holds
( [x,y] in the InternalRel of it iff x divides y ) ) );

existence
ex b₁ being strict RelStr st
( the carrier of b₁ = Bags n & ( for x, y being bag of n holds
( [x,y] in the InternalRel of b₁ iff x divides y ) ) )

proof end;

uniqueness
for b₁, b₂ being strict RelStr st the carrier of b₁ = Bags n & ( for x, y being bag of n holds
( [x,y] in the InternalRel of b₁ iff x divides y ) ) & the carrier of b₂ = Bags n & ( for x, y being bag of n holds
( [x,y] in the InternalRel of b₂ iff x divides y ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def11 defines NaivelyOrderedBags BAGORDER:def 11 :
for n being Nat
for b₂ being strict RelStr holds
( b₂ = NaivelyOrderedBags n iff ( the carrier of b₂ = Bags n & ( for x, y being bag of n holds
( [x,y] in the InternalRel of b₂ iff x divides y ) ) ) );

theorem Th29: :: BAGORDER:32

for n being Nat holds the carrier of (product (n --> OrderedNAT)) = Bags n

proof end;

theorem Th30: :: BAGORDER:33

for n being Nat holds NaivelyOrderedBags n = product (n --> OrderedNAT)

proof end;

theorem :: BAGORDER:34

for n being Nat
for o being TermOrder of n st o is admissible holds
( the InternalRel of (NaivelyOrderedBags n) c= o & o is well-ordering )

proof end;

definition

let R be non empty connected Poset;
let X be Element of Fin the carrier of R;
assume A1: not X is empty ;

func PosetMin X -> Element of R means :: BAGORDER:def 12
( it in X & it is_minimal_wrt X, the InternalRel of R );

existence
ex b₁ being Element of R st
( b₁ in X & b₁ is_minimal_wrt X, the InternalRel of R )

proof end;

uniqueness
for b₁, b₂ being Element of R st b₁ in X & b₁ is_minimal_wrt X, the InternalRel of R & b₂ in X & b₂ is_minimal_wrt X, the InternalRel of R holds
b₁ = b₂

proof end;

func PosetMax X -> Element of R means :Def13: :: BAGORDER:def 13
( it in X & it is_maximal_wrt X, the InternalRel of R );

existence
ex b₁ being Element of R st
( b₁ in X & b₁ is_maximal_wrt X, the InternalRel of R )

proof end;

uniqueness
for b₁, b₂ being Element of R st b₁ in X & b₁ is_maximal_wrt X, the InternalRel of R & b₂ in X & b₂ is_maximal_wrt X, the InternalRel of R holds
b₁ = b₂

proof end;

end;

:: deftheorem defines PosetMin BAGORDER:def 12 :
for R being non empty connected Poset
for X being Element of Fin the carrier of R st not X is empty holds
for b₃ being Element of R holds
( b₃ = PosetMin X iff ( b₃ in X & b₃ is_minimal_wrt X, the InternalRel of R ) );

:: deftheorem Def13 defines PosetMax BAGORDER:def 13 :
for R being non empty connected Poset
for X being Element of Fin the carrier of R st not X is empty holds
for b₃ being Element of R holds
( b₃ = PosetMax X iff ( b₃ in X & b₃ is_maximal_wrt X, the InternalRel of R ) );

definition

let R be non empty connected Poset;

func FinOrd-Approx R -> sequence of (bool [:(Fin the carrier of R),(Fin the carrier of R):]) means :Def14: :: BAGORDER:def 14
( dom it = NAT & it . 0 = { [x,y] where x, y is Element of Fin the carrier of R : ( x = {} or ( x <> {} & y <> {} & PosetMax x <> PosetMax y & [(PosetMax x),(PosetMax y)] in the InternalRel of R ) ) } & ( for n being Nat holds it . (n + 1) = { [x,y] where x, y is Element of Fin the carrier of R : ( x <> {} & y <> {} & PosetMax x = PosetMax y & [(x \ {(PosetMax x)}),(y \ {(PosetMax y)})] in it . n ) } ) );

existence
ex b₁ being sequence of (bool [:(Fin the carrier of R),(Fin the carrier of R):]) st
( dom b₁ = NAT & b₁ . 0 = { [x,y] where x, y is Element of Fin the carrier of R : ( x = {} or ( x <> {} & y <> {} & PosetMax x <> PosetMax y & [(PosetMax x),(PosetMax y)] in the InternalRel of R ) ) } & ( for n being Nat holds b₁ . (n + 1) = { [x,y] where x, y is Element of Fin the carrier of R : ( x <> {} & y <> {} & PosetMax x = PosetMax y & [(x \ {(PosetMax x)}),(y \ {(PosetMax y)})] in b₁ . n ) } ) )

proof end;

uniqueness
for b₁, b₂ being sequence of (bool [:(Fin the carrier of R),(Fin the carrier of R):]) st dom b₁ = NAT & b₁ . 0 = { [x,y] where x, y is Element of Fin the carrier of R : ( x = {} or ( x <> {} & y <> {} & PosetMax x <> PosetMax y & [(PosetMax x),(PosetMax y)] in the InternalRel of R ) ) } & ( for n being Nat holds b₁ . (n + 1) = { [x,y] where x, y is Element of Fin the carrier of R : ( x <> {} & y <> {} & PosetMax x = PosetMax y & [(x \ {(PosetMax x)}),(y \ {(PosetMax y)})] in b₁ . n ) } ) & dom b₂ = NAT & b₂ . 0 = { [x,y] where x, y is Element of Fin the carrier of R : ( x = {} or ( x <> {} & y <> {} & PosetMax x <> PosetMax y & [(PosetMax x),(PosetMax y)] in the InternalRel of R ) ) } & ( for n being Nat holds b₂ . (n + 1) = { [x,y] where x, y is Element of Fin the carrier of R : ( x <> {} & y <> {} & PosetMax x = PosetMax y & [(x \ {(PosetMax x)}),(y \ {(PosetMax y)})] in b₂ . n ) } ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def14 defines FinOrd-Approx BAGORDER:def 14 :
for R being non empty connected Poset
for b₂ being sequence of (bool [:(Fin the carrier of R),(Fin the carrier of R):]) holds
( b₂ = FinOrd-Approx R iff ( dom b₂ = NAT & b₂ . 0 = { [x,y] where x, y is Element of Fin the carrier of R : ( x = {} or ( x <> {} & y <> {} & PosetMax x <> PosetMax y & [(PosetMax x),(PosetMax y)] in the InternalRel of R ) ) } & ( for n being Nat holds b₂ . (n + 1) = { [x,y] where x, y is Element of Fin the carrier of R : ( x <> {} & y <> {} & PosetMax x = PosetMax y & [(x \ {(PosetMax x)}),(y \ {(PosetMax y)})] in b₂ . n ) } ) ) );

theorem Th32: :: BAGORDER:35

for R being non empty connected Poset
for x, y being Element of Fin the carrier of R holds
( [x,y] in union (rng (FinOrd-Approx R)) iff ( x = {} or ( x <> {} & y <> {} & PosetMax x <> PosetMax y & [(PosetMax x),(PosetMax y)] in the InternalRel of R ) or ( x <> {} & y <> {} & PosetMax x = PosetMax y & [(x \ {(PosetMax x)}),(y \ {(PosetMax y)})] in union (rng (FinOrd-Approx R)) ) ) )

proof end;

theorem Th33: :: BAGORDER:36

for R being non empty connected Poset
for x being Element of Fin the carrier of R st x <> {} holds
not [x,{}] in union (rng (FinOrd-Approx R))

proof end;

theorem Th34: :: BAGORDER:37

for R being non empty connected Poset
for a being Element of Fin the carrier of R holds a \ {(PosetMax a)} is Element of Fin the carrier of R

proof end;

Lm1: for R being non empty connected Poset
for n being Nat
for a being Element of Fin the carrier of R st card a = n + 1 holds
card (a \ {(PosetMax a)}) = n

proof end;

theorem Th35: :: BAGORDER:38

for R being non empty connected Poset holds union (rng (FinOrd-Approx R)) is Order of (Fin the carrier of R)

proof end;

definition

let R be non empty connected Poset;

func FinOrd R -> Order of (Fin the carrier of R) equals :: BAGORDER:def 15
union (rng (FinOrd-Approx R));

coherence
union (rng (FinOrd-Approx R)) is Order of (Fin the carrier of R) by Th35;

end;

:: deftheorem defines FinOrd BAGORDER:def 15 :
for R being non empty connected Poset holds FinOrd R = union (rng (FinOrd-Approx R));

definition

let R be non empty connected Poset;

func FinPoset R -> Poset equals :: BAGORDER:def 16
RelStr(# (Fin the carrier of R),(FinOrd R) #);

correctness
coherence
RelStr(# (Fin the carrier of R),(FinOrd R) #) is Poset;
;

end;

:: deftheorem defines FinPoset BAGORDER:def 16 :
for R being non empty connected Poset holds FinPoset R = RelStr(# (Fin the carrier of R),(FinOrd R) #);

registration

let R be non empty connected Poset;

cluster FinPoset R -> non empty ;

correctness
coherence
not FinPoset R is empty ;
;

end;

theorem Th36: :: BAGORDER:39

for R being non empty connected Poset
for a, b being Element of (FinPoset R) holds
( [a,b] in the InternalRel of (FinPoset R) iff ex x, y being Element of Fin the carrier of R st
( a = x & b = y & ( x = {} or ( x <> {} & y <> {} & PosetMax x <> PosetMax y & [(PosetMax x),(PosetMax y)] in the InternalRel of R ) or ( x <> {} & y <> {} & PosetMax x = PosetMax y & [(x \ {(PosetMax x)}),(y \ {(PosetMax y)})] in FinOrd R ) ) ) )

proof end;

registration

let R be non empty connected Poset;

cluster FinPoset R -> connected ;

correctness
coherence
FinPoset R is connected ;

proof end;

end;

definition

let R be non empty connected RelStr ;
let C be non empty set ;
assume that
A1: R is well_founded and
A2: C c= the carrier of R ;

func MinElement (C,R) -> Element of R means :Def17: :: BAGORDER:def 17
( it in C & it is_minimal_wrt C, the InternalRel of R );

existence
ex b₁ being Element of R st
( b₁ in C & b₁ is_minimal_wrt C, the InternalRel of R )

proof end;

uniqueness
for b₁, b₂ being Element of R st b₁ in C & b₁ is_minimal_wrt C, the InternalRel of R & b₂ in C & b₂ is_minimal_wrt C, the InternalRel of R holds
b₁ = b₂

proof end;

end;

:: deftheorem Def17 defines MinElement BAGORDER:def 17 :
for R being non empty connected RelStr
for C being non empty set st R is well_founded & C c= the carrier of R holds
for b₃ being Element of R holds
( b₃ = MinElement (C,R) iff ( b₃ in C & b₃ is_minimal_wrt C, the InternalRel of R ) );

theorem Th37: :: BAGORDER:40

for R being non empty RelStr
for s being sequence of R
for j being Nat st s is descending holds
s ^\ j is descending

proof end;

theorem :: BAGORDER:41

for R being non empty connected Poset st R is well_founded holds
FinPoset R is well_founded

proof end;