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

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

``{i+1=3}i:=i+1{i=3} ``

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

``{???}i:=i+1{i=i+1} ``

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

``{i=0}i:=i+1{i=1} ``

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

``{i+1=0}i:=i+1{i=1} ``

Something like

``{i=i}...i:=i+1{i=i+1}      ``

would be good