Loop invariant for adding 2 arrays storing binary value of integer Question:

Given 2 arrays of size $n$, $A = \langle a_1,a_2,\dots,a_n \rangle$ and $B = \langle b_1,b_2,\dots,b_n\rangle$, where $A$ and $B$ store the binary value of an integer. Find $A + B$ and stores the result in array $C$ of size $[n+1]$, $C = \langle c_1,c_2,\dots,c_{n+1}\rangle$.

Pseudocode:

ADD-BINARY(A,B)
C = new integer[A.length + 1]
carry = 0

for i = A.length to i = 1
    C[i] = (A[i] + B[i] + carry) % 2
    carry = (A[i] + B[i] + carry) / 2

C[1] = carry

return c


After writing the pseudo-code, I'm trying to find the loop invariant. One of the statement I can think of is 

At the start of each iteration in the for loop, C[A.length...i] consists of the sum of binary A[A.length...i] and B[A.length...i].

But I check the initialization stage and found out that it is invalid because at the beginning of the for loop C[A.length] does not have the sum yet(it just got initialized). So I'm puzzled whether I'm approaching it the right way.
Step 1: Fix the typo in c[i=]. That's obviously wrong. (Done). 

Step 1a: Try what happens when your algorithm adds 11 and 01. Notice that the result is wrong. 

Step 1b: Fix the bug in your code. Check what happens in your algorithm again. 

Step 2: Write down what is true at the end of the function which proves that the code is correct. 

Step 3: Write down what is correct after the last iteration where i = 1, before setting C [1] = carry, which will lead to the statement in Step 2. 

Step 4: Write down what is correct after each loop iteration, for each value of i. 

Step 5: Write down what must be true before each loop iteration to get the result in Step 4. 

Step 6: Figure out how Step 4 leads to Step 5. 

Step 7: Check that Step 5 is true before the first iteration.