How can the weakest preconditions and the verification conditions for the following specification statements be derived using the postcondition hoisting technique and proof rules for sequence and assignment?

{ true } 
 
M := X; 
N := Y; 
A := 2 * M + N; 
N := N – 1; 
M := A 
 
{ M > N}