environ
vocabularies HIDDEN, NUMBERS, FINSET_1, XBOOLE_0, SUBSET_1, TARSKI, FUNCT_1, RELAT_1, FUNCOP_1, FUNCT_4, PBOOLE, FINSEQ_1, CARD_3, PARTFUN1, FUNCT_5, FUNCT_2, ZFMISC_1, FUNCT_6, NAT_1, CARD_1, ARYTM_3, MCART_1, FINSEQ_2, TREES_1, TREES_3, TREES_2, ORDINAL4, TREES_A, XXREAL_0, TREES_4, ARYTM_1, REAL_1;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, XCMPLX_0, XREAL_0, XTUPLE_0, MCART_1, CARD_1, RELAT_1, FUNCT_1, FINSET_1, PARTFUN1, FUNCT_2, ORDINAL1, NUMBERS, XXREAL_0, XXREAL_2, BINOP_1, FUNCOP_1, FUNCT_4, FUNCT_7, CARD_3, TREES_2, TREES_1, TREES_3, TREES_4, FUNCT_5, FUNCT_6, PBOOLE, FINSEQ_1, FINSEQ_2, NAT_1, NAT_D;
definitions TARSKI, FUNCOP_1, WELLORD2, FUNCT_1, RELAT_1, PBOOLE, XBOOLE_0, FINSET_1;
theorems TARSKI, ZFMISC_1, FINSEQ_1, FINSEQ_3, FUNCT_1, FUNCT_2, FUNCT_4, FUNCT_5, TREES_1, TREES_2, TREES_3, TREES_4, NAT_1, RELAT_1, CARD_3, FUNCOP_1, MCART_1, PBOOLE, CARD_2, CARD_1, FUNCT_6, FINSET_1, XBOOLE_0, XBOOLE_1, XCMPLX_1, ORDERS_1, XREAL_1, XXREAL_0, XXREAL_2, XREAL_0, PARTFUN1, FINSEQ_2, ORDINAL1;
schemes DOMAIN_1, PBOOLE, FUNCT_1, FRAENKEL, FINSEQ_1, NAT_1;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, FUNCOP_1, FINSET_1, XREAL_0, MEMBERED, FINSEQ_1, CARD_3, PBOOLE, TREES_2, TREES_3, XXREAL_2, CARD_1, RELSET_1, TREES_1, XTUPLE_0, NAT_1;
constructors HIDDEN, WELLORD2, BINOP_1, FUNCT_4, SETWISEO, XXREAL_0, NAT_1, FUNCT_5, CARD_3, SEQ_4, PBOOLE, TREES_4, BINARITH, INT_1, XXREAL_2, PARTFUN1, RELSET_1, FUNCT_7, XTUPLE_0, NAT_D;
requirements HIDDEN, NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
equalities FINSEQ_2;
expansions TARSKI, XBOOLE_0, FINSET_1;
scheme
LambdaRecCorrD{
F1()
-> non
empty set ,
F2()
-> Element of
F1(),
F3(
Nat,
Element of
F1())
-> Element of
F1() } :
( ex
f being
sequence of
F1() st
(
f . 0 = F2() & ( for
i being
Nat holds
f . (i + 1) = F3(
i,
(f . i)) ) ) & ( for
f1,
f2 being
sequence of
F1() st
f1 . 0 = F2() & ( for
i being
Nat holds
f1 . (i + 1) = F3(
i,
(f1 . i)) ) &
f2 . 0 = F2() & ( for
i being
Nat holds
f2 . (i + 1) = F3(
i,
(f2 . i)) ) holds
f1 = f2 ) )
:: Many Sorted Sets and Functions
::---------------------------------------------------------------------------
::$CT