virtual substitution がよく分からない。 Fourier-Motzkin variable elimination とは違うのかな。