// Another example of a combination of a loop and an array.  The proof
// tableau is minimally commented so you will have to figure it out by
// yourselves.

ASSERT(2 <= n <= max)
ASSERT(2 <= n)
ASSERT(ForAll (k=2; k<2) (A|1 -> 1|0 -> 1)[k] == (A|1 -> 1|0 -> 1)[k-1] + (A|1 -> 1|0 -> 1)[k-2] 
       && 2 <= 2 <= n)
i = 2;
ASSERT(ForAll (k=2; k<i) (A|1 -> 1|0 -> 1)[k] == (A|1 -> 1|0 -> 1)[k-1] + (A|1 -> 1|0 -> 1)[k-2] 
       && 2 <= i <= n)
A[0] = 1;
ASSERT(ForAll (k=2; k<i) (A|1 -> 1)[k] == (A|1 -> 1)[k-1] + (A|1 -> 1)[k-2] 
       && 2 <= i <= n)
A[1] = 1;
ASSERT(ForAll (k=2; k<i) A[k] == A[k-1] + A[k-2] && 2 <= i <= n)
while (i < n) {
    ASSERT(ForAll (k=2; k<i) A[k] == A[k-1] + A[k-2] && 2 <= i <= n && i<n)
    ASSERT(ForAll (k=2; k<i) A[k] == A[k-1] + A[k-2] && 2 <= i+1 <= n && i<n)
    ASSERT(ForAll (k=2; k<i) A[k] == A[k-1] + A[k-2] && 2 <= i+1 <= n )
    ASSERT(ForAll (k=2; k<i) A[k] == A[k-1] + A[k-2]
           && A[i-1] + A[i-2] == A[i-1] + A[i-2] && 2 <= i+1 <= n )
    ASSERT(ForAll (k=2; k<i) (A|i -> A[i-1] + A[i-2])[k] == 
                             (A|i -> A[i-1] + A[i-2])[k-1] + (A|i -> A[i-1] + A[i-2])[k-2]
        && (A|i -> A[i-1] + A[i-2])[i] == (A|i -> A[i-1] + A[i-2])[i-1] + (A|i -> A[i-1] + A[i-2])[i-2]
        && 2 <= i+1 <= n )
    ASSERT(ForAll (k=2; k<i+1) (A|i -> A[i-1] + A[i-2])[k] == 
                               (A|i -> A[i-1] + A[i-2])[k-1] + (A|i -> A[i-1] + A[i-2])A[k-2]
        && 2 <= i+1 <= n )
    A[i] = A[i-1] + A[i-2];
    ASSERT(ForAll (k=2; k<i+1) A[k] == A[k-1] + A[k-2] && 2 <= i+1 <= n )
    i++;
    ASSERT(ForAll (k=2; k<i) A[k] == A[k-1] + A[k-2] && 2 <= i <= n )
}
ASSERT(ForAll (k=2; k<i) A[k] == A[k-1] + A[k-2] && i >= n && 2 <= i <= n )  // invariant
ASSERT(ForAll (k=2; k<n) A[k] == A[k-1] + A[k-2] && i >= n && 2 <= i <= n )  // add range
ASSERT(ForAll (k=2; k<n) A[k] == A[k-1] + A[k-2] && i >= n)  // add while condition
ASSERT(ForAll (k=2; k<n) A[k] == A[k-1] + A[k-2])