environ
vocabularies HIDDEN, XBOOLE_0, SUBSET_1, MARGREL1, PARTIT1, BVFUNC_1, XBOOLEAN, FUNCT_1, EQREL_1, BVFUNC_2;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, XBOOLEAN, MARGREL1, RELAT_1, FUNCT_1, FUNCT_2, EQREL_1, BVFUNC_1, BVFUNC_2;
definitions BVFUNC_1, FUNCT_2;
theorems BVFUNC_1, BVFUNC_2, MARGREL1, XBOOLEAN, EQREL_1;
schemes ;
registrations XBOOLEAN, MARGREL1;
constructors HIDDEN, BINARITH, BVFUNC_1, BVFUNC_2, NUMBERS;
requirements HIDDEN, SUBSET, BOOLE, ARITHM, NUMERALS;
equalities BVFUNC_1, XBOOLEAN, BVFUNC_2;
expansions BVFUNC_1, BVFUNC_2;