defpred S_{1}[ Nat] means (3 * (Fib $1)) + (Lucas $1) = 2 * (Fib ($1 + 2));

let n be Nat; :: thesis: (3 * (Fib n)) + (Lucas n) = 2 * (Fib (n + 2))

(0 + 1) + 1 = 2 ;

then A1: Fib 2 = 1 by PRE_FF:1;

A2: for k being Nat st S_{1}[k] & S_{1}[k + 1] holds

S_{1}[k + 2]

then Fib 3 = 2 by A1, PRE_FF:1;

then A4: S_{1}[1]
by Th11, PRE_FF:1;

A5: S_{1}[ 0 ]
by A1, Th11, PRE_FF:1;

for k being Nat holds S_{1}[k]
from FIB_NUM:sch 1(A5, A4, A2);

hence (3 * (Fib n)) + (Lucas n) = 2 * (Fib (n + 2)) ; :: thesis: verum

let n be Nat; :: thesis: (3 * (Fib n)) + (Lucas n) = 2 * (Fib (n + 2))

(0 + 1) + 1 = 2 ;

then A1: Fib 2 = 1 by PRE_FF:1;

A2: for k being Nat st S

S

proof

((0 + 1) + 1) + 1 = 3
;
let k be Nat; :: thesis: ( S_{1}[k] & S_{1}[k + 1] implies S_{1}[k + 2] )

assume A3: ( S_{1}[k] & S_{1}[k + 1] )
; :: thesis: S_{1}[k + 2]

(3 * (Fib (k + 2))) + (Lucas (k + 2)) = (3 * ((Fib k) + (Fib (k + 1)))) + (Lucas (k + 2)) by FIB_NUM2:24

.= ((3 * (Fib k)) + (3 * (Fib (k + 1)))) + ((Lucas k) + (Lucas (k + 1))) by Th12

.= (2 * (Fib (k + 2))) + (2 * (Fib ((k + 1) + 2))) by A3

.= 2 * ((Fib (k + 2)) + (Fib ((k + 2) + 1)))

.= 2 * (Fib ((k + 2) + 2)) by FIB_NUM2:24 ;

hence S_{1}[k + 2]
; :: thesis: verum

end;assume A3: ( S

(3 * (Fib (k + 2))) + (Lucas (k + 2)) = (3 * ((Fib k) + (Fib (k + 1)))) + (Lucas (k + 2)) by FIB_NUM2:24

.= ((3 * (Fib k)) + (3 * (Fib (k + 1)))) + ((Lucas k) + (Lucas (k + 1))) by Th12

.= (2 * (Fib (k + 2))) + (2 * (Fib ((k + 1) + 2))) by A3

.= 2 * ((Fib (k + 2)) + (Fib ((k + 2) + 1)))

.= 2 * (Fib ((k + 2) + 2)) by FIB_NUM2:24 ;

hence S

then Fib 3 = 2 by A1, PRE_FF:1;

then A4: S

A5: S

for k being Nat holds S

hence (3 * (Fib n)) + (Lucas n) = 2 * (Fib (n + 2)) ; :: thesis: verum