Overview of the Simplification of the Induction Conclusion

In this message the system is saying that Subgoal *1/2' has been rewritten T using the rules noted. The word ``But'' at the beginning of the sentence is a signal that the goal has been proved.

Click here to step through the proof of Subgoal *1/2'.