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