PROOF OBLIGATION 2 We must show that PRE ==> P4 P4 can be rewritten as x >= 0 and x = x The first clause is exactly PRE The second clause is an axiom of arithmetic QED
We must show that
PRE ==> P4
x >= 0 and x = x
The second clause is an axiom of arithmetic
QED