[ProofPower] How to use previously proved theorems

Roger Bishop Jones rbj01 at rbjones.com
Thu Sep 16 09:30:19 EDT 2004


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




More information about the Proofpower mailing list