IF-THEN Proof

 { PRE: x > 3 }

    if ( x < 25 ) then x := 2 * x

 { POST: x >= 8 }



 1) show { PRE and x < 25 } x := 2*x { POST }

    { 2*x >= 8 } x := 2*x { x >= 8 }        ax.assn.
    { x >= 4 } x := 2*x { x >= 8 }           conseq.
        since x >= 4 ==> 2*x >= 8