environ
vocabularies HIDDEN, BOR_CANT, REALSET1, ABIAN, SIN_COS, ARYTM_3, CARD_3, EQREL_1, COMPLEX1, NUMBERS, ZFMISC_1, CARD_1, XXREAL_0, NEWTON, REAL_1, RELAT_1, PROB_1, SEQ_1, SEQ_2, ARYTM_1, ORDINAL2, RPR_1, XBOOLE_0, SUBSET_1, PROB_2, SERIES_1, NAT_1, FUNCT_1, PROB_3, SERIES_3, LIMFUNC1, SETLIM_1, XXREAL_2, FUNCOP_1, FUNCT_7, ASYMPT_1;
notations HIDDEN, XXREAL_0, XCMPLX_0, XREAL_0, ORDINAL1, REAL_1, XBOOLE_0, SUBSET_1, NUMBERS, NAT_1, COMPLEX1, SEQ_1, COMSEQ_2, SEQ_2, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, FUNCOP_1, PROB_1, PROB_2, SETLIM_1, SERIES_1, PROB_3, VALUED_0, VALUED_1, ZFMISC_1, LIMFUNC1, SERIES_3, NEWTON, ABIAN, SIN_COS;
definitions FUNCT_1, FUNCT_2;
theorems XCMPLX_0, SIN_COS, SERIES_1, PROB_1, SEQ_2, PROB_3, SUBSET_1, XBOOLE_0, XBOOLE_1, ABIAN, NAT_1, FUNCT_1, FUNCT_2, XXREAL_0, ORDINAL1, TARSKI, XREAL_1, PROB_2, ABSVALUE, VALUED_1, SEQ_4, LIMFUNC1, SETLIM_1, SERIES_3, NEWTON, POWER, FUNCOP_1, XREAL_0, SEQ_1;
schemes NAT_1, RECDEF_1, FUNCT_2;
registrations FUNCT_2, XCMPLX_0, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XREAL_0, NAT_1, MEMBERED, VALUED_0, VALUED_1, ABIAN, XXREAL_0, RELAT_1, SEQ_4, NEWTON, FUNCOP_1, PROB_2, PROB_3, SETLIM_1, RELSET_1, SIN_COS, INT_1, SEQ_1, SEQ_2;
constructors HIDDEN, RELSET_1, BINARITH, SQUARE_1, COMSEQ_3, RVSUM_1, SIN_COS, REAL_1, LIMFUNC1, SETLIM_1, SEQ_2, SERIES_1, KURATO_0, RINFSUP1, PROB_3, SERIES_3, ABIAN, NEWTON, NUMBERS, NAT_D, SEQ_4, RFUNCT_1, RCOMP_1, SEQM_3, FUNCT_4, COMSEQ_2, SEQ_1;
requirements HIDDEN, REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
equalities SIN_COS, PROB_1;
expansions FUNCT_2;
definition
let n1,
n2 be
Nat;
existence
ex b1 being sequence of NAT st
for n being Nat holds b1 . n = IFGT (n,n1,(n + n2),n)
uniqueness
for b1, b2 being sequence of NAT st ( for n being Nat holds b1 . n = IFGT (n,n1,(n + n2),n) ) & ( for n being Nat holds b2 . n = IFGT (n,n1,(n + n2),n) ) holds
b1 = b2
end;
definition
let k be
Nat;
existence
ex b1 being sequence of NAT st
for n being Nat holds b1 . n = IFGT (n,k,0,1)
uniqueness
for b1, b2 being sequence of NAT st ( for n being Nat holds b1 . n = IFGT (n,k,0,1) ) & ( for n being Nat holds b2 . n = IFGT (n,k,0,1) ) holds
b1 = b2
end;
definition
let n1,
n2 be
Nat;
existence
ex b1 being sequence of NAT st
for n being Nat holds b1 . n = IFGT (n,(n1 + 1),(n + n2),n)
uniqueness
for b1, b2 being sequence of NAT st ( for n being Nat holds b1 . n = IFGT (n,(n1 + 1),(n + n2),n) ) & ( for n being Nat holds b2 . n = IFGT (n,(n1 + 1),(n + n2),n) ) holds
b1 = b2
end;