IF-THEN-ELSE Proof

 { PRE: x0 = x and y0 = y }

    if (x > y) then y := x

               else x := y

 { POST: x = y = max(x0,y0) }



 1) show { PRE and x > y } y := x { POST }

    { x = x = max(x0,y0) } y := x { POST }       ax.assn.   
    PRE and x > y  
      ==> x0 = x and y0 = y and x0 > y0     arith. subst.
      ==> x = max(x0,y0)                    arith. subst.             
          since x = x0 and x0 > y0