Problem
Write pseudocode for a simple algorithm for addition of two n-digit numbers (one of them could be < n digits with 0's appended to the left) in base-10, as follows. Assume the digits are stored in arrays A and B, with A[1] and B[1] being the rightmost digits and A[n] and B[n] being the leftmost digits. Use a for loop to go from right to left adding the digits and keeping track of the carry. Now, here's the real task: write a loop invariant that is true each time the loop iterates, prove that it is indeed an invariant, and that the algorithm therefore accomplishes the goal.