environ
vocabularies HIDDEN, NUMBERS, STRUCT_0, MSAFREE2, XBOOLE_0, MSUALG_1, FINSET_1, RELAT_1, PBOOLE, GLIB_000, FUNCT_1, UNIALG_2, SUBSET_1, FINSEQ_1, FUNCOP_1, FUNCT_6, FSM_1, CARD_3, MARGREL1, TREES_3, TREES_4, PARTFUN1, MSAFREE, TREES_2, ARYTM_3, TREES_1, ZFMISC_1, LANG1, DTCONSTR, TREES_A, TDGROUP, TARSKI, NAT_1, ORDINAL4, CARD_1, XXREAL_0, MEMBERED, ARYTM_1, FUNCT_4, REAL_1, CIRCUIT1;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, CARD_1, NUMBERS, XCMPLX_0, XREAL_0, REAL_1, NAT_1, MEMBERED, RELAT_1, FUNCT_1, PBOOLE, PARTFUN1, FINSEQ_1, FINSEQ_2, RELSET_1, FINSET_1, CARD_3, FUNCT_4, FUNCT_6, TREES_1, TREES_2, TREES_3, TREES_4, STRUCT_0, LANG1, DTCONSTR, MSUALG_1, MSUALG_2, MSAFREE, XXREAL_2, FUNCOP_1, MSAFREE2, XXREAL_0;
definitions TARSKI, MEMBERED;
theorems TARSKI, ZFMISC_1, NAT_1, FINSEQ_1, FINSEQ_2, FINSEQ_3, FUNCT_1, FUNCT_2, TREES_1, TREES_2, TREES_3, TREES_4, CARD_1, CARD_2, CARD_3, FUNCOP_1, PBOOLE, PRALG_2, MSUALG_1, MSUALG_2, RELAT_1, MSAFREE1, MSAFREE, PRE_CIRC, DTCONSTR, LANG1, MSAFREE2, FUNCT_4, FUNCT_6, XBOOLE_0, XBOOLE_1, MEMBERED, FINSET_1, XREAL_1, XXREAL_0, ORDINAL1, PARTFUN1, XXREAL_2, XTUPLE_0;
schemes NAT_1, FINSEQ_1, PRE_CIRC, PBOOLE, FRAENKEL, DOMAIN_1;
registrations XBOOLE_0, RELAT_1, FUNCT_1, ORDINAL1, FINSET_1, XXREAL_0, XREAL_0, NAT_1, MEMBERED, FINSEQ_1, TREES_1, CARD_3, PBOOLE, TREES_2, TREES_3, PRE_CIRC, STRUCT_0, DTCONSTR, MSUALG_1, MSAFREE, MSAFREE2, FUNCT_2, XXREAL_2, CARD_1, RELSET_1;
constructors HIDDEN, FUNCT_4, REAL_1, MSUALG_2, MSAFREE2, SEQ_4, RELSET_1, NUMBERS;
requirements HIDDEN, REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
equalities TARSKI, MSAFREE2;
expansions MSAFREE2;
defpred S1[ set ] means verum;
:: Circuits
::---------------------------------------------------------------------------