Hi there, I'm working on a specification and I'm a little bit confused.
Given a simple state, %SZS% State %BH%%BH%%BH%%BH% %BV% a: %bbR% %BV% b: %bbB% %EZ%%BH%%BH%%BH%%BH%%BH% And one operation over that state, %SZS% OpState %BH%%BH%%BH%%BH% %BV% %Delta%State %BT%%BH%%BH%%BH%%BH% %BV% a = real 0; %BV% %theta%(State \%down%s (a))' = %BV% %theta%(State \%down%s (a)) %EZ%%BH%%BH%%BH%%BH%%BH% 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] %EFT% In a new operation, the predicate presented before is not accepted in ProofPower. How to say that the rest of the state is left unchanged? %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% Regards, -- Artur Oliveira Gomes
_______________________________________________ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
