> > 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 >> > >
elevatorSpecV5_P1.doc.gz
Description: GNU Zip compressed data
_______________________________________________ Proofpower mailing list [email protected] http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
