logic n, s, i: int

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


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


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