Jon,
On Tuesday 16 Oct 2012 01:12, Jon Lockhart wrote:
> I guess I didn't quite understand or comprehend properly
> the second point you were trying to make. I inserted an
> existance proof like I had done for the state schemas
> and I unfortunately get a very interesting goal after
> the rewrite
Roger,
As for the change to the Intial Condition block I changed to what I have
read for literature over here, which is what Jacky claims is best practice.
I only switched it back to the original so that I could work from what was
original to the specifciation before moving to ProofPower and becua
Roger,
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. This does not bode well for the rest of the
opera
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 opera
