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