logic i, n, s: int

goal intra_loop:
(i<=(n-1) and 
(2*s)=(i*(i+1)) and 
i<=n  ->
     (2*(s+(i+1)))=((i+1)*((i+1)+1)) and 
     (i+1)<=n)


goal exit:
((i>=n) and 
(2*s)=(i*(i+1)) and 
i<=n  ->
     (2*s)=(n*(n+1)))


goal start:
((n>=1)  ->
     (2*1)=(1*(1+1)) and 
     1<=n)