[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: What have I missed ? (a proof failed)
Your proof can be completed with the following commands:
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
e : T % a constant
% Existence TCC generated (line 9) for e: T
% May need to add an assuming clause to prove this.
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',
stack_0 [T : NONEMPTY_TYPE] : THEORY
e : T
The TCC is no longer generated in this case.
Hope that helps,
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: firstname.lastname@example.org