Show postcondition i:=i+1 using Hoare assginment rule

as far as I understand the hoare assignment rule works like:


E.g. to get the precondition I take the postcondition {i=3} and replace every occurence of i against i+1.

But what if i want to show that if i holds a certain value before


that after the assignment i is increased by one, i.e. {i=i+1} is true? I cant replace i against i+1, otherwise i will get something like which is

{i+1=i+1+1}i:=i+1{i=i+1}  {i+1=i+2}i:=i+1{i=i+1}       i+1=i+2 is not equal 

Another example:

I want


But replacing i against i+1 in the postcondition I get


Something like


would be good