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?

On Wed, Oct 17, 2012 at 1:16 PM, Jon Lockhart <> wrote:

> Roger,
> Thanks, I overlooked the symbol I had used, I appreciate that, that
> cleared the proof right up.
> Any thoughts on my email before those?
> Regards,
> Jon
> On Wed, Oct 17, 2012 at 2:21 AM, Roger Bishop Jones <>wrote:
>> On Wednesday 17 Oct 2012 04:18, Jon Lockhart wrote:
>> > Attached is my latest attempt. With both the delta
>> > operator and priming Button_State, with the existance
>> > and precondition proof, I run into a wall. I get close,
>> > but can't seem to give it the right witness to solve
>> > this simple init operation.
>> The binding display for your witness uses "=" but should use
>> "=^" (equal with hat).
>> Roger
Proofpower mailing list

Reply via email to