Re: [ProofPower] Trying to Prove my Zed Specifications

2012-10-16 Thread Roger Bishop Jones
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

Re: [ProofPower] Trying to Prove my Zed Specifications

2012-10-16 Thread Jon Lockhart
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

Re: [ProofPower] Trying to Prove my Zed Specifications

2012-10-16 Thread Jon Lockhart
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

Re: [ProofPower] Trying to Prove my Zed Specifications

2012-10-16 Thread Roger Bishop Jones
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