This is a simple example to try to explain what I have now.
My current problem is bigger than that. I have a state with
many components. To load any operation over that state,
ProofPower takes a long time without response. Few months
ago, I sent a doc file to Rob Arthan and he suggested to use
%V% St %def% [St : State]
That is what I am using so far, every operation is similar to
%SZS% OpNewState %BH%%BH%%BH%%BH%
%BV% Old.a = real 0;
and it works fine, loading quickly.
>For a similar predicate to work you would need the signature
>of NewState to be the same as for State.
Is there any other solution for my problem?
Artur Oliveira Gomes
Proofpower mailing list