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

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

A1: S_{1}[1]
by Th32;

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

S_{1}[i + 2]
_{1}[ 0 ]
by Th32;

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

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

defpred S

A1: S

A2: for i being Nat st S

S

proof

A3:
S
let i be Nat; :: thesis: ( S_{1}[i] & S_{1}[i + 1] implies S_{1}[i + 2] )

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

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

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

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

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

end;assume ( S

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

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

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

hence S

for k being Nat holds S

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