environ
vocabularies HIDDEN, FINSEQ_1, CARD_1, ORDINAL4, SUBSET_1, NUMBERS, ARYTM_3, TARSKI, RELAT_1, XBOOLE_0, FUNCT_1, XBOOLEAN, MODELC_2, CQC_THE1, NAT_1, XXREAL_0, ARYTM_1, PARTFUN1, MARGREL1, HILBERT2, ZFMISC_1, ZF_MODEL, FINSET_1, RFINSEQ, LTLAXIO1, LTLAXIO5;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, DOMAIN_1, SUBSET_1, PARTFUN1, XCMPLX_0, NUMBERS, NAT_1, XXREAL_0, NAT_D, FUNCT_1, RELSET_1, FUNCT_2, FINSET_1, FINSEQ_1, RFINSEQ, HILBERT1, HILBERT2, XBOOLEAN, MARGREL1, LTLAXIO1;
definitions TARSKI, XBOOLE_0, LTLAXIO1;
theorems TARSKI, NAT_1, XBOOLE_0, XXREAL_0, FINSEQ_1, NAT_D, XBOOLEAN, PARTFUN1, XREAL_1, ZFMISC_1, ORDINAL1, XREAL_0, FINSEQ_4, RFINSEQ, RELAT_1, FINSEQ_5, FUNCT_1, FINSEQ_3, XBOOLE_1, LTLAXIO1, LTLAXIO2, LTLAXIO4;
schemes NAT_1, FUNCT_2, RECDEF_1, FRAENKEL, FINSEQ_1;
registrations SUBSET_1, ORDINAL1, NAT_1, XBOOLEAN, RELSET_1, MARGREL1, XBOOLE_0, XREAL_0, HILBERT1, FINSET_1, LTLAXIO1;
constructors HIDDEN, NAT_D, RELSET_1, HILBERT2, RFINSEQ, DOMAIN_1, LTLAXIO1;
requirements HIDDEN, NUMERALS, BOOLE, SUBSET, ARITHM, REAL;
equalities XBOOLEAN, FINSEQ_1;
expansions TARSKI, LTLAXIO1;