task : THEORY BEGIN sq( n:nat, m:nat ) : RECURSIVE nat = IF n <= m THEN 1 ELSE n*n + sq( n - 1, m ) ENDIF MEASURE n sum_squares_theorem : THEOREM FORALL ( n:nat ): FORALL ( m:nat ): (n >= m+2) IMPLIES sq( n, m ) = n * (n+1) * (2*n + 1)/6 + 1 - m*(m+1)*(2*m+1)/6 END task