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 <[email protected]> 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 [email protected] http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
