let n be Element of NAT ; :: thesis: EvenFibs ((2 * n) + 2) = (EvenFibs (2 * n)) ^ <*(Fib ((2 * n) + 2))*>
defpred S1[ Element of NAT ] means EvenFibs ((2 * $1) + 2) = (EvenFibs (2 * $1)) ^ <*(Fib ((2 * $1) + 2))*>;
A1:
S1[ 0 ]
by Th23, Th55, Th57, FINSEQ_1:47;
A2:
for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be
Element of
NAT ;
:: thesis: ( S1[k] implies S1[k + 1] )
assume
S1[
k]
;
:: thesis: S1[k + 1]
set LEFTk =
EvenFibs ((2 * (k + 1)) + 2);
set RIGHTk =
(EvenFibs (2 * (k + 1))) ^ <*(Fib ((2 * (k + 1)) + 2))*>;
reconsider RS =
FIB | (EvenNAT /\ (Seg ((2 * k) + 2))) as
FinSubsequence ;
reconsider ARR =
{[1,(FIB . ((2 * k) + 4))]} as
FinSubsequence by Th19;
set RR =
((2 * k) + 3) Shift ARR;
A3:
dom RS c= EvenNAT /\ (Seg ((2 * k) + 2))
by RELAT_1:87;
EvenNAT /\ (Seg ((2 * k) + 2)) c= Seg ((2 * k) + 2)
by XBOOLE_1:17;
then A4:
dom RS c= Seg ((2 * k) + 2)
by A3, XBOOLE_1:1;
(2 * k) + 3
> (2 * k) + 2
by XREAL_1:8;
then consider p1 being
FinSequence such that A5:
(
RS c= p1 &
dom p1 = Seg ((2 * k) + 3) )
by A4, Th21;
consider p2 being
FinSequence such that A6:
ARR c= p2
by Th22;
len p1 = (2 * k) + 3
by A5, FINSEQ_1:def 3;
then consider RSR being
FinSubsequence such that A7:
RSR = RS \/ (((2 * k) + 3) Shift ARR)
and A8:
(Seq RS) ^ (Seq ARR) = Seq RSR
by A5, A6, PNPROC_1:82;
1
+ ((2 * k) + 3) = (2 * k) + 4
;
then A9:
((2 * k) + 3) Shift ARR = {[((2 * k) + 4),(FIB . ((2 * k) + 4))]}
by Th20;
(EvenFibs (2 * (k + 1))) ^ <*(Fib ((2 * (k + 1)) + 2))*> =
(Seq (FIB | (EvenNAT /\ (Seg ((2 * k) + 2))))) ^ <*(FIB . ((2 * k) + 4))*>
by Def2
.=
Seq RSR
by A8, PNPROC_1:3
.=
EvenFibs ((2 * (k + 1)) + 2)
by A7, A9, Th60
;
hence
S1[
k + 1]
;
:: thesis: verum
end;
for k being Element of NAT holds S1[k]
from NAT_1:sch 1(A1, A2);
hence
EvenFibs ((2 * n) + 2) = (EvenFibs (2 * n)) ^ <*(Fib ((2 * n) + 2))*>
; :: thesis: verum