On Friday 14 Sep 2012 21:14, Jon Lockhart wrote:

> Now I have moved on to trying to do the same thing for
> masterReset, using the exact same code that Roger has
> implemented in my spec, but now I am getting an error
> when I try to push the consistency goal.

That's because its a single specification for two constants, 
and you have already proven the consistency goal.

Recall that the proof offered a composite witness, a binding 
with one component for each of the constituents of the 
signature of the axiomatic specification, both set to True.


Proofpower mailing list

Reply via email to