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