environ
vocabularies HIDDEN, NUMBERS, SUBSET_1, INT_1, NAT_1, ARYTM_3, INT_2, CARD_1, XXREAL_0, ORDINAL1, SQUARE_1, ABIAN, RELAT_1, ARYTM_1, FINSET_1, FUNCT_1, XBOOLE_0, COMPLEX1, TARSKI, PYTHTRIP;
notations HIDDEN, TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, FINSET_1, ORDINAL1, CARD_1, NUMBERS, XCMPLX_0, XXREAL_0, INT_1, INT_2, NAT_1, NAT_D, SQUARE_1, ABIAN, PEPIN, DOMAIN_1, RELAT_1, FUNCT_1;
definitions INT_1, INT_2, ABIAN;
theorems SQUARE_1, NAT_1, INT_2, WSIERP_1, EULER_2, ABIAN, EULER_1, INT_1, ENUMSET1, FINSET_1, TARSKI, RELAT_1, FUNCT_1, ORDINAL1, ZFMISC_1, XBOOLE_0, XCMPLX_1, NEWTON, XREAL_1, COMPLEX1, XXREAL_0, PREPOWER, NAT_D, AFINSQ_1;
schemes NAT_1;
registrations ORDINAL1, FINSET_1, XXREAL_0, XREAL_0, NAT_1, INT_1, NEWTON, ABIAN, XBOOLE_0, RELAT_1;
constructors HIDDEN, DOMAIN_1, REAL_1, NAT_1, NAT_D, LIMFUNC1, ABIAN, PEPIN, VALUED_1;
requirements HIDDEN, SUBSET, BOOLE, NUMERALS, REAL, ARITHM;
equalities SQUARE_1, RELAT_1, ORDINAL1, CARD_1;
expansions INT_1, INT_2, ABIAN;