*** file: /net/cs/htdocs/users/goguen/kumo/sum/sum.duck
*****************************************
style: beijing
*****************************************
spec: /net/cs/htdocs/users/goguen/kumo/sum/nat.obj
*****************************************
proof: <<SumThm>>
  goal: (forall N : Nat) sum(N)+sum(N) = N * s N .
  by: induction on N with scheme {0, s}; []
*****************************************
display: <<SumThm>>
  title: "Sum of the First n Natural Numbers"
  dir: /net/cs/htdocs/groups/tatami/kumo/exs/sum
  homepage: /net/cs/htdocs/users/goguen/kumo/sum/home
  specexpl: /net/cs/htdocs/users/goguen/kumo/sum/spec-exp

  <<SumThm>>
    intro: "We will show that<math>1+...+n</math> equals" + 
              "<math>n(n+1)/2</math>."
    expl:  /net/cs/htdocs/users/goguen/kumo/sum/exp0

  <<SumThm.1>>
    intro: "The Base Case"

  <<SumThm.2>> 
    intro: "The Induction Step"
[]