I moved on to the next area of my specification, which is the
initializations of the states declared earlier, and I am stuck on the first
one. No errors or anything, just not sure how to proceed to reduce the goal
any further. As of now I actually think what I have done is made the goal
more complex. Was using the z_"there exists"_tac to try and eliminate
portions so then I could feed the goal a tac proving the last bit which is
not a precondition. Unfortunately using the "there exists" tactic increased
the goal length and just added more. I have tried setting the values to
other items with no avail either in reducing the goal.

Attached as always is the current spec.


On Tue, Sep 18, 2012 at 5:05 PM, Jon Lockhart <> wrote:

> Thanks guys for the help. Those were a couple of little errors that I
> overlooked.
> Regards,
> Jon
> On Tue, Sep 18, 2012 at 4:06 PM, Rob Arthan <> wrote:
>> Jon,
>> On 18 Sep 2012, at 20:37, Jon Lockhart wrote:
>> > So I have run into an error again while working on my specification.
>> This time it is with the second axiomatic definition, the one right after
>> Roger helped me with last time. Using what he had done, and from the
>> integer example in the tutorial notes, I set up the evidence for how I
>> thought the system would want it to be given to it. Unfortunately this
>> throws an exception and I can't seem to massage it to be what it wants.
>> >
>> > Attached is the spec and a document containing the error.
>> >
>> In ProofPower-Z syntax, when you write down binding, you need to use the
>> equals with a hat (or a double equals sign) between the signature variables
>> and their values (as you did when you supplied the witness to an
>> existential goal in an earlier proof). Also you forgot the prime on the
>> bound variable name numOfButtons'. If you fix that and apply rewrite_tac
>> your goal will be proved.
>> Regards,
>> Rob.

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

Proofpower mailing list

Reply via email to