environ
vocabularies HIDDEN, NUMBERS, NAT_1, XBOOLE_0, SUBSET_1, ARYTM_1, ARYTM_3, XXREAL_0, ABIAN, INT_1, POWER, RELAT_1, NEWTON, PREPOWER, SQUARE_1, FINSET_1, MEMBERED, SETFAM_1, FUNCT_1, FINSEQ_1, TARSKI, TURING_1, CARD_1, XXREAL_2, FUNCOP_1, VALUED_1, FUNCT_4, ZFMISC_1, PRE_FF, FIB_NUM, INT_2, ORDINAL4, CARD_3, PYTHTRIP, FIB_NUM2, REAL_1, XCMPLX_0;
notations HIDDEN, TARSKI, ORDINAL1, ENUMSET1, SUBSET_1, XBOOLE_0, SETFAM_1, CARD_1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, VALUED_1, SQUARE_1, INT_1, NAT_1, INT_2, NAT_D, FINSET_1, MEMBERED, RELAT_1, FUNCT_1, FUNCT_2, PRE_FF, RVSUM_1, ZFMISC_1, NEWTON, PREPOWER, POWER, XXREAL_2, ABIAN, DOMAIN_1, FINSEQ_1, FUNCT_4, FIB_NUM, PYTHTRIP, PEPIN, TREES_4;
definitions TARSKI, XBOOLE_0;
theorems NAT_1, PRE_FF, INT_2, SQUARE_1, WSIERP_1, PYTHTRIP, POWER, NEWTON, PREPOWER, XCMPLX_1, NAT_2, FINSEQ_1, XBOOLE_1, RELAT_1, ORDINAL1, CARD_2, FINSEQ_3, RVSUM_1, XBOOLE_0, FIB_NUM, TARSKI, FUNCT_1, FUNCT_2, ZFMISC_1, PEPIN, GRFUNC_1, FUNCT_4, FINSEQ_2, ENUMSET1, SETFAM_1, XREAL_1, XXREAL_0, NAT_D, XXREAL_2, XREAL_0, XTUPLE_0, VALUED_1, NUMBERS;
schemes NAT_1, FIB_NUM, FUNCT_2, DOMAIN_1, BINOP_2;
registrations XBOOLE_0, SETFAM_1, RELAT_1, FUNCT_1, ORDINAL1, FINSET_1, XXREAL_0, XREAL_0, SQUARE_1, NAT_1, INT_1, MEMBERED, FINSEQ_1, NEWTON, PREPOWER, ABIAN, NAT_2, VALUED_0, XXREAL_2, RELSET_1, XCMPLX_0;
constructors HIDDEN, REAL_1, NAT_D, FINSOP_1, NEWTON, PREPOWER, POWER, PRE_FF, BINARITH, WSIERP_1, ABIAN, PEPIN, PYTHTRIP, FIB_NUM, XXREAL_2, RELSET_1, DOMAIN_1, NUMBERS;
requirements HIDDEN, SUBSET, NUMERALS, REAL, ARITHM, BOOLE;
equalities SQUARE_1, FINSEQ_1, ORDINAL1;
expansions TARSKI, XBOOLE_0, FINSEQ_1;
scheme
FibInd1{
P1[
set ] } :
for
k being non
zero Nat holds
P1[
k]
provided
A1:
P1[1]
and A2:
P1[2]
and A3:
for
k being non
zero Nat st
P1[
k] &
P1[
k + 1] holds
P1[
k + 2]
scheme
FibInd2{
P1[
set ] } :
provided
A1:
P1[2]
and A2:
P1[3]
and A3:
for
k being non
trivial Nat st
P1[
k] &
P1[
k + 1] holds
P1[
k + 2]
Lm1:
for k being Nat holds Fib ((2 * (k + 2)) + 1) = (Fib ((2 * k) + 3)) + (Fib ((2 * k) + 4))
theorem Th47:
for
k being
Nat holds
(
Fib k = 1 iff (
k = 1 or
k = 2 ) )