:: On Ordering of Bags
:: by Gilbert Lee and Piotr Rudnicki
::
:: Received March 12, 2002
:: Copyright (c) 2002 Association of Mizar Users
theorem Th1: :: BAGORDER:1
theorem :: BAGORDER:2
theorem Th3: :: BAGORDER:3
theorem Th4: :: BAGORDER:4
theorem Th5: :: BAGORDER:5
:: deftheorem Def1 defines -cut BAGORDER:def 1 :
theorem Th6: :: BAGORDER:6
:: deftheorem defines Fin BAGORDER:def 2 :
theorem Th7: :: BAGORDER:7
theorem Th8: :: BAGORDER:8
theorem :: BAGORDER:9
:: deftheorem Def3 defines non-increasing BAGORDER:def 3 :
theorem Th10: :: BAGORDER:10
theorem Th11: :: BAGORDER:11
theorem Th12: :: BAGORDER:12
:: deftheorem Def4 defines TotDegree BAGORDER:def 4 :
theorem Th13: :: BAGORDER:13
theorem Th14: :: BAGORDER:14
theorem :: BAGORDER:15
theorem Th16: :: BAGORDER:16
theorem Th17: :: BAGORDER:17
theorem Th18: :: BAGORDER:18
theorem :: BAGORDER:19
theorem Th20: :: BAGORDER:20
theorem Th21: :: BAGORDER:21
theorem :: BAGORDER:22
:: deftheorem BAGORDER:def 5 :
canceled;
:: deftheorem BAGORDER:def 6 :
canceled;
:: deftheorem Def7 defines admissible BAGORDER:def 7 :
theorem Th23: :: BAGORDER:23
theorem :: BAGORDER:24
:: deftheorem Def8 defines InvLexOrder BAGORDER:def 8 :
theorem Th25: :: BAGORDER:25
theorem Th26: :: BAGORDER:26
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 ) ) )
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: :: BAGORDER:27
:: deftheorem defines GrLexOrder BAGORDER:def 10 :
:: deftheorem defines GrInvLexOrder BAGORDER:def 11 :
theorem Th28: :: BAGORDER:28
theorem :: BAGORDER:29
theorem Th30: :: BAGORDER:30
theorem :: BAGORDER:31
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
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
Element of
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
:: deftheorem Def13 defines NaivelyOrderedBags BAGORDER:def 13 :
theorem Th33: :: BAGORDER:33
theorem Th34: :: BAGORDER:34
theorem :: BAGORDER:35
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 )
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
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 )
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
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:
:: 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
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: :: BAGORDER:36
theorem Th37: :: BAGORDER:37
theorem Th38: :: BAGORDER:38
Lm1:
for R being non empty connected Poset
for n being Element of NAT
for a being Element of Fin the carrier of R st card a = n + 1 holds
card (a \ {(PosetMax a)}) = n
theorem Th39: :: BAGORDER:39
:: deftheorem defines FinOrd BAGORDER:def 17 :
:: deftheorem defines FinPoset BAGORDER:def 18 :
theorem Th40: :: BAGORDER:40
:: deftheorem Def19 defines MinElement BAGORDER:def 19 :
theorem Th41: :: BAGORDER:41
theorem :: BAGORDER:42