Jon, 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. Roger _______________________________________________ Proofpower mailing list [email protected] http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
