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
%SFT%Z %V% St %def% [St : State] %EFT% That is what I am using so far, every operation is similar to %SZS% OpNewState %BH%%BH%%BH%%BH% %BV% %Delta%NewState %BT%%BH%%BH%%BH%%BH% %BV% Old.a = real 0; %EZ%%BH%%BH%%BH%%BH%%BH% 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? Thanks, -- Artur Oliveira Gomes
_______________________________________________ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
