Proving equality of functions defined by primitive recursion

126 Views Asked by At

Suppose $\mathbb{N}$ contains $0$. Let $G^1 : \mathbb{N} \rightarrow \mathbb{N}$ and $H^2 : \mathbb{N}^2 \rightarrow \mathbb{N}$. We define $F^2$: $$ F(x,0) := G(x) \\ F(x,z+1):= F(H(x,z),z). $$ Now we define $h^3$: $$ h(x,z,0) := x \\ h(x,z,y+1) := H(h(x,z,y), z-y -1). $$ I want to prove that $$F(x,y) = G(h(x,y,y)), \ \forall x,y \in \mathbb{N}.$$ Now, I don't really know the equality holds so I was maybe trying to prove something that is wrong, but it seems to me that the equality holds for the first couple of $y$ and fixed $x \in \mathbb{N}$. I tried using mathematical induction on $y$ for a fixed $x \in \mathbb{N}$, but it seems very messy and I don't how else am I supposed to prove this without using the induction.

EDIT: Forgot to mention that here for $x,y\in \mathbb{N}$ $x-y$ is defined as $x-y := max\{x-y,0\}$.

BIG EDIT: Suprisingly how noone noticed that but the old definition doesn't hold for h(x,1,1) for example. It's fixed now.