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 term you have to contrive to get the
required signature variables into scope.
One way to do this is to use a quantifier.

Here's one way to do this how for your original example:


open_theory "z_reals";
new_theory "temp";

%SZS% State %BH%%BH%%BH%%BH%
%BV% a: %bbR%;
%BV% b: %bbB%

%SZS% OpState %BH%%BH%%BH%%BH%
%BV% %Delta%State
%BV% a = real 0;
%BV% %theta%(State \%down%s (a))' = %theta%(State \%down%s (a))

%BV% NewState %def% [OldState : State]

%SZS% OpNewState %BH%%BH%%BH%%BH%
%BV% %Delta%NewState
%BV% %exists%OpState%spot% %theta%(State) = OldState %and% %theta%(State)' = 



Proofpower mailing list

Reply via email to