Could someone check my recursive program correctness proof that returns $F(x, y) \rightarrow x + y$?

Question

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 > 0$. Suppose $Q(j)$ holds whenever $0 \leq j < k$ [I.H]

What to prove: $Q(k)$ holds

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

Therefore two cases: $y > 0$ and $y \leq 0$

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

Since $0 \leq k - 1 < 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 < 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?