EXAMPLE (continued)

Now we take the new invariant,
L2: {input1 = div * y + x and
x >= 0 and y = input2}

and the negation of the loop condition,
{ x < y}, their conjunction is

{input1 = div * input2 + x and
0 =< x < input2}

This is the desired result, i.e.
{I and not cond} should be what
we want as the post condition