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, ORDINAL1, ARYTM_1, ZF_LANG, PARTFUN1, MARGREL1, HILBERT2, ZFMISC_1, ZF_MODEL, GLIB_000, FINSET_1, ABCMIZ_0, HENMODEL, PRE_POLY, RFINSEQ, FIB_NUM, REWRITE1, MATROID0, MCART_1, UNIALG_2, TREES_1, TREES_2, TREES_4, SETFAM_1, NECKLA_3, MEMBER_1, AOFA_I00, FINSEQ_4, FINSEQ_2, RFINSEQ2, TREES_9, INT_1, VECTSP_1, LTLAXIO1, LTLAXIO2, LTLAXIO3, LTLAXIO4, GOEDCPUC, XCMPLX_0;
notations HIDDEN, TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, SETFAM_1, ORDINAL1, CARD_1, RELAT_1, FUNCT_1, 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, AFINSQ_1, LEXBFS, RFINSEQ, RFINSEQ2, HILBERT1, HILBERT2, STRUCT_0, XBOOLEAN, MARGREL1, AOFA_I00, MATROID0, RLAFFIN3, LTLAXIO1, LTLAXIO2, LTLAXIO3;
definitions TARSKI, XBOOLE_0, FINSEQ_2, FINSET_1, LTLAXIO1;
theorems TARSKI, NAT_1, XBOOLE_0, XXREAL_0, FINSEQ_1, NAT_D, XBOOLEAN, PARTFUN1, XREAL_1, ZFMISC_1, ORDINAL1, HILBERT2, XREAL_0, FINSEQ_4, RFINSEQ, RELAT_1, FINSEQ_5, FUNCT_1, FINSEQ_3, FINSEQ_6, XBOOLE_1, PRE_POLY, STIRL2_1, RLAFFIN3, HILBERT1, RFINSEQ2, NUMBERS, PARTFUN2, TREES_9, TREES_1, TREES_2, LTLAXIO1, LTLAXIO2, LTLAXIO3;
schemes NAT_1, FUNCT_2, HILBERT2, RECDEF_1, FRAENKEL, FINSEQ_4, FINSEQ_2, TREES_9, TREES_2;
registrations SUBSET_1, ORDINAL1, FUNCT_1, XXREAL_0, NAT_1, XBOOLEAN, RELSET_1, MARGREL1, XBOOLE_0, XREAL_0, HILBERT1, FINSET_1, FINSEQ_1, JORDAN23, FINSEQ_2, CARD_1, TREES_9, TREES_2, XTUPLE_0, LTLAXIO1, LTLAXIO3;
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, LTLAXIO3;
requirements HIDDEN, NUMERALS, BOOLE, SUBSET, ARITHM, REAL;
equalities XBOOLEAN, FINSEQ_1, TREES_2, LTLAXIO1, LTLAXIO2, LTLAXIO3;
expansions TARSKI, XBOOLE_0, LTLAXIO1, LTLAXIO3;
set l = LTLB_WFF ;
set pairs = [:(LTLB_WFF **),(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));