Roger, I tried using that before, and ProofPower gave me an exception. I asked about it in the beginning from Rob, and he said == worked in the latest update on the source page, which I believe I have a few versions older. I tried updating myself, but my advisor has some odd permissions so he have to do it, and he just hasn't yet, so untill he does I am stuck with the ^=.

## Advertising

After fixing the correction you pointed out, I was able to get the existance proofs completed and I removed the precondition proofs for those init operations. You can see this in the attached specification file. Now this brings up a previous question again, along with a new one. 1) Is it necessary to have the precondtion proofs with the exsistance proofs in the specification? If not necessary is it wise to use both, or are both redundant in terms of what they are showing and not necessary? 2) I am now on to the first main operation of the specification, and I have a precondition proof outlined, albeit some changes are required of it, to begin proving properties of said operation. Should I stick with the precondition proof for this and the other opertations or is there another proof I should be using? What other proofs just on the operations should I be looking to use? Regards, Jon On Thu, Oct 18, 2012 at 6:03 AM, Rob Arthan <r...@lemma-one.com> wrote: > > On 17 Oct 2012, at 07:21, Roger Bishop Jones wrote: > > The binding display for your witness uses "=" but should use > "=^" (equal with hat). > > > As an aside, you can now also use "==" like the Z standard. This is a bit > easier to find on the keyboard when you are in a hurry doing a proof. > > Regards, > > Rob. >

**
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