What is the inverse of this binary, bijective function? The following function $\operatorname{encode}$ is a binary, bijective function:
$$\operatorname{encode}(x,y) := \binom{x+y+1}{2} + x = z$$
This function comes up in the context of theoretical computer science in order to prove that LOOP-computable functions are primitive recursive. Because it is bijective, the function can be used to encode two numbers inside one.
Now given this function, what are the two inverse functions that decode a given $z$ into $x$ and $y$?
$$\operatorname{decode}_x(z) := \; ? \\
\operatorname{decode}_y(z) := \; ?$$
Do explicit forms of these function even exist? I can calculate the inverse of the function with respect to $x$ or $y$ individually, but these functions always depend on $z$ and the other parameter:
$$\operatorname{decode}_x(z, y) := \frac{1}{2} \left( \pm \sqrt{8z + 8y + 9} - 2y -3 \right) \\
\operatorname{decode}_y(z, x) := \frac{1}{2} \left( \pm \sqrt{8z - 8x + 1} - 2x - 1 \right) $$

As @AndréNicolas correctly noted, this encoding function is the Cantor pairing function. Given
$$\operatorname{encode}(x,y) = \binom{x+y+1}{2} + x = \frac{1}{2} (x+y)(x+y+1) + x = z$$
we introduce additional variables to help derive the $\operatorname{decode}$ functions:
\begin{align}
 w &:= x + y \\
 t &:= \binom{x+y+1}{2} = \frac{1}{2} w (w+1) \\
 z &:= t + x
\end{align}
We write the second equation as a function of $w$ and derive its inverse:
\begin{align}
 t &= T(w) = \frac{1}{2} w (w+1) \\
 0 &= w^2 + w - 2t \\
 w &= T^{-1}(t) = \frac{1}{2} \left( \sqrt{8t+1} - 1 \right).
\end{align}
From this, we can follow an upper and lower bound for $w$:
\begin{array}{rcl}
 t            \leq& t + x      &< t + x + y + 1 \\
 t            \leq& z          &< t + (w + 1) \\
 t            \leq& z          &< \frac{1}{2} ((w+1)^2 + (w+1)) \\
 T(w)         \leq& z          &< T(w+1) \\
 w            \leq& \frac{1}{2} \left( \sqrt{8z+1} - 1 \right) &< w+1 \\
\end{array}
Because $w \in \mathbb{N}_0$, we get:
\begin{align}
 w &= \left\lfloor \frac{1}{2} \left( \sqrt{8z+1} - 1 \right) \right\rfloor \\
 \operatorname{decode}_x(z) &= z \: - t \, = \phantom{-} z - \frac{1}{2} w (w + 1) \\
 \operatorname{decode}_y(z) &= w - x = - z + \frac{1}{2} w (w + 3)
\end{align}
