:: BAGORDER semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

theorem Th1: :: BAGORDER:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n, k being Nat holds
( k in Seg n iff ( k - 1 is Nat & k - 1 < n ) )
proof end;

registration
let f be natural-yielding Function;
let X be set ;
cluster f | X -> natural-yielding ;
coherence
f | X is natural-yielding
proof end;
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 Th3: :: BAGORDER:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being Function
for x being set st x in dom f holds
f * <*x*> = <*(f . x)*>
proof end;

theorem Th4: :: BAGORDER:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Nat st k in j -' i holds
it . k = b . (i + k);
existence
ex b1 being ManySortedSet of j -' i st
for k being Nat st k in j -' i holds
b1 . k = b . (i + k)
proof end;
uniqueness
for b1, b2 being ManySortedSet of j -' i st ( for k being Nat st k in j -' i holds
b1 . k = b . (i + k) ) & ( for k being Nat st k in j -' i holds
b2 . k = b . (i + k) ) holds
b1 = b2
proof end;
end;

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

registration
let n, i, j be Nat;
let b be natural-yielding ManySortedSet of n;
cluster i,j -cut b -> natural-yielding ;
coherence
i,j -cut b is natural-yielding
proof end;
end;

registration
let n, i, j be 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 Th6: :: BAGORDER:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 empty 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
{ y where y is Subset of x : ( y is finite & not y is empty & Card y <=` n ) } is set
;
end;

:: deftheorem defines Fin BAGORDER:def 2 :
for x being non empty set
for n being non empty Nat holds Fin x,n = { y where y is Subset of x : ( y is finite & not y is empty & Card y <=` n ) } ;

registration
let x be non empty set ;
let n be non empty Nat;
cluster Fin x,n -> non empty ;
coherence
not Fin x,n is empty
proof end;
end;

theorem Th7: :: BAGORDER:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 :Def3: :: BAGORDER:def 3
for i being Nat holds [(s . (i + 1)),(s . i)] in the InternalRel of R;
end;

:: deftheorem Def3 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 Th10: :: BAGORDER:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th11: :: BAGORDER:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th12: :: BAGORDER:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 -> 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 b1 being Nat ex f being FinSequence of NAT st
( b1 = Sum f & f = b * (SgmX (RelIncl n),(support b)) )
proof end;
uniqueness
for b1, b2 being Nat st ex f being FinSequence of NAT st
( b1 = Sum f & f = b * (SgmX (RelIncl n),(support b)) ) & ex f being FinSequence of NAT st
( b2 = Sum f & f = b * (SgmX (RelIncl n),(support b)) ) holds
b1 = b2
;
end;

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

theorem Th13: :: BAGORDER:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Ordinal
for a, b being bag of n holds TotDegree (a + b) = (TotDegree a) + (TotDegree b)
proof end;

theorem :: BAGORDER:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Ordinal
for b being bag of n holds
( TotDegree b = 0 iff b = EmptyBag n )
proof end;

theorem Th17: :: BAGORDER:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i, j, n being Nat holds i,j -cut (EmptyBag n) = EmptyBag (j -' i)
proof end;

theorem Th18: :: BAGORDER:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set holds support (EmptyBag X) = {}
proof end;

theorem Th20: :: BAGORDER:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for b being bag of X st support b = {} holds
b = EmptyBag X
proof end;

theorem Th21: :: BAGORDER:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 :
canceled;

:: deftheorem BAGORDER:def 6 :
canceled;

:: deftheorem Def7 defines admissible BAGORDER:def 7 :
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 Th23: :: BAGORDER:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
ex b1 being TermOrder of n st b1 is admissible
proof end;
end;

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

theorem :: BAGORDER:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
ex b1 being TermOrder of n st
for p, q being bag of n holds
( [p,q] in b1 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 b1, b2 being TermOrder of n st ( for p, q being bag of n holds
( [p,q] in b1 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 b2 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
b1 = b2
proof end;
end;

:: deftheorem Def8 defines InvLexOrder BAGORDER:def 8 :
for n being Ordinal
for b2 being TermOrder of n holds
( b2 = InvLexOrder n iff for p, q being bag of n holds
( [p,q] in b2 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 Th25: :: BAGORDER:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th25;
end;

theorem Th26: :: BAGORDER:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
ex b1 being TermOrder of n st
for a, b being bag of n holds
( [a,b] in b1 iff ( TotDegree a < TotDegree b or ( TotDegree a = TotDegree b & [a,b] in o ) ) )
proof end;
uniqueness
for b1, b2 being TermOrder of n st ( for a, b being bag of n holds
( [a,b] in b1 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 b2 iff ( TotDegree a < TotDegree b or ( TotDegree a = TotDegree b & [a,b] in o ) ) ) ) holds
b1 = b2
proof end;
end;

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

theorem Th27: :: BAGORDER:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
Graded (LexOrder n) is TermOrder of n
;
func GrInvLexOrder n -> TermOrder of n equals :: BAGORDER:def 11
Graded (InvLexOrder n);
coherence
Graded (InvLexOrder n) is TermOrder of n
;
end;

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

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

theorem Th28: :: BAGORDER:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th28;
end;

theorem :: BAGORDER:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for o being infinite Ordinal holds not GrLexOrder o is well-ordering
proof end;

theorem Th30: :: BAGORDER:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th30;
end;

theorem :: BAGORDER:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 :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
ex b1 being TermOrder of n st
for p, q being bag of n holds
( [p,q] in b1 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 b1, b2 being TermOrder of n st ( for p, q being bag of n holds
( [p,q] in b1 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 b2 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
b1 = b2
proof end;
end;

:: deftheorem Def12 defines BlockOrder BAGORDER:def 12 :
for i, n being Nat
for o1 being TermOrder of (i + 1)
for o2 being TermOrder of (n -' (i + 1))
for b5 being TermOrder of n holds
( b5 = BlockOrder i,n,o1,o2 iff for p, q being bag of n holds
( [p,q] in b5 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:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 :Def13: :: BAGORDER:def 13
( 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 b1 being strict RelStr st
( the carrier of b1 = Bags n & ( for x, y being bag of n holds
( [x,y] in the InternalRel of b1 iff x divides y ) ) )
proof end;
uniqueness
for b1, b2 being strict RelStr st the carrier of b1 = Bags n & ( for x, y being bag of n holds
( [x,y] in the InternalRel of b1 iff x divides y ) ) & the carrier of b2 = Bags n & ( for x, y being bag of n holds
( [x,y] in the InternalRel of b2 iff x divides y ) ) holds
b1 = b2
proof end;
end;

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

theorem Th33: :: BAGORDER:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat holds the carrier of (product (n --> OrderedNAT )) = Bags n
proof end;

theorem Th34: :: BAGORDER:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat holds NaivelyOrderedBags n = product (n --> OrderedNAT )
proof end;

theorem :: BAGORDER:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 14
( it in X & it is_minimal_wrt X,the InternalRel of R );
existence
ex b1 being Element of R st
( b1 in X & b1 is_minimal_wrt X,the InternalRel of R )
proof end;
uniqueness
for b1, b2 being Element of R st b1 in X & b1 is_minimal_wrt X,the InternalRel of R & b2 in X & b2 is_minimal_wrt X,the InternalRel of R holds
b1 = b2
proof end;
func PosetMax X -> Element of R means :Def15: :: BAGORDER:def 15
( it in X & it is_maximal_wrt X,the InternalRel of R );
existence
ex b1 being Element of R st
( b1 in X & b1 is_maximal_wrt X,the InternalRel of R )
proof end;
uniqueness
for b1, b2 being Element of R st b1 in X & b1 is_maximal_wrt X,the InternalRel of R & b2 in X & b2 is_maximal_wrt X,the InternalRel of R holds
b1 = b2
proof end;
end;

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

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

definition
let R be non empty connected Poset;
func FinOrd-Approx R -> Function of NAT , bool [:(Fin the carrier of R),(Fin the carrier of R):] means :Def16: :: BAGORDER:def 16
( 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 Element of 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 b1 being Function of NAT , bool [:(Fin the carrier of R),(Fin the carrier of R):] st
( dom b1 = NAT & b1 . 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 Element of NAT holds b1 . (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 b1 . n ) } ) )
proof end;
uniqueness
for b1, b2 being Function of NAT , bool [:(Fin the carrier of R),(Fin the carrier of R):] st dom b1 = NAT & b1 . 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 Element of NAT holds b1 . (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 b1 . n ) } ) & dom b2 = NAT & b2 . 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 Element of NAT holds b2 . (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 b2 . n ) } ) holds
b1 = b2
proof end;
end;

:: deftheorem Def16 defines FinOrd-Approx BAGORDER:def 16 :
for R being non empty connected Poset
for b2 being Function of NAT , bool [:(Fin the carrier of R),(Fin the carrier of R):] holds
( b2 = FinOrd-Approx R iff ( dom b2 = NAT & b2 . 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 Element of NAT holds b2 . (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 b2 . n ) } ) ) );

theorem Th36: :: BAGORDER:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th37: :: BAGORDER:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th38: :: BAGORDER:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th39: :: BAGORDER:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 17
union (rng (FinOrd-Approx R));
coherence
union (rng (FinOrd-Approx R)) is Order of Fin the carrier of R
by Th39;
end;

:: deftheorem defines FinOrd BAGORDER:def 17 :
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 18
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 18 :
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 Th40: :: BAGORDER:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 -> non empty 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 :Def19: :: BAGORDER:def 19
( it in C & it is_minimal_wrt C,the InternalRel of R );
existence
ex b1 being Element of R st
( b1 in C & b1 is_minimal_wrt C,the InternalRel of R )
proof end;
uniqueness
for b1, b2 being Element of R st b1 in C & b1 is_minimal_wrt C,the InternalRel of R & b2 in C & b2 is_minimal_wrt C,the InternalRel of R holds
b1 = b2
proof end;
end;

:: deftheorem Def19 defines MinElement BAGORDER:def 19 :
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 b3 being Element of R holds
( b3 = MinElement C,R iff ( b3 in C & b3 is_minimal_wrt C,the InternalRel of R ) );

definition
let R be non empty RelStr ;
let s be sequence of R;
let j be Nat;
func SeqShift s,j -> sequence of R means :Def20: :: BAGORDER:def 20
for i being Nat holds it . i = s . (i + j);
existence
ex b1 being sequence of R st
for i being Nat holds b1 . i = s . (i + j)
proof end;
uniqueness
for b1, b2 being sequence of R st ( for i being Nat holds b1 . i = s . (i + j) ) & ( for i being Nat holds b2 . i = s . (i + j) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def20 defines SeqShift BAGORDER:def 20 :
for R being non empty RelStr
for s being sequence of R
for j being Nat
for b4 being sequence of R holds
( b4 = SeqShift s,j iff for i being Nat holds b4 . i = s . (i + j) );

theorem Th41: :: BAGORDER:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R being non empty RelStr
for s being sequence of R
for j being Nat st s is descending holds
SeqShift s,j is descending
proof end;

theorem :: BAGORDER:42  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R being non empty connected Poset st R is well_founded holds
FinPoset R is well_founded
proof end;