Proving a function is a fixed point I'm taking a class in University which involves proving the correctness of computer programs and I'm really bad a proofs, I don't really understand them at all.
Can anyone tell me if my proof actually makes any sense, I frequently think I've written a proof but usually I've proved nothing.
Given this (T1 is a function that takes another function (F) as one of its parameters):
T1(F,x,y) == if y = 0 then x else F(x−1,y−1)

I had to suggest a fixed point solution, I suggested:
f1(x,y) == x - y

Because T1 is a recursive function that implements subtraction. And below I had to prove my suggestion was correct.
To show T1(f1) = f1

T1(f1, x, y) == if y = 0 then x else f1(x−1,y−1)

if y = 0 then x
else (x-1) - (y-1)

if y = 0 then x
else x - y - 2

x - y - 2 = f1(x-1,y-1)

x - y = f1(x,y)

Does my proof have some obvious hole in it that I'm not seeing or is there some mistake I can't see, I think it works but I'm not really sure why it proves anything?
 A: You are thinking of the map:
$$T_1(f,x,y)
=\begin{cases}
x & \text{if } y=0
\\f(x-1,y-1) & \text{otherwise}
\end{cases},
$$
and want to show that the function
$$
f(x,y)=x-y
$$
is a fixed point. This amounts to showing
$$
T_1(f,x,y)=f(x,y)=x-y\
$$
for any $x$ and $y$.
There are only two cases one has to check, $y=0$ and $y\neq 0$. If $y=0$, then $T_1(f,x,0)=x=x-0=f(x,0)$, just as we want. If $y\neq 0$, then $T_1(f,x,y)=f(x-1,y-1)=x-1-y+1=x-y=f(x,y)$, and the proof is done.
I don't fully understand the programmatic notation you are using, but I think this is what you are trying to do. However you have evaluated $f(x-1,y-1)$ to $x-y+2$ rather than $x-1-y+1=x-y$, possibly you have forgotten to distribute the minus sign. I hope this helps!
A: Your idea is correct, but in the way it's written I don't recognize it as a proof. You want to show that $T_1(f_1,x,y)=f_1(x,y)$ for all $x$ and $y$ in whatever your domain is. So start with $x$ and $y$, distinguish cases for $y=0$ and $y\neq0$, and then show that in both cases $T_1(f_1,x,y)=f_1(x,y)$.
