*** Original PC ***
   0 <= Y0 - 3
   Y0 - 3 <= 0 && 0 <= Y0 - 1
*** Minimized PC ***
   0 <= Y0 - 3
   Y0 - 3 <= 0 && 0 <= Y0 - 1