Phil, Moving them all to there own paragraph worked great. Now I am up to proving the consistency of the axioms, which is where I am run into my next stumbling block. Got the spec load and the consistency goal using the commands no problem. This generates a sub goal which looks relatively straight forward. It using the "there exist" symbol at the front of the goal, so my initial assumption is to use the z_"there exists"_tac, as seen in the provided spec. Unfortunately just giving it masterStop is not enough, and I can't feed it a list of masterStop and masterReset. Next thought was there should be some tactic like this that also has list in it, but I can't seem to find one. So that is where I am at right now.
Thanks, Jon On Thu, Sep 13, 2012 at 7:30 PM, Phil Clayton <[email protected]>wrote: > On 13/09/12 23:48, Jon Lockhart wrote: > >> I see now, I did not know that. You can lump them together in the Word >> document when I am using those tools but that is b/c when it is parsed >> each is separated into its own paragraph on the back end. I will be sure >> to correct that and see where I can get from there. Thanks for the help. >> > > You're welcome. By the way, I don't think any dialect of Z allows > multiple horizontal definitions in one paragraph. > > > > As for the zipped file I used the gzip command, which is short for >> gunzip. Was the first couple I sent you corrupted? >> > > No, all the other GZ attachments have been fine - it must have been > corrupted somewhere. > > > Phil > > > ______________________________**_________________ > Proofpower mailing list > [email protected] > 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 [email protected] http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
