let a, b, n be non zero Element of NAT ; :: thesis: GenFib (a,b,n) = ((GenFib (a,b,0)) * (Fib (n -' 1))) + ((GenFib (a,b,1)) * (Fib n))

thus GenFib (a,b,n) = ((GenFib (a,b,0)) * (Fib (n -' 1))) + ((GenFib (a,b,1)) * (Fib n)) :: thesis: verum

thus GenFib (a,b,n) = ((GenFib (a,b,0)) * (Fib (n -' 1))) + ((GenFib (a,b,1)) * (Fib n)) :: thesis: verum

proof

defpred S_{1}[ Nat] means GenFib (a,b,$1) = ((GenFib (a,b,0)) * (Fib ($1 -' 1))) + ((GenFib (a,b,1)) * (Fib $1));

GenFib (a,b,1) = ((GenFib (a,b,0)) * (Fib 0)) + ((GenFib (a,b,1)) * (Fib 1)) by PRE_FF:1

.= ((GenFib (a,b,0)) * (Fib (1 -' 1))) + ((GenFib (a,b,1)) * (Fib 1)) by XREAL_1:232 ;

then A1: S_{1}[1]
;

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

S_{1}[k + 2]

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

GenFib (a,b,2) = GenFib (a,b,(0 + 2))

.= ((GenFib (a,b,0)) * (Fib (1 + 0))) + ((GenFib (a,b,1)) * (Fib 2)) by A6, Th34, PRE_FF:1

.= ((GenFib (a,b,0)) * (Fib (1 + (1 -' 1)))) + ((GenFib (a,b,1)) * (Fib 2)) by XREAL_1:232

.= ((GenFib (a,b,0)) * (Fib ((1 + 1) -' 1))) + ((GenFib (a,b,1)) * (Fib 2)) by NAT_D:38

.= ((GenFib (a,b,0)) * (Fib (2 -' 1))) + ((GenFib (a,b,1)) * (Fib 2)) ;

then A7: S_{1}[2]
;

for k being non zero Nat holds S_{1}[k]
from FIB_NUM2:sch 1(A1, A7, A2);

hence GenFib (a,b,n) = ((GenFib (a,b,0)) * (Fib (n -' 1))) + ((GenFib (a,b,1)) * (Fib n)) ; :: thesis: verum

end;GenFib (a,b,1) = ((GenFib (a,b,0)) * (Fib 0)) + ((GenFib (a,b,1)) * (Fib 1)) by PRE_FF:1

.= ((GenFib (a,b,0)) * (Fib (1 -' 1))) + ((GenFib (a,b,1)) * (Fib 1)) by XREAL_1:232 ;

then A1: S

A2: for k being non zero Nat st S

S

proof

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

assume that

A3: S_{1}[k]
and

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

1 <= k by NAT_2:19;

then A5: (Fib (k -' 1)) + (Fib ((k + 1) -' 1)) = (Fib (k -' 1)) + (Fib ((k -' 1) + 1)) by NAT_D:38

.= Fib (((k -' 1) + 1) + 1) by PRE_FF:1

.= Fib ((k -' 1) + 2)

.= Fib ((k + 2) -' 1) by Th4 ;

GenFib (a,b,(k + 2)) = (((GenFib (a,b,0)) * (Fib (k -' 1))) + ((GenFib (a,b,1)) * (Fib k))) + (GenFib (a,b,(k + 1))) by A3, Th34

.= ((a * (Fib (k -' 1))) + ((GenFib (a,b,1)) * (Fib k))) + (GenFib (a,b,(k + 1))) by Th32

.= ((a * (Fib (k -' 1))) + (b * (Fib k))) + (GenFib (a,b,(k + 1))) by Th32

.= (((a * (Fib (k -' 1))) + (b * (Fib k))) + ((GenFib (a,b,0)) * (Fib ((k + 1) -' 1)))) + ((GenFib (a,b,1)) * (Fib (k + 1))) by A4

.= (((a * (Fib (k -' 1))) + (b * (Fib k))) + (a * (Fib ((k + 1) -' 1)))) + ((GenFib (a,b,1)) * (Fib (k + 1))) by Th32

.= (((a * (Fib (k -' 1))) + (b * (Fib k))) + (a * (Fib ((k + 1) -' 1)))) + (b * (Fib (k + 1))) by Th32

.= (a * ((Fib (k -' 1)) + (Fib ((k + 1) -' 1)))) + (b * ((Fib k) + (Fib (k + 1))))

.= (a * (Fib ((k + 2) -' 1))) + (b * (Fib (k + 2))) by A5, FIB_NUM2:24

.= (a * (Fib ((k + 2) -' 1))) + ((GenFib (a,b,1)) * (Fib (k + 2))) by Th32

.= ((GenFib (a,b,0)) * (Fib ((k + 2) -' 1))) + ((GenFib (a,b,1)) * (Fib (k + 2))) by Th32 ;

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

end;assume that

A3: S

A4: S

1 <= k by NAT_2:19;

then A5: (Fib (k -' 1)) + (Fib ((k + 1) -' 1)) = (Fib (k -' 1)) + (Fib ((k -' 1) + 1)) by NAT_D:38

.= Fib (((k -' 1) + 1) + 1) by PRE_FF:1

.= Fib ((k -' 1) + 2)

.= Fib ((k + 2) -' 1) by Th4 ;

GenFib (a,b,(k + 2)) = (((GenFib (a,b,0)) * (Fib (k -' 1))) + ((GenFib (a,b,1)) * (Fib k))) + (GenFib (a,b,(k + 1))) by A3, Th34

.= ((a * (Fib (k -' 1))) + ((GenFib (a,b,1)) * (Fib k))) + (GenFib (a,b,(k + 1))) by Th32

.= ((a * (Fib (k -' 1))) + (b * (Fib k))) + (GenFib (a,b,(k + 1))) by Th32

.= (((a * (Fib (k -' 1))) + (b * (Fib k))) + ((GenFib (a,b,0)) * (Fib ((k + 1) -' 1)))) + ((GenFib (a,b,1)) * (Fib (k + 1))) by A4

.= (((a * (Fib (k -' 1))) + (b * (Fib k))) + (a * (Fib ((k + 1) -' 1)))) + ((GenFib (a,b,1)) * (Fib (k + 1))) by Th32

.= (((a * (Fib (k -' 1))) + (b * (Fib k))) + (a * (Fib ((k + 1) -' 1)))) + (b * (Fib (k + 1))) by Th32

.= (a * ((Fib (k -' 1)) + (Fib ((k + 1) -' 1)))) + (b * ((Fib k) + (Fib (k + 1))))

.= (a * (Fib ((k + 2) -' 1))) + (b * (Fib (k + 2))) by A5, FIB_NUM2:24

.= (a * (Fib ((k + 2) -' 1))) + ((GenFib (a,b,1)) * (Fib (k + 2))) by Th32

.= ((GenFib (a,b,0)) * (Fib ((k + 2) -' 1))) + ((GenFib (a,b,1)) * (Fib (k + 2))) by Th32 ;

hence S

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

GenFib (a,b,2) = GenFib (a,b,(0 + 2))

.= ((GenFib (a,b,0)) * (Fib (1 + 0))) + ((GenFib (a,b,1)) * (Fib 2)) by A6, Th34, PRE_FF:1

.= ((GenFib (a,b,0)) * (Fib (1 + (1 -' 1)))) + ((GenFib (a,b,1)) * (Fib 2)) by XREAL_1:232

.= ((GenFib (a,b,0)) * (Fib ((1 + 1) -' 1))) + ((GenFib (a,b,1)) * (Fib 2)) by NAT_D:38

.= ((GenFib (a,b,0)) * (Fib (2 -' 1))) + ((GenFib (a,b,1)) * (Fib 2)) ;

then A7: S

for k being non zero Nat holds S

hence GenFib (a,b,n) = ((GenFib (a,b,0)) * (Fib (n -' 1))) + ((GenFib (a,b,1)) * (Fib n)) ; :: thesis: verum