Q: Formal proof for what algorithm return I need to formal proof that below algorithm return 1 for n = 1 and 0 in other cases. 
function K( n: word): word;
begin
   if (n < 2) then K := n
   else K := K(n − 1) * K(n − 2);
end;

Anyone could help? Thank you

A: This can be proven by induction, but as previous posters have shown, it's tricky to get formally correct when referring to K directly in the proof.
Here's my suggestion: Let P(n) be the property we want to show:
    P(n)    holds iff    K(n) yields 1 for n = 1, and 0 for n ≠ 1.
Now we can clearly express what we want to show: Ɐn.P(n)


*

*Base case: n &leq; 2
Trivial check by case analysis:
P(0) is ok, since K(0) = 0
P(1) is ok, since K(1) = 1

*Induction hypothesis:
P(n) holds for all 2 &leq; n < c.

*Inductive step: Show that P(c) holds


*

*By definition of K we have K(c) = K(c-1) × K(c-2)

*By the induction hypothesis, we know that P(c-1) and P(c-2) hold.

*Since at most one of K(c-1) and K(c-2) can be 1 (and the other must be 0) the product is 0.

*Which means that P(c) holds



Qed.

A: For n=1 by invoking the algorithm the answer is K=n=1, so we're done with that case.
For n=0, by definition, K(0) = 0.
For the case where n>1, we can solve it by induction:
Base: for n=2, we get: K(2) = K(1)*K(0) = 1*0 = 0
For n=3, we get: K(3) = K(2)*K(1) = 0*1 = 0 Note that K(2)=0 because we just showed it one line up.
Claim: For any 1<k<n, we get K(k) = 0
Proof for any n>3: K(n) = K(n-1)*K(n-2) =(1) 0*0 = 0

(1): Induction hypothesis, and since K(n-1),K(n-2) are both apply for it, since n-1,n-2>1

P.S. Note that the claim is true for non-negative numbers, for example, if you allow n=-5, you get K(-5)=-5 - which is a counter example to the claim.

A: Say n = 0. Since 0 < 2 we get 0 as result.
Say n = 1. Since 1 < 2 we get 1 as result.
Say n = 2. K(2) = K(1)*K(0). Since K(0) = 0 we get 0 as result.
For n > 2 now we suppose that statement about algorithm is true, i.e. K(n) = 0.
Now let show that it is also true for n + 1:
K(n + 1) = K(n)*K(n - 1). Since K(n) = 0 it is obvious that K(n)*K(n - 1) = 0.
