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 <phil.clay...@lineone.net>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
> Proofpower@lemma-one.com
> http://lemma-one.com/mailman/**listinfo/proofpower_lemma-one.**com<http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com>
>
_______________________________________________
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

Reply via email to