# [PVS-Help] TCC Question (Stack followup)

```Hello all,

This is a followup to my previous stack question. Suppose I defined a
predicated subtype of Stack called Nonempty_Stack, in order to define
the "top" operation on only nonempty stacks.

Now, later, I have a recursive function called multiple_push_pop:

multiple_push_pop(s: Stack, values: list[Value]): RECURSIVE Stack =
IF (values = null) THEN
s
ELSE
LET (first_value, remaining_values) = (car(values), cdr(values)) IN
pop(multiple_push_pop(push(first_value,s), remaining_values))
ENDIF
MEASURE length(values)

I have a TCC now to prove that the result of the recursive call to
multiple_push_pop(push(first_value,s), remaining_values) returns a
nonempty stack:

multiple_push_pop_TCC3 :

|-------
{1}   FORALL (s: Stack, values: list[Value],
v:
[{z: [Stack, list[Value]] |
length(z`2) < length(values)} ->
Stack]):
NOT (values = null) IMPLIES
(FORALL (first_value: Value, remaining_values: list[Value]):
remaining_values = cdr(values) AND first_value = car(values)
IMPLIES
NOT is_empty?(v(push(first_value, s), remaining_values)))

How do I go about proving this?  Attached is the complete .pvs file.

Thanks,
David```
```stack_as_function1: THEORY
BEGIN

Value: NONEMPTY_TYPE
Stack: TYPE = [# size: nat, elements: [nat -> Value] #]

is_empty?(s: Stack):bool = s`size = 0

Nonempty_Stack: TYPE = {s:Stack | NOT is_empty?(s)}

push(v: Value, s: Stack):Nonempty_Stack =
(# size := s`size+1, elements := s`elements WITH [(s`size) := v ] #)

pop(s:Nonempty_Stack): Stack =
(# size := s`size-1, elements := s`elements #)

top(s:Nonempty_Stack):Value =
s`elements(s`size-1)

equals(s1:Stack, s2:Stack):bool =
s1`size = s2`size AND
FORALL (i:nat | i < s1`size):
s1`elements(i) = s2`elements(i)

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%pop_empty_is_empty: THEOREM
%  FORALL (s:Stack):
%    is_empty?(s) => is_empty?(pop(s))

not_empty_after_push: THEOREM
FORALL (s:Stack, v: Value): NOT is_empty?(push(v,s))

push_pop_return_same : THEOREM
FORALL (s:Stack, v: Value): equals(pop(push(v,s)),s)

top_element_after_push : THEOREM
FORALL (s:Stack, v: Value): top(push(v,s)) = v

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

double_push_pop : THEOREM
FORALL (s:Stack, v1: Value, v2: Value):
equals(pop(pop(push(v2, push(v1,s)))), s)

%multiple_push_pop_of_nonempty_is_nonempty: JUDGEMENT
%  multiple_push_pop(s: Nonempty_Stack, values: list[Value]) HAS_TYPE
%    Nonempty_Stack

multiple_push_pop(s: Stack, values: list[Value]): RECURSIVE Stack =
IF (values = null) THEN
s
ELSE
LET (first_value, remaining_values) = (car(values), cdr(values)) IN
pop(multiple_push_pop(push(first_value,s), remaining_values))
ENDIF
MEASURE length(values)

multiple_push_pop_size: LEMMA
FORALL (s:Stack, values: list[Value]):
multiple_push_pop(s, values)`size = s`size

multiple_push_pop_values: LEMMA
FORALL (s:Stack, values: list[Value], i:nat | i < s`size):
multiple_push_pop(s, values)`elements(i) = s`elements(i)

multiple_push_pop: THEOREM
FORALL (s:Stack, values: list[Value]):
equals(multiple_push_pop(s, values), s)

END stack_as_function1
```