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 <phil.clay...@lineone.net>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
> Proofpower@lemma-one.com
> http://lemma-one.com/mailman/**listinfo/proofpower_lemma-one.**com<http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com>
>

Attachment: 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

Reply via email to