Phil, Are you saying then for the Boolean block I have to just replace it with the one that you have provided in the email? Seems odd to be to just through True and False in there like that where I am describing sets but if it works, then I am all for it, I just need to see or understand how to use it properly.
As for the version of ProofPower, I have version 2.9.1w2, which is what you were saying does not support ==. Looks like I might have to update here when the latest stable version is released on the site. What I was saying on the masterStop / masterReset axiom, along with the minNumberFloors, maxNumberFloors, etc axioms, since I am using those as global variables essentially, is how do I prove them and preconditions on them like I have down for my States so far? Is is necessary too, or if I just get the spec of them they are already shown to be theorems? Thanks, Jon Lockhart On Wed, Sep 12, 2012 at 9:53 PM, Phil Clayton <[email protected]>wrote: > On 13/09/12 02:47, Phil Clayton wrote: > >> BOOLEAN that was defined to be 0 .. 5 >> > > I meant to say {0, 1}, of course! > > > > ______________________________**_________________ > Proofpower mailing list > [email protected] > http://lemma-one.com/mailman/**listinfo/proofpower_lemma-one.**com<http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com> >
_______________________________________________ Proofpower mailing list [email protected] http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
