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
proof
defpred S1[ 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)) * ()) + ((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: S1 ;
A2: for k being non zero Nat st S1[k] & S1[k + 1] holds
S1[k + 2]
proof
let k be non zero Nat; :: thesis: ( S1[k] & S1[k + 1] implies S1[k + 2] )
assume that
A3: S1[k] and
A4: S1[k + 1] ; :: thesis: S1[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
.= ((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
.= (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 S1[k + 2] ; :: thesis: verum
end;
(0 + 1) + 1 = 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
.= ((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: S1 ;
for k being non zero Nat holds S1[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;