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 Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
