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 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 [email protected] http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
