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.


On Thu, Sep 13, 2012 at 7:30 PM, Phil Clayton <>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

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

Proofpower mailing list

Reply via email to