[ProofPower] How to use previously proved theorems

[Marcel Oliveira]

Hi There,

In the last proof of the attached document, I've reached a point (before the
... ) in which I believe I can use two previously proved theorems in order
to conclude the proof of the current subgoal.  Actually, I've been
unsuccessfully trying to do this. I believe that it has somethign to do with
sub-terms.

Can any one help me to conclude this proof using the two previously defined
theorems?

Thanks in advance,
Marcel

==================================
Marcel Oliveira
PhD Student - Formal Methods
Computing Laboratory
University of Kent
Canterbury, Kent, UK  CT2 7NF
Tel: 44 (0)1227 823192
E-Mail: mvmo2 at kent.ac.uk
URL: http://www.cs.kent.ac.uk/~mvmo2
==================================
-------------- next part --------------
A non-text attachment was scrubbed...
Name: using_thms.doc
Type: application/msword
Size: 12027 bytes
Desc: not available
URL: <http://lemma-one.com/pipermail/proofpower_lemma-one.com/attachments/20040916/a8218a73/attachment.doc>