let a, b, n be Element of NAT ; :: thesis: GenFib (b,(a + b),n) = GenFib (a,b,(n + 1))

defpred S_{1}[ Nat] means GenFib (b,(a + b),$1) = GenFib (a,b,($1 + 1));

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

S_{1}[k + 2]

.= GenFib (a,b,(0 + 1)) by Th32 ;

then A2: S_{1}[ 0 ]
;

GenFib (b,(a + b),1) = a + b by Th32

.= a + (GenFib (a,b,1)) by Th32

.= (GenFib (a,b,0)) + (GenFib (a,b,(0 + 1))) by Th32

.= GenFib (a,b,(0 + 2)) by Th34

.= GenFib (a,b,(1 + 1)) ;

then A3: S_{1}[1]
;

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

hence GenFib (b,(a + b),n) = GenFib (a,b,(n + 1)) ; :: thesis: verum

defpred S

A1: for k being Nat st S

S

proof

GenFib (b,(a + b),0) =
b
by Th32
let k be Nat; :: thesis: ( S_{1}[k] & S_{1}[k + 1] implies S_{1}[k + 2] )

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

then GenFib (b,(a + b),(k + 2)) = (GenFib (a,b,(k + 1))) + (GenFib (a,b,(k + 2))) by Th34

.= GenFib (a,b,(k + 3)) by Th35

.= GenFib (a,b,((k + 2) + 1)) ;

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

end;assume ( S

then GenFib (b,(a + b),(k + 2)) = (GenFib (a,b,(k + 1))) + (GenFib (a,b,(k + 2))) by Th34

.= GenFib (a,b,(k + 3)) by Th35

.= GenFib (a,b,((k + 2) + 1)) ;

hence S

.= GenFib (a,b,(0 + 1)) by Th32 ;

then A2: S

GenFib (b,(a + b),1) = a + b by Th32

.= a + (GenFib (a,b,1)) by Th32

.= (GenFib (a,b,0)) + (GenFib (a,b,(0 + 1))) by Th32

.= GenFib (a,b,(0 + 2)) by Th34

.= GenFib (a,b,(1 + 1)) ;

then A3: S

for k being Nat holds S

hence GenFib (b,(a + b),n) = GenFib (a,b,(n + 1)) ; :: thesis: verum