environ
vocabularies HIDDEN, MMLQUER2, RELAT_1, XBOOLE_0, SUBSET_1, AOFA_000, RELAT_2, TARSKI, FUNCT_1, NUMBERS, MMLQUERY, ARYTM_3, ORDINAL1, PARTFUN1, ORDERS_1, ORDINAL4, ZFMISC_1, XXREAL_0, FINSEQ_1, FINSEQ_4, SETFAM_1, CARD_1, NAT_1, FUNCT_7, WELLORD1, REWRITE1, FINSET_1, PEPIN, AFINSQ_1, WELLORD2, ORDINAL2;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, RELAT_1, AOFA_000, RELAT_2, FUNCT_1, FINSET_1, FINSEQ_1, CARD_1, NAT_1, MEMBERED, ORDERS_1, ORDINAL1, NUMBERS, PARTFUN1, FUNCT_2, MMLQUERY, ORDINAL2, ORDINAL4, AFINSQ_1, XXREAL_0, XCMPLX_0, WELLORD1, FUNCT_7, RELSET_1, REWRITE1, WELLORD2, TOLER_1;
definitions TARSKI, XBOOLE_0, RELAT_1, RELAT_2, WELLORD1, FUNCT_1, PARTFUN1, REWRITE1, MMLQUERY;
theorems XBOOLE_0, XBOOLE_1, ZFMISC_1, RELAT_1, RELAT_2, ORDERS_1, MMLQUERY, NAT_1, XXREAL_0, SETFAM_1, AFINSQ_1, ORDINAL3, ORDINAL1, FUNCT_1, CARD_2, TARSKI, FINSEQ_3, FUNCT_7, RELSET_1, FUNCT_2, AFINSQ_2, RELSET_2, WELLORD1, WELLORD2, PARTFUN1, CARD_1, ORDINAL4, XTUPLE_0;
schemes NAT_1, RELAT_1, RECDEF_1, FINSET_1, FUNCT_1;
registrations RELAT_1, RELSET_1, ARMSTRNG, VALUED_0, ARROW, FINSEQ_1, XXREAL_0, CARD_1, SUBSET_1, XCMPLX_0, ORDINAL1, NAT_1, FUNCT_7, MEMBERED, FINSET_1, XBOOLE_0, AFINSQ_1;
constructors HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, RELAT_2, MMLQUERY, XXREAL_0, ORDINAL1, VALUED_0, ORDERS_1, FINSEQ_4, XCMPLX_0, FUNCT_1, FUNCT_7, ZFMISC_1, WELLORD2, PARTFUN1, FUNCT_2, NUMBERS, NAT_1, REWRITE1, MEMBERED, RELSET_1, WELLORD1, TOLER_1, ORDINAL2, ORDINAL3, ORDINAL4;
requirements HIDDEN, BOOLE, SUBSET, NUMERALS;
equalities RELAT_1, CARD_1, ORDINAL1;
expansions XBOOLE_0, RELAT_2, WELLORD1, FUNCT_1, REWRITE1, MMLQUERY;
definition
let R be
Relation;
redefine attr R is
transitive means :
Def1:
for
x,
y,
z being
set st
x,
y in R &
y,
z in R holds
x,
z in R;
compatibility
( R is transitive iff for x, y, z being set st x,y in R & y,z in R holds
x,z in R )
compatibility
( R is antisymmetric iff for x, y being set st x,y in R & y,x in R holds
x = y )
end;
theorem Th9:
for
R1,
R2 being
Relation for
x,
y being
set holds
(
x,
y in R1 \, R2 iff (
x,
y in R1 or (
y,
x nin R1 &
x,
y in R2 ) ) )
definition
let X be
set ;
let O be
Operation of
X;
assume A1:
(
O is
co-well_founded &
O is
irreflexive &
O is
finite )
;
existence
ex b1 being Relation of X ex f being Function of X,NAT st
( b1 = value_of f & ( for x being Element of X st x in X holds
ex n being Nat st
( f . x = n & ( x . (iter (O,n)) <> {} or ( n = 0 & x . (iter (O,n)) = {} ) ) & x . (iter (O,(n + 1))) = {} ) ) )
uniqueness
for b1, b2 being Relation of X st ex f being Function of X,NAT st
( b1 = value_of f & ( for x being Element of X st x in X holds
ex n being Nat st
( f . x = n & ( x . (iter (O,n)) <> {} or ( n = 0 & x . (iter (O,n)) = {} ) ) & x . (iter (O,(n + 1))) = {} ) ) ) & ex f being Function of X,NAT st
( b2 = value_of f & ( for x being Element of X st x in X holds
ex n being Nat st
( f . x = n & ( x . (iter (O,n)) <> {} or ( n = 0 & x . (iter (O,n)) = {} ) ) & x . (iter (O,(n + 1))) = {} ) ) ) holds
b1 = b2
end;
definition
let X be
finite set ;
let O be
Operation of
X;
let R be
connected Order of
X;
existence
ex b1 being Relation of X st
for x, y being Element of X holds
( x,y in b1 iff ( x . O <> {} & ( y . O = {} or ( y . O <> {} & (order ((x . O),R)) /. 0,(order ((y . O),R)) /. 0 in R & (order ((x . O),R)) /. 0 <> (order ((y . O),R)) /. 0 ) ) ) )
uniqueness
for b1, b2 being Relation of X st ( for x, y being Element of X holds
( x,y in b1 iff ( x . O <> {} & ( y . O = {} or ( y . O <> {} & (order ((x . O),R)) /. 0,(order ((y . O),R)) /. 0 in R & (order ((x . O),R)) /. 0 <> (order ((y . O),R)) /. 0 ) ) ) ) ) & ( for x, y being Element of X holds
( x,y in b2 iff ( x . O <> {} & ( y . O = {} or ( y . O <> {} & (order ((x . O),R)) /. 0,(order ((y . O),R)) /. 0 in R & (order ((x . O),R)) /. 0 <> (order ((y . O),R)) /. 0 ) ) ) ) ) holds
b1 = b2
end;