Thanks, I overlooked the symbol I had used, I appreciate that, that cleared
the proof right up.
Any thoughts on my email before those?
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).
Proofpower mailing list