Hi Roger,

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% %Delta%NewState
%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

Reply via email to