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 \text{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 <= 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.
Your are almost right.
However there is a mistake when you say: "Since $0\leq k−1 <k$, this mean IH will apply to $FUN(x+3,y−1)$"
You assumed that $k=x+y$ thus $(x+3+y-1)=k+2$ and you cannot apply the IH !
For a correct proof I would go for 2 steps:
First prove that Fun(x,0) return 0+x (by induction on x)
Then prove that Fun(x,y) return x+y (by induction on y)