environ
vocabularies HIDDEN, MYCIELSK, FINSET_1, DILWORTH, CARD_1, ARYTM_3, ARYTM_1, FUNCT_1, RELAT_1, RELAT_2, YELLOW_0, TARSKI, EQREL_1, CIRCUIT2, SUBSET_1, COMBGRAS, NECKLACE, NEWTON, XXREAL_0, NAT_1, XBOOLE_0, ORDERS_2, STRUCT_0, ZFMISC_1, FUNCT_2, NUMBERS, REAL_1, XCMPLX_0;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, FINSET_1, SUBSET_1, STRUCT_0, ORDINAL1, CARD_1, ORDERS_2, XCMPLX_0, XXREAL_0, XREAL_0, NAT_D, RELAT_1, RELSET_1, RELAT_2, EQREL_1, FUNCT_1, FUNCT_2, NEWTON, YELLOW_0, NECKLACE, DILWORTH, NUMBERS;
definitions TARSKI, XBOOLE_0, RELAT_2, FUNCT_1, DILWORTH, NECKLACE;
theorems NEWTON, NAT_1, NAT_D, XREAL_0, XREAL_1, XXREAL_0, ORDINAL1, FUNCT_1, DILWORTH, XBOOLE_0, XBOOLE_1, TARSKI, NECKLACE, PENCIL_1, ZFMISC_1, ORDERS_2, EULER_1, CARD_2, CARD_1, YELLOW_0, RELSET_1, EQREL_1, FUNCT_2, RELAT_1, FINSET_1, FINSEQ_4, RELAT_2, SUBSET_1, XTUPLE_0;
schemes RECDEF_1, NAT_1, CLASSES1, PRE_CIRC, FUNCT_1, FUNCT_2, DILWORTH;
registrations SUBSET_1, XBOOLE_0, STRUCT_0, XCMPLX_0, XXREAL_0, XREAL_0, NAT_1, CARD_1, RELSET_1, ORDINAL1, EQREL_1, NECKLA_3, FUNCT_2, FINSET_1, DILWORTH, NEWTON, ORDERS_2;
constructors HIDDEN, NECKLACE, RELSET_1, NAT_1, NAT_D, NEWTON, YELLOW_0, DILWORTH, DOMAIN_1;
requirements HIDDEN, SUBSET, BOOLE, NUMERALS, ARITHM, REAL;
equalities STRUCT_0, TARSKI, SUBSET_1, ORDINAL1, CARD_1;
expansions TARSKI, XBOOLE_0, RELAT_2, FUNCT_1, DILWORTH, NECKLACE;
defpred S1[ set ] means verum;
theorem Th3:
for
A,
B,
C,
D,
E,
X being
set st (
X c= A or
X c= B or
X c= C or
X c= D or
X c= E ) holds
X c= (((A \/ B) \/ C) \/ D) \/ E
theorem Th4:
for
A,
B,
C,
D,
E,
x being
set holds
(
x in (((A \/ B) \/ C) \/ D) \/ E iff (
x in A or
x in B or
x in C or
x in D or
x in E ) )
definition
let n be
Nat;
let R be
NatRelStr of
n;
existence
ex b1 being NatRelStr of (2 * n) + 1 st the InternalRel of b1 = ((( the InternalRel of R \/ { [x,(y + n)] where x, y is Element of NAT : [x,y] in the InternalRel of R } ) \/ { [(x + n),y] where x, y is Element of NAT : [x,y] in the InternalRel of R } ) \/ [:{(2 * n)},((2 * n) \ n):]) \/ [:((2 * n) \ n),{(2 * n)}:]
uniqueness
for b1, b2 being NatRelStr of (2 * n) + 1 st the InternalRel of b1 = ((( the InternalRel of R \/ { [x,(y + n)] where x, y is Element of NAT : [x,y] in the InternalRel of R } ) \/ { [(x + n),y] where x, y is Element of NAT : [x,y] in the InternalRel of R } ) \/ [:{(2 * n)},((2 * n) \ n):]) \/ [:((2 * n) \ n),{(2 * n)}:] & the InternalRel of b2 = ((( the InternalRel of R \/ { [x,(y + n)] where x, y is Element of NAT : [x,y] in the InternalRel of R } ) \/ { [(x + n),y] where x, y is Element of NAT : [x,y] in the InternalRel of R } ) \/ [:{(2 * n)},((2 * n) \ n):]) \/ [:((2 * n) \ n),{(2 * n)}:] holds
b1 = b2
end;
:: article with preliminaries where RelStr represents a graph.
:: But then some stuff from NECKLACE would have to be moved.
:: I decided not to move stuff around until there is much more
:: material and then a bigger reorganisation would be in place
:: 2009.08.06