Roger, Thanks for making that clear about how the system handles that. I was thinking that is what had happened but I wanted to make sure and get a clearer picture.
Now time to keep pushing forward. Thanks, Jon On Fri, Sep 14, 2012 at 4:56 PM, Roger Bishop Jones <r...@rbjones.com> wrote: > 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 > 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
