Loop invariants and a constraint relaxation are used to solve this problem.

Your browser can't display this PDF inline. Open it directly.