begin
theorem Th1:
theorem
theorem Th3:
theorem Th4:
theorem Th5:
:: deftheorem Def1 defines -cut BAGORDER:def 1 :
theorem Th6:
:: deftheorem defines Fin BAGORDER:def 2 :
theorem Th7:
theorem Th8:
theorem
:: deftheorem Def3 defines non-increasing BAGORDER:def 3 :
theorem Th10:
theorem Th11:
theorem Th12:
begin
:: deftheorem Def4 defines TotDegree BAGORDER:def 4 :
theorem Th13:
theorem Th14:
theorem
theorem Th16:
theorem Th17:
theorem Th18:
theorem
theorem Th20:
theorem Th21:
theorem
begin
:: deftheorem BAGORDER:def 5 :
canceled;
:: deftheorem BAGORDER:def 6 :
canceled;
:: deftheorem Def7 defines admissible BAGORDER:def 7 :
theorem Th23:
theorem
:: deftheorem Def8 defines InvLexOrder BAGORDER:def 8 :
theorem Th25:
theorem Th26:
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:
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 ) ) )
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
end;
:: deftheorem Def9 defines Graded BAGORDER:def 9 :
theorem Th27:
:: deftheorem defines GrLexOrder BAGORDER:def 10 :
:: deftheorem defines GrInvLexOrder BAGORDER:def 11 :
theorem Th28:
theorem
theorem Th30:
theorem
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:
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 ) ) )
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
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
:: deftheorem Def13 defines NaivelyOrderedBags BAGORDER:def 13 :
theorem Th33:
theorem Th34:
theorem
begin
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
means
(
it in X &
it is_minimal_wrt X,the
InternalRel of
R );
existence
ex b1 being Element of st
( b1 in X & b1 is_minimal_wrt X,the InternalRel of R )
uniqueness
for b1, b2 being Element of 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
func PosetMax X -> Element of
means :
Def15:
(
it in X &
it is_maximal_wrt X,the
InternalRel of
R );
existence
ex b1 being Element of st
( b1 in X & b1 is_maximal_wrt X,the InternalRel of R )
uniqueness
for b1, b2 being Element of 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
end;
:: deftheorem defines PosetMin BAGORDER:def 14 :
:: deftheorem Def15 defines PosetMax BAGORDER:def 15 :
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:
(
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 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 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 ) } ) )
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 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 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
end;
:: deftheorem Def16 defines FinOrd-Approx BAGORDER:def 16 :
theorem Th36:
theorem Th37:
theorem Th38:
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
theorem Th39:
:: deftheorem defines FinOrd BAGORDER:def 17 :
:: deftheorem defines FinPoset BAGORDER:def 18 :
theorem Th40:
:: deftheorem Def19 defines MinElement BAGORDER:def 19 :
theorem Th41:
theorem