environ
vocabularies HIDDEN, NUMBERS, STRUCT_0, GROUP_1, SUBSET_1, GROUP_2, FINSET_1, INT_2, CARD_1, GRAPH_1, RELAT_1, TARSKI, ALGSTR_0, ZFMISC_1, PBOOLE, REALSET1, NEWTON, INT_1, ARYTM_3, GROUP_4, ARYTM_1, NAT_1, FINSEQ_1, FUNCT_1, XXREAL_0, CQC_SIM1, XBOOLE_0, SETFAM_1, GROUP_8;
notations HIDDEN, XBOOLE_0, CARD_1, TARSKI, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, RELAT_1, REALSET1, FUNCT_1, FUNCT_2, PBOOLE, INT_1, NAT_1, FINSET_1, GROUP_2, GROUP_4, GR_CY_1, FINSEQ_1, DOMAIN_1, STRUCT_0, ALGSTR_0, GROUP_1, INT_2;
definitions TARSKI, FUNCT_1, WELLORD2, STRUCT_0;
theorems GROUP_2, GR_CY_1, GR_CY_2, NAT_1, TARSKI, XBOOLE_0, GROUP_1, CARD_1, GROUP_6, ALTCAT_1, FUNCT_2, GROUP_4, INT_2, XCMPLX_1, INT_1, FINSEQ_1, FUNCT_1, NEWTON, ORDINAL1, NAT_D, XXREAL_0, RELAT_1, PARTFUN1;
schemes SUBSET_1, NAT_1, FINSEQ_1, FUNCT_2;
registrations XBOOLE_0, SUBSET_1, RELSET_1, XXREAL_0, XREAL_0, NAT_1, INT_1, FINSEQ_1, STRUCT_0, GROUP_1, GROUP_2, GR_CY_1, ORDINAL1, FINSET_1;
constructors HIDDEN, WELLORD2, BINOP_1, REAL_1, NAT_D, BINOP_2, REALSET2, GROUP_4, GR_CY_1, RELSET_1;
requirements HIDDEN, REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
equalities REALSET1, ALGSTR_0, CARD_1, ORDINAL1;
expansions TARSKI, STRUCT_0;