[ProofPower] How to use previously proved theorems

[Marcel Oliveira]

Sorry Roger,

I truly believed the file was ok. Now you can load the file until beofre the
last theorem, and then, execute the proof of the last theorem until the ...
!!! From there, my question applies?

Thanks for the correction and sorry for the incovenience,

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
==================================
----- Original Message ----- 
From: "Roger Bishop Jones" <rbj01 at rbjones.com>
To: "ProofPower Mailing List" <proofpower at lemma-one.com>
Sent: Thursday, September 16, 2004 2:30 PM
Subject: Re: [ProofPower] How to use previously proved theorems


> On Thursday 16 September 2004 11:58 am, Marcel Oliveira wrote:
>
> > 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?
>
> When I try to load this in a bare zed database I don't
> get anywhere near the end of the script.
> Did you actually check it out before you posted it?
>
> Roger Jones
>
> _______________________________________________
> Proofpower mailing list
> Proofpower at lemma-one.com
> http://dropkick.trouble-free.net/mailman/listinfo/proofpower_lemma-one.com
-------------- next part --------------
A non-text attachment was scrubbed...
Name: using_thms.doc
Type: application/msword
Size: 8356 bytes
Desc: not available
URL: <http://lemma-one.com/pipermail/proofpower_lemma-one.com/attachments/20040916/32be830c/attachment.doc>