Verify the validity of the following correctness statement by adding all the intermediate assertions and so producing the proof tableau. State all the mathematical facts used. All variables are of type int.

ASSERT(true)

if (x >= y) x = y - 1; else y = y + 1;

z = y + 1;

ASSERT(x < y < z)