Simplify the following:

wp("a = a + 2; b = b + 2",  a == b+1);

If you don't remember wp() notation, then consider the following:

assert(            );
a = a + 2;
b = b + 2;
assert(a == b+1);