Sophie: pvs-sbcl-4.2-4.20100126svn.fc13 x86

pvs-sbcl-4.2-4.20100126svn.fc13.x86_64.rpm

Info
Deps
Files
Scripts
ChangeLog
Location
Others versions
Analyse

sum: THEORY
 BEGIN

 n: VAR nat

 sum(n): RECURSIVE nat =
  (IF n = 0 THEN 0 ELSE n + sum(n - 1) ENDIF)
  MEASURE id

 closed_form: THEOREM sum(n) = (n * (n + 1))/2

 END sum