Fourier–Motzkin elimination

Remarks

The main property: $(x_1, \dots, x_{n-1})$ satisfies $S'$ if and only if there is $x_n \in \R$ such that $(x_1, \dots, x_n)$ satisfies $S$. Indeed, inequalities in $I_+$ give upper bounds on $x_n$ and those in $I_-$ give lower bounds, and $S'$ says exactly that each lower bound is at most each upper bound. So the solution set of $S'$ is the projection of the solution set of $S$ forgetting $x_n$.

Example: for $-x \le 0$, $-y \le 0$, $x + y \le 1$, eliminating $y$ pairs $x + y \le 1$ (in $I_+$) with $-y \le 0$ (in $I_-$) and gives $x \le 1$. With $-x \le 0$ from $I_0$, the result is $0 \le x \le 1$, the projection of the triangle onto the $x$-axis.

Non-example: the method does not work for integer solutions. The system $x - 2y \le 0$, $-x + 2y \le 0$ with $x = 1$ has the real solution $y = 1/2$, but no integer solution $y$, while elimination of $y$ gives no condition that excludes $x = 1$.

The new system can have up to $\abs{I_0} + \abs{I_+} \cdot \abs{I_-}$ inequalities, at most $m^2/4$ when $I_0$ is empty, so repeated elimination can blow up quickly.