[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: What have I missed ? (a proof failed)




Yechiel ---

Your proof can be completed with the following commands:

(grind)
(use "equal_ax")
(grind)

Check the on-line help for the commands `use' and `lemma'
for more information on what they do (i.e. "(help use)").

On another note, you have an unprovable type correctness 
condition (TCC) in your theory, as you declare a constant
`e' of the parameter type:

stack_0[T: TYPE]: THEORY
  BEGIN

    ...

    e    : T					% a constant

    ...

END stack_0

% Existence TCC generated (line 9) for  e: T
    % 
% May need to add an assuming clause to prove this.
  % untried
e_TCC1: OBLIGATION (EXISTS (x: T): TRUE);


As `T' is declared as `TYPE', it can be an *empty* type,
and as such declaring a constant of that type would be unsound.
You can eliminate this problem by changing the declaration 
to a nonempty type by using the keywords `TYPE+' or `NONEMPTY_TYPE',
for example:

stack_0 [T : NONEMPTY_TYPE] : THEORY
BEGIN

  e : T

END stack_0

The TCC is no longer generated in this case.

Hope that helps,

Dave

-- 
Dr Dave Stringer-Calvert, Software Engineer, Computer Science Laboratory,
SRI International, 333 Ravenswood Avenue, Menlo Park, CA 94025-3493, USA.
Phone: (650) 859-3291    Fax: (650) 859-2844   Email: dave_sc@csl.sri.com