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.

## Advertising

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
automatically.
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
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com