This is known as the frame rule (named after the frame problem) and enables local reasoning. It says that a program that executes safely in a small state (satisfying formula_12), can also execute in any bigger state (satisfying formula_60) and that its execution will not affect the additional part of the state (and so formula_15 will remain true in the postcondition). The side condition enforces this by specifying that none of the variables modified by formula_53 occur free in formula_15, i.e. none of them are in the 'free variable' set formula_64 of formula_15.