Now that you have seen the theorem prover in action you might be curious as to how you guide it.
Look at the picture above. It is meant to suggest that Q is an important lemma needed for the proof of P. Note that to lead the prover to the proof of P the user first proves Q. In a way, the formulation and proof of Q is a hint to the prover about how to prove P.
The user usually doesn't think of Q or recognize the need to prove it separately until he or she sees the theorem prover fail to prove P without it ``knowing'' Q.
The way the user typically discovers the need for Q is to look at failed proofs.
