Доказательство правильности алгоритма максимального подмассива грубой силы

Question

Я пытаюсь доказать правильность версии грубой силы проблемы максимального подмассива, приведенной ниже:

def max_subarray_bf(lst):
    left = 0
    right = 0
    max = lst[0]
    for i in range(len(lst)):
        current_sum=0
        for j in range(i, len(lst)):
            current_sum+=lst[j]
            if current_sum>max:
                max=current_sum
                left=i
                right=j
    return (left, right, max)

но я, кажется, застрял при разработке инварианта цикла, возможно, потому, что внутренний цикл изменяет глобальную переменную (max), из-за чего мне трудно изобразить то, что (max) представляет в инварианте цикла, соответствующем внутреннему циклу.

Моя попытка:

В целом алгоритм работает путем нахождения максимального подмассива из следующих подмассивов:

{[0],[0,1],...,[0,...,n]

 [1],[1,2],...,[1,...,n]

 .

 .

 .

 [n]}

• Инвариант внутренней петли:
  • Current_sum - это сумма всех элементов в массиве [i...j]
  • Застрял здесь, потому что я не могу понять, что будет макс с точки зрения I и J, и, следовательно, влево и вправо