environ
vocabularies HIDDEN, NUMBERS, XBOOLE_0, SUBSET_1, FINSEQ_1, ARYTM_1, ARYTM_3, XXREAL_0, CARD_1, NAT_1, PRE_POLY, FUNCT_1, RELAT_1, TARSKI, CLASSES1, CARD_3, FINSEQ_2, PBOOLE, GRAPH_2, VALUED_0, FINSUB_1, FINSET_1, RELAT_2, ORDERS_2, WAYBEL_4, STRUCT_0, WELLFND1, WELLORD1, ORDERS_1, ORDINAL1, WELLORD2, ORDINAL4, REAL_1, FUNCOP_1, FUNCT_4, PARTFUN1, DICKSON, RLVECT_2, ZFMISC_1, MCART_1, BAGORDER, XCMPLX_0;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, XCMPLX_0, RELAT_1, PBOOLE, RELAT_2, RELSET_1, PARTFUN1, FINSET_1, FINSUB_1, ORDINAL1, FUNCT_7, XTUPLE_0, MCART_1, WELLORD1, ORDERS_1, WELLFND1, CARD_1, NUMBERS, VALUED_0, XXREAL_0, XREAL_0, FUNCT_1, PRE_POLY, CARD_3, NAT_D, FINSEQ_1, FINSEQ_2, RVSUM_1, WSIERP_1, FUNCOP_1, FUNCT_2, SEQ_4, DOMAIN_1, FINSEQOP, CLASSES1, RECDEF_1, NAT_1, STRUCT_0, WAYBEL_0, YELLOW_1, WAYBEL_4, PRALG_1, ORDERS_2, DICKSON;
definitions TARSKI, RELAT_2, WELLFND1;
theorems WELLORD1, TARSKI, RELAT_2, RELSET_1, ZFMISC_1, ORDERS_2, NAT_1, FUNCT_1, AXIOMS, CARD_3, PBOOLE, YELLOW_1, PRALG_1, FUNCOP_1, PARTIT_2, WELLFND1, RELAT_1, DICKSON, FINSEQ_1, INTEGRA5, RVSUM_1, FINSEQ_2, CARD_1, WAYBEL_0, WAYBEL_4, ORDINAL1, FUNCT_2, CARD_2, FINSUB_1, ORDERS_1, FUNCT_7, WELLORD2, FINSEQ_3, FINSEQ_5, FINSEQOP, RFINSEQ, XBOOLE_0, XBOOLE_1, PARTFUN1, XREAL_1, XXREAL_0, VALUED_0, VALUED_1, XXREAL_2, XREAL_0, NAT_D, CLASSES1, PRE_POLY, XTUPLE_0, NUMBERS;
schemes NAT_1, RELSET_1, FINSET_1, RECDEF_1, FUNCT_2, ORDINAL1, CLASSES1;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, FUNCT_2, FINSET_1, FINSUB_1, NUMBERS, XXREAL_0, XREAL_0, NAT_1, CARD_1, MEMBERED, FINSEQ_1, CARD_5, STRUCT_0, ORDERS_2, WAYBEL_0, YELLOW_1, DICKSON, VALUED_0, XXREAL_2, RELSET_1, PRE_POLY, WELLORD1, WELLORD2, XTUPLE_0;
constructors HIDDEN, DOMAIN_1, FINSEQOP, NAT_D, WSIERP_1, PRALG_1, TRIANG_1, WAYBEL_4, WELLFND1, DICKSON, RECDEF_1, BINOP_2, SEQ_4, CLASSES1, RELSET_1, FUNCT_7, REAL_1, XTUPLE_0, WELLORD1, PRE_POLY, NUMBERS;
requirements HIDDEN, SUBSET, NUMERALS, REAL, BOOLE, ARITHM;
equalities FINSEQ_2, CARD_1, ORDINAL1;
expansions TARSKI, RELAT_2, WELLFND1;
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
;
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;
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:
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 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 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 ) ) ) );
definition
let R be non
empty connected Poset;
existence
ex b1 being sequence of (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 sequence of (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;
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