Could someone check my recursive program correctness proof that returns $F(x, y) \rightarrow x + y$? For $k \in \mathbb N$, we define $Q(k)$ as follows:

$Q(k): $ let $x, y \in \mathbb N$ and $x$ is a multiple of $3$ and $k = x + y$, then $FUN(x, y)$ terminates and returns $x + y$

I will prove $Q(k)$ using induction

Base Case: let $k = 0 \to iff (x = 0, y = 0)$

By line 1, 2, 5, $FUN(x, y)$ terminates and returns $0 + 0 = x + y$ as wanted

Inductive step: Let $k &gt; 0$. Suppose $Q(j)$ holds whenever $0 \leq j &lt; k$ [I.H]

What to prove: $Q(k)$ holds

Since $k &gt; 0$, it follows that line 3-7 could run since line 1 is not satisfied.

Therefore two cases: $y &gt; 0$ and $y \leq 0$

Case 1: If $y &gt; 0$, then line 3, 4, and 7 will run. 

Since $0 \leq k - 1 &lt; k$, this mean IH will apply to $FUN(x+3, y - 1)$

By IH, $FUN(x+3, y - 1)$ terminates and returns $x + 3 + y - 1$

By line 3, 4 and 7. $FUN(x, y)$ terminates and returns $x + 3 + y - 1 - 2 = x + y$ by algebra, and as wanted

Case 2: If $y \leq 0$, then line 5, 6, and 7 will run since line 1, 3 are not satisfied

Since $0 \leq k - 1 &lt; k$, this mean IH will apply to $FUN(x - 3, y )$

By IH, $FUN(x - 3, y )$ terminates and returns $x - 3 + y$

By line 5, 6 and 7. $FUN(x, y)$ terminates and returns $x - 3 + y + 3 = x + y$ by algebra, and as wanted

Therefore $Q(k)$ holds as wanted

This is my attempt above, not sure if I'm correct. I'm pretty confused on how to use IH in this or if my input size is even good. Is it correct?
As mentioned by Apass.Jack, you cannot apply IH to the $y&gt;0$ case, since $ (x+3)+(y-1)=x+y+2&gt;k$. I think you will want to do induction on $k=\min(x,\,y)$. Then you have no problem applying IH, since either $x$ or $y$ will always be smaller in the recursive call. The only difficulty here is that in your base case, you now need to cover when one of $x$ or $y$ is zero and the other is arbitrary. I will omit the case when both are zero, for brevity.

In the case that $y$ is zero, then the result will be $\text{FUN}(x-3,\,0)+3$. If $x$ is a multiple of 3 and positive, then this will eventually give $\text{FUN}(0,\,0)$ and then 3s will be added until you get $x$ again. This is what you wanted, since $x+y=x+0=x$. Note that the recursive calls retain the conditions that $x\geq0$ and a multiple of 3.

In the case that $x$ is zero, then the result will be $\text{FUN}(3,\,y-1)-2$, assuming your algorithm terminates, since if the algorithm took the $\text{FUN}(-3,\,y)+3$ branch, then there would be an infinite recursion. This implies that $y&gt;0$ initially. Then this branch will continue to be taken until $y=0$, in which case we will return $\text{FUN}(3y-3,\,0)+3$. This is the case when $x&gt;0$ and $y=0$, covered above. Then we get $3y-3+3-2y=y=0+y=x+y$. The $-2y$ comes from subtracting 2 recursively $y$ times.