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

Reply via email to