helphomeduck scriptspecificationfirst proof page


Duck Proof Script
Sum of the Squares of the First n Natural Numbers


*** file: /net/cs/htdocs/users/goguen/kumo/sumsq/sumsq.duck
*****************************************
style: beijing
*****************************************
spec: /net/cs/htdocs/users/goguen/kumo/sumsq/sumsq.bob
*****************************************

proof: <<Sumsq>>
  goal: (forall N : Nat) 6 * sumsq(N) = (2 * N * N * N) + (3 * N * N) + N  .
  by: induction on N with scheme {0, s} ;
[]

*****************************************
display: <<Sumsq>>
   title: "Sum of the Squares of the First n Natural Numbers"
   dir: /net/cs/htdocs/groups/tatami/kumo/exs/sumsq
  <<Sumsq>>
[]