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

Reply via email to