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, PARTFUN1, MARGREL1, ZF_MODEL, RFINSEQ, FINSEQ_4, LTLAXIO1, LTLAXIO2, XCMPLX_0;
notations HIDDEN, TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, SETFAM_1, ORDINAL1, CARD_1, RELAT_1, FUNCT_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, BINOP_1, FUNCOP_1, FINSEQ_1, FINSEQ_2, FINSEQ_4, AFINSQ_1, LEXBFS, RFINSEQ, RFINSEQ2, HILBERT1, STRUCT_0, XBOOLEAN, MARGREL1, AOFA_I00, LTLAXIO1, RLAFFIN3;
definitions LTLAXIO1;
theorems NAT_1, XXREAL_0, FINSEQ_1, NAT_D, XBOOLEAN, PARTFUN1, XREAL_1, ORDINAL1, XREAL_0, LTLAXIO1, FINSEQ_4, RFINSEQ, RELAT_1, FINSEQ_5, FUNCT_1, FINSEQ_3, FINSEQ_6, FINSEQ_2, PARTFUN2;
schemes NAT_1, FINSEQ_1, RECDEF_1;
registrations ORDINAL1, XXREAL_0, NAT_1, XBOOLEAN, RELSET_1, MARGREL1, XBOOLE_0, XREAL_0, HILBERT1, FINSEQ_1, LTLAXIO1, CARD_1;
constructors HIDDEN, XXREAL_0, NAT_D, RELSET_1, AOFA_I00, HILBERT2, LTLAXIO1, 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;
requirements HIDDEN, NUMERALS, BOOLE, SUBSET, ARITHM, REAL;
equalities XBOOLEAN, LTLAXIO1, FINSEQ_1, ORDINAL1;
expansions LTLAXIO1;
set l = LTLB_WFF ;
Lm1:
for f being FinSequence holds f . 0 = 0
set tf = TFALSUM ;
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));