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. >> >> >
Description: GNU Zip compressed data
_______________________________________________ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com