That a computed expression i + 1 can be assumed to be positive for non-zero i follows mathematically from overflow being undefined.