I have one problem with the pvs language, and I'll be grateful of your help.
I want to express substitution of a variable X by a term T in another algebraic term. For instance:
subst(X, T, OP1(X,OP2(Y,Z),Y))
X and T are typed with a previous written datatype. Is there ever exist a theory which allows this feature, or have you got ideas/tracks about that ?
Thank you very much,
-- Gwen Salaün, PhD Student Tel: 02 51 12 58 22 Fax: 02 51 12 58 12 IRIN, 2 rue de la Houssinière BP 92208 - 44322 Nantes cedex 3 - FRANCE mailto:Gwen.Salaun@irin.univ-nantes.fr http://www.sciences.univ-nantes.fr/info/perso/permanents/salaun