Roger,
I tried what you mentioned after Phil brought it up and if you try to do
State' and then push' = {} the system throws an error saying "No free types
allowed in predicates" which to me means that push is not accessible in the
predicate section. I also agree that doing the precondition seems redundant
now after you explain things, b/c since they are not operators so far,
there have been no way to show there were correct unless specifying
everything that was in the paragraph, as there was nothing changing, i.e.
having a prime after it.

## Advertising

So ProofPower won't let me use the 2 prime idea, so that must mean it is
not in the ISO Standard as good practice. So maybe I should go with what
Spivey is using.
Thanks,
Jon
On Fri, Sep 21, 2012 at 7:00 AM, Roger Bishop Jones <r...@rbjones.com> wrote:
> On Friday 21 Sep 2012 11:52, Roger Bishop Jones wrote:
> > I checked Spivey (Understanding Z)
>
> In fact it was "The Z Notation" I checked.
>
> 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