I see what you did there, and that makes since to me know. That is what I
was trying to achieve, but I was not getting there. Thanks for clearing
that up.


Now I have moved on to trying to do the same thing for masterReset, using
the exact same code that Roger has implemented in my spec, but now I am
getting an error when I try to push the consistency goal.

:) z_get_spec ñmasterReset®;
val it = ô (masterStop  BOOLEAN ± masterReset  BOOLEAN) ± true : THM
:) z_push_consistency_goal ñmasterReset®;
Exception Fail * Specification of z'masterReset is not of the form:
 (Ì vs[x1,...,xn]·p[x1,...,xn]) ô ...' [z_push_consistency_goal.46007] *

Is this because the that it has already because it was proven consistent
with the masterStop?


On Fri, Sep 14, 2012 at 2:07 PM, Phil Clayton <>wrote:

> On 14/09/12 18:48, Roger Bishop Jones wrote:
>> (I attach a revised version of your document with the proof
>> fixed).
> In order for z_get_spec to drop the consistency hypothesis, it is
> necessary to use save_consistency_thm on the resulting theorem.  So after
> the proof you need a line like:
> save_consistency_thm %SZT%masterStop%>% (pop_thm ());
> I tend to write such proofs with the following form, for some global
> variable C:
> save_consistency_thm %SZT%C%>% (
> z_push_consistency_thm %SZT%C%>%;
> (* proof steps here *)
> pop_thm ()
> );
> Phil
> ______________________________**_________________
> Proofpower mailing list

Attachment: elevatorSpecV5_P1.doc.gz
Description: GNU Zip compressed data

Proofpower mailing list

Reply via email to