# [ProofPower] Schemas and Operations

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