logic i, k, n: int

goal intra_loop:
forall a : int farray.

((i<n) and 
(forall k: int. 0<= k <= i-2 -> a[k]=(2*k)) and 
((i>0)  ->
     a[i-1]=(2*(i-1)))
 and 
(forall k: int. i<= k <= n-1 -> a[k]=k) and 
i<=n  ->
     (forall k: int. 0<= k <= i+1-2 -> a[k]=(2*k)) and 
     (((i+1)>0)  ->
          (a[i]*2)=(2*i))
 and 
     (forall k: int. i+1<= k <= n-1 -> a[k]=k) and 
     (i+1)<=n)


goal exit:
forall a : int farray.

((i>=n) and 
(forall k: int. 0<= k <= i-2 -> a[k]=(2*k)) and 
((i>0)  ->
     a[i-1]=(2*(i-1)))
 and 
(forall k: int. i<= k <= n-1 -> a[k]=k) and 
i<=n  ->
     (forall k: int. 0<= k <= n-1 -> a[k]=(2*k)))


goal start:
forall a : int farray.

((n>=1) and 
(forall k: int. 0<= k <= n-1 -> a[k]=k)  ->
     (forall k: int. 0<= k <= 0-2 -> a[k]=(2*k)) and 
     ((0>0)  ->
          a[0-1]=(2*(0-1)))
 and 
     (forall k: int. 0<= k <= n-1 -> a[k]=k) and 
     0<=n)