>
> 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 <r...@rbjones.com>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
>>
>
>

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