Re: pvs, temporal logic and stacks

To use a temporal logic you need a temporal modality, i.e. a machine. In TLA, the machine is explicit. What you have is a specification of three mathematical functions, not a machine. You can describe the stack itself as a machine (that interprets "push", "pop" and "top"), which in TLA(+), would require s to be a variable, say, a sequence, which you can then hide with the temporal existential operator. Alternatively, you can keep push/pop/top as functions or operators, and describe just your theorem as a machine. The specification of your theorem would contain the constant N, which is the number of push/pop operations. You would then initialize two variables, m and n in the starting state to N, and in each step, nondeterministically do a push or a pop, decrementing m or n respectively until they reach zero.