On Monday 03 Sep 2012 21:03, Jon Lockhart wrote:

> Most of the tactics return the
> exact same goal and the comment printed with the goal is
> that it is alpha-convertible to its goal.

The significance of this is simply that the proof step you 
have just done has not moved you forward.
i.e. it says that what you ended up with is essentially the 
same as what you started with.

> I am assuming
> it is saying that this subgoal is alpha-convertible to
> the main goal I am trying to prove.

Just the alpha-equivalent to the goal or subgoal from which 
it was obtained.

> Now I looked at the
> reference manual and there appears to be some commands
> that I can use to eliminate alpha-convertible components
> and that this is what I should use for simplifying the
> sub goal and thus proving it and the main goal.

No this is a red herring.

You are not reasoning from your subgoal to the main goal.
You have to prove the subgoal independently of the main 
goal, and when you have proved them all you have a proved 
the main goal.

> So based on the scenario above and where I am at does
> anyone have any suggestions on what commands I should
> use to handle the alpha-conversion and completing the
> proof of the subgoal?

Normally you would not need to do anything about alpha 
conversion, if you were within alpha conversion of the 
target then the system would sort that out for you 

So your problem here is that you have misunderstood the 
significance of the alpha conversion message.
Forget about alpha conversion.

No-one can help you at this point, because we don't know 
anything at all about what you are trying to prove.
If you want help you should show us the problem you are 
working on.

Roger Jones

Proofpower mailing list

Reply via email to