title: Need help proving loop invariant (simple bubble sort, partial correctness)
body: <p>The bubble-sort algorithm (pseudo-code):</p>
  
  <pre><code>Input: Array A[1...n]
  for i &lt;- n,...,2 do
      for j &lt;- 2,...,i do
          if A[j - 1] &gt;= A[j] then
              swap the values of A[j-1] and A[j];
  </code></pre>
  
  <p>I am not sure but my proof seems to work, but is overly convoluted. Could you help me clean it up?</p>
  
  <blockquote>
    <p>Loop-invariant: After each iteration i, the i - n + 1 greatest
    elements of A are in the position they would be were A sorted
    non-descendingly. In the case that array A contains more than one
    maximal value, let the greatest element be the one with the smallest index
    of all the possible maximal values.</p>
    
    <p>Induction-basis (i = n): The inner loop iterates over every element of
    A. Eventually, j points to the greatest element. This value will be
    swapped until it reaches position i = n, which is the highest position
    in array A and hence the final position for the greatest element of A.</p>
    
    <p>Induction-step: (i = m -> i = m - 1 for all m > 3): The inner loop
    iterates over every element of A. Eventually, j points to the greatest
    element of the ones not yet sorted. This value will be swapped until
    it reaches position i = m - 1, which is the highest position of the
    positions not-yet-sorted in array A and hence the final position for
    the greatest not-yet-sorted element of A.</p>
    
    <p>After the algorithm was fully executed, the remaining element at
    position 1 is also in its final position because were it not, the
    element to its right side would not be in its final position, which is
    a contradiction. Q.E.D.</p>
  </blockquote>