[ProofPower] Problems using var_subst

[Marcel Oliveira]

Hi all,

I am trying to use the function var_subst but I am not getting what I
believe it should return. As far as I understood, this function receives a
list of pairs, a term and returns a term replacing all the free occurences
of each first element (variable) in the list by the corresponding second
element. However, my example (attached) is not working as it "should"!!!
Does anyone have any idea why?

Thanks,

Marcel

P.S.: I've attached an ascii document. In order to get a better view of the
example run conv_extended testing-renaming before open the document in PP.

===============================
Marcel Oliveira
PhD Researcher - Circus Project
Formal Methods
Computing Laboratory
University of Kent
Canterbury, Kent, UK  CT2 7NF
Tel: 44 (0)1227 823192
E-Mail: mvmo2 at kent.ac.uk
===============================
-------------- next part --------------
A non-text attachment was scrubbed...
Name: testing-renaming.doc
Type: application/msword
Size: 352 bytes
Desc: not available
URL: <http://lemma-one.com/pipermail/proofpower_lemma-one.com/attachments/20040506/59e48ba5/attachment.doc>