defpred S1[ Nat] means Fib ($1 + 2) = (Fib $1) + (Fib ($1 + 1));
let n be Nat; Fib (n + 2) = (Fib n) + (Fib (n + 1))
A1:
for k being Nat st S1[k] & S1[k + 1] holds
S1[k + 2]
proof
let k be
Nat;
( S1[k] & S1[k + 1] implies S1[k + 2] )
assume
S1[
k]
;
( not S1[k + 1] or S1[k + 2] )
assume
S1[
k + 1]
;
S1[k + 2]
Fib ((k + 2) + 2) =
Fib (((k + 2) + 1) + 1)
.=
(Fib (k + 2)) + (Fib ((k + 2) + 1))
by PRE_FF:1
;
hence
S1[
k + 2]
;
verum
end;
Fib (0 + 2) =
Fib ((0 + 1) + 1)
.=
(Fib 0) + (Fib 1)
by PRE_FF:1
;
then A2:
S1[ 0 ]
;
A3:
S1[1]
by PRE_FF:1;
for n being Nat holds S1[n]
from FIB_NUM:sch 1(A2, A3, A1);
hence
Fib (n + 2) = (Fib n) + (Fib (n + 1))
; verum