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, ZF_LANG, PARTFUN1, MARGREL1, FUNCT_2, HILBERT2, ZFMISC_1, FUNCOP_1, ZF_MODEL, PBOOLE, GLIB_000, FINSET_1, ABCMIZ_0, HENMODEL, PRE_POLY, RFINSEQ, FIB_NUM, REWRITE1, MATROID0, MCART_1, UNIALG_2, MEMBER_1, FINSEQ_5, LTLAXIO1, LTLAXIO2, LTLAXIO3, XCMPLX_0;
notations HIDDEN, TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, SETFAM_1, ORDINAL1, CARD_1, RELAT_1, FUNCT_1, XTUPLE_0, MCART_1, RELSET_1, PARTFUN1, DOMAIN_1, NUMBERS, XCMPLX_0, NAT_1, XXREAL_0, TREES_1, TREES_2, TREES_4, TREES_9, XREAL_0, NAT_D, FUNCT_2, FINSET_1, BINOP_1, FUNCOP_1, FINSEQ_1, FINSEQ_2, FINSEQ_4, FINSEQ_5, AFINSQ_1, LEXBFS, RFINSEQ, RFINSEQ2, HILBERT1, HILBERT2, PBOOLE, STRUCT_0, XBOOLEAN, MARGREL1, AOFA_I00, MATROID0, LTLAXIO1, LTLAXIO2;
definitions TARSKI, XBOOLE_0, FINSET_1, LTLAXIO1;
theorems TARSKI, NAT_1, XBOOLE_0, XXREAL_0, FINSEQ_1, XBOOLEAN, FUNCT_2, PARTFUN1, XREAL_1, ZFMISC_1, ORDINAL1, FUNCOP_1, HILBERT2, XREAL_0, FINSEQ_4, RFINSEQ, FINSEQ_5, CARD_1, FUNCT_1, FINSEQ_3, FINSEQ_6, FINSEQ_2, XBOOLE_1, FINSET_1, PRE_POLY, CARD_2, LTLAXIO1, LTLAXIO2;
schemes NAT_1, XBOOLE_0, HILBERT2, RECDEF_1, FRAENKEL;
registrations SUBSET_1, ORDINAL1, FUNCT_1, XXREAL_0, NAT_1, XBOOLEAN, RELSET_1, MARGREL1, XREAL_0, HILBERT1, FINSET_1, FINSEQ_1, LTLAXIO1, JORDAN23, CARD_1, XTUPLE_0;
constructors HIDDEN, XXREAL_0, NAT_D, RELSET_1, AOFA_I00, HILBERT2, FINSET_1, RFINSEQ, DOMAIN_1, AFINSQ_2, REAL_1, STRUCT_0, FUNCOP_1, XREAL_0, MATROID0, LEXBFS, MCART_1, CARD_1, RLAFFIN3, FINSEQ_4, FINSEQ_5, FINSEQ_2, RFINSEQ2, BINOP_2, ENUMSET1, SETFAM_1, TREES_9, TREES_2, TREES_4, AFINSQ_1, LTLAXIO1, LTLAXIO2, XTUPLE_0;
requirements HIDDEN, NUMERALS, BOOLE, SUBSET, ARITHM, REAL;
equalities XBOOLEAN, FINSEQ_1, XBOOLE_0, FINSEQ_5, LTLAXIO1, LTLAXIO2, CARD_1, ORDINAL1;
expansions TARSKI, XBOOLE_0, LTLAXIO1;
set l = LTLB_WFF ;
deffunc H1( FinSequence of LTLB_WFF ) -> Element of LTLB_WFF = 'not' ((con (nega $1)) /. (len (con (nega $1))));
deffunc H2( FinSequence of LTLB_WFF ) -> Element of LTLB_WFF = (con $1) /. (len (con $1));
set pairs = [:(LTLB_WFF **),(LTLB_WFF **):];