:: by Gilbert Lee and Piotr Rudnicki

::

:: Received March 12, 2002

:: Copyright (c) 2002-2019 Association of Mizar Users

registration
end;

::$CT

definition

let n, i, j be Nat;

let b be ManySortedSet of n;

ex b_{1} being ManySortedSet of j -' i st

for k being Element of NAT st k in j -' i holds

b_{1} . k = b . (i + k)

for b_{1}, b_{2} being ManySortedSet of j -' i st ( for k being Element of NAT st k in j -' i holds

b_{1} . k = b . (i + k) ) & ( for k being Element of NAT st k in j -' i holds

b_{2} . k = b . (i + k) ) holds

b_{1} = b_{2}

end;
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 for k being Element of NAT st k in j -' i holds

it . k = b . (i + k);

ex b

for k being Element of NAT st k in j -' i holds

b

proof end;

uniqueness for b

b

b

b

proof end;

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

for n, i, j being Nat

for b being ManySortedSet of n

for b_{5} being ManySortedSet of j -' i holds

( b_{5} = (i,j) -cut b iff for k being Element of NAT st k in j -' i holds

b_{5} . k = b . (i + k) );

for n, i, j being Nat

for b being ManySortedSet of n

for b

( b

b

registration

let n, i, j be Nat;

let b be natural-valued ManySortedSet of n;

coherence

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

end;
let b be natural-valued ManySortedSet of n;

coherence

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

proof end;

registration

let n, i, j be Element of NAT ;

let b be finite-support ManySortedSet of n;

coherence

(i,j) -cut b is finite-support ;

end;
let b be finite-support ManySortedSet of n;

coherence

(i,j) -cut b is finite-support ;

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

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 ;

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

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

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

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

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 ;

coherence

not Fin (x,n) is empty

end;
let n be non zero Element of NAT ;

coherence

not Fin (x,n) is empty

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

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 )

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 )

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;

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

for i being Nat holds [(s . (i + 1)),(s . i)] in the InternalRel of R;

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

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

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

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

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;

ex b_{1} being Nat ex f being FinSequence of NAT st

( b_{1} = Sum f & f = b * (SgmX ((RelIncl n),(support b))) )

for b_{1}, b_{2} being Nat st ex f being FinSequence of NAT st

( b_{1} = Sum f & f = b * (SgmX ((RelIncl n),(support b))) ) & ex f being FinSequence of NAT st

( b_{2} = Sum f & f = b * (SgmX ((RelIncl n),(support b))) ) holds

b_{1} = b_{2}
;

end;
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 f being FinSequence of NAT st

( it = Sum f & f = b * (SgmX ((RelIncl n),(support b))) );

ex b

( b

proof end;

uniqueness for b

( b

( b

b

:: deftheorem Def4 defines TotDegree BAGORDER:def 4 :

for n being Ordinal

for b being bag of n

for b_{3} being Nat holds

( b_{3} = TotDegree b iff ex f being FinSequence of NAT st

( b_{3} = Sum f & f = b * (SgmX ((RelIncl n),(support b))) ) );

for n being Ordinal

for b being bag of n

for b

( b

( 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

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

for a, b being bag of n st b divides a holds

TotDegree (a -' b) = (TotDegree a) - (TotDegree b)

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)

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

proof end;

::$CT 2

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

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

registration
end;

registration

let n be Ordinal;

ex b_{1} being TermOrder of n st b_{1} is admissible

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

proof end;

definition

let n be Ordinal;

ex b_{1} being TermOrder of n st

for p, q being bag of n holds

( [p,q] in b_{1} 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 b_{1}, b_{2} being TermOrder of n st ( for p, q being bag of n holds

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

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

ex b

for p, q being bag of n holds

( [p,q] in b

( 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

( [p,q] in b

( 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

( 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

proof end;

:: deftheorem Def6 defines InvLexOrder BAGORDER:def 6 :

for n being Ordinal

for b_{2} being TermOrder of n holds

( b_{2} = InvLexOrder n iff for p, q being bag of n holds

( [p,q] in b_{2} 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 n being Ordinal

for b

( b

( [p,q] in b

( i in n & p . i < q . i & ( for k being Ordinal st i in k & k in n holds

p . k = q . k ) ) ) ) );

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 ;

ex b_{1} being TermOrder of n st

for a, b being bag of n holds

( [a,b] in b_{1} iff ( TotDegree a < TotDegree b or ( TotDegree a = TotDegree b & [a,b] in o ) ) )

for b_{1}, b_{2} being TermOrder of n st ( for a, b being bag of n holds

( [a,b] in b_{1} 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_{2} iff ( TotDegree a < TotDegree b or ( TotDegree a = TotDegree b & [a,b] in o ) ) ) ) holds

b_{1} = b_{2}

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

ex b

for a, b being bag of n holds

( [a,b] in b

proof end;

uniqueness for b

( [a,b] in b

( [a,b] in b

b

proof 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_{3} being TermOrder of n holds

( b_{3} = Graded o iff for a, b being bag of n holds

( [a,b] in b_{3} iff ( TotDegree a < TotDegree b or ( TotDegree a = TotDegree b & [a,b] in o ) ) ) );

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

( b

( [a,b] in b

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

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;

coherence

Graded (LexOrder n) is TermOrder of n ;

coherence

Graded (InvLexOrder n) is TermOrder of n ;

end;
coherence

Graded (LexOrder n) is TermOrder of n ;

coherence

Graded (InvLexOrder n) is TermOrder of n ;

:: deftheorem defines GrLexOrder BAGORDER:def 8 :

for n being Ordinal holds GrLexOrder n = Graded (LexOrder n);

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

for n being Ordinal holds GrInvLexOrder n = Graded (InvLexOrder n);

definition

let i, n be Nat;

let o1 be TermOrder of (i + 1);

let o2 be TermOrder of (n -' (i + 1));

ex b_{1} being TermOrder of n st

for p, q being bag of n holds

( [p,q] in b_{1} 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 b_{1}, b_{2} being TermOrder of n st ( for p, q being bag of n holds

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

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

ex b

for p, q being bag of n holds

( [p,q] in b

proof end;

uniqueness for b

( [p,q] in b

( [p,q] in b

b

proof 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_{5} being TermOrder of n holds

( b_{5} = BlockOrder (i,n,o1,o2) iff for p, q being bag of n holds

( [p,q] in b_{5} 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 i, n being Nat

for o1 being TermOrder of (i + 1)

for o2 being TermOrder of (n -' (i + 1))

for b

( b

( [p,q] in b

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

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;

ex b_{1} being strict RelStr st

( the carrier of b_{1} = Bags n & ( for x, y being bag of n holds

( [x,y] in the InternalRel of b_{1} iff x divides y ) ) )

for b_{1}, b_{2} being strict RelStr st the carrier of b_{1} = Bags n & ( for x, y being bag of n holds

( [x,y] in the InternalRel of b_{1} iff x divides y ) ) & the carrier of b_{2} = Bags n & ( for x, y being bag of n holds

( [x,y] in the InternalRel of b_{2} iff x divides y ) ) holds

b_{1} = b_{2}

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

ex b

( the carrier of b

( [x,y] in the InternalRel of b

proof end;

uniqueness for b

( [x,y] in the InternalRel of b

( [x,y] in the InternalRel of b

b

proof end;

:: deftheorem Def11 defines NaivelyOrderedBags BAGORDER:def 11 :

for n being Nat

for b_{2} being strict RelStr holds

( b_{2} = NaivelyOrderedBags n iff ( the carrier of b_{2} = Bags n & ( for x, y being bag of n holds

( [x,y] in the InternalRel of b_{2} iff x divides y ) ) ) );

for n being Nat

for b

( b

( [x,y] in the InternalRel of b

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 )

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 ;

ex b_{1} being Element of R st

( b_{1} in X & b_{1} is_minimal_wrt X, the InternalRel of R )

for b_{1}, b_{2} being Element of R st b_{1} in X & b_{1} is_minimal_wrt X, the InternalRel of R & b_{2} in X & b_{2} is_minimal_wrt X, the InternalRel of R holds

b_{1} = b_{2}

ex b_{1} being Element of R st

( b_{1} in X & b_{1} is_maximal_wrt X, the InternalRel of R )

for b_{1}, b_{2} being Element of R st b_{1} in X & b_{1} is_maximal_wrt X, the InternalRel of R & b_{2} in X & b_{2} is_maximal_wrt X, the InternalRel of R holds

b_{1} = b_{2}

end;
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 ( it in X & it is_minimal_wrt X, the InternalRel of R );

ex b

( b

proof end;

uniqueness for 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 ( it in X & it is_maximal_wrt X, the InternalRel of R );

ex b

( b

proof end;

uniqueness for b

b

proof 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_{3} being Element of R holds

( b_{3} = PosetMin X iff ( b_{3} in X & b_{3} is_minimal_wrt X, the InternalRel of R ) );

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

( b

:: 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_{3} being Element of R holds

( b_{3} = PosetMax X iff ( b_{3} in X & b_{3} is_maximal_wrt X, the InternalRel of R ) );

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

( b

definition

let R be non empty connected Poset;

ex b_{1} being sequence of (bool [:(Fin the carrier of R),(Fin the carrier of R):]) st

( dom b_{1} = NAT & b_{1} . 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_{1} . (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_{1} . n ) } ) )

for b_{1}, b_{2} being sequence of (bool [:(Fin the carrier of R),(Fin the carrier of R):]) st dom b_{1} = NAT & b_{1} . 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_{1} . (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_{1} . n ) } ) & dom b_{2} = NAT & b_{2} . 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_{2} . (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_{2} . n ) } ) holds

b_{1} = b_{2}

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

ex b

( dom b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def14 defines FinOrd-Approx BAGORDER:def 14 :

for R being non empty connected Poset

for b_{2} being sequence of (bool [:(Fin the carrier of R),(Fin the carrier of R):]) holds

( b_{2} = FinOrd-Approx R iff ( dom b_{2} = NAT & b_{2} . 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_{2} . (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_{2} . n ) } ) ) );

for R being non empty connected Poset

for b

( b

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

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

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

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;

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

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

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

:: deftheorem defines FinOrd BAGORDER:def 15 :

for R being non empty connected Poset holds FinOrd R = union (rng (FinOrd-Approx R));

for R being non empty connected Poset holds FinOrd R = union (rng (FinOrd-Approx R));

definition

let R be non empty connected Poset;

correctness

coherence

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

;

end;
correctness

coherence

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

;

:: deftheorem defines FinPoset BAGORDER:def 16 :

for R being non empty connected Poset holds FinPoset R = RelStr(# (Fin the carrier of R),(FinOrd R) #);

for R being non empty connected Poset holds FinPoset R = RelStr(# (Fin the carrier of R),(FinOrd R) #);

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

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

ex b_{1} being Element of R st

( b_{1} in C & b_{1} is_minimal_wrt C, the InternalRel of R )

for b_{1}, b_{2} being Element of R st b_{1} in C & b_{1} is_minimal_wrt C, the InternalRel of R & b_{2} in C & b_{2} is_minimal_wrt C, the InternalRel of R holds

b_{1} = b_{2}

end;
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 ( it in C & it is_minimal_wrt C, the InternalRel of R );

ex b

( b

proof end;

uniqueness for b

b

proof 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_{3} being Element of R holds

( b_{3} = MinElement (C,R) iff ( b_{3} in C & b_{3} is_minimal_wrt C, the InternalRel of R ) );

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

( b

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

for s being sequence of R

for j being Nat st s is descending holds

s ^\ j is descending

proof end;