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