In the answer by Jacques Carette to this question, Jacques Carette suggests a possibility of adding extra variables and introducing extra equations to an already given set of equations in order to explicitly encode that certain variables cannot assume the value zero as solutions to these equations. Unfortunately, Jacques Carette does not go into detail on how this can be done. Therefore, I'd like to ask here if someone could explain this to me?
To be more explicit, let's consider the following system of equations
$$x+y=0$$ $$x^2+2y+1=0$$
Clearly, the solution set consists of $x= 1,y=- 1$. More importantly, $x$ and $y$ are never zero on the solution set. So let us now pretend that we do not know the solutions yet, but only know that $x$ cannot be zero. Introducing a new variable $z$ and a new equation to the system, how would we now polynomially encode that $x\neq0$?
How about $xz=1$ ?
A prime example is the Rabinowitsch trick.