helphomeduck scriptspecificationfirst proof page

Duck Proof Script
Sum of the First n Natural Numbers

*** file: /net/cs/htdocs/users/goguen/kumo/sum/
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

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

    intro: "The Base Case"

    intro: "The Induction Step"