# [PVS-Help] Confused about proving extensionality of overriddenfunctions

```Hello all,

I'm trying to learn PVS, and need a gentle push in the right direction.

Assume this specification for a function-based implementation of stacks:

stacks: THEORY BEGIN

stack: TYPE = [# size: nat, elements: ARRAY[nat->int] #]
empty: stack = (# size:=0, elements:=(LAMBDA (j: nat): 0) #)

push(x: int, s:stack): { s: stack | s`size>=1 } =
(# size:=s`size+1,
elements:=s`elements WITH [(s`size):=x] #)

pop(s:stack | s`size>=1): stack =
(# size:=s`size-1,
elements:=s`elements WITH [(s`size-1):=0] #)

% Hack for now
all_above_are_zero: LEMMA
FORALL (s: stack, x: int): x>s`size => s`elements(x) = 0

push_pop: THEOREM
FORALL (s: stack, x: int): pop(push(x, s))=s

END stacks

(skolem!)
(expand* "push" "pop")
(lemma "all_above_are_zero" ("s" "s!1" "x" "s!1`size"))
(assert)
(apply-extensionality)

This results in the sequent:

[-1]  s!1`elements(s!1`size) = 0
|-------
{1}   s!1`elements WITH [(s!1`size) := 0] = s!1`elements
[2]   (# size := s!1`size,
elements := s!1`elements WITH [(s!1`size) := 0] #)
= s!1

Question #1: Now what? Shouldn't formula -1 be enough for formula 1?

Question #2: I tried writing all_above_are_zero as an axiom, but didn't
know how to utilize it in my proof. Is there some way to "use" an axiom?

Question #3: How do I rewrite my axiom so that it is higher-level, stating
that all stacks are either the empty stack, or derived from it?

Thanks,
David

_____________________________________________________________________
David Coppit                           david@coppit.org
The College of William and Mary        http://coppit.org/

"They have computers, and they may have other weapons of mass destruction."
Former Attorney General Janet Reno, speaking at LLNL of modern criminals

```