Roger, 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.
Gentlemen, 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: `Consistent (Ì vs[x1,...,xn]·p[x1,...,xn]) ô ...' [z_push_consistency_goal.46007] * raised Is this because the that it has already because it was proven consistent with the masterStop? Thanks, Jon On Fri, Sep 14, 2012 at 2:07 PM, Phil Clayton <phil.clay...@lineone.net>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 > Proofpower@lemma-one.com > http://lemma-one.com/mailman/**listinfo/proofpower_lemma-one.**com<http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com> >
elevatorSpecV5_P1.doc.gz
Description: GNU Zip compressed data
_______________________________________________ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
