I want to use double induction (induction on two variables, right?) and I'm unsure of how to use the proposition for recursive functions. For a double induction I figured I needed two proofs, one for $x \rightarrow x+1$ and for $y \rightarrow y+1$.
Now let's say I want to proof $f(x,y) = x - y$ where $f$ is some recursive function declared prior to that. Part of this recursive function is $f(x,y) = f(x - 1, y - 1)$.
Proposition = $f(x,y) = x - y$
Step1: $x \rightarrow x+1$: \begin{align*} f(x + 1, y) &\stackrel{\text{Def. f}}{=} f(x, y - 1) \\&\stackrel{\text{Proposition}}{=} x - (y - 1) \\& etc. \end{align*}
Step2: $y \rightarrow y+1$: \begin{align*} f(x, y + 1) &\stackrel{\text{Def. f}}{=} f(x - 1, y) \\&\stackrel{\text{Proposition}}{=} (x - 1) - y \\& etc. \end{align*}
Is my use of the proposition right?
Furthermore if $f(x,y) = f(x - 2, y - 2)$.
Step1: $x \rightarrow x+1$: \begin{align*} f(x + 1, y) &\stackrel{\text{Def. f}}{=} f(x - 1, y - 2) \\&\stackrel{\text{Proposition}}{=} (x - 1) - (y - 2) \\& etc. \end{align*} would be wrong, right?
You’re problem is, that you’re moving (-1,-1) , not (-1,0) and (0,-1).Suppose you use as your base case: f(0,0)=0; then you can only prove f(x,y)=x-y for pairs (x,y) where x-y=0. If you could prove it for all pairs of integers, then there would be no other function g such that g(x-1,y-1) =g(x,y) and g(0,0)= 0, however the function g(x,y)=5(x-y) is also a solution to these constraints. In order to prove f(x,y)=x-y for all (x,y), you would have to have a second relation, perhaps f(x,y) = f(x-1,y)+1, so you could move in more than one direction.