*** file: /net/cs/htdocs/users/goguen/kumo/stack/stack.duck
*****************************************
style: beijing
*****************************************
spec: /net/cs/htdocs/users/goguen/kumo/stack/stack.bob
*****************************************
cobasis:
   op top _ : Stack -> Nat .
   op pop _ : Stack -> Stack .
[]
*****************************************
proof: <<StackThm1>>
  goal:  pop empty = empty  and 
   ((forall N I : Nat  A : Arr)  top push(N, <I, A>) = N  ) and
   ((forall N I : Nat  A : Arr)  pop push(N, <I, A>) = <I, A> ) .
[]
*****************************************
proof: <<ArrayLemma>>
  goal: (forall I J N : Nat A : Arr)
           (I <= J  implies <I, put(N, J, A)> = <I, A>) .
  by: induction on I with scheme {0, s}; 
[]
*****************************************
proof: <<StackThm2>>
  goal:  pop empty = empty  and 
   ((forall N I : Nat  A : Arr)  top push(N, <I, A>) = N  ) and
   ((forall N I : Nat  A : Arr)  pop push(N, <I, A>) = <I, A> ) .
[]

*****************************************
display: <<ArrayLemma>>
   title:  "A Behavioral Property of Pointer-Array Pairs"
   dir: /net/cs/htdocs/groups/tatami/kumo/exs/stack/lemma
   homepage: /net/cs/htdocs/users/goguen/kumo/stack/stacklemma.hp
   specexpl: /net/cs/htdocs/users/goguen/kumo/stack/stackspec.exp

 <<ArrayLemma>>
  expl: /net/cs/htdocs/users/goguen/kumo/stack/stacklemma.exp
[]
*****************************************
display: <<StackThm1 StackThm2>>
   title:  "Implementing Stack with Pointer and Array"
   dir: /net/cs/htdocs/groups/tatami/kumo/exs/stack
   homepage: /net/cs/htdocs/users/goguen/kumo/stack/stack.hp
   specexpl: /net/cs/htdocs/users/goguen/kumo/stack/stackspec.exp
   closing:  /net/cs/htdocs/users/goguen/kumo/stack/stack.close

 <<StackThm1>>
  subtitle:  "This proof does not succeed, because a lemma is needed."
  expl: /net/cs/htdocs/users/goguen/kumo/stack/stack.exp1

 <<StackThm2>>
  subtitle:  "This time we succeed using the lemma."
  expl: /net/cs/htdocs/users/goguen/kumo/stack/stack.exp2
[]