Thanks guys for the help. Those were a couple of little errors that I


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.
Proofpower mailing list

Reply via email to