logic sigma : int -> int
axiom A1: sigma(1)=1
axiom A2: forall n: int. n>1 -> sigma(n)=n*n+sigma(n-1)

logic n, s, i: int

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


goal exit:
((i>=n) and 
s=sigma(i) and 
i<=n and 
(i>=1)  ->
     s=sigma(n))


goal start:
(1<=n  ->
     1=sigma(1) and 
     1<=n and 
     (1>=1))