defpred S1[ Nat] means OddFibs ((2 * $1) + 3) = (OddFibs ((2 * $1) + 1)) ^ <*(Fib ((2 * $1) + 3))*>;
let n be Nat; OddFibs ((2 * n) + 3) = (OddFibs ((2 * n) + 1)) ^ <*(Fib ((2 * n) + 3))*>
A1:
for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
reconsider ARR =
{[1,(FIB . ((2 * k) + 5))]} as
FinSubsequence by Th17;
assume
S1[
k]
;
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 ;
set RR =
Shift (
ARR,
((2 * k) + 4));
A2:
(2 * k) + 4
> (2 * k) + 3
by XREAL_1:6;
(
dom RS c= OddNAT /\ (Seg ((2 * k) + 3)) &
OddNAT /\ (Seg ((2 * k) + 3)) c= Seg ((2 * k) + 3) )
by RELAT_1:58, XBOOLE_1:17;
then consider p1 being
FinSequence such that A3:
RS c= p1
and A4:
dom p1 = Seg ((2 * k) + 4)
by A2, Th19, XBOOLE_1:1;
A5:
ex
p2 being
FinSequence st
ARR c= p2
by Th20;
1
+ ((2 * k) + 4) = (2 * k) + 5
;
then A6:
Shift (
ARR,
((2 * k) + 4))
= {[((2 * k) + 5),(FIB . ((2 * k) + 5))]}
by Th18;
len p1 = (2 * k) + 4
by A4, FINSEQ_1:def 3;
then consider RSR being
FinSubsequence such that A7:
RSR = RS \/ (Shift (ARR,((2 * k) + 4)))
and A8:
(Seq RS) ^ (Seq ARR) = Seq RSR
by A3, A5, VALUED_1:64;
(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, FINSEQ_3:157
.=
OddFibs ((2 * (k + 1)) + 3)
by A7, A6, Th63
;
hence
S1[
k + 1]
;
verum
end;
A9:
S1[ 0 ]
by Th22, Th60, Th61;
for k being Nat holds S1[k]
from NAT_1:sch 2(A9, A1);
hence
OddFibs ((2 * n) + 3) = (OddFibs ((2 * n) + 1)) ^ <*(Fib ((2 * n) + 3))*>
; verum