SUCCESIVE USE OF BACKWARD SUBSTITUTION

read(a);read(b);
x:=a+b;
write(x);
{output=input1 + input2}

Step 3:
a:=input1; b:=input2;
{a+b = input1 + input2}
x := a+b;

Step 4:
{input1+input2 = input1+input2}
a:=input1; b:=input2;

The results is a tautology (a statement that is always true), thus proving the correctness of the program.