environ
vocabularies HIDDEN, NUMBERS, SUBSET_1, AFINSQ_1, NAT_1, ORDINAL4, XBOOLE_0, TARSKI, RELAT_1, FUNCT_1, ZFMISC_1, XXREAL_0, ARYTM_3, CARD_1, FINSEQ_1, PRE_POLY, NEWTON, SETFAM_1, FLANG_1;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, FUNCT_1, RELSET_1, FUNCT_2, SETFAM_1, XXREAL_0, NAT_1, AFINSQ_1, CATALAN2;
definitions TARSKI;
theorems AFINSQ_1, NAT_1, ORDINAL1, SUBSET_1, TARSKI, XBOOLE_0, XBOOLE_1, XREAL_1, ZFMISC_1, XXREAL_0, FUNCT_2, RELAT_1;
schemes CARD_FIL, DOMAIN_1, NAT_1, RECDEF_1, SUBSET_1;
registrations XBOOLE_0, SUBSET_1, RELAT_1, ORDINAL1, XXREAL_0, XREAL_0, NAT_1, AFINSQ_1, CATALAN2, FUNCT_1, FINSET_1;
constructors HIDDEN, XREAL_0, NAT_1, CATALAN2, RELSET_1;
requirements HIDDEN, NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
equalities ;
expansions TARSKI;
theorem Th1:
for
n,
n1,
n2 being
Nat st (
n1 > n or
n2 > n ) holds
n1 + n2 > n
theorem Th2:
for
n,
n1,
n2 being
Nat st
n1 + n <= n2 + 1 &
n > 0 holds
n1 <= n2
theorem Th3:
for
n1,
n2 being
Nat holds
(
n1 + n2 = 1 iff ( (
n1 = 1 &
n2 = 0 ) or (
n1 = 0 &
n2 = 1 ) ) )
Lm1:
for i, j being Nat
for p being XFinSequence st len p = i + j holds
ex q1, q2 being XFinSequence st
( len q1 = i & len q2 = j & p = q1 ^ q2 )
by AFINSQ_1:61;