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.

## Advertising

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