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 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: =TEX =SML open_theory "z_reals"; new_theory "temp"; =TEX %SZS% State %BH%%BH%%BH%%BH% %BV% a: %bbR%; %BV% b: %bbB% %EZ%%BH%%BH%%BH%%BH%%BH% %SZS% OpState %BH%%BH%%BH%%BH% %BV% %Delta%State %BT%%BH%%BH%%BH%%BH% %BV% a = real 0; %BV% %theta%(State \%down%s (a))' = %theta%(State \%down%s (a)) %EZ%%BH%%BH%%BH%%BH%%BH% %SFT%Z %BV% NewState %def% [OldState : State] %EFT% %SZS% OpNewState %BH%%BH%%BH%%BH% %BV% %Delta%NewState %BT%%BH%%BH%%BH%%BH% %BV% %exists%OpState%spot% %theta%(State) = OldState %and% %theta%(State)' = OldState' %EZ%%BH%%BH%%BH%%BH%%BH% =TEX regards, Rpger _______________________________________________ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
