Thank you, Roger.
Regards,
--
Artur Oliveira Gomes
___
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
Artur,
After my last post I remembered the previous conversation
and realised that you were reducing the width of your
schemas and then having a problem translating the
theta expressions in the original.
I've been a bit busier than usual so I didn't get
back. In fact I forgot.
To use a theta ter
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
Artur,
On Monday 09 February 2009 14:58:17 Artur Oliveira Gomes wrote:
> To represent that everything except "a" is unchanged in State, we use:
>
> %BV% %theta%(State \%down%s (a))' =
> %BV% %theta%(State \%down%s (a))
>
> But, using this,
>
> %SFT%Z
> %BV% NewState %def% [OldState : State]
