proof: <<SumThm>> 
    spec: nat.obj
    goal: (forall N : Nat) sum(N) + sum(N) = N * s N  .

  by: induction on N by scheme {0, s} []

  *** **********************************************

  display:
    title: "Sum of the First n Natural Numbers"
    putdir: /tmp/nat
    gethomepage: home.html
    getspecexpl: spec.html

  <<SumThm>>
    subtitle: "We show that <math>1+...+n</math>"+
              " equals <math>n(n+1)/2</math>. "
    getexpl: expl.html
  []

The Specification of Natural Number

  obj NAT is
    sort Nat .
    op 0 : -> Nat .
    op s_ : Nat -> Nat [prec 1] .
    op _+_ : Nat Nat -> Nat [assoc comm prec 20] .
    vars M N K : Nat .
    eq M + 0 = M .
    eq M + s N = s(M + N) .
    op _*_ : Nat Nat -> Nat [assoc comm prec 10] .
    eq M * 0 = 0 .
    eq M * s N = (M * N) + M .
  endo 

  obj SUM-NAT is
    pr NAT .
    var N : Nat .
    op sum : Nat -> Nat .
    eq sum(0) =  0 .
    eq sum(s N) = (s N) + sum(N)  .
  endo