What have I missed ? (a proof failed)

```Shalom PVS People,

Here is a simple example of a stack, based on your tutorials,
which I fail to prove a simple CONJECTURE.
I was sure missing a simple method, while looking at the documentation/HELP etc.
but I cannot figure out what it was.

Yechiel
--------------------------------------------------------------------------------

Happy Independence Day
Israel is 50 years young

TIME cannot be saved !!!
You can either borrow it - and PAY high interest in return,
or     invest it - and GET high interest in return.

Yechiel M. Kimchi			yechiel@cs.technion.ac.il
Faculty Comp. Sc.			The Technion, Haifa, 32000 IL
Office: (04) 829 4333			FAX: +(972) 4 822 1128
Homepage: http://www.cs.technion.ac.il/users/yechiel/
--------------------------------------------------------------------------------

Here is the problem (the full theory is enclosed below):

I want to prove

push_pop : CONJECTURE  pop(push(x, s)) = s

where, on top of the definitions I have an AXIOM

equal_ax : AXIOM
(FORALL s, st : (size(s) = size(st) AND (FORALL i:
(i < size(s) => lmnts(s)(i) = lmnts(st)(i))))
IMPLIES s = st)

Here how the proof goes:

push_pop :

|-------
{1}    (FORALL (s: stack, x: T): pop(push(x, s)) = s)

Rule? (grind :theories("stack_0"))
Date is Wed May 6 07:48:03 IDT 1998	;;  It activates my .cshrc :-]

size rewrites size(s)
to  PROJ_1(s)
lmnts rewrites lmnts(s)
to  PROJ_2(s)
push rewrites push(x, s)
to  (1 + PROJ_1(s), PROJ_2(s) WITH [(PROJ_1(s)) := x])
size rewrites size(1 + PROJ_1(s), PROJ_2(s) WITH [(PROJ_1(s)) := x])
to  1 + PROJ_1(s)
lmnts rewrites lmnts(1 + PROJ_1(s), PROJ_2(s) WITH [(PROJ_1(s)) := x])
to  PROJ_2(s) WITH [(PROJ_1(s)) := x]
pop rewrites pop(1 + PROJ_1(s), PROJ_2(s) WITH [(PROJ_1(s)) := x])
to  (PROJ_1(s), PROJ_2(s) WITH [(PROJ_1(s)) := x])
size rewrites size(PROJ_1(s), PROJ_2(s) WITH [(PROJ_1(s)) := x])
to  PROJ_1(s)
lmnts rewrites lmnts(PROJ_1(s), PROJ_2(s) WITH [(PROJ_1(s)) := x])
to  PROJ_2(s) WITH [(PROJ_1(s)) := x]
size rewrites size(PROJ_1(s), PROJ_2(s) WITH [(PROJ_1(s)) := x])
to  PROJ_1(s)
size rewrites size(s)
to  PROJ_1(s)
lmnts rewrites lmnts(PROJ_1(s), PROJ_2(s) WITH [(PROJ_1(s)) := x])
to  PROJ_2(s) WITH [(PROJ_1(s)) := x]
lmnts rewrites lmnts(s)
to  PROJ_2(s)
Date is Wed May 6 07:48:07 IDT 1998	;; It activates my .cshrc again

size rewrites size(PROJ_1(s!1), PROJ_2(s!1) WITH [(PROJ_1(s!1)) := x!1])
to  PROJ_1(s!1)
size rewrites size(s!1)
to  PROJ_1(s!1)
lmnts rewrites lmnts(PROJ_1(s!1), PROJ_2(s!1) WITH [(PROJ_1(s!1)) := x!1])
to  PROJ_2(s!1) WITH [(PROJ_1(s!1)) := x!1]
lmnts rewrites lmnts(s!1)
to  PROJ_2(s!1)
Date is Wed May 6 07:48:09 IDT 1998	;; Twice more

Date is Wed May 6 07:48:10 IDT 1998

Trying repeated skolemization, instantiation, and if-lifting,
this simplifies to:
push_pop :

|-------
{1}    (PROJ_1(s!1), PROJ_2(s!1) WITH [(PROJ_1(s!1)) := x!1]) = s!1

Rule?

It seems that a direct application of the AXIOM (equal_ax) suffices
and should be done automatically (since I asked (grind :theories("stack_0"))).
But it did not, and neither I found a command that will direct
the prover to using it.

What did I do wrong ?

--------------------------------------------------------------------------------
Here is the full theory:

stack_0[T: TYPE]: THEORY
BEGIN
stack: TYPE = [ nat, ARRAY[nat -> T] ]	% a type

s, st: VAR stack				% variables
x, y : VAR T
i, j : VAR nat

e    : T					% a constant
empty: stack = (0, (LAMBDA j: e))

lmnts(s)    : ARRAY[nat -> T] = proj_2(s)
size(s)     : nat             = proj_1(s)
nonempty?(s): bool            = (size(s) > 0)

push(x, s)  : (nonempty?)     =
(size(s)+1, lmnts(s) WITH [(size(s)) := x])
ns   : VAR (nonempty?)
top(ns)     : T               = lmnts(ns)(size(ns)-1)
pop(ns)     : stack           = (size(ns)-1, lmnts(ns))

equal_ax : AXIOM
(FORALL s, st : (size(s) = size(st) AND (FORALL i:
(i < size(s) => lmnts(s)(i) = lmnts(st)(i))))
IMPLIES s = st)

push_pop : CONJECTURE  pop(push(x, s)) = s

END stack_0

```