|1 2 3 x|
|This proofweb is a good demonstration of the way that failed proof attempts
can suggest what to do next in a term reduction based approach to theorem
proving. We started (see the proof homepage) trying to prove a
result which looked simple, but which in fact required two lemmas. With a
little analysis, we were able to formulate a lemma which we hoped would
complete the proof, and our attempt to prove it then led to the discovery of
the second lemma.
Of course, these remarks can only be validated by showing that trying to prove these three results in the reverse order of that in which they were discovered does in fact prove the original goal; this is done in our second proofweb for this goal.
On the other hand, it should not be expected that things will always be so easy; for example, if our initial goal were to prove Fermat's Last Theorem, then a proof attempt by induction on the exponent (or any other variable) would not yield a useful lemma.