Gentlemen,

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.

Regards,
Jon


On Tue, Sep 18, 2012 at 5:05 PM, Jon Lockhart <jal...@bucknell.edu> 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 <r...@lemma-one.com> 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
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

Reply via email to