Proof step 1 from proof kadane-correct (conclusion)

User applied rule call right

And obtained the following new goals

• Proof step 2:

  ⊦ ⟪let size = # a, max_so_far = 0, max_ending_here = 0, n = 0 in {while n < size do {/* kadane-correct : invariant 0 ≤ max_ending_here ∧ max_ending_here ≤ max_so_far ∧ n ≤ size ∧ maximum-sum(subarray(a, 0, n), max_so_far) ∧ (∃ m. maximum-suffix-sum(subarray(a, 0, n), m, max_ending_here)) wfbound size - n; */; max_ending_here := max_ending_here + a[n]; if max_ending_here < 0 then max_ending_here := 0 else if max_so_far < max_ending_here then max_so_far := max_ending_here; n := n + 1}; res := max_so_far}⟫ maximum-sum(a, res)

Rule argument

Additional information

Used simplifier rules: max-sub-array-sum: ⊦ ;